A sequential SAT solver, Satori, was recently proposed (Iyer, M.K. et al., Proc. IEEE/ACM Int. Conf. on Computer-Aided Design, 2003) as an alternative to combinational SAT in verification applications. This paper describes the design of Seq-SAT, an efficient sequential SAT solver with improved search strategies over Satori. The major improvements include: (1) a new and better heuristic for minimizing the set of assignments to state variables; (2) a new priority-based search strategy and a flexible sequential search framework which integrates different search strategies; (3) a decision variable selection heuristic more suitable for solving the sequential problems. We present experimental results to demonstrate that our sequential SAT solver can achieve orders-of-magnitude speedup over Satori. We plan to release the source code of Seq-SAT.

In this paper we address the problem of verifying the equivalence of two sequential circuits. State-of-the-art sequential optimization techniques such as retiming and sequential redundancy removal can handle designs with up to hundreds or even thousands of flip-flops. However, the BDD-based approaches for verifying sequential equivalence can easily run into memory explosion for such designs. In an attempt to handle larger circuits, we modify test pattern-generation techniques for verification. The suggested approach utilizes the popular efficient backward-justification technique used in most sequential ATPG programs. We present several techniques to enhance the efficiency of this approach by (1) identifying equivalent flip-flop pairs using an induction-based algorithm, and (2) generalizing the idea of exploring the structural similarity between circuits to perform verification in stages. This ATPG-based framework is suitable for verifying circuits either with or without a reset state. In order to extend this approach to verify retimed circuits, we introduce a delay-compensation-based algorithm for preprocessing the circuits. The experimental results of verifying the correctness of circuits after sequential redundancy removal and retiming with up to several hundred flip-flops are presented.

In this paper, we present a practical method for verifying the functional equivalence of two synchronous sequential designs. This tool is based on our earlier framework that uses Automatic Test Pattern Generation (ATPG) techniques for verification. By exploring the structural similarity between the two designs under verification, the complexity can be reduced substantially. We enhance our framework by three innovative features. First, we develop a local BDD-based technique which constructs Binary Decision Diagram (BDD) in terms of some internal signals, for identifying equivalent signal pairs. Second, we incorporate a technique called partial justification to explore not only combinational similarity, but also sequential similarity. This is particularly important when the two designs have a different number of flip-flops. Third, we extend our gate-to-gate equivalence checker for RTL-to-gate verification. Two major issues are considered in this extension: (1) how to model and utilize the external don't care information for verification; and (2) how to extract a subset of unreachable states to speed up the verification process. Compared with existing approaches based on symbolic Finite State Machine (FSM) traversal techniques, our approach is less vulnerable to the memory explosion problem and, therefore, is more suitable for a lot of real-life designs. Experimental results of verifying designs with hundreds of flip-flops will be presented to demonstrate the effectiveness of this approach.

We address the problem of rectifying an erroneous combinational circuit. Based on the symbolic binary decision diagram techniques, we consider the rectification process as a sequence of partial corrections. Each partial correction reduces the size of the input vector set that produces error responses. Compared with the existing approaches, this approach is more general, and thus, suitable for circuits with multiple errors and for the engineering change problem. Also, we derive the necessary and sufficient condition of general single-gate correction to improve the quality of rectification. To handle larger circuits, we develop a hybrid approach that makes use of the information of structural correspondence between specification and implementation. Experiments are performed on a suite of industrial examples as well as the entire set of ISCAS'85 benchmark circuits to demonstrate its effectiveness.

During the process of very large scale integration design, specifications are often changed. To preserve as large a portion of the engineering effort as possible, it is desirable that such changes will not lead to a very different design. In this work, we consider logic synthesis algorithms for handling engineering changes. To solve it, we propose a combination of multiple-error diagnosis and logic minimization techniques. Given a new specification and an existing synthesized network, our algorithms first identify the candidate signals in the network, and then synthesize the candidate functions. The synthesis step utilizes the existing network as much as possible so that the new specification can be realized with minimal changes.

This paper addresses the problem of locating design errors in a sequential circuit. For single-error circuits, we consider a signal ƒ as a potential error source only if the circuit can be completely rectified by re-synthesizing ƒ (i.e., changing the function of signal ƒ). In order to handle larger circuits, we do not rely on Binary Decision Diagram. Instead, we search for potential error sources by a modified sequential fault simulation process. The main contributions of this paper are two-fold: (1) we derive the necessary and sufficient condition of whether an erroneous input sequence (i.e., an input sequence producing erroneous responses) can be corrected by changing the function of a particular internal signal; and (2) we propose a modified fault simulation procedure to check this condition. Our approach does not rely on any error model, and thus, is suitable for general types of errors. Furthermore, it can be easily extended to identify multiple errors. Experimental results on ISCAS89 benchmark circuits are presented to demonstrate its capability.

Conventional scan design imposes considerable area and delay overheads. To establish a scan chain in the test mode, multiplexers at the inputs of flip-flops and scan wires are added to the actual design. However, the functionality of the functional logic has not been utilized for the test purposes. We propose a low-overhead scan design methodology, called cost-free scan, which exploits the controllability of primary inputs to establish scan paths through the functional logic. We show how to analyze the circuit to determine all the free-scan flip-flops and select the best input vector to establish the maximum number of free-scan flip-flops for the scan chain design. Significant reduction in the scan overhead is achieved on ISCAS89 benchmarks. In full-scan designs, as many as 89% of the flip-flops are found free-scannable. In the partial-scan designs, we assume that selecting flip-flops for scan to break sequential cycles is used to increase circuit testability. Reduction can be as high as 97% in scan flip-flops needed to break sequential cycles.

In this paper, we address the problem of verifying the equivalence of two sequential circuits. A hybrid approach that combines the advantages of BDD-based and ATPG-based approaches is introduced. Furthermore, we incorporate a technique called partial justification to explore the sequential similarity between the two circuits under verification to speed up the verification process. Compared with existing approaches, our method is much less vulnerable to the memory explosion problem, and therefore can handle larger designs. The experimental results show that in a few minutes of CPU time, our tool can verify the sequential equivalence of an intensively optimized benchmark circuit with hundreds of flip-flops against its original version.

This paper addresses the problem of locating error sources in an erroneous combinational circuit. We use a fault simulation-based technique to approximate each signal's correcting power. The correcting power of a particular signal is measured in terms of the signal's correctable set, namely, the maximum set of erroneous input vectors that can be corrected by re-synthesizing the signal. Only the signals that can correct every erroneous input vector are considered as a potential error source. Our algorithm offers three major advantages over existing methods. First, unlike symbolic approaches, it is applicable for large circuits. Secondly, it delivers more accurate results than other simulation-based approaches because it is based on a more stringent condition for identifying potential error sources. Thirdly, it can be easily generalized to identify multiple errors. Experimental results on diagnosing circuits with one and two random errors are presented to show the effectiveness and efficiency of this new approach.

We address the problem of rectifying an incorrect combinational circuit against a given specification. Based on the symbolic BDD techniques, we consider the rectification process as a sequence of partial corrections. Each partial correction reduces the size of the input vector set producing error responses. Compared with existing approaches, this approach is more general, and able to handle circuits with multiple errors. We also formulate the necessary and sufficient condition of general single-gate correction to achieve better results for some circuits with a single error. To handle larger circuits, we develop a hybrid approach that makes use of the information of structural correspondence between specification and implementation. Experimental results on industrial examples as well as ISCAS85 benchmark circuits are presented to show the effectiveness of our approach.

In this paper, we address the problem of correcting a combinational circuit that is an incorrect implementation of a given specification. Most existing error-correction approaches can only handle circuits with certain types of errors. Here, we propose a general approach that can correct a circuit with multiple errors without assuming any error model. We identify internal equivalent pairs to narrow down the possible error locations using local BDD's with dynamic support. We also employ a technique called back-substitution to correct the circuit incrementally. This approach can also be used to verify circuit equivalence. The experimental results of correcting fully SIS-optimized benchmark circuits with a number of injected errors will be presented.

Transistor-level power simulators have been popularly used to esi:imate the power dissipation of a CMOS circuit. These tools strike a good balance between the conventional transistor-level simulators, such as SPICE, and the logic-level power estimators with regard to accuracy and speed. However, it is still too time-consuming to run these tools for large designs. To simulate one-million functional vectors for a 5OK-gate circuit, these power simulators may take months to complete. In this paper, we propose an approach to generate a compact set of vectors that can mimic tb: transition behavior of a much larger set of functional vectors, which is given by the designer or extracted from application programs. This compact set of vectors can then replace the functional vectors for power simulation to reduce the simulation time while still retaining a high degree of accuracy. We present

We address the problem of verifying a retimed circuit. After retiming, some latches in a sequential circuit are repositioned to reduce the clock cycle time and thus the behavior of the combinational portion is changed. Here, we present a novel approach to check the correctness of a retimed circuit according to the definition of 3-valued equivalence. This approach is based on our verification framework using sequential ATPG techniques. We further incorporate an algorithm to pre-process the circuits and make the verification process even more efficient. We will present the experimental results of verifying the retimed circuits with hundreds of flip-flops on ISCAS89 benchmark circuits to show its capability.

Transistor-level power simulators, which are more accurate than logic-level power estimators, are popular to estimate the power dissipation of CMOS circuits. We introduce a method which extends the Monte-Carlo approach for deriving the average power dissipation of a circuit using transistor-level power simulators. To reduce the simulation time, we propose a mixed-level extrapolation technique to speed up the convergence rate of the process, and thereby to achieve a good balance between simulation time and accuracy. Experimental results show that this is a promising method for deriving the accurate power dissipation of a circuit within a reasonable time budget.

In this paper, we address the problem of verifying the equivalence of two sequential circuits. State-of-the-art sequential optimization techniques such as retiming and sequential redundancy removal can handle designs with up to hundreds or even thousands of flip-flops. The BDD-based approaches for equivalence checking can easily run into memory explosion for such designs. With an attempt to handle larger circuits, we modify the test pattern generation techniques for verification. The suggested approach utilizes the efficient backward justification technique popularly used in most sequential ATPG programs. The method explores the structural similarity between circuits under verification, and performs the verification in stages to improve the efficiency. An effective algorithm to identify equivalent hip-hops is presented. This ATPG-based framework is suitable for verifying circuits with or without a reset state. Experimental results of verifying the correctness of circuits after sequential redundancy removal are presented.

No abstract available.

In the process of VLSI design, specifications are often changed. It is desirable that such changes will not lead to a very different design so that a large part of engineering effort can be preserved. We consider synthesis algorithms for handling such engineering changes. Given a synthesized network, our algorithm modifies it minimally to realize a new specification.

In this paper we examine three different problems related to FPGA placement: timing driven placement of a technology mapped circuit, timing driven reconfiguration for yield enhancement and fault tolerance in FPGAs and timing driven design re-engineering for FPGAs. We show that timing driven relocation which transforms an infeasible placement into a feasible one is a key problem the solution of which will lead to good algorithms for all three of these optimization problems. We introduce the concept of a slack neighborhood graph (SNG) as a general tool for timing driven relocation of modules in an infeasible placement with a bounded increase in critical path delay. The slack neighborhood graph approach provides a unified approach to the solution of three timing driven optimization problems of interest in this paper.

Conventional scan design imposes considerable area and delay overhead by using larger scan flip-flops and additional scan wires without utilizing the functionality of the combinational logic. We propose a novel low-overhead scan design methodology, called cost-free scan, which exploits the controllability of primary inputs to establish scan paths through the combinational logic. The methodology aims at reducing scan overhead by (1) analyzing the circuit to determine all the cost-free scan flip-flops, and (2) selecting the best primary input vector to establish the maximum number of cost-free scan flip-flops on the scan chain. Significant reduction in the scan overhead is achieved on ISCAS89 benchmarks, where in full scan environment, as many as 89% of the total flip-flops are found cost-free scannable, while in partial scan environment, reduction can be as high as 97% in scan flip-flops needed to break sequential loops.

In a typical design flow, the design may be altered slightly several times after the initial design cycle according to minor changes in the design specification either as a result of design debugging or as a result of changes in engineering requirements. These modifications are usually local and are referred to as engineering changes. In this paper we study the problem of timing driven placement re-engineering: the problem of altering the placement of a circuit to incorporate engineering changes without degrading the timing performance of the circuit. We focus on the re-engineering problem for regular architectures such as FPGAs and gate arrays. Our algorithms exploit the locality of the re-engineering design changes and use the current placement to generate the new placement for the altered circuit. Our experiments on the Xilinx 3000 FPGA architecture demonstrate the effectiveness of our algorithm in handling engineering changes efficiently.

A graph-based technology mapping algorithm, called DAG-Map, for delay optimization in lookup-table-based field programmable gate array (FPGA) designs is presented. The algorithm carries out technology mapping and delay optimization on the entire Boolean network, instead of decomposing it into fanout-free trees and mapping each tree separately as in most previous algorithms. As a preprocessing step, a general algorithm that transforms an arbitrary n-input network into a two-input network with only O(1) factor increase in the network depth is introduced. Also presented is a graph-matching-based technique used as a postprocessing step which optimizes the area without increasing the delay. The DAG-Map algorithm was tested on the MCNC logic synthesis benchmarks. Compared with previous algorithms, it reduces both the network depth and the number of lookup-tables.>

Article Free AccessA resynthesis approach for network optimization Authors: Kuang-Chien Chen Fujitsu America Inc. Fujitsu America Inc.View Profile , Yusuke Matsunaga Fujitsu Labs. Ltd., Japan Fujitsu Labs. Ltd., JapanView Profile , Saburo Muroga University of Illinois University of IllinoisView Profile , Masahiro Fujita Fujitsu Labs. Ltd., Japan Fujitsu Labs. Ltd., JapanView Profile Authors Info & Claims DAC '91: Proceedings of the 28th ACM/IEEE Design Automation ConferenceJune 1991Pages 458–463https://doi.org/10.1145/127601.127712Published:01 June 1991Publication History 11citation196DownloadsMetricsTotal Citations11Total Downloads196Last 12 Months13Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The authors present various applications of Boolean unification to combinational logic synthesis. Three topics of combinational logic synthesis are discussed: redesign, multilevel logic minimization, and minimization of Boolean relations. All of these problems can be uniformly formalized as Boolean unification problems. Experimental results are also reported.>

An algorithm called C-RENO (Concurrent Resynthesis for Network Optimization) is presented for the optimization of multilevel combinational networks. In C-RENO, a given network is optimized for global optimality by resynthesizing a set of gates concurrently, using other gates in the network. C-RENO uses the generalized ratio-set algorithm, which enables one to resynthesize complex gates instead of only simple gates (e.g. NAND and NOR), exploring larger reconfiguration space. High-quality networks are derived by C-RENO even if no network don't-cares are used, and results which are not achievable by other methods have been obtained.>

This paper presents a timing optimization algorithm SDLR (acronym of SYLON-DREAM Level-Reduction), which is used in the SYLON-DREAM logic synthesizer for speeding up combinational multi-level networks. In SDLR, gates on critical paths are identified and their level numbers counted from the inputs of the network are maximally reduced by a level-reduction procedure. Gates which are not on the critical paths are processed by an area reduction procedure to reduce network area without increasing its maximum depth. SDLR uses the concept of permissible functions in both level and area reduction procedures, and it can directly process networks consisting of simple gates or negative gates (i.e., MOS cells). Experimental results obtained for benchmark functions show that SDLR is an effective algorithm which can reduce network delay with no or minimal area increase.

SYLON-DREAM, a logic network synthesizer which consists of SYLON-DREAM-INI for designing initial networks and SYLON-DREAM-MIN for further optimization, is presented. Unlike the networks designed by other approaches, those designed by SYLON-DREAM consist of MOS cells satisfying given constraints on the maximum number of series and parallel transistors. Such networks can be easily realized by a cell generator or mapped to the gates in existing cell libraries.>

A heuristic algorithm for assigning input variables to the decoders of a decoded-programmable logic array (PLA) is presented. In this algorithm, the number of inputs to each decoder is not restricted to two and the area overhead incurred by using multi-input decoders is considered in the cost function. Experimental results show that the areas of multi-input decoded-PLAs designed by this algorithm are smaller in many cases than those of decoded-PLAs with two-input decoders or standard PLAs.>