Advanced Formal Verification – Rolf Drechsler

Keim et. al. [24] proved for a certain class of multipliers (unsigned integer Wallace-tree type) that the backward traversal approach is of polynomial space and time complexity. The proof is based on a circuit representation of the multiplier consisting of the AND gates implementing the partial product bits and of full adder cells. Unfortunately, in practice, multiplier netlists are composed of general logic gates and information about the arithmetic sub-components is not available. We experimented with a large number of multipliers generated by our own tools as well as by commercial generators with the goal to im- prove *BMD synthesis by backward traversal as proposed by Hamaguchi.

However, we were only partially successful. In the following section, we report on these experiments to show where the major problems are. 4.4 Experiments with *BMD synthesis The general intuition behind preferring a backward traversal over a forward traversal is that the former makes better use of the special char- acteristics of *BMDs when representing arithmetic functions.

Represent- ing a pseudo-Boolean function in the *BMD should always be better than representing a bit-level Boolean function. However, if the network cut is not chosen appropriately, the pseudo-Boolean function implemented by the logic between the cut variables and the (integer) circuit output need not necessarily yield a compact *BMD. The work of [19] suggests a simple topological ordering among the nodes of the circuit when com- posing the *BMD. In our experiments, this node ordering worked well for text-book multipliers generated by our own tool.

However, for in- dustrial multipliers, we were not able to construct *BMDs using simple topological ordering. In this section we report on a number of experi- ments evaluating where the problems are and how *BMD synthesis could be improved. It has been pointed out by a number of authors [18, 25, 24] that knowledge about the sub-components of a multiplier is very useful in *BMD construction. However, in a gate netlist this information is not available. In order to successfully build a *BMD, however, information about the circuit structure should be exploited.

The goal is to derive as much information about the internal structure of the gate netlist as possible. As a first improvement over simple topological ordering of nodes to be composed into the *BMD, we experimented with partitioning the gate netlist of a multiplier into non-overlapping cones.

Each circuit node belongs to exactly one cone.

©2004 Kluwer Academic Publishers New York, Boston, Dordrecht, London, Moscow Print ©2004 Kluwer Academic Publishers 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: http://kluweronline.com and Kluwer’s eBookstore at: http://ebooks.kluweronline.com Dordrecht 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 Eugene Goldberg 1 Introduction 1 2 Hard Equivalence Checking CNF formulas 3 2.1 Introduction 3 2.2 Common Specification of Boolean Circuits 5 2.3 Equivalence Checking as SAT 11 2.4 Class M(p) and general resolution 12 2.5 Computation of existentially implied functions 13 2.6 Equivalence Checking in General Resolution 14 2.7 Equivalence Checking of Circuits with Unknown CS 20 2.8 A Procedure of Equivalence Checking for Circuits with a Known CS 22 2.9 Experimental Results 23 2.10 Conclusions 26 3 Stable Sets of Points 26 3.1 Introduction 26 3.2 Stable Set of Points 28 3.3 SSP as a reachable set of points 31 3.4 Testing Satisfiability of CNF Formulas by SSP Con- struction 32 3.5 Testing Satisfiability of Symmetric CNF Formulas by SSP Construction 35 3.6 SSPs with Excluded Directions 39 3.7 Conclusions 42 v vi ADVANCED FORMAL VERIFICATION 2 Advancements in mixed BDD and SAT techniques 45 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?

This is a short excerpt from the opening of “” by Unknown, quoted for review and introduction purposes. All rights belong to the copyright holders.

Book Information

• Unique ID: 440bf6cc3f3d5353
• File Extension: .pdf
• File Size: 2,303,932 bytes (2.197 MB)
• Title: –
• Author: Unknown
• ISBN: 1402025300, 1402077211
• Pages: 277
• Language: English (en)

Reading & Word Statistics

• Estimated Reading Time: 438.5 minutes
• Total Words: 87,699
• Total Characters: 529,531
• Average Words per Page: 316.6
• Average Characters per Page: 1911.66

Most Frequent Words

verification (453), formal (370), state (354), checking (347), property (339), design (303), circuit (291), set (252), variables (245), equivalence (224), figure (215), boolean (210), sat (208), example (204), function (195), circuits (193), space (191), model (180), system (178), one (178), time (177), point (172), two (171), using (166), variable (158), formula (156), functions (153), systems (149), problem (148), advanced (145), specification (145), verification (144), arithmetic (144), section (144), cnf (141), output (141), used (140), let (130), bdd (129), input (127), approach (120), points (116), based (115), techniques (113), level (112), also (112), analog (110), values (109), number (108), properties (107), given (107), value (105), however (103), assertion (102), size (101), results (98), bit (97), formulas (96), logic (95), algorithm (94), proof (94), representation (93), data (92), path (92), order (90), bdds (89), since (89), general (86), clause (85), decision (83), tion (82), different (81), problems (80), structure (78), described (78), signal (78), following (78), step (78), approaches (77), temporal (76), resolution (75), shown (75), addition (74), see (74), primary (74), states (72), proc (72), first (71), called (71), equation (71), result (70), simulation (70), assignment (70), satisfiability (69), procedure (68), possible (68), nonlinear (67), definition (67), new (66), use (65).

PDF Download