Utilizing High-level Synthesis Techniques in High-level to RT-level Equivalence Checking
Date Issued
2012
Date
2012
Author(s)
Chao, Yueh-Tung
Abstract
Equivalence checking between high-level designs and register-transfer-level designs has been a very challenging and important problem in the context of system on chips (SoCs). Due to the very different language constructs and features in high-level languages, such as C/C++/SystemC and RT-level languages, like Verilog/VHDL, the traditional definition of equivalence is not suitable anymore.
In this work, we analyze the whole problem space and define a subset of it, called FSM-compatible equivalence checking, which can be solved efficiently utilizing high-level synthesis techniques. That is, we extract a FSM from RT-level design and verify whether there exists a way to synthesize the high-level design into an equivalent FSM. If there exists, we can conclude that the two designs are equivalent.
Furthermore, we propose the flattened program dependence graph, which has more flexibilities than the conventional control data flow graph, to represent a high-level model and enlarge the search space. We utilize bi-simulation to quickly prune infeasible solution and then apply formal engine to verify the equivalence of two FSMs as well.
We conduct several unit tests and utilize three case studies to show the language constructs that we can support. We demonstrate the effectiveness of our methodologies, too.
Subjects
high-level
behavioral-level
high-level synthesis (HLS)
behavioral-level synthesis
finite-state machine (FSM)
register-transfer level (RTL)
verification
equivalence checking
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-101-R98943089-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):642b89f5ad7b3dcdd394ac32ad0cea3f