Report

ABC: An Academic “Industrial-Strength” Verification Tool (based on a tutorial given at CAV’10) BVSRC Berkeley Verification and Synthesis Research Center UC Berkeley Robert Brayton, Niklas Een, Alan Mishchenko Jiang Long, Sayak Ray, Baruch Sterin Thanks to: NSF, NSA, SRC, and industrial sponsors, Actel, Altera, Atrenta, IBM, Intel, Jasper, Magma, Oasys, Real Intent, Synopsys, Tabula, and Verific Overview General introduction to ABC Synergy between synthesis and verification Introduction to AIGs Contrast between classical synthesis and ABC synthesis ABC+ - orchestrated verification flow Simplification Extraction of constraints Phase abstraction Forward and minimum FF retimiing K-step induction Abstraction Abstraction Speculation Last gasp: BMC, BDDs, interpolation Verification example Future work 2 ABC A synthesis and verification tool under development at Berkeley Started 6 years ago as a replacement for SIS Academic public domain tool “Industrial-strength” Has been employed in commercial offerings of various CAD companies In both synthesis and verification Exploits the synergy between synthesis and verification 3 A Plethora of ABCs http://en.wikipedia.org/wiki/Abc ABC (American Broadcasting Company) ABC (Active Body Control) In C++, these are generic classes at the base of the inheritance tree; objects of such abstract classes cannot be created… Atanasoff-Berry Computer ABC is designed to minimize body roll in corner, accelerating, and braking. The system uses 13 sensors which monitor body movement to supply the computer with information every 10 ms… ABC (Abstract Base Class) A television network… The Atanasoff–Berry Computer (ABC) was the first electronic digital computing device.[1] Conceived in 1937, the machine was not programmable, being designed only to solve systems of linear equations. It was successfully tested in 1942. ABC (supposed to mean “as simple as ABC”) A system for sequential synthesis and verification at Berkeley 4 Design Flow ABC - Property Checking System Specification Equivalence checking RTL Logic synthesis Technology mapping Verification ABC Physical synthesis Manufacturing 5 Areas Addressed by ABC Combinational synthesis AIG rewriting technology mapping resynthesis after mapping Sequential synthesis retiming structural register sweep merging seq. equiv. nodes Verification combinational equivalence checking bounded sequential verification unbounded sequential verification equivalence checking using synthesis history property checking (safety and liveness) 6 Synergy – Two Kinds 1. The algorithms and advancements in verification can be used in synthesis, and vice versa. 2. One enables the other Verification enables synthesis - equivalence checking capability enables acceptance of sequential transformations retiming use of unreachable states sequential signal correspondence, etc Synthesis enables verification Desire to use sequential synthesis operations (shown by superior results) spurs verification developments 7 Examples of The Synergy Similar solutions Algorithm migration e.g. BDDs, SAT, induction, interpolation, rewriting Related complexity e.g. retiming in synthesis / retiming in verification scalable synthesis <=> scalable verification (approximately) Common data-structures e.g. combinational and sequential AIGs 8 Evidence of Synergy Between Synthesis and Verification IBM ABC Has a very capable sequential verification engine – SixthSense. Used throughout IBM to verify property and equivalence Designers more willing to consider sequential transformations now. Sequential verification was developed to check that new algorithms were implemented correctly Example of a startup company Had developed sequential methods to reduce power Needed a verification tool to double check if their ideas and implementations were correct. Needed a tool to assure customers that results were correct. 9 AIG (And-Inverter Graphs) Definition and Examples AIG is a Boolean network composed of two-input ANDs and inverters ab 00 01 11 10 00 0 0 1 0 01 0 0 1 1 11 0 1 1 0 10 0 0 1 0 cd F(a,b,c,d) = ab + d(ac’+bc) a 6 nodes d b 4 levels a a c b c F(a,b,c,d) = ac’(b’d’)’ + c(a’d’)’ = ac’(b+d) + bc(a+d) 00 01 11 10 00 0 0 1 0 01 0 0 1 1 11 0 1 1 0 7 nodes 10 0 0 1 0 3 levels cd b a c b d b c a d 10 AIGs Structural hashing F = abc G = (abc)’ H = abc’ Performs AIG compaction Applied on-the-fly during construction Propagates constants Makes each node structurally unique Before After 11 AIGs (And-Inverter Graphs) Why AIGs? Same reasons hold for both synthesis and verification Easy to construct, relatively compact, robust Can be efficiently stored on disk 3-4 bytes / AIG node (1M AIG ~ 4Mb file) Unifying representation 1M AIG ~ 12Mb RAM Used by all the different verification engines Easy to pass around, duplicate, save Compatible with SAT solvers Efficient AIG-to-CNF conversion available Circuit-based SAT solvers work directly on AIG “AIGs + simulation + SAT” works well in many cases 12 AIG Memory Usage Memory allocation Use fixed amount of memory for each node Can be done by a simple custom memory manager Dynamic fanout manipulation is supported! Allocate memory for nodes in a topological order Optimized for traversal in the same topological order Mostly AIG can be stored in cache – fewer cache misses. Small static memory footprint in many applications Compute fanout information on demand 13 Quick Overview of “Classical” (technology independent) Logic Synthesis Boolean network Network manipulation (algebraic) f Elimination (substituting a node into its fanouts) Decomposition (commondivisor extraction) xd y ydydxy yd z x+c xx Espresso Don’t cares Resubstitution (algebraic or Boolean) ze z Node minimization (Boolean) Boolean network in SIS y abab cd cd e a b c d 14 “Classical” Logic Synthesis Boolean network in SIS Equivalent AIG in ABC f f z ze xd yd xy x z y ab x cd cd y e a b c d e a b c d AIG is a Boolean network of 2-input 15 AND nodes and invertors (dotted lines) One AIG Node – Many Cuts Combinational AIG f AIG can be used to compute many cuts for each node Each cut in AIG represents a different SIS node a b c d e Different cuts for the same node SIS node logic represented by AIG between cut and root. No a priori fixed boundaries Implies that AIG manipulation with cuts is equivalent to working on many Boolean networks at the same time 16 Combinational Synthesis AIG rewriting minimizes the number of AIG nodes without increasing the number of AIG levels Rewriting AIG subgraphs Pre-computing AIG subgraphs Rewriting node A Consider function f = abc Subgraph 1 Subgraph 2 A A a b Subgraph 3 a c b a c Subgraph 2 Subgraph 1 Rewriting node B a a b a c b b c B a B c a a b a c b c Subgraph 2 a b a c Subgraph 1 In both cases 1 node is saved 17 Combinational Rewriting iterate 10 times { for each AIG node { for each k-cut derive node output as function of cut variables if ( smaller AIG is in the pre-computed library ) rewrite using improved AIG structure } } Note: For 4-cuts, each AIG node has, on average, 5 cuts compared to a SIS node with only 1 cut Rewriting at a node can be very fast – using hash-table lookups, truth table manipulation, disjoint decomposition 18 Comparison of Two Syntheses “Contemporary” synthesis “Classical” synthesis Boolean network Network manipulation (algebraic) AIG network DAG-aware AIG rewriting (Boolean) Espresso Don’t cares computed using BDDs Resubstitution Several related algorithms Elimination Decomposition (common kernel extraction) Node minimization Node minimization Rewriting Refactoring Balancing Boolean decomposition Don’t cares computed using simulation and SAT Resubstitution with don’t cares Note: here all algorithms are scalable: no SOP, no BDDs, no Espresso 19 Sequential Verification Property checking Create miter from the design and the safety property Special construction for liveness p 0 Biere, Artho, Schuppan D1 Equivalence checking Property checking miter Create miter from two versions of the same design Assuming the initial state is given The goal is to prove that the output of the miter is 0, for all states reachable from the initial state. Equivalence checking miter 0 D1 D2 20 Integrated Verification Flow 1. 2. 3. 4. Simplification Abstraction Speculation High effort verification 21 Integrated Verification Flow 1. Simplification Initial fast simplification of the logic Forward retime and do FF correspondence Min FF retime Extract implicit constraints** and use them to find signal equivalences (ABC command scorr –c) Fold back the constraints add a FF so that if ever a constraint is not satisfied, make the output 0 forever after that. Trim away irrelevant inputs (do not fanout to FF or POs) Try phase abstraction (look for periodic signals) Heavy simplify (k-step signal correspondence and deep rewriting) ** (see paper of Cabodi et. al.) 22 Sequential SAT Sweeping (signal correspondence) Related to combinational CEC • Naïve approach • Build output miter – call SAT D1 D2 ? SAT-2 D ? C SAT-1 A B works well for many easy problems Better approach - SAT sweeping • based on incremental SAT solving • detects possibly equivalent nodes using simulation • candidate constant nodes • candidate equivalent nodes • runs SAT on the intermediate miters in a topological order • Proving internal equivalences in a topological order refines candidates using counterexamples 23 Improved CEC For hard CEC instances Heuristic: skip some equivalences results in 5x reduction in runtime solving previously unresolved problems Given a combinational miter with equivalence class {A, B, A’, B’} Possible equivalences: A = B, A = A’, A = B’, B = A’, B = B’, A’ = B’ A B D1 A’ B’ D2 - only try to prove A=A’ and B=B’ - do not try to prove A = B, A’ = B’, A’ = B A = B’ 24 Sequential SAT Sweeping (signal correspondence) Similar to combinational SAT sweeping detects node equivalences But the equivalences are sequential guaranteed to hold only on the reachable state space Every combinational equivalence is a sequential one run combinational SAT sweeping first A set of sequential equivalences are proved by k-step induction Base case Inductive case Efficient implementation of induction is key! 25 k-step Induction Base Case (just BMC) Inductive Case ? Candidate equivalences: {A = B}, {C = D} Proving internal equivalences in a topological order in frame k+1 ? SAT-4 D ? ? C D SAT-1 A B PIk k=2 D PI0 ? C SAT-1 A B initial state Proving internal equivalences in initialized frames 1 through k Assuming internal equivalences in uninitialized frames 1 through k If proof of any one equivalence fails need to start over 0 C SAT-2 D ? C 0 SAT-3 A B PI1 SAT-2 A 0 B PI1 D 0 C A PI0 B arbitrary state 26 Efficient Implementation Two observations: 1. Both base and inductive cases of k-step induction are combinational SAT sweeping problems Tricks and know-how from the above are applicable base case is just BMC The same integrated package can be used starts with simulation performs node checking in a topological order benefits from the counter-example simulation Speculative reduction Deals with how assumptions are used in the inductive case 2. 27 Integrated Verification Flow (continued) 2. Abstraction Use new CBA/PBA method* Uses single instance of SAT solver Uses counter-example based abstraction which is refined with proof-based abstraction Checked afterward with BMC, BDDs, and simulation for CEX’s and refined with CBA if found. * N. Een, A. Mishchenko, and N. Amla, "A single-instance incremental SAT formulation of proof- and counterexample-based abstraction". Proc. IWLS'10. 28 Integrated Verification Flow (continued) 3. Speculation ** Especially useful for SEC Simulation used to find candidate equivalences. These are equivalences that we could not prove by induction (sequential SAT sweeping) These are used to build a “speculative miter” The result is double-checked with BMC, BDDs or simulation for CEX’s and refined if necessary. ** H. Mony, J. Baumgartner, V. Paruthi, and R. Kanzelman, “Exploiting suspected redundancy without proving it”. Proc. DAC’05. 29 Integrated Verification Flow (continued) 4. Final high-effort verification (prove or disprove) Prove: (give long run-time limits and/or large conflict limits) Try BDD reachability if problem is small enough (< 200 PI, < 200 FFs) Try interpolation Try induction In rare cases, can prove outputs using induction. Disprove: (give large run-time and conflict limits) Try heavy BMC on initial simplified circuit (before abstraction or speculation done). 30 Interpolation Input: Sequential AIG with single output representing a property Property holds when the output is 0 Method: Over-approximate reachability analysis Using over-approximations, instead of exact sets of reachable states Output: Proof that 1. 2. 3. the property holds, or a real CEX is provided, or “undecided” Implementation: A sequence of SAT calls on unrolled time-frames that is similar to BMC A inter I 21 k T1 B T2 T3 L Tn ~property P=1 UNSAT interpolan t 31 BDD-Based Reachability Still an important back-end of the verification flow Also useful to find CEX’s during abstraction and speculation refinement Several ideas, old and new, can be put together to implement a new improved engine Long live BDDs! BDD We tried to ban BDDs in ABC 32 Examples of Running ABC+ 1. Example 1 of simplifying and final proof with interpolation 2. Prove python code 33 Read_file IE1.aig PIs = 532, POs = 1, FF = 2389, ANDs = 12049 prove Example (use of prove) Simplifying Number of constraints = 3 Forward retiming, quick_simp, scorr_constr, trm: PIs = 532, POs = 1, FF = 2342, ANDs = 11054 Simplify: PIs = 532, POs = 1, FF = 2335, ANDs = 10607 Phase abstraction: PIs = 283, POs = 2, FF = 1460, ANDs = 8911 quick_verify Abstracting Initial abstraction: PIs = 1624, POs = 2, FF = 119, ANDs = 1716, max depth = 39 Testing with BMC bmc3 -C 100000 -T 50 -F 78: No CEX found in 51 frames Latches reduced from 1460 to 119 Simplify: PIs = 1624, POs = 2, FF = 119, ANDs = 1687, max depth = 51 Trimming: PIs = 158, POs = 2, FF = 119, ANDs = 734, max depth = 51 Simplify: PIs = 158, POs = 2, FF = 119, ANDs = 731, max depth = 51 quick_verify Speculating Initial speculation: PIs = 158, POs = 26, FF = 119, ANDs = 578, max depth = 51 Fast interpolation: reduced POs to 24 Testing with BMC bmc3 -C 150000 -T 75: No CEX found in 1999 frames PIs = 158, POs = 24, FF = 119, ANDs = 578, max depth = 1999 Simplify: PIs = 158, POs = 24, FF = 119, ANDs = 535, max depth = 1999 Trimming: PIs = 86, POs = 24, FF = 119, ANDs = 513, max depth = 1999 Verifying Running reach -v -B 1000000 -F 10000 -T 75: BDD reachability aborted RUNNING interpolation with 20000 conflicts, 50 sec, max 100 frames: 'UNSAT‘ Elapsed time: 457.87 seconds, total: 458.52 seconds 34 Python Code for prove def prove(a): global x_factor,xfi,f_name max_bmc = -1 K=0 set_globals() status = pre_simp() if status <= Unsat: return RESULT[status] ABC('trm') ABC('write backup 0’) K = K +1 set_globals() if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)): status = quick_verify(0) if ((status == Unsat) or (status == Sat)): return RESULT[status]' status = abstract() ABC('trm') status = process_status(status) if ((status <= Unsat) or status == Error): return RESULT[status] ABC('write backup 1’) K = K +1 if status == Undecided_reduction: status = quick_verify(1) status = process_status(status) if status <= Unsat: if status == Sat: status = final_verify_recur(K-1) return RESULT[status] if n_ands() > 15000: K=2 else: status = speculate() ABC('trm') status = process_status(status) if ((status == Unsat) or status == Error): return RESULT[status] if status == Sat: K = K-1 else: ABC('write backup 2’) K = K +1 status = final_verify_recur(K) return RESULT[status] 35 Verification Engines (Summary) Simplifiers Combinational synthesis Sequential synthesis Re-parametrization (not implemented yet in ABC currently) Retiming (most forward and minimum FF) Bug-hunters (also part of abstraction methods) Retiming Sequential SAT sweeping (k-step induction) random simulation (sequential) bounded model checking (BMC) hybrid of simulation and BMC (“semi-formal”) BDD reachability Provers K-step induction, with and without constraints Interpolation (over-approximate reachability) BDDs (exact reachability) Explicit state space enumeration (‘era’) 36 Future Work Improved BDD reachability engine (we hope) We have three Improved interpolation engine One is quite weak (HWMCC’08) We have just integrated a better one May have a much better one later. Working on a new version Improved circuit-based SAT solver Currently used in signal correspondence to simplify larger circuits Faster but sometimes limited quality Will be improved to see if it can compete with MiniSat 1.14c 37 To Learn More Read recent papers http://www.eecs.berkeley.edu/~alanmi/publications Send email [email protected] [email protected] Visit BVSRC webpage www.bvsrc.org 38 39 end 40