Advanced Formal Verification
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 f
- PDF / 3,311,361 Bytes
- 269 Pages / 432 x 684 pts Page_size
- 102 Downloads / 355 Views
Advanced Formal Verification Edited by
Rolf Drechsler University of Bremen, Germany
KLUWER ACADEMIC PUBLISHERS NEW YORK, BOSTON, DORDRECHT, LONDON, MOSCOW
eBook ISBN: Print ISBN:
1-4020-2530-0 1-4020-7721-1
©2004 Kluwer Academic Publishers New York, Boston, Dordrecht, London, Moscow Print ©2004 Kluwer Academic Publishers Dordrecht All rights reserved No part of this eBook may be reproduced or transmitted in any form or by any means, electronic, mechanical, recording, or otherwise, without written consent from the Publisher Created in the United States of America Visit Kluwer Online at: and Kluwer's eBookstore at:
http://kluweronline.com http://ebooks.kluweronline.com
Contents
Preface
xi
Contributing Authors
xiii
Introduction Rolf Drechsler 1 Formal Verification 2 Challenges 3 Contributions to this Book
xix xix xxi xxiii
1 What Sat-Solvers can and cannot do Eugene Goldberg 1 Introduction 2 Hard Equivalence Checking CNF formulas 2.1 Introduction 2.2 Common Specification of Boolean Circuits 2.3 Equivalence Checking as SAT 2.4 Class M (p) and general resolution 2.5 Computation of existentially implied functions 2.6 Equivalence Checking in General Resolution 2.7 Equivalence Checking of Circuits with Unknown CS 2.8 A Procedure of Equivalence Checking for Circuits with a Known CS 2.9 Experimental Results 2.10 Conclusions 3 Stable Sets of Points 3.1 Introduction 3.2 Stable Set of Points 3.3 SSP as a reachable set of points 3.4 Testing Satisfiability of CNF Formulas by SSP Construction 3.5 Testing Satisfiability of Symmetric CNF Formulas by SSP Construction 3.6 SSPs with Excluded Directions 3.7 Conclusions
v
1 1 3 3 5 11 12 13 14 20 22 23 26 26 26 28 31 32 35 39 42
vi
ADVANCED FORMAL VERIFICATION 2 45 Advancements in mixed BDD and SAT techniques Gianpiero Cabodi and Stefano Quer 1 Introduction 45 2 Background 47 2.1 SAT Solvers 47 2.2 Binary Decision Diagrams 48 2.2.1 Zero-Suppressed Binary Decision Diagrams 49 2.2.2 Boolean Expression Diagrams 50 2.3 Model Checking and Equivalence Checking 52 3 Comparing SAT and BDD Approaches: Are they different? 54 3.1 Theoretical Considerations 54 3.2 Experimental Benchmarking 55 3.2.1 Bug Hunting in an Industrial Setting 56 3.2.2 Modifying BDD-based Techniques to Perform BMC 56 3.2.3 Conclusions 58 3.3 Working on Affinities: Variable Order 58 3.3.1 Affinities on circuit-width correlation 59 3.3.2 Recursion tree and Variable Order 59 3.3.3 A Common Static Variable Order Heuristic 60 3.3.4 Conclusions 60 4 Decision Diagrams as a Slave Engine in general SAT: Clause Compression by Means of ZBDDs 61 ZBDDs for Symbolic Davis-Putnam Resolution 61 4.1 ZBDDs for Symbolic DLL 62 4.2 ZBDDs for Breadth-First SAT 62 4.3 Conclusions 62 4.4 5 Decision Diagram Preprocessing and Circuit-Based SAT 62 5.1 BED Preprocessing 63 5.2 Circuit-Based SAT 64 5.2.1 BDD Sweeping and SAT 64 5.2.2 SAT on BEDs 66 5.3 Preprocessing by Approximate Reachability 67 6 Using SAT in Symbolic Reachability Analysis 68 6.0.1 BDDs at SAT leaves 69 6.0.2 SAT-Based Symbolic Image and Pre-image 70 7 Conclusions, Remar
Data Loading...
