Modern solvers for the Boolean Satisfiability (SAT) problem rely heavily on the analysis of conflicts in a backtrack search to learn useful constraints to guide the search. Other families of constraints such as linear pseudo-Boolean and cardinality constraints may more naturally express constraints normally found in many EDA applications, making the underlying structure more transparent. These constraints may be handled by generic integer linear programming (ILP) solvers, but they may ignore the Boolean nature of the variables.
We generalize learning schemes from recent SAT solvers to efficiently handle the more expressive constraints. Theoretical results have shown that there may be exponential improvements in runtime in moving from conjunctive normal form to cardinality constraints, which are exhibited in some of our experiments.
Fishbone is a block-level placement and routing scheme that has been developed. The routing uses a two-layer spine topology. The pin locations are configurable and restricted to certain routing grids in order to ensure full routability and precise predictability. With this scheme, exact net topologies are determined by pin positions only. Hence, during block placement, net parameters such as wire length and delay can be derived directly. The construction of Fishbone nets is much faster than for Steiner trees. This enables the integration of block placement and routing. There is no separate routing stage.
We propose two regular circuit structures based on the programmable logic array (PLA). They provide alternatives to the widely used standard cell structure and have better predictability and simpler design methodologies. A whirlpool PLA is a cyclic four-level structure, which has a compact layout. Doppio-ESPRESSO, a four-level logic minimization algorithm, is developed for the synthesis of Whirlpool PLAs. A river PLA is a stack of multiple output PLAs, which uses river routing for the interconnections of the adjacent PLAs. A synthesis algorithm for river PLAs uses simulated annealing, targeting a combination of minimal area and delay.
MVSIS is an experimental software infrastructure for optimization and synthesis of sequential multi-valued logic networks. It is a network of nodes, where each node represents multi-valued relation. It is a structural representation of a non-deterministic finite automaton. The model is general enough for reasoning about formal verification, control synthesis, and synthesis for both hardware and software. It represents new synthesis challenges that were never addressed before. Some initial study is highlighted in .
Some synthesis results have been obtained for algebraic and Boolean optimizations, as presented in , which are extensions of corresponding algorithms in the binary domain. We intend to continue research in the technology independent optimization of such non-deterministic logic networks.
Technology dependent optimization techniques are also being studied for various applications. Binary encoding techniques have been studied for synchronous hardware implementations. We also research design flow and mapping techniques that produce delay-insensitive asynchronous circuits, which are more power efficient than their synchronous counterpart, and are correct by construction. For software synthesis in a hw/sw codesign context, we are studying efficient algorithms to generate fast code from an optimal generalized cofactoring structure.
Algebraic operations were developed for binary logic synthesis and extended later to apply to multi-valued (MV) logic. Operations in the MV domain were considered more complex and slower. We show that MV algebraic operations are essentially as easy as binary ones, with only a slight overhead (linear in the expressions) in transformation into and out of the binary domain.
By introducing co-singleton sets as a new basis, any MV sum-of-products expression can be rewritten and parsed to a binary logic synthesizer for fast execution. The optimized results can be directly interpreted in the MV domain. This process, called EBD, reduces MV algebraic operations to binary.
A pure MV operation differs mainly from its corresponding EBD one in that the former possesses "semi-algebraic" generality, which has not been implemented for binary logic. Preliminary experimental results show that the proposed methods are significantly faster, with little or no loss in quality when run in comparable scripts of sequences of logic synthesis operations.
We also show that in principle through the co-singleton transform, all MV semi-algebraic operations could be reproduced in the binary domain if the binary operations had semi-algebraic extensions. This result suggests that semi-algebraic operations in the binary domain should be investigated in the future.
1Postdoctoral Researcher, Portland State University
The state explosion problem limits formal verification on large sequential circuits partly because BDD sizes heavily depend on the number of variables dealt with. In the worst case, a BDD size grows exponentially with the number of variables. Reducing this number can possibly enlarge the verification capacity. In particular, we show how sequential equivalence checking can be done in the sum state space.
Given two finite state machines M1 and M2 with numbers of state variables m1 and m2 respectively, conventional formal methods verify equivalence by traversing the state space of the product machine, with m1 + m2 registers. In contrast, we introduce a different possibility, based on partitioning the state space defined by a multiplexed machine, which can have merely max m1,m2 + 1 registers. This substantial reduction in state variables potentially enables the verification of larger instances. Experimental results show the approach can verify benchmarks with up to 312 registers, including all of the control outputs of microprocessor 8085.
We are currently exploring techniques to extend the verification capacity. One possiblity would be using output transformation such that equivalence classes of states induced by the new outputs are reduced and amortized. Another would be using structure similarities between two sequential circuits to reduce the verification complexity. In addition, we are investigating how to make our verification approach more scalable especially for high performance IC design methodologies.
Faster on-chip clock rates, increasing delay along global interconnects, and the need for IP reuse have provided an impetus for globally asynchronous design. In such a design environment, increased latency along global interconnects no longer affects functional correctness, but instead affects the performance of the design. Thus, performance estimation becomes a critical part of the floorplanning and physical layout of the design. Our research examines how abstract modeling of system behavior can be used to provide such performance estimation as an integrated part of the floorplanning process.
In this work we are studying techniques for logic synthesis which lead to circuits which are "better" for placement and for routing. In the current framework, we still separate logic synthesis from physical design. We are trying to characterize properties of Boolean networks which allow for better layout. Thus in addition to the traditional literal count, we seek other metrics for boolean networks which may be better indicators of the wiring complexity during physical design. We hope to modify the traditional logic synthesis algorithms (which optimize for literal count) to optimize for a different cost function which takes into account these new metrics in addition to literal count.
In a platform-based design context, we target (1) standardized or application specific processing platforms, and (2) automatic software generation from functional models. With a focus on control-intensive embedded systems, for instance, automobile engine, airplane, and network protocol controls, we use a network of extended finite state machines (EFSMs) as the model of computation. The research goal is to derive proper flow and point algorithms for code generation and mapping, given an existing architecture platform. Initial results are highlighted in [1,2]. Further research includes the following.
Generalized cofactoring from multi-valued relations: given a multi-valued relation, we want to find the optimal cofactoring structure that minimizes the functional evaluation cost. The generalized cofactoring structure is a DAG, where each node is associated with a binary cofactoring function, and the two out going edges represent the positive and negative cofactor. The goal is to find a set of cofactoring functions that minimize the average path length  of the structure.
State minimization and re-encoding: given a sequential logic network, we want to find sequential and parallel decompositions of the state machine, so that the output evaluation can be made faster.