http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
New algorithms for logic verification and sequential redundancy identification
xiv, 119 leaves : illustrations ; 28 cm.
Recent advances in VLSI technology have made testing and verification of integrated circuits more and more important. In this dissertation, we propose new algorithms for combinational logic verification, automatic flip-flop matching and sequential redundancy identification. This dissertation first proposes a new approach to sequential redundancy identification. The proposed algorithm first performs uncontrollability and unobservability analysis to find states that are necessary for the detection of some faults, then uses recursive learning to identify whether a state is illegal or not. If a state is illegal, then faults whose detection requires the state as a necessary condition are untestable. We prove that, with a validation procedure, a subset of the identified untestable faults can be further classified as c-cycle redundant faults. The proposed algorithm can identify faults which require conflicting assignments on multiple lines. In this sense, it is a generalization of FIRES, a state-of-the-art redundancy identification algorithm. This dissertation also presents a new algorithm for logic equivalence checking of combinational circuits. The algorithm combines a Binary Decision Diagram (BDD) trimming technique with a Boolean satisfiability method. It provides an integrated framework that allows different Boolean space search paradigms to be combined. The proposed algorithm is guaranteed to work with the BDD size remaining within a designated range, and avoid the problem of memory blow-up. The proposed algorithm provides a fundamental framework of integration of two commonly used Boolean search techniques. It can be combined with other heuristics easily. In practice, most of the circuits to be verified are sequential ones. If the correspondence of the memory elements (flip-flops) of the two circuits can be established, we can use combinational equivalence checkers to verify the equivalence of the combinational blocks of the sequential circuits and thus make the sequential equivalence problem become much easier combinational equivalence checking problem. Some algorithms have been proposed to solve the automatic memory matching problem. But none gives a satisfactory answer even to all the ISCAS 89 benchmark circuits. We propose an approach that combines two complementary simulation-based methods for fast and accurate storage correspondence. The proposed method is scalable and is applicable to large sequential circuits.
Issued also on microfiche from University Microfilm Inc.
Includes bibliographical references (leaves 108-118).