Synchronous Equivalence

  • Harry Hsieh
  • Felice Balarin
  • Alberto Sangiovanni-Vincentelli

Abstract

Formal verification tools such as [34, 10] are very powerful in automatically proving that some arbitrary properties hold for an arbitrary design. Essentially, they perform exhaustive simulation for all possible input traces or system design parameters in an efficient manner. Unfortunately, for real-life embedded systems, the size of the design and the complexity of the analysis algorithms themselves cause the computer to consume too much time or memory. The verification is often unable to complete. To remedy this complexity problem, extensive user intervention is required to abstract away unnecessary details in the design representation. Figuring out the right abstraction for a given property is as hard as the verification problem itself, though designers usually have ideas as to what is the right abstraction for a given property. User intervention in the formal verification methodology is unavoidable.

Keywords

Formal Verification Exact Representation Sequential Circuit Asynchronous Circuit Input Trace 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2001

Authors and Affiliations

  • Harry Hsieh
    • 1
  • Felice Balarin
    • 2
  • Alberto Sangiovanni-Vincentelli
    • 1
  1. 1.University of California at BerkeleyUSA
  2. 2.Cadence Berkeley LaboratoriesUSA

Personalised recommendations