Word-level predicate-abstraction and refinement rechniques 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...

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron: Jain, H, Kroening, D, Sharygina, N, al., E
Fformat: Journal article
Cyhoeddwyd: Institute of Electrical and Electronics Engineers 2008