Publication Date

2012

Document Type

Dissertation

Committee Members

Henry Chen (Committee Member), Travis Doom (Committee Chair), John Gallagher (Committee Member), Meilin Liu (Committee Member), Sridhar Ramachandran (Committee Member)

Degree Name

Doctor of Philosophy (PhD)

Abstract

Throughout its design process (from specification to implementation) a digital circuit goes through a variety of structural changes. These changes are introduced primarily due to the use of automated tools in the design process. Checking whether the Boolean functions representing the two designs are equivalent is thus necessary to verify if a design implementation adheres to its specification. Combinational Equivalence Checking (CEC) - a process of determining whether two combinational design functions are equiv-alent, has been one of the most researched Boolean matching problems. The well-known CEC techniques that have been proposed adopt some kind of a formal approach such as Canonical Form (ROBDD, BMDs, etc.) isomorphism or Boolean Satisfiability in order to prove or disprove equivalence. Hybrid techniques that adopt a combination of the above mentioned two techniques have also been proposed.

Knowing the exact nature of variable mappings / correspondences between the two designs a priori is advantageous during the CEC process. However, situations may arise arise wherein the knowledge of these mappings is unknown or lost. Not knowing the variable mappings between the two designs a priori increases the computational complexity of CEC techniques. The CEC problem, under unknown variable mappings, is a more complex Boolean matching problem - the problem of determining if an input and an output variable mapping/permutation exists under which the two designs are functionally equivalent. The use of signatures/filters has proven to be a well-known approach taken by the design verification community quickly detect and prune those variable mappings that do not make the two designs equivalent.

In our work we propose and implement three novel output behavior based signatures known as Behavioral signatures. Behavioral signatures are computed solely based on the binary output behavior exhibited by the designs and thus distance themselves from relying on Boolean equations, canonical forms or any other functional representations for their computation. This property makes the Behavioral signatures useful to all digital design domains including those that might not possess any knowledge of the Boolean functions representing the designs that face the problem of determining design equivalence under unknown variable correspondences. The Grouped Row Sum and the Row Difference signatures that we propose are used to identify unsatisfiable input variable mappings between the two designs. Our Grouped Column Sum signature on the other hand is used to identify the unsatisfiable output variable mappings.

The success of a Behavioral signature lies in the fineness with which it summarizes the design behavior. However there exists a tradeoff between the degree of fineness achieved and the execution time. For instance, amongst the input variable signatures that we propose, the Row Difference signature is more adept in summarizing the design behavior than its counterpart the Grouped Row Sum signature. However the computation cost associated with the Row Difference signature is higher as compared to the Grouped Row Sum signature. We thus define a framework for using these signatures based on the nature of the designs under consideration.

Page Count

130

Department or Program

Department of Computer Science and Engineering

Year Degree Awarded

2012

Download


Share

COinS