Synthesis and Verification Formal and Semi-Formal Verification Contract #: TJ-684 Task Students Advisor Edmund Clarke Abstraction in Model Checking Yuan Lu, Pankaj Chauhan, Anubhav Gupta Steven German, IBM Rob Gerth, Intel Carl Pixley, Motorola Somnath Viswanath, AMD Xudong Xhao, Richard Raimi
684.005 Sergey Berezin Edmund Clarke Rob Gerth, Intel Richard Raimi, Motorola Xudong Zhao, Intel Anubhav Gupta, Pankaj Chauhan Edmund Clarke Cindy Eisner, IBM Haifa Carl Pixley, Motorola Pankaj Chauhan
Edmund Clarke Jim Kukula, Synopsys 684.004 Combining Model Checking with Theorem Proving 684.007 Model Checking without BDDs New Task Efficient Image Computation Algorithms Mentors Accomplishments! Yuan Lu (now at BroadComm Inc.) and
Marius Minea (now PostDoc at Berkeley) graduated in the year 2000! January 25, 2020 2 Automatic Abstraction by Counterexample-guided Refinement Edmund M. Clarke Yuan Lu Pankaj Chauhan Anubhav Gupta Joint work with Orna Grumberg, Somesh Jha, Helmut Veith 684.004: Abstraction in Model Checking Description: Counterexample-guided Abstraction Refinement
Goals: To provide a new abstraction technique to verify large designs. January 25, 2020 4 684.004: Abstraction in Model Checking Plans and directions for the current year (2000): Experiment with other abstraction refinement techniques Experiment on benchmark and industrial designs Abstraction in the context of bounded model checking Experiment on industrial designs (PCI bus protocol) January 25, 2020 5
684.004: Abstraction in Model Checking Accomplishments for the current year (2000): Yuan Lu graduated! Automatic abstraction generation Release of aSMV tool Extensive experimentation with impressive results January 25, 2020 6 684.004: Abstraction in Model Checking Plans and directions for the next year (2001): Extending the methodology to include all ACTL countertexamples Using SAT for refinement of large state spaces January 25, 2020 7
684.004: Abstraction in Model Checking Milestones Automatic abstraction function generation (31-Dec2000) X Development of hierarchical verification algorithms (31Dec-2000) Extending the methodology to include all ACTL* counterexamples and implementation (31-Dec-2001) Using SAT based techniques for refinement of large state spaces (31-March-2001) January 25, 2020 8 684.004: Abstraction in Model Checking Deliverables X Report on hierarchical model checking without flattening for hierarchical circuit descriptions (Planned 31-Dec-2000) X Report on model checking of hierarchically structured SMV and StateCharts for embedded systems and mixed hardware designs (Planned 31-Dec-2001)
Report/Paper on Extension of methodology for all counterexamples (Planned 31-Dec-2001) New version of aSMV with this feature (Planned 30-March-2001) Report/Paper on refinement using large state spaces (Planned 31June-2001) New version of aSMV with SAT based refinement (Planned 31Dec-2002) January 25, 2020 9 Existential Abstraction Given an abstraction function h : S Sh, the concrete states are grouped and mapped into abstract states Mh h h h M < Mh and Mh |= M |= M January 25, 2020 10 Our Abstraction Methodology (CAV2000) M and generate initial abstraction Mh Mh |= model check Mh |=
refinement Th is spurious January 25, 2020 generate counterexample Th Th check spurious counterexample stop Th is not spurious 11 Highlights of Our Methodology Impressive results, on average, 3.5x time, 17x space improvements! A large Fujitsu multimedia processor verified Handles all ACTL* loop/path counterexample
But. What about non-loop/non-path counterexamples? What if infeasible to check validity of counterexamples? January 25, 2020 12 General Counterexamples for ACTL* Not all the counterexamples in ACTL* are linear (path or loop). How to refine the abstraction when a counterexample is not linear? What are counterexamples?
How to generate readable counterexamples? January 25, 2020 13 Tree-like Counterexamples What does the counterexample for (AG p) (AF q) look like? (AG p) (AF q) EF p (EF p) (EG q) (EF p) (EG q) q EG q q q
q p q January 25, 2020 q q p q 14 Counterexamples for ACTL Theorem All ACTL formulas have tree-like counterexamples. Why tree-like counterexamples ? easy to diagnose
decomposable to simple paths and loops January 25, 2020 15 Generate Counterexamples for ACTL We propose an algorithm to generate tree-like counterexamples for ACTL Traverse the parse tree of the formula in DFS order Generate path or loop counterexamples for each node in the parse tree.
Glue all the sub-counterexamples for the total Symbolic! January 25, 2020 16 Using SAT for Abstraction Refinement Problem Domain: Hardware circuits with more than 5000 latches! Path/loop counterexamples only
I C A I : Primary Inputs R: Visible Variables A: Invisible Variables V=RUA |R| << |V| January 25, 2020 A L R R 17
Spurious Path Counterexample failure state Th is spurious January 25, 2020 The concrete states mapped to the failure state are partitioned into 3 sets states dead-end yes reachable no out edges bad no yes
irrelevant no no 18 Checking the Validity of Counterexample Describe the abstract counterexample using propositional formula Feed the formula to SAT checker Size of SAT problem is linear in the circuit size For a spurious trace, dead end states Si,0 are obtained Set of dad states is Si ,1 {s h 1 (si ) | s' h 1 ( si 1 )I .F ( s, I ) s'} could be empty January 25, 2020 19 Example of Approximation x' y z y ' w
z ' w w' w AG ( x) h( x, y , z , w) ( x, y, z ) I {(0,0,1,0)} January 25, 2020 w 0 w 1 (0,0,1) (0,1,0) (0,1,1) 20 Modified Refinement Methodology M, Mh and Mh |=
Model Check Mh|= ? Mh |= generate counterexample Th refinement BadStates is empty Check Th with SAT Th stop Th is real SAT for BadStates SAT for Bad & DeadEnd January 25, 2020
21 Heuristics for Refinement Use GRASP (Sakellah et. al.)/Chaff(Mallik et.al.) for checking validity of counterexample Modify these procedures to identify important variables Most backtracked to variable Largest transitive fanout in implication graph(IG) Unique Implication Points Variables from conflicting clauses .. January 25, 2020
22 Implementation Details visible boolean x; .. Th, M, Bad, DeadEnd Th , M Intermediate Block Modified NuSMV Modified GRASP/Chaff New vars Mh|= January 25, 2020
Sat?, Auxiliary Info 23 Future Work Generate non-path/non-loop counterexamples Refinement using those counterexamples Formalize and evaluate the heuristics for picking up visible variables using GRASP/Chaff Experiments! January 25, 2020 24 Model Checking and Theorem Proving: A Unified Framework Sergey Berezin Edmund M. Clarke
684.005: Combining Model Checking with Theorem Proving Description: An approach to unifying Model Checking and Theorem Proving in a single framework Goals: Design a framework to combine new state-of-the-art model checking and theorem proving techniques efficiently Develop a tool that supports this framework January 25, 2020 26 684.005: Combining Model Checking with Theorem Proving Plans and directions for the current year (2000): Verify a large hardware example (like PCI bus) Study how the combination of model checking and
theorem proving improves both techniques Continue the development of the implementation January 25, 2020 27 684.005: Combining Model Checking with Theorem Proving Accomplishments for the current year (2000): Formulated a framework that unifies model checking and theorem proving in a very general way Came up with a new methodology for efficient specialization of theorem proving to particular problem domains Implemented a "prover generator" as a new version of SyMP based on the above methodology Implemented the necessary components of the proof system for combining model checking and theorem proving as an instance of a prover generated by SyMP Verified an example of an IBM cache coherence protocol January 25, 2020
28 684.005: Combining Model Checking with Theorem Proving Plans and directions for the next year (2001): Include several powerful reduction rules into the default proof-system of SyMP (like various forms of abstraction, compositional reasoning techniques, etc.) Verify a few more examples using these reduction rules Implement one or more other proof systems (either completely different or specialized and more automated versions of the default system) in the tool and demonstrate that it works as a prover generator January 25, 2020 29 684.005: Combining Model Checking with Theorem Proving
Milestones Implementation of the tool's core, detailed tool design, preliminary experiments on known hardware examples like Tomasulo's algorithm (30-Sep-1999) Experimental alpha release of the tool (31-Dec-1999) Extensions to the verification methodology and experiments on larger examples (30-Jun-2000) Extensions to the theorem prover and the model checking back-end (30-Jun-2001) January 25, 2020 30 684.005: Combining Model Checking with Theorem Proving Deliverables Prototype of the tool for combining model checking and theorem proving (Completed: 16-Feb-2000), Related Publication(s):P000258 , P000259 Release of tool for combining model checking and
theorem proving (Completed: 10-Jan-2001), P001813 Doctoral dissertation on combining model checking and theorem proving for hardware verification (Planned: 30-Aug-2001) Report on verification methodology for complex hardware using model checking and theorem proving (Planned: 31-Dec-2001) January 25, 2020 31 Model Checking and Theorem Proving: A Unified Framework Sergey Berezin Computer Science Department Carnegie Mellon University Example: IBM Cache Coherence Protocol P1
P2 Cache Shared1 Cache2 reqShared grantShared ... Home Node Shared: ExclGranted: January 25, 2020 Pn
... Cache Excl n reqExcl grantExcl invalidate invAck 33 Coherence Property At any point in time, if any cache is Exclusive then all the other caches are Invalid: AG c1,c2: c1 != c2 & c1.state = Exclusive c2.state = Invalid P1 P2 Cache1
Shared Cache2 Pn ... Cache Excl n Home Node Shared: ... ExclGranted: January 25, 2020 34
Coding the Model in SyMP Module with parameter module M[type Index] = begin datatype State = Invalid | Shared | Excl stateVar (cache: Index -> State), (channel: Index -> Message), (exclGranted: bool), (Shared: Index -> bool) init(cache) := fn _ => Invalid; init(exclGranted) := false State variables choose i: channel(i) = Invalidate => next(cache) := (fn x => if x=i then Invalid else cache x endif) | !exclGranted & channel(i) = reqExcl => next(channel i) := grantExcl next(exclGranted) := true Property
[......] endchoose Transition system theorem coherence = self |= AG(forall i,j: i!=j & cache(i) = Excl -> cache(j) = Invalid) end January 25, 2020 35 Formal Verification Options Model Checking M |= F (F is true in M) Theorem Proving |= F (F must be valid in general) + Model and property are cleanly
separated: M |= F - Model has to be encoded as a + State reduction techniques + Can analyze extremely complex behaviors - Model structure lost, hard to apply similar reductions formula: |= Enc(M) Enc(F) Both have strong and weak points. Can we combine best features of the two? January 25, 2020 36
Combining MC & TP Add expressiveness to efficient decision procedures Cancel out drawbacks of both techniques Perhaps, find something new in the middle ground... January 25, 2020 37 Modifying Gentzens Sequent Theorem proving uses Gentzens Sequent format: A1, A2, => B1, B2, The model from model checking has to be translated into HOL to fit into this sequent. But we can add the model to the sequent: M; A1, A2, => B1, B2, Also, make the logic temporal, not just HOL. January 25, 2020
38 Adding Model Checking Model checking becomes just another rule: ModelCheck(M, , ) = true M; => MC Other transformations from model checking are added as rules, e.g. Cone of Influence reduction: V = COI(M, , ) M|V; => M; => January 25, 2020 Cone
39 Other Types of Rules Induction on time: M; => , A M; A => AX A, where M=(S, , S) M; => , AG A January 25, 2020 AG Induct 40 Verifying Cache Coherence Property in First-Order CTL: AG(c1,c2: c1 != c2 & c1.state = Exclusive c2.state = Invalid) How to prove: Find an inductive invariant
Induction on time (the AG Induct rule) Skolemize, split choose statement, abstract-split (eliminate skolem constants), compute cone of influence, model check Verified in our tool SyMP January 25, 2020 41 New Methodology: Features Adequate representation for the problem domain Right level of abstraction Rules perform exactly the transformations we have in mind while doing verification Specialized rules for temporal logic Efficient use of model structure Model checking and theorem proving at the same prompt Interactive proof construction Full user control with possibility of automation
January 25, 2020 42 Overall Picture Specification language P2 P1 Pn ... Cac he2 Cac Shar he ed1
Cac Excl hen Specialized proof system Home Node Shared: => , A1 ... => , A2 R ExclGranted: => , A1 A2
=> true Axiom Proof Management Axiom a=2 => 2>0 a=2 => a>0 Replace Axiom a=2 => 2+2=4 Replace a=2 => a+a=4 a=2 => a>0 a+a=4 => a=2 a>0 a+a=4 => x. x=2 x>0 x+x=4 January 25, 2020
R User Interface R R 43 Generalizing Further ? What made it possible to integrate Model Checking and Theorem Proving? Customized sequent and proof system Adequate representation for the problem domain ? How about other problem domains? (Security protocols, Software verification, highly specialized hardware, etc.) The same guidelines should work (*) ? But do I have to code it all from scratch again?
There is certainly some common core that can be reused January 25, 2020 44 Architecture with Shared Core Specification language-2 Specification language-1 P2 P1 ... Cach e2 Cach Share
ed1 P1 P2 Cac Shar he ed1 Cac he2 Pn Pn Cach Excl en
... Cac Excl hen Home Node Home Node Shared: Shared: ... ... ExclGranted: ExclGranted: proof system - 1
Proof Management Axiom => , A1 => , A2 a=2 => 2>0 R => , A1 A2 => true Axiom a=2 => a>0
Replace Axiom a=2 => 2+2=4 Replace a=2 => a+a=4 proof system - 2 => , A1 => , A2 R R => , A1 A2 => true a=2 => a>0 a+a=4 => a=2 a>0 a+a=4
=> x. x=2 x>0 x+x=4 R R User Interface January 25, 2020 45 Axiom SyMP: Symbolic Model Prover Theorem prover generator Common proof management core Common interactive user interface Plug-in proof systems well-defined interface to custom proof system modules Each proof system defines custom sequent and custom set of rules
Currently implemented proof systems: Default: combines MC & TP Athena: security protocol verification (in progress) January 25, 2020 46 Verified Example: IBM Cache Coherence Coded in Default proof system in SyMP Verified coherence of the Home Node Other lemmas are still in progress Proof: 139 elementary steps (proof rules) about half of them are model check rules January 25, 2020 47
Conclusion New methodology for combining model checking and theorem proving New framework for specializing theorem proving to various problem domains In particular, MC + TP is one such problem domain A tool SyMP that implements the framework Implementation of MC + TP system in the tool Many existing methodologies can be expressed in the framework and implemented in SyMP January 25, 2020 48 Future Work Finish the default proof system Ideally, it should include all basic theorem proving for FO temporal logic and most of known model checking transformations
Implement more proof systems for other problem domains Athena is being implemented for security protocols Plans for software verification system Plans for toy systems: natural deduction, CFG, etc. Improve proof search techniques January 25, 2020 49 Using Fourier Analysis for AbstractionRefinement in Model Checking Anubhav Gupta Edmund M. Clarke 684.007: Model Checking Without BDDs Description: Symbolic model checking without BDDs using
alternative data structures and algorithms. Goals: To develop an alternative method of doing model checking without BDDs. January 25, 2020 51 684.007: Model Checking Without BDDs Plans and directions for the current year (2000): Explore the use of SAT procedures and BEDs for fixpoint computations. January 25, 2020 52 684.007: Model Checking Without
BDDs Accomplishments for the current year (2000): Implemented a full CTL model checker that combines SAT procedures with BEDs for fixpoint computations. Proposed a new methodology that uses learning algorithms for identifying important variables in hardware circuits. Came up with a new approach for counterexampleguided abstraction-refinement that views refinement as the standard AI classification problem. January 25, 2020 53 684.007: Model Checking Without BDDs Plans and directions for the next year (2001): Implement a tool that identifies important variables in a circuit and uses this information to generate good BDD and SAT-split orderings. Formalize a counterexample-guided abstractionrefinement framework based on the Fourier Transform.
Implement a counterexample-guided abstractionrefinement framework based on the Fourier Transform and other learning algorithms. January 25, 2020 54 684.007: Model Checking Without BDDs Milestones Verifier that combines fixed point computation for mode checking with a sat-solver (31-Jan-2001). Formalize counterexample-guided abstractionrefinement framework based on the Fourier Transform (15-May-2001). Implement counterexample-guided abstractionrefinement framework based on the Fourier Transform and other learning algorithms and perform experiments (31-Nov-2001). Generates good BDD and SAT splitting-orders based on important variables in the circuit (31-Mar-2002). January 25, 2020 55
684.007: Model Checking Without BDDs Deliverables Verifier that combines fixed point computation for mode checking with a sat-solver (Completed : 31-Jan-2001), Related Publication(s): P001653, P000728 Report that formalizes counterexample-guided abstractionrefinement framework based on the Fourier Transform (31-May2001). Tool that implements counterexample-guided abstractionrefinement framework based on the Fourier Transform and other learning algorithms (31-Dec-2001). Tool that generates good BDD and SAT splitting-orders based on important variables in the circuit (31-Apr-2002). January 25, 2020 56 Technical presentation for this task follows in PDF format January 25, 2020
57 Efficient Image Computation Algorithms Pankaj Chauhan Dong Wang Edmund M. Clarke Joint work with Somesh Jha, Jim Kukula, Helmut Veith Efficient Image Computation Algorithms Description: Various techniques for faster image computation Goals: A collection of algorithms for efficient image computation Integration of algorithms in NuSMV model checker and extensive experimental evaluation January 25, 2020
59 Efficient Image Computation Algorithms Plans and directions for the current year (2000): Compare existing techniques and understand their limitations Explore alternate metrics for predicting image computation costs Propose, evaluate and tune algorithms that improve these metrics to aid image computation January 25, 2020 60 Efficient Image Computation Algorithms Accomplishments for the current year (2000): A collection of algorithms based on combinatorial optimization for various metrics All these techniques are made available in NuSMV
model checker and built an evaluation framework January 25, 2020 61 Efficient Image Computation Algorithms Plans and directions for the next year (2001): Continue the implementation to include even more techniques Evaluate the algorithms on more strength examples Explore the use of efficient partitioning schemes for image computation Use the techniques for other applications, including efficient abstraction generation January 25, 2020 62 Efficient Image Computation Algorithms
Milestones Experimental evaluation of combinatorial optimization based methods (31-Jan-2001) Paper on efficient image computation using combinatorial optimization methods (31-June-2001) Paper on VarScore algorithm and improved version of Kernighan-Lin based heuristics (31-Sept-2001) Improved partitioning method for image compuation (31-Dec-2001) Application of techniques to abstraction and non BDD based image computation January 25, 2020 63 Introduction Image Computation is the heart of Symbolic Model Checking Partitioned Transition relations are required for all real world designs Conjunctive and Disjunctive Partitioning are the
fundamental partitioning techniques January 25, 2020 64 The Problem The goal is to reduce the size of intermediate BDDs Image Computation depends on: Clustering: How the clusters C1, C2,,Cm are derived from T1, T2,,Tk? Ordering: How the clusters are ordered in the formula for Im(S) Variants are NP-Complete January 25, 2020 65 Current State of the Art
Heuristic score based (Ranjan et. al., IWLS95, Yang99) Dependency matrices (Somenzi, Moon et.al. DAC00, FMCAD00) SAT+BDD (Gupta, FMCAD00) January 25, 2020 Procedure: Order the conjuncts Cluster the conjuncts to form larger clusters Order the clusters 66 Dependency Matrices
Rows correspond to functions T1, T2,,Tm , columns correspond to variables v1,v2,,vn D[i,j]=1 iff vj is in the support of fi, otherwise 0 Average active life-time 1j m January 25, 2020 v1 v2 v3 v1 v2 v3 T1 1 0 0
1 0 0 T2 1 1 0 0 1 0 T3 1
1 1 0 0 1 Dependency matrix for 3-bit counter (h j l j 1) n m 67 Overview of New Techniques Procedure: Break large conjuncts by cut-pointing
Order the conjuncts Ordering Algorithms based on sharing graphs Ordering algorithms based on minimization of Cluster the conjuncts to form larger clusters VarScore Algorithms Order the clusters January 25, 2020 68 Sharing Graph based Ordering Construct a sharing graph whose vertices correspond to conjuncts
The weight of the edge E(Ti,Tj) is w1 Supp(Ti ) Supp(T j ) Supp(Ti ) Supp(T j ) w2 BddSize(Ti T j ) BddSize(Ti ) BddSize(T j ) w1 0, w2 0 are parameters High weight strong interaction Propose two algorithms to order the vertices of this graph January 25, 2020 69 Ordering Algorithm KLin KLinOrder(G(V,E),W)
1. Split V into L,Li,Ri and R Find a good split L,R with Kernighan-Lin Heuristic Li and Ri are vertices adjacent to the other half (interface vertices) 2. Recursively order L-Li,Li,Ri and R-Ri 3.
Order the vertices as L-Li < Li < Ri < R-Ri January 25, 2020 G L Li Ri R 70 Ordering Algorithm METIS While partitioning a smaller graph, consider other preplaced vertices as well Assign node weight 0 to
preplaced nodes, while retain edge weights Partition and order vertices in depth-first fashion January 25, 2020 71 Overview of New Techniques Procedure: Break large conjuncts by cut-pointing Order the conjuncts Ordering Algorithms based on sharing graphs Ordering algorithms based on minimization of
Cluster the conjuncts to form larger clusters VarScore Algorithms Order the clusters January 25, 2020 72 Ordering by Minimization of Average active lifetime indicates the interaction among various components 1j m (h j l j 1) n m
Lower means relatively disjoint support We want to minimize Rows and columns of dependency matrix are permuted to improve Moon et.al. (FMCAD00) use an indirect method (PPP) Dependency matrix is restricted to the variables that are to be quantified January 25, 2020 73 Optimization of s Use combinatorial optmization to reorder conjuncts to get better s (eg. Hill climbing, Simulated Annealing, GA, etc.) Require careful tuning of many parameters Provide good performance as long the metric being optimized relates directly to image computation costs
January 25, 2020 74 Simulated Annealing Algorithm SimAnnealOrder(D) Compute for D for i=1 to NumStarts do let ti=t0ri for j=1 to NumStarts2 do permute two random rows of D to get Di if (i < ) then set = i, D = Di else with probability exp(-(i-)/ti) set = i, D = Di endfor endfor January 25, 2020 75 Overview of New Techniques Procedure: Break large conjuncts by cut-pointing Order the conjuncts Ordering Algorithms based on sharing graphs Ordering algorithms based on minimization of Cluster the conjuncts to form larger clusters VarScore Algorithms Order the clusters January 25, 2020
76 VarScore Algorithms Image computation equation: Im(S ) CWV (Tm ...T1 S ) Can be seen as building a parse tree for Im(S) Variables not appearing other subtrees can be quantified away immediately Instead of ordering the conjuncts linearly, build a tree so that intermediate BDDs are small January 25, 2020 77 VarScore Algorithms We propose two versions of VarScore algorithms Dynamic version builds the parse tree for each image computation Static version builds the parse tree once, albeit with some inaccuracies
Clustering is very similar to ordering January 25, 2020 78 VarScore (Dynamic Version) v1 Exists And v2 AndExists Conjunct v3 T1 (v'1 v1 ) T1 (v'1 v1 ) T3 (v'3 (v1 v2 ) v3 ) January 25, 2020
S v1 79 VarScore (Static Version) Dynamic version repeats lots of same operations across image computation Build a psuedo-tree without S, assuming S contains all variables in support Size of BDDs are estimated from some function of number of support variables All subtrees not in the path from S to root can be evaluated in the beginning Present state variables cant be quantified January 25, 2020 80 Initial Experimental Results We get about 30-40% average space
improvement Best 2x speedup, average 30-40% We complete 4 examples which FMCAD00 couldnt do Smaller BDDs yield better running time for larger circuits January 25, 2020 81 Conclusions Simulated Annealing performs well on large circuits Sharing graph based techniques show promise, though not as good as simulated annealing Spending more time in initial ordering phase speeds up image computation January 25, 2020 82
Future Work More experimentation, evaluation Complete the implementation Improved algorithms for partitioning Complete the evaluation of VarScore algorithms Application of these techniques to other areas(?) January 25, 2020 83 Questions? January 25, 2020
84 Partitioned Transition Relations V= v1,,vn : current state variables V= v1,,vn : next state variables W= w1,,wk : input variables Q={V U W} The transition relation T(V,W,V) is typically given as a conjunction T (V ,W ,V ' ) ... T (V ,W ,V ' ) 1 k Typically, each Ti is a transition relation for one state variable The set of variables on which Ti depends denoted by Supp(Ti) January 25, 2020
85 Image Computation Monolithic Representation Im( S ) WV (T (V , W , V ' ) S (V )) Infeasible in practice as the BDD for T is too large January 25, 2020 86 Early Quantification Result of early quantification: Im(S ) Qm (Tm Qm 1 (Tm 1 ...Q1 (T1 S )...)) where Q1 appear only in Supp(T1 ) Q2 appear only in Supp(T1 ) Supp(T2 )
Gain: Smaller intermediate results January 25, 2020 87 A Toy Example A 3-bit counter V {v1 , v2 , v3 } V ' {v'1 , v'2 , v'3 } T1 (v'1 v1 ) T2 (v'2 v1 v2 ) Supp(T1 ) {v1 , v'1 } Supp(T2 ) {v1 , v2 , v'2 } Supp(T3 ) {v1 , v2 , v3 , v'3 } T3 (v'3 (v1 v2 ) v3 ) T T1 T2 T3 S (V ) v1 (all even numbers) January 25, 2020
88 Cutpoints for Finer Partitioning Clustering helps when the circuit is finely partitioned What if the partition is too coarse (in other words, to large to be represented by a single BDD? Idea: Introduce cut-points in the circuit of the next state function of a variable [Burch, Singhal ICCAD98] No need to introduce a latch For a conjunct Ti with cut-point c representing a sub-circuit fc, generate two conjuncts Ti[c] and c fc Need to quantify away cut-points while computing the image, no need to introduce a latch January 25, 2020 89
Benchmark Characteristics Ckt #FFs #inputs log2(#reach) Ckt #FFs #inputs log2(#reach) IU35 35
163 22.49 TCAS 139 0 106.87 IU40 40 159 25.85 S1269
37 18 30.07 IU45 45 183 29.82 21512 57 29
40.59 IU50 50 615 31.57 S5378 179 35 57.71 (after 8 steps) IU55 55
625 33.94 S4863 104 49 72.35 IU65 65 632 39.32
S3271 116 26 79.83 IU70 70 635 42.07 S3330 132 40
86.64 Sfeistel IU75 75 322 46.59 293 69 218.77 s1423 IU80
80 350 49.8 74 17 37.41 (after 16 steps) IU85 85 362 52.14
January 25, 2020 90 Which to use? For each version of we can either take total lifetime or active lifetime We ran iu40 with getting different values of various s and found the following correlation coefficients Original Size based Active Total Active Total Run Time 0.559762 0.303281 0.468684 0.297907 Space 0.609686 0.227472 0.435179 0.235179
January 25, 2020 91 Ordering by Minimization of (contd.) We have shown that this problem is NPComplete Idea 1 : Use standard AI heuristics! Might be slower, but definitely better then indirect approach, experiments support this hypothesis We propose using variations of hill climbing and simulated annealing January 25, 2020 92 Ordering by Minimization of (contd.) Metricas defined does not take into account
relative sizes of conjuncts Define a new metric size that weighs each conjunct by the size of its BDD 1j m size BddSize(i) l j i h j m BddSize(i ) 1i n January 25, 2020 93