Symbolic Simulation Methods for Industrial Formal Verification
contains two distinct, but related, approaches to the verification
problem. Both are based on symbolic simulation. The first approach
is applied at the gate level and has been successful in verifying
sub-circuits of industrial microprocessors with tens and even
hundreds of thousands of gates. The second approach is applied at a
high-level of abstraction and is used for high-level descriptions
of designs.
Historically, it has been difficult to apply formal verification
methods developed in academia to the verification problems
encountered in commercial design projects. This book describes new
ideas that enable the use of formal methods, specifically symbolic
simulation, in validating commercial hardware designs of remarkable
complexity. These ideas are demonstrated on circuits with many
thousands of latches-much larger circuits than those previously
formally verified. The book contains three main topics:
- Self consistency, a technique for deriving a formal
specification of design behavior from the design itself;
- The use of the parametric representation to encode predicates
as functional vectors for symbolic simulation, an important step in
addressing the state-explosion problem;
- Incremental flushing, a method used to verify high-level
descriptions of out-of-order execution.
Symbolic Simulation Methods for Industrial Formal Verification
concludes with work on verification of simplified models of
out-of-order processors.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!