As first step, most model checkers used in the hardware industry convert a high-level register transfer language (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels, and thus, are less scalable. The RTL level of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. We describe a hardware model checking tool, VCEGAR, which performs verification at the RTL level using software verification techniques. It implements predicate abstraction and a refinement loop as used in software verification. The novel aspects are the generation of new word-level predicates, an efficient predicate image computation in presence of a large number of predicates, and precise modeling of the bit-vector semantics of hardware designs.
@inproceedings { conf/tacas/JainK, title = {VCEGAR: Verilog CounterExample Guided Abstraction Refinement.}, booktitle = {Lecture Notes in Computer Science}, volume = {4424}, year = {2007}, pages = {583-586}, publisher = {Springer}, organization = {Springer}, type = {inproceedings}, ISBN = {978-3-540-71208-4}, author = { Jain, Himanshu and Kroening, Daniel and Sharygina, Natasha and Clarke, Edmund M.} editor = {Orna Grumberg and Michael Huth}, }
Attachment | Size |
---|---|
vcegar-tool.pdf | 94.32 KB |