Journal article icon

Journal article

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog

Abstract:

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 RTL 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. This paper uses predic...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1109/TCAD.2007.907270

Authors


More by this author
Department:
Oxford, MPLS, Computer Science
Sharygina, N More by this author
Publisher:
Institute of Electrical and Electronics Engineers Publisher's website
Journal:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems Journal website
Volume:
27
Issue:
2
Pages:
366-379
Publication date:
2008-02-01
DOI:
EISSN:
1937-4151
ISSN:
0278-0070
Pubs id:
pubs:327165
URN:
uri:ebc6ba1b-cfb7-46e5-a404-c93e21668076
UUID:
uuid:ebc6ba1b-cfb7-46e5-a404-c93e21668076
Local pid:
pubs:327165
Keywords:

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP