Symbolic Simulation Methods for Industrial Formal Verification / Edition 1

Symbolic Simulation Methods for Industrial Formal Verification / Edition 1

by Robert B. Jones
     
 

ISBN-10: 1402071035

ISBN-13: 9781402071034

Pub. Date: 06/30/2002

Publisher: Springer US

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.

Overview

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.

Product Details

ISBN-13:
9781402071034
Publisher:
Springer US
Publication date:
06/30/2002
Edition description:
2002
Pages:
151
Product dimensions:
6.10(w) x 9.25(h) x 0.36(d)

Table of Contents

List of Figuresxi
List of Tablesxiii
Acknowledgmentsxv
Forewordxvii
1.Introduction1
1.1Motivation and Philosophy1
1.2Approach3
1.3Verification Realities4
1.4Introduction to Symbolic Simulation5
1.4.1BDDs and Bit-Level Symbolic Simulation7
1.4.2High-Level Symbolic Simulation9
1.5Other Approaches11
1.5.1Theorem Proving11
1.5.2Symbolic Model Checking11
1.5.3Justification for Using Symbolic Simulation12
1.6Scope of the Book13
1.6.1Self Consistency13
1.6.2Parametric Representations in Symbolic Simulation14
1.6.3Incremental Flushing14
1.7Outline15
Part ISelf Consistency
2.Self Consistency19
2.1Computer Architecture Concepts and Terms19
2.2Introduction to Self Consistency22
2.3Definitions25
2.4Pragmatics26
2.5Verification Reduction27
2.6Examples29
2.6.1Pipeline Bypassing29
2.6.2Superscalar Arbitration30
2.7Related Work32
2.8Summary33
3.Self Consistency in Practice35
3.1Overview35
3.1.1Forte and Symbolic Trajectory Evaluation36
3.1.2The Examples37
3.2P6 Retirement Pipeline38
3.2.1Verification42
3.2.2Bugs44
3.3IA-32 Instruction-Length Decoder44
3.3.1Verification46
3.3.2Bugs49
3.4Summary50
Part IIParametric Representations
4.The Parametric Representation55
4.1Introduction55
4.2Verification Decomposition57
4.3Computation and Correctness60
4.4Input-Space Partitioning64
4.5Integration with STE and Theorem Proving67
4.6Related Work68
4.7Summary71
5.Using the Parametric Representation73
5.1Overview of Examples73
5.2Instruction-Length Decoder (IM)75
5.2.1Specification75
5.2.2Using the Specification80
5.2.3Verification Decomposition82
5.2.4Bugs84
5.2.5Verification Reuse86
5.3Floating-Point Addition and Subtraction87
5.3.1Floating-Point Overview88
5.3.2Specification89
5.3.3Addition89
5.3.4Subtraction92
5.4Summary92
Part IIIIncremental Flushing
6.Background on Processor Verification97
6.1Introduction97
6.2Burch/Dill Flushing98
6.3The Logic and Validity Checking100
6.4The Stanford Validity Checker102
6.5Related Verification Examples103
6.6Summary104
7.Incremental Flushing105
7.1Introduction106
7.2Preliminaries107
7.3The Approach109
7.4M[subscript I] Flush-Point Simulates M[subscript A]110
7.5M[subscript A] Flush-Point Simulates M[subscript S]112
7.5.1Self Consistency of M[subscript A]112
7.5.2Restricted M[subscript A] Flush-Point Simulates M[subscript S]118
7.6Mechanical Verification119
7.7Related Work119
7.8Discussion122
8.Conclusions125
Appendices127
Proofs127
A.1Proof of Theorem 3127
A.2Proof of Theorem 5131
A.3Statement and Proof of Lemma 1132
A.4Proof of Theorem 8133

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >