Static learning in the form of logic implications captures Boolean relationships between various gates in a circuit. In the past, logic implications have been applied in several areas of electronic design automation (EDA) including: test-pattern-generation, logic and fault simulation, fault diagnosis, logic optimization, etc. While logic implications have assisted in solving several EDA problems, their usefulness has not been fully explored. We believe that logic implications have not been carefully analyzed in the past, and this lack of thorough investigation has limited their applicability in solving hard EDA problems. In this dissertation, we offer deeper insights into the Boolean relationships exhibited in a circuit, and present techniques to extract their full potential in solving two hard problems in test and verification: (1) Efficient identification of sequentially untestable stuck-at faults, and (2) Equivalence checking of sequential circuits. Additionally, for the dissertation, we define a new concept called multi-cycle path delay faults (M-pdf) for latch based designs with multiple clock domains, and propose an implications-based methodology for the identification of untestable M-pdfs for such designs. One of the main bottlenecks in the efficiency of test-pattern-generation (TPG) is the presence of untestable faults in a design. State-of-the-art automatic test pattern generators (ATPG) spend a lot of effort (in both time and memory) targeting untestable faults before aborting on such faults, or, eventually identifying these faults as untestable (if given enough computational resources). In either case, TPG is considerably slowed down by the presence of untestable faults. Thus, efficient methods to identify untestable faults are desired. In this dissertation, we discuss a number of solutions that we have developed for the purpose of untestable fault identification. The techniques that we propose are fault-independent and explore properties associated with logic implications to derive conclusions about untestable faults. Experimental results for benchmark circuits show that our techniques achieve a significant increase in the number of untestable faults identified, at low memory and computational overhead. The second related problem that we address in this proposal is that of determining the equivalence of sequential circuits. During the design phase, hardware goes through several stages of optimizations (for area, speed, power, etc). Determining the functional correctness of the design after each optimization step by means of exhaustive simulation can be prohibitively expensive. An alternative to prove functional correctness of the optimized design is to determine the design's functional equivalence w.r.t. some golden model which is known to be functionally correct. Efficient techniques to perform this process, known as equivalence checking, have been investigated in the research community. However, equivalence checking of sequential circuits still remains a challenging problem. In an attempt to solve this problem, we propose a Boolean SAT (satisfiability) based framework that utilizes logic implications for the purpose of sequential equivalence checking. Finally, we define a new concept called multi-cycle path-delay faults (M-pdfs). Traditionally, path delay faults have been analyzed for flip-flop based designs over the boundary of a single clock cycle. However, path delay faults may span multiple clock cycles, and a technique is desired to model and analyze such path delay faults. This is especially essential for latch based designs with multiple clock domains, because the problem of identifying untestable faults is more complex in such design environments. In this dissertation, we propose a three-step methodology to identify untestable M-pdfs in latch-based designs with multiple clocks using logic implications. / Ph. D.

An effective silicon debug technique uses a trace buffer to monitor and capture a portion of the circuit response during its functional, post-silicon operation. Due to the limited space of the available trace buffer, selection of the critical trace signals plays an important role in both minimizing the number of signals traced and maximizing the observability/restorability of other untraced signals during post-silicon validation. In this thesis, a new method is proposed for trace buffer signal selection for the purpose of post-silicon debug. The selection is performed by favoring those signals with the most number of implications that are not implied by other signals. Then, based on the values of the traced signals during silicon debug, an algorithm which uses a SAT-based multi-node implication engine is introduced to restore the values of untraced signals across multiple time-frames. A new multiplexer-based trace signal interconnection scheme and a new heuristic for trace signal selection based on implication-based correlation are also described. By this approach, we can effectively trace twice as many signals with the same trace buffer width. A SAT-based greedy heuristic is also proposed to prune the selected trace signal list further to take into account those multi-node implications. A state restoration algorithm is developed for the multiplexer-based trace signal interconnection scheme. Experimental results show that the proposed approaches select the trace signals effectively, giving a high restoration percentage compared with other techniques. We finally propose a lossless compression technique to increase the capacity of the trace buffer. We propose real-time compression of the trace data using Frequency-Directed Run-Length (FDR) code. In addition, we also propose source transformation functions, namely difference vector computation, efficient ordering of trace flip-flops and alternate vector reversal that reduces the entropy of the trace data, making them more amenable for compression. The order of the trace flip-flops is computed off-chip using a probabilistic algorithm. The difference vector computation and alternate vector reversal are implemented on-chip and incurs negligible hardware overhead. Experimental results for sequential benchmark circuits shows that this method gives a better compression percentage compared to dictionary-based techniques and yields up to 3X improvement in the diagnostic capability. We also observe that the area overhead of the proposed approach is less compared to dictionary-based compression techniques. / Master of Science

With the advances in VLSI and System-On-Chip (SOC) technology, the complexity of hardware systems has increased manifold. Today, 70% of the design cost is spent in verifying these intricate systems. The two most widely used formal methods for design verification are Equivalence Checking and Model Checking. Equivalence Checking requires that the implementation circuit should be exactly equivalent to the specification circuit (golden model). In other words, for each possible input pattern, the implementation circuit should yield the same outputs as the specification circuit. Model checking, on the other hand, checks to see if the design holds certain properties, which in turn are indispensable for the proper functionality of the design. Complexities in both Equivalence Checking and Model Checking are exponential to the circuit size. In this thesis, we firstly propose a novel technique to improve SAT-based Combinational Equivalence Checking (CEC) and Bounded Model Checking (BMC). The idea is to perform a low-cost preprocessing that will statically induce global signal relationships into the original CNF formula of the circuit under verification and hence reduce the complexity of the SAT instance. This efficient and effective preprocessing quickly builds up the implication graph for the circuit under verification, yielding a large set of logic implications composed of direct, indirect and extended backward implications. These two-node implications (spanning time-frame boundaries) are converted into two-literal clauses, and added to the original CNF database. The added clauses constrain the search space of the SAT-solver engine, and provide correlation among the different variables, which enhances the Boolean Constraint Propagation (BCP). Experimental results on large and difficult ISCAS'85, ISCAS'89 (full scan) and ITC'99 (full scan) CEC instances and ISCAS'89 BMC instances show that our approach is independent of the state-of-the-art SAT-solver used, and that the added clauses help to achieve more than an order of magnitude speedup over the conventional approach. Also, comparison with Hyper-Resolution [Bacchus 03] suggests that our technique is much more powerful, yielding non-trivial clauses that significantly simplify the SAT instance complexity. Secondly, we propose a novel global learning technique that helps to identify highly non-trivial relationships among signals in the circuit netlist, thereby boosting the power of the existing implication engine. We call this new class of implications as 'extended forward implications', and show its effectiveness through additional untestable faults they help to identify. Thirdly, we propose a suite of lemmas and theorems to formalize global learning. We show through implementation that these theorems help to significantly simplify a generic CNF formula (from Formal Verification, Artificial Intelligence etc.) by identifying the necessary assignments, equivalent signals, complementary signals and other non-trivial implication relationships among its variables. We further illustrate through experimental results that the CNF formula simplification obtained using our tool outshines the simplification obtained using other preprocessors. / Master of Science

Relations among various nodes in the circuit, as captured by static and inductive invariants, have shown to have a positive impact on a wide range of EDA applications. Techniques such as boolean constraint propagation for static learning and assume-then-verify approach to reason about inductive invariants have been possible due to efficient SAT solvers. Although a significant amount of research effort has been dedicated to the development of effective invariant learning techniques over the years, the computation time for deriving powerful multi-node invariants is still a bottleneck for large circuits. Fast computation of static and inductive invariants is the primary focus of this thesis. We present a novel technique to reduce the cost of static learning by intelligently identifying redundant computations that may not yield new invariants, thereby achieving significant speedup. The process of inductive invariant reasoning relies on the assume-then-verify framework, which requires multiple iterations to complete, making it infeasible for cases with a large set of multi-node invariants. We present filtering techniques that can be applied to a diverse set of multi-node invariants to achieve a significant boost in performance of the invariant checker. Mining and reasoning about all possible potential multi-node invariants is simply infeasible. To alleviate this problem, strategies that narrow down the focus on specific types of powerful multi-node invariants are also presented. Experimental results reflect the promise of these techniques. As a measure of quality, the invariants are utilized for untestable fault identification and to constrain ATPG for path delay fault testing, with positive results. / Master of Science