Department of EECS, University of California, Berkeley

Research Overview

MVSIS Group

Department of EECS, University of California, Berkeley

Contents

1. AND-INV Graph Basics

2. Applications of FRAIGs

2.1. Logic Synthesis

2.2. Technology Mapping

2.3. Formal Verification

3. RecentWork by Our Group

References

1AND-INV Graph Basics

Definition. AND-INV graph (AIG) is a Boolean network composed of two-input AND-gates and inverters.

The traditional AIGs are used in logic synthesis [5], technology mapping [12], and verification [9]. They are not canonical, that is, the same function can be represented by two functionally equivalent AIGs, which have different structure. An example is shown in Figure 1.

Figure 1. Two different AIGs for the same function.

Definition. The size of an AIG is the number of AND nodes in it. The number of logic levels is the number of ANDs on the longest path from a primary input to a primary output.

The inverters are ignored when counting nodes and logic levels. In software, inverters are implemented by flipping the least significant bit on the node pointers.

Definition. The function of an AIG node n, denoted fn(x), is a Boolean function of the AIG subgraph rooted in n and expressed in terms of the PI variables x assigned to the leaves of the graph.

Definition. A functionally reduced AIG (FRAIG) is an AIG, in which, for any pair of nodes, n1 and n2, and .

In the known AIG-based applications, functional reduction is performed as a post-processing step [13][11]. Recently we developed an algorithm [21] to perform functional reduction on-the-fly. This algorithm takes only a few seconds to construct FRAIGs for the largest benchmarks, which is much faster than using the post-processing.

The resulting FRAIGs are useful as a compact functional representation whose special properties facilitate solving difficult tasks in logic synthesis, technology mapping, and formal verification.

2Applications of FRAIGs

2.1Logic Synthesis

A straight-forward use of FRAIGs in logic synthesis is to compact circuits by detecting and merging functionally equivalent nodes, similarly to [5]. Global FRAIGs for all the nodes are constructed. Next, the nodes are grouped into classes according to the underlying FRAIG nodes. One representative of each class is selected and substituted for other nodes of the same class.

Other potential applications of FRAIGs in synthesis include: (a) a uniform representation of algebraic factored forms and DAGs resulting from Boolean decomposition, (b)a robust representation of node functions, manipulated by a logic synthesis system when it performs operations, such as elimination, collapsing, and node immunization, (c)an alternative computation engine to solve Boolean problems, such as don’t-care computation.

2.2Technology Mapping

A known approach to technology mapping [12] uses AIGs to represent the “object” graph. Of particular importance in this approach is implicit enumeration of mapping choices, achieved by collecting and storing multiple AIGs structures for the logic functions found in the original network to be mapped. The more mapping choices are present in the graph, the better is the mapping quality. In[12], mapping choices are derived by considering various algebraic decompositions of the SOPs of the nodes.

FRAIG construction can be seen as a natural way to prepare circuits for technology mapping. Each FRAIG node is associated with its equivalence class, that is, a set of functionally equivalent nodes with different AIG structures (structurally identical nodes are collapsed by one-level strashing performed as part of the FRAIG construction). These functionally equivalent nodes constitute a set of choices, which can be used for technology mapping.

An additional advantage is that FRAIGs can be constructed for multiple versions of the same network, derived by different optimizations. For example, a sequence of networks derived by applying an optimization script, one command at a time, can be FRAIGed into one object graph. Technology mapping applied to this cumulative graph selects the best mapping over all available choices, which may originate from different versions of the same network.

2.3Formal Verification

In formal verification, FRAIGs can be used instead of the traditional AIGs as a data structure for combinational equivalence checking (CEC) and model checking [9][11]. Using FRAIGs in CEC is similar to using BDDs. FRAIGs are constructed for the circuit outputs. The circuits are equivalent if and only if the corresponding pairs of outputs are represented by the same FRAIG nodes.

A more sophisticated use of FRAIGs is to be a uniform representation for circuits and interpolants [15][16]. Using FRAIGs in this context may extend the applicability of the previous work and lead to the development of new methods for sequential equivalence checking.

3Recent Work by Our Group

This section contains several references to the research publications of our group. Some of the papers are still in preparation.

3.1Functionally Reduced AIGs

A. Mishchenko, J.-H. R. Jiang, S. Chatterjee, R. K. Brayton. “FRAIGs: Functionally reduced AND-INV graphs” (DRAFT). To be submitted to DAC ’05.

This paper introduces FRAIGs and compares them with other functional representations for combinational equivalence checking.

3.2Technology Mapping

A. Mishchenko, X. Wang, T. Kam, “A new enhanced constructive decomposition and mapping algorithm”, Proc. DAC 2003, Los Angeles, pp. 143-147.

This paper describes our experience of developing a new technology mapper based on Boolean decomposition.

A. Mishchenko, S. Chatterjee, R. K. Brayton, X. Wang, T. Kam, “A new enhanced approach to technology mapping” (DRAFT). To be submitted to DAC ’05.

This paper describes our recent experience of developing a new technology mapper based on FRAIGs using a mixture of algebraic and Boolean techniques.

3.3Don’t-Care Computation

A. Mishchenko, R. K. Brayton. “Simplification of non-deterministic multi-valued networks”. Proc. ICCAD ‘02, pp. 557-562.

This paper provides the background on complete don’t-care computation in multi-valued non-deterministic networks.

A. Mishchenko, R. K. Brayton. “SAT-based complete don’t-care computation for network optimization”. (DRAFT). Submitted to DATE ’05.

This paper describes an efficient implementation of the complete don’t-care computation algorithm using Boolean satisfiability (SAT) for the special case of binary networks.

3.4Layout-Aware Logic Synthesis

S. Chatterjee, R. K. Brayton, “A new incremental placement algorithm and its application to congestion-aware divisor extraction”, Accepted to ICCAD ’04.

This paper describes our experience of performing logic synthesis transformations (divisor extraction) taking into account physical design information (wire-length and congestion).

3.5Functional Dependency

J.-H. R. Jiang, R. K. Brayton, “Functional dependency for verification reduction”, Proc. CAV ’04.

This paper defines the notion of functional dependency useful for sequential synthesis and verification and proposes an algorithm to compute it using BDDs. A more efficient computation method using AIGs and SAT can be developed.

References

[1]R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, “Multilevel logic synthesis”, Proc. IEEE, Vol. 78, No. 2, February 1990, pp. 264-300.

[2]R. E. Bryant, "Graph-based algorithms for Boolean function manipulation," IEEE Trans. Comp., Vol. C-35, No. 8 (August, 1986), pp. 677-691.

[3]S. Chatterjee, R. K. Brayton, “A new incremental placement algorithm and its application to congestion-aware divisor extraction”, Accepted to ICCAD ’04.

[4]N. Eén, N. Sörensson, “An extensible SAT-solver”, Proc. SAT ‘03.

[5]M. K. Ganai, A. Kuehlmann, “On-the-fly compression of logical circuits”. Proc. IWLS ‘00.

[6]E. Goldberg, M.Prasad, R.K.Brayton. “Using SAT for combinational equivalence checking”. Proc. DATE ‘01, pp.114 -121.

[7]J.-H. R. Jiang, R. K. Brayton, “Functional dependency for verification reduction”, Proc. CAV ’04.

[8]V. N. Kravets, P. Kudva, “Implicit enumeration of structural changes in circuit optimization”, Proc. DAC ’04.

[9]A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, “Robust Boolean reasoning for equivalence checking and functional property verification”, IEEE Trans. CAD, Vol.21(12), Dec 2002, pp. 1377-1394.

[10]Y. Kukimoto, R. K. Brayton, P. Sawkar, “Delay-optimal technology mapping by DAG covering”, Proc. DAC ’98, pp.348-351.

[11]A. Kuehlmann, “Dynamic Transition Relation Simplification for Bounded Property Checking”. Proc. IWLS 2004.

[12]E. Lehman, Y. Watanabe, J. Grodstein, and H. Harkness, “Logic decomposition during technology mapping,” IEEE Trans. CAD, 16(8), 1997, pp. 813-833.

[13]F. Lu, L. Wang, K. Cheng, R. Huang. “A circuit SAT solver with signal correlation guided learning”. Proc. DATE ‘03, pp. 892-897.

[14]J. P. Marques-Silva, K. A. Sakallah, “GRASP: A search algorithm for propositional satisfiability”, IEEE Trans. Comp, vol. 48, no. 5, pp. 506-521, May 1999.

[15]K.L. McMillan. “Applying SAT methods in unbounded symbolic model checking”. Proc. CAV ‘02, LNCS, vol. 2404, pp. 250-264.

[16]K.L. McMillan, “Interpolation and SAT-based model checking”. Proc. CAV ‘03, pp. 1-13, LNCS 2725, Springer, 2003.

[17]A. Mishchenko, R. Brayton, J.-H. R. Jiang, T. Villa, and N. Yevtushenko, “Efficient solution of language equations using partitioned representations”, Proc. IWLS ‘04.

[18]A. Mishchenko, R. K. Brayton. “Simplification of non-deterministic multi-valued networks”. Proc. ICCAD ‘02, pp. 557-562.

[19]A. Mishchenko, X. Wang, T. Kam, “A new enhanced constructive decomposition and mapping algorithm”, Proc. DAC 2003, Los Angeles, pp. 143-147.

[20]A. Mishchenko, R. K. Brayton. “SAT-based complete don’t-care computation for network optimization”. Proc. IWLS ’04.

[21]A. Mishchenko, J.-H. R. Jiang, S. Chatterjee, R. K. Brayton. “FRAIGs: Functionally reduced AND-INV graphs”. To be submitted to DAC ’05.

[22]A. Mishchenko, S. Chatterjee, R. K. Brayton, X. Wang, T. Kam, “A new enhanced approach to technology mapping”, to be submitted to DAC ’05.

[23]MVSIS Group. MVSIS: Multi-Valued Logic Synthesis System. UC Berkeley.

[24]H. Savoj, R. K. Brayton. “The use of observability and external don’t-cares for the simplification of multi-level networks”. Proc. DAC’ 90. pp. 297-301.

[25]H. Savoj. Don't cares in multi-level network optimization. Ph.D. Dissertation, UC Berkeley, May 1992.

[26]E. Sentovich et al. “SIS: A system for sequential circuit synthesis”. Tech. Rep. UCB/ERI, M92/41, ERL, Dept. EECS, UC Berkeley, 1992.