Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (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 RT...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|