Research Overview

MVSIS Group

Department of EECS, University of California, Berkeley

1. AND-INV Graph Basics

2. Applications of FRAIGs

2.1. Logic Synthesis

2.2. Technology Mapping

2.3. Formal Verification

3. Recent Work by Our Group

References

1 AND-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 f_n(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, n₁ and n₂, 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.

2 Applications of FRAIGs

2.1 Logic 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.2 Technology 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.3 Formal 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.

3 Recent 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.1 Functionally 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.2 Technology 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.3 Don’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.4 Layout-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.5 Functional 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.

3.6 Sequential Flexibility Computation

A. Mishchenko, R. K. Brayton, J.-H. R. Jiang, T. Villa, N. Yevtushenko, “Efficient Solution of Language Equations Using Partitioned Representations” (DRAFT). Submitted to DATE ’05.

This paper describes the computation of complete sequential flexibility for a component in a sequential network. The flexibility is defined as a set of FSMs that can be realized instead of the given component, without violating the functionality of the network. The use of partitioning makes sequential flexibility computation applicable to larger networks. (Our approach to partitioning is similar to partitioning of the transition relation in the image computation, and provides comparable improvements.)