UC Berkeley

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.