Sciweavers

Share
TCAD
2008

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

8 years 11 months ago
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog
el Predicate Abstraction and Refinement Techniques for Verifying RTL Verilog Himanshu Jain, Daniel Kroening, Natasha Sharygina, and Edmund M. Clarke, Fellow, IEEE As a first step, most model checkers used in the hardware industry convert a high-level register transfer level (RT-level/RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure igher abstraction levels, and thus, are less scalable. The RT-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. er uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) The compuf the abstract model in presence of a large number of predicates, and 2) the discovery of suitable word-level predicates raction refinement. We address the first problem using a...
Himanshu Jain, Daniel Kroening, Natasha Sharygina,
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCAD
Authors Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Comments (0)
books