Advanced Formal Verification

by Drechsler, Rolf

• ISBN13: 9781402077210
• ISBN10: 1402077211
• Format: Hardcover
• Copyright: 2004-05-01
• Publisher: Kluwer Academic Pub

Summary

Modern circuits may contain up to several hundred million transistors. In the meantime it has been observed that verification becomes the major bottleneck in design flows, i.e. up to 80% of the overall design costs are due to verification. This is one of the reasons why several methods have been proposed as alternatives to classical simulation. Simulation alone cannot guarantee sufficient coverage of the design resulting in bugs that may remain undetected. As alternatives formal verification techniques have been proposed. Instead of simulating a design the correctness is proven by formal techniques. There are different areas where these approaches can be used: equivalence checking, property checking or symbolic simulation. These methods have been successfully applied in many industrial projects and have become the state-of-the-art technique in several fields. However, the deployment of the existing tools in real-world projects also showed the weaknesses and problems of formal verification techniques. This gave motivating impulses for tool developers and researchers. Advanced Formal Verification shows the latest developments in the verification domain from the perspectives of the user and the developer. World leading experts describe the underlying methods of today's verification tools and describe various scenarios from industrial practice. In the first part of the book the core techniques of today's formal verification tools, such as SAT and BDDs are addressed. In addition, multipliers, which are known to be difficult, are studied. The second part gives insight in professional tools and the underlying methodology, such as property checking and assertion based verification. Finally, analog components have to be considered to cope with complete system on chip designs. In this book the state-of-the-art in many important fields of formal verification are described. Besides the description of the most recent research results, open problems and challenging research areas are addressed. Because of this, the book is intended for CAD developers and researchers in the verification domain, where formal techniques become a core technology to successful circuit and system design. Furthermore, the book is an excellent reference for users of verification tools in order to acquire a better understanding of the internal principles and subsequently drive the tools to the highest performance. In this context the book is dedicated to those in industry and academia to stay informed about the most recent developments in the field of formal verification.

Table of Contents

Preface	xi
Contributing Authors	xiii
Introduction	xix
Rolf Drechsler
1 Formal Verification	xix
2 Challenges	xxi
3 Contributions to this Book	xxiii
1 What Sat-Solvers can and cannot do	1	(44)
Eugene Goldberg
1 Introduction	1	(2)
2 Hard Equivalence Checking CNF formulas	3	(23)
2.1 Introduction	3	(2)
2.2 Common Specification of Boolean Circuits	5	(6)
2.3 Equivalence Checking as SAT	11	(1)
2.4 Class M(p) and general resolution	12	(1)
2.5 Computation of existentially implied functions	13	(1)
2.6 Equivalence Checking in General Resolution	14	(6)
2.7 Equivalence Checking of Circuits with Unknown CS	20	(2)
2.8 A Procedure of Equivalence Checking for Circuits with a Known CS	22	(1)
2.9 Experimental Results	23	(3)
2.10 Conclusions	26	(1)
3 Stable Sets of Points	26	(19)
3.1 Introduction	26	(2)
3.2 Stable Set of Points	28	(3)
3.3 SSP as a reachable set of points	31	(1)
3.4 Testing Satisfiability of CNF Formulas by SSP Construction	32	(3)
3.5 Testing Satisfiability of Symmetric CNF Formulas by SSP Construction	35	(4)
3.6 SSPs with Excluded Directions	39	(3)
3.7 Conclusions	42	(3)
2 Advancements in mixed BDD and SAT techniques	45	(32)
Gianpiero Cabodi and Stefano Quer
1 Introduction	45	(2)
2 Background	47	(7)
2.1 SAT Solvers	47	(1)
2.2 Binary Decision Diagrams	48	(4)
2.2.1 Zero-Suppressed Binary Decision Diagrams	49	(1)
2.2.2 Boolean Expression Diagrams	50	(2)
2.3 Model Checking and Equivalence Checking	52	(2)
3 Comparing SAT and BDD Approaches: Are they different?	54	(7)
3.1 Theoretical Considerations	54	(1)
3.2 Experimental Benchmarking	55	(3)
3.2.1 Bug Hunting in an Industrial Setting	56	(1)
3.2.2 Modifying BDD-based Techniques to Perform BMC	56	(2)
3.2.3 Conclusions	58	(1)
3.3 Working on Affinities: Variable Order	58	(3)
3.3.1 Affinities on circuit-width correlation	59	(1)
3.3.2 Recursion tree and Variable Order	59	(1)
3.3.3 A Common Static Variable Order Heuristic	60	(1)
3.3.4 Conclusions	60	(1)
4 Decision Dia rams as a Slave Engine in general SAT: Clause Compression by Means of ZBDDs	61	(1)
4.1 ZBDDs for Symbolic Davis-Putnam Resolution	61	(1)
4.2 ZBDDs for Symbolic DLL	62	(1)
4.3 ZBDDs for Breadth-First SAT	62	(1)
4.4 Conclusions	62	(1)
5 Decision Diagram Preprocessing and Circuit-Based SAT	62	(6)
5.1 BED Preprocessing	63	(1)
5.2 Circuit-Based SAT	64	(3)
5.2.1 BDD Sweeping and SAT	64	(2)
5.2.2 SAT on BEDs	66	(1)
5.3 Preprocessing by Approximate Reachability	67	(1)
6 Using SAT in Symbolic Reachability Analysis	68	(3)
6.0.1 BDDs at SAT leaves	69	(1)
6.0.2 SAT-Based Symbolic Image and Pre-image	70	(1)
7 Conclusions, Remarks and Future Works	71	(6)
3 Equivalence Checking of Arithmetic Circuits	77	(48)
Dominik Stoffel, Evgeng Karibaev, Irina Kufareva and Wolfgang Kunz
1 Introduction	78	(3)
2 Verification Using Functional Properties	81	(4)
3 Bit-Level Decision Diagrams	85	(3)
4 Word-Level Decision Diagrams	88	(17)
4.1 Pseudo-Boolean functions and decompositions	89	(3)
4.2 *BMDs	92	(2)
4.3 Equivalence Checking Using *BMDs	94	(3)
4.4 Experiments with *BMD synthesis	97	(8)
5 Arithmetic Bit-Level Verification	105	(13)
5.1 Verification at the Arithmetic Bit Level	108	(4)
5.2 Extracting the Half Adder Network	112	(3)
5.3 Verification Framework	115	(1)
5.4 Experimental Results	115	(3)
6 Conclusion	118	(1)
7 Future Perspectives	119	(6)
4 Application of Property Checking and Underlying Techniques	125	(42)
Raik Brinkmann, Peer Johannsen and Klaus Winkelmann
1 Circuit Verification Environment: User's View	126	(3)
1.1 Tool Environment	126	(1)
1.2 The gateprop Property Checker	127	(2)
2 Circuit Verification Environment: Underlying Techniques	129	(4)
2.1 From Property to Satisfiability	129	(2)
2.2 Preserving Structure during Problem Construction	131	(1)
2.3 The Experimental Platform RtProp	132	(1)
3 Exploiting Symmetries	133	(9)
3.1 Symmetry in Property Checking Problems	133	(3)
3.2 Finding Symmetrical Value Vectors	136	(4)
3.3 Practical Results	140	(2)
4 Automated Data Path Scaling to Speed Up Property Checking	142	(10)
4.1 Bitvector Satisfiability Problems	143	(2)
4.2 Formal Abstraction Techniques	145	(1)
4.3 Speeding Up Hardware Verification by One-To-One Abstraction	146	(1)
4.4 Data Path Scaling of Circuit Designs	147	(5)
5 Property Checking Use Cases	152	(10)
5.1 Application Example: Reverse Engineering	155	(3)
5.1.1 Functionality	155	(1)
5.1.2 Task	155	(1)
5.1.3 Examples for a property	156	(1)
5.1.4 Results	157	(1)
5.2 Application Example: Complete Block-Level ASIC Verification	158	(3)
5.2.1 Verification Challenge and Approach	158	(1)
5.2.2 Verifying the Control Path	159	(1)
5.2.3 Data Path Results	160	(1)
5.2.4 Overall Result	160	(1)
5.3 Productivity Statistics	161	(1)
6 Summary	162	(5)
6.1 Achievements	162	(1)
6.2 Challenges and Perspectives	163	(4)
5 Assertion-Based Verification	167	(38)
Claudionor Nunes Coelho Jr. and Harry D. Foster
1 Introduction	167	(10)
1.1 Specifying properties	169	(2)
1.2 Observability and controllability	171	(1)
1.3 Formal property checking framework	172	(5)
2 Assertion Specification	177	(6)
2.1 Temporal logic	177	(2)
2.2 Property Specification Language (PSL)	179	(7)
2.2.1 Boolean layer	180	(1)
2.2.2 Temporal layer	180	(2)
2.2.3 Verification layer	182	(1)
3 Assertion libraries	183	(1)
4 Assertion simulation	184	(2)
5 Assertions and formal verification	186	(5)
5.1 Handling complexity	186	(4)
5.2 Formal property checking role	190	(1)
6 Assertions and synthesis	191	(6)
6.1 On-line validation	191	(1)
6.2 Synthesizable assertions	192	(2)
6.3 Routing scheme for assertion libraries	194	(1)
6.4 Assertion processors	195	(2)
6.5 Impact of Assertions in Real Circuits	197	(1)
7 PCI property specification example	197	(5)
7.1 PCI overview	198	(1)
7.2 PCI master reset requirement	199	(1)
7.3 PCI burst order encoding requirement	199	(1)
7.4 PCI basic read transaction	200	(2)
8 Summary	202	(3)
6 Formal Verification for Nonlinear Analog Systems	205	(38)
Walter Hartong, Ralf Klausen and Lars Hedrich
1 Introduction	206	(1)
2 System Description	206	(5)
2.1 Analog Circuit Classes	208	(1)
2.2 State Space Description	208	(3)
2.2.1 Index	209	(1)
2.2.2 Solving a DAE System	209	(2)
2.2.3 Linearized System Description	211	(1)
3 Equivalence Checking	211	(16)
3.1 Basic Concepts	212	(1)
3.1.1 Nonlinear Mapping of State Space Descriptions	212	(1)
3.2 Equivalence Checking Algorithm	213	(4)
3.2.1 Sampling the State Space	213	(2)
3.2.2 Consistent Sample Point	215	(2)
3.3 Linear Transformation Theory	217	(5)
3.3.1 System Transformation to a Kronecker Canonical Form	217	(2)
3.3.2 DAE System Transformation into the Virtual State Space	219	(3)
3.3.3 Error Calculation	222	(1)
3.4 Experimental Results	222	(5)
3.4.1 Schmitt Trigger Example	222	(3)
3.4.2 Bandpass Example	225	(2)
4 Model Checking	227	(15)
4.1 Model Checking Language	227	(3)
4.2 Analog Model Checking Algorithm	230	(9)
4.2.1 Transition Systems	230	(1)
4.2.2 Discrete Time Steps	231	(1)
4.2.3 State Space Subdivision	232	(2)
4.2.4 Transition Relation	234	(2)
4.2.5 Border Problems	236	(1)
4.2.6 Input Value Model	237	(2)
4.2.7 Optimizations	239	(1)
4.3 Experimental Results	239	(3)
4.3.1 Schmitt Trigger Example	239	(1)
4.3.2 Tunnel Diode Oscillator Example	240	(2)
5 Summary	242	(1)
6 Acknowledgement	242	(1)
Appendix: Mathematical Symbols	243	(4)
Index	247