SAT-based Methods

SAT-based Methods

Integrating AIG Package, Simulator, and SAT Solver Alan Mishchenko Department of EECS UC Berkeley Overview AIG, SIM, SAT Traditional use of SIM and SAT Motivation for a deeper integration Additional book-keeping Window-based computing Local fanout for nodes in the window Modifying SIM and SAT to use local fanout Experiments Conclusion and future work 2 And-Inverter Graph (AIG) AIG is a Boolean network composed of two-input ANDs and inverters. 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

ab F(a,b,c,d) = ab + d(ac+bc) a 6 nodes d b 4 levels a 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 ab c b c F(a,b,c,d) = ac(bd) + c(ad) = ac(b+d) + bc(a+d) 7 nodes 3 levels a c b

d b c a d Simulation (SIM) Assigns particular (or random) values at the primary inputs Multiple simulation patterns are packed into 32- or 64-bit strings Simulates in a topological order Works well for an AIG due to The uniformity of AND-nodes Speed of bitwise simulation Topological ordering of memory reducing CPU cache misses when accessing the simulation patterns 1 0 2 0

3 0 4 1 1 0 2 0 3 1 4 1 a b c d 1 0 1 0 1

2 1 0 0 0 3 1 0 1 1 4 1 1 0 1 1 0 2 0 3 1

4 0 SAT in Practical Applications Netlist Answer: SAT or UNSAT Design constraints CNF CNF CNF generator SAT solver If SAT, a counter-example If UNSAT, a core User cost functions Both counter-examples and cores are useful in SAT-based applications. In practice, cores are often represented as subsets of assumptions that make the problem UNSAT. SIM and SAT SIM is faster than SAT (P vs NP) It takes SAT longer to disprove properties not disproved by SIM

Re-simulating each assignment over a large AIG is very slow But, if we do not re-simulate, SAT is very slow Previous solution: batching This is why, state-of-the-art engines re-simulate CEXes returned by earlier SAT calls to disprove new properties before trying SAT on them The problem is SIM is often used before SAT to disprove easy properties Collect and re-simulate N (for example, N=16) assignments at once Both SIM and SAT runtime is better (but is still slow) In this work, we propose a better solution It is based on a deeper integration of SIM and SAT Case Study: SAT sweeping SAT sweeping computes functionally equivalent nodes, to be used in Combinational / sequential synthesis and verification Computing structural choices needed to improve area/delay after tech-mapping

Transferring names from the initial netlist to the netlist after synthesis (with modifications) Optimization with dont-cares and redundancy removal SAT sweeping is hard for AIGs with 100+ logic levels and 1M+ of nodes Efficient use of SIM and SAT is needed In this work, SAT sweeping is used as a case-study to illustrate a deeper integration of SIM and SAT Past work on SAT sweeping F. Lu, L. Wang, K. Cheng, R. Huang. A circuit SAT solver with signal correlation guided learning. Proc. DATE 03. A. Kuehlmann, Dynamic transition relation simplification for bounded property checking. Proc. ICCAD 04. A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton, "FRAIGs: A unifying representation for logic synthesis and verification". ERL Technical Report, EECS Dept., UC Berkeley, March 2005. SAT Sweeping Ecosystem Equivalence class manager - maintains all cand. equivs. - keeps track of proved ones - refines disproved ones SAT sweeping manager - initializes managers and equivalence classes - iterates over nodes in a topological order - defines windows for SIM / SAT ndows - updates candidate equivalence classes Window simulator - disproves candidate equivs.

- enables fast CEX simulation Window SAT solver - proves/disproves cand. equivs. - generates CEXes for simulator Window local fanout manager - keeps fanouts for the nodes in the window - enables fast local simulation and SAT Window-Based Computation Our goals: scalability, fast runtime, low-memory SIM and SAT work on nodes in the window Considering the whole circuit is counter-productive Instead, we consider a moving window Book-keeping info is kept only for these nodes Windowing is dynamic When computation moves to a different location, window is updated (and book-keeping information re-computed) Boolean network (AIG) Current window Target nodes Future window Previous window

Circuit-Based Solver (CBS) Works on nodes in a window Uses circuit for BCP and CNF for learned clauses Otherwise, similar to MiniSAT / Glucose Generates incomplete assignments Data structure resizes when new nodes are added to the window This reduces work by both SAT and SIM Incomplete assignments are possible due to the use of J-frontier, a key feature of CBS Using Local Fanout in SAT Our SAT solver works on the circuit Using global fanout info (fanouts for all nodes) is not efficient This is because SAT solver propagates constraints to all fanouts,

including those outside of the cone of influence of the target node(s) This is why we maintain local fanout info Propagating in the direction of fanins is easy Propagating in the direction of fanouts requires having fanout info available Only for the nodes in the window (excluding side nodes and their fanouts) Local fanout is kept in a dedicated manager and dynamically updated Boolean network (AIG) Target node whose value is computed by the SAT solver Useless fanouts Useful fanouts Current window Node looked at by the solver Using Local Fanout in SIM In the past, when SAT solver produces a CEX, window is re-simulated Computation can be improved using local fanouts of the nodes In the process, even nodes whose values did not change are re-simulated This way if a CEX is incomplete, re-simulation is applied to a fraction of the nodes, which reduces runtime, without changing the result of simulation The local fanout enables incremental event-driven simulation for the

nodes whose values have changed under the latest CEX Boolean network (AIG) In the past, the complete window is re-simulated Primary inputs whose values did not change Target node whose simulation info is being computed by SIM A fraction of the window is re-simulated in the event-driven fashion using local fanout Primary inputs whose values have changed according to the CEX Deeper Integration of SIM and SAT Recall that previous work resorts to batching Collects and re-simulates N (for example, N=16) assignments at once Both SIM and SAT take less time (but still slow) In this work, we propose a better solution The idea is to perform eager re-simulation (no batching) of CEXes while relying on deeper integration of SIM and SAT The runtime is not a problem because

Circuit-based SAT is fast and produces incomplete assignments SIM is fast when applied to only affected nodes in the window The cumulative runtime reduction of SAT sweeping is 2-5x Experimental Results Preliminary experiments, comparing two SAT solvers CNF-based solver MiniSAT Circuit-based solver CBS developed for the proposed ecosystem The benchmarks are two AIGs derived by recording the sequence of SAT calls while processing a large design with Sequential signal correspondence (command scorr in ABC) Computing structural choices (command dch in ABC) Table 1: Problem statistics Testcase scorr_aig dch_aig Primary inputs 135476 13601 SAT calls 98192

84460 AND nodes 544369 538014 Experimental Results Table 2: SAT call count comparison Testcase Total calls scorr_aig dch_aig 98192 84460 Unsat calls Sat calls Undecided calls MiniSAT CBS MiniSAT CBS MiniSAT CBS 31346 31811 65249 65549 1597 832 14053 13268 26660 39287 43747 31905 Table 3: Runtime comparison (in seconds) Testcase scorr_aig dch_aig Unsat calls MiniSAT CBS 1.20 0.18 1.38 0.11 Sat calls MiniSAT CBS

7.28 0.60 23.71 4.66 Undecided calls MiniSAT CBS 0.51 0.11 60.23 9.03 Discussion CBS It is faster than MiniSAT because does not need to generate and load CNF Saves time because the majority of runs are easy (solved by BCP without conflicts) It generates incomplete assignments Less It BCP to do and less work for the simulator uses local fanout and incremental window updating Conclusion Reviewed state-of-the-art in SIM and SAT

Motivated the need for a deeper integration Showed how to achieve it by designing new engines for SIM and SAT Developed a new AIG package to enable efficient windowing and managing local fanouts in the window Experimental results show that the new circuit-based solver CBS is efficient Future work Finish integration and tuning of SAT and SIM, as discussed above Propagate changes to relevant ABC packages (&cec, &scorr, dch, pdr, ) Extend the ecosystem to work with dont-cares (resub, mfs, ) Customize circuit-based solver for other netlists (XAIG, MXAIG, MIG, 4LUT, ) Abstract This presentation discusses computations where the interdependence of simulation and Boolean satisfiability (SAT) is critical. A modified AIG data-structure is proposed to optimize the speed of logic manipulation for large problems of this type. Experimental results confirm that the new implementation is faster, compared to the old one, in which runtime and scalability has been a known issue.

Recently Viewed Presentations

  • LIS 605 - University of Hawaii

    LIS 605 - University of Hawaii

    Boolean, bibliometrics, and beyond Part 1 LIS 670 donna Bair-Mundy
  • mentor.ieee.org

    mentor.ieee.org

    met in Berlin (July 2017), Hawaii (Sept 2017), Orlando (Nov 2017), Irvine (Jan 2018), Chicago (Mar 2018), Warsaw (May 2018), San Diego (July 2018), Hawaii (Sept 2018), Bangkok (No
  • Mythological Creatures Mythological Creatures Monsters and hybrids (human-animal

    Mythological Creatures Mythological Creatures Monsters and hybrids (human-animal

    Charybdis. Charybdis (Greek mythology) is one of several Greek monsters that appeared in multiple famous myths. She is often known only in her most vicious form - a swirling whirlpool of death that swallowed enormous amounts of water and anything...
  • Object Oriented Software Analysis and Design

    Object Oriented Software Analysis and Design

    Identifying Things Outside The Scope of The System. Identifying Synonyms. Identifying Potential Classes. Identifying Potential Attributes. Identifying Potential Methods. Identifying Common Characteristics. Refining Our Design using CRC Cards. Elaborating Classes.
  • PowerPoint 簡報 - 國立臺灣大學

    PowerPoint 簡報 - 國立臺灣大學

    Second-order Circuits. Steps for solving by differential equation. 1. List the differential equation (Chapter 9.3) 2. Find natural response (Chapter 9.3) There are some unknown variables in the natural response. 3. Find forced response (Chapter 9.4) 4. Find initial conditions...
  • Digital Games and Sociology Research Alex Burns (aburns@swin.edu.au)

    Digital Games and Sociology Research Alex Burns ([email protected])

    Digital Games and Sociology Research Alex Burns ([email protected]) Smart Internet Technology CRC 13 September 2005 Industry & Government Partners Agenda Computer Game History Global and Australian Industry Context Auteurs and Independents Digital Game-Based Learning Game Studies Computer Game History 1...
  • doc.: IEEE 802. 15-09-0804-14-004f June 2010 Project: IEEE

    doc.: IEEE 802. 15-09-0804-14-004f June 2010 Project: IEEE

    This is an important issue for OOK modulation since no synchronization update can be made within the receiver unless a "1" is received. For this reason, a long sequence of zeros will cause a long period between frequency drift updates...
  • Main Parts of a Book - West Geauga High School

    Main Parts of a Book - West Geauga High School

    Main Parts of a Book Non-fiction Texts Introduction Knowing the parts of a book help you find information faster and more efficiently. It will save you time and effort especially when it comes to writing your bibliography.