The ever shrinking feature size of modern electronic chips leads to
more designs being done as well as more complex chips being
designed. These in turn lead to greater use of high-level
specifications and to more sophisticated optimizations applied at the
word -level. These steps make it more difficult to verify that the
final design is faithful to the initial specification. We tackle two
steps in this process and their formal equivalence checking to help
verify the correctness of the steps.
First, we present LEC, a combinational equivalence checking tool that is learning driven. It focuses on data-path equivalence
checking with the goal of transforming the two logics under comparison to be more
similar in order to reduce the complexity of a final Boolean (bit-level)
solving. LEC does equivalence checking of combinational logic between two RTL (word-level) designs, one the original and one an optimized RTL version. LEC features an open architecture such that users and developers can
learn with the system as new designs and optimizations are met, and then it can be modularly extended with new proof procedures as they are discovered.
To address the use of higher level specifications, we build a simple trusted C to Verilog translation procedure based on the
LLVM compiler infrastructure. The translator was designed to implement an almost vertatim
translation of the C language operators and control structures into
the Verilog \emph{always\_ff} and \emph{always\_comb} blocks through traversing LLVM
Bytecode programs. The procedure reliably bridges the language barrier
between software and hardware and allows hardware synthesis
and verification techniques to be applied readily.
In combination, these two procedures allow for equivalence checking
between a software-like specification and an optimized word-level RTL
implementation.