Jiang Long

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2017-150

August 14, 2017

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-150.pdf

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 trans- lation 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 always ff and always comb blocks through traversing LLVM Bytecode pro- grams. 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.

Advisors: Robert K. Brayton

---

BibTeX citation:

@phdthesis{Long:EECS-2017-150,
    Author= {Long, Jiang},
    Title= {Reasoning about High-Level Constructs in Hardware/Software Formal Verification},
    School= {EECS Department, University of California, Berkeley},
    Year= {2017},
    Month= {Aug},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-150.html},
    Number= {UCB/EECS-2017-150},
    Abstract= {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 trans- lation 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 always ff and always comb blocks through traversing LLVM Bytecode pro- grams. 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.},
}

EndNote citation:

%0 Thesis
%A Long, Jiang 
%T Reasoning about High-Level Constructs in Hardware/Software Formal Verification
%I EECS Department, University of California, Berkeley
%D 2017
%8 August 14
%@ UCB/EECS-2017-150
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-150.html
%F Long:EECS-2017-150