Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors

  • Miroslav N Velev (5415224)
  • Randal E. Bryant (5409038)
ORKG logo Add to ORKG
Publication date
June 2018

Abstract

We study the applicability of the logic of Positive Equality with Uninterpreted Functions (PEUF) [2][3] to the verification of pipelined microprocessors with very large Instruction Set Architectures (ISAs). Abstraction of memory arrays and functional units is employed, while the control logic of the processors is kept intact from the original gate-level designs. PEUF is an extension of the logic of Equality with Uninterpreted Functions, introduced by Burch and Dill [4], that allows us to use distinct constants for the data operands and instruction addresses needed in the symbolic expression for the correctness criterion. We present several techniques that make PEUF scale very efficiently for the verification of pipelined microprocessors wit...

Extracted data

Related items

Exploiting Positive Equality and Partial Nonconsistency in the Formal Verification of Pipelined Microprocessors
  • Miroslav N. Velev (5415272)
  • Randal Bryant (3892378)
June 2018

We study the applicability of the logic of Positive Equality with Uninterpreted Functions (PEUF) [2...

Exploiting Positive Equality in a Logic of Equality With Uninterpreted Functions
  • Randal Bryant (3892378)
  • Steven German (5416814)
  • Miroslav N. Velev (5415272)
June 2018

In using the logic of equality with unininterpreted functions to verify hardware systems, specific ...

Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions
  • Randal E. Bryant (5409038)
  • Steven German (5416814)
  • Miroslav N Velev (5415224)
January 1999

Modern processors have relatively simple specificationsbased on their instruction set architectures....

We use cookies to provide a better user experience.