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...

• Type: Journal
• Year: 2008
• Where: TCAD
• Authors: Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
• Keywords: Abstraction, Predicate Abstraction, RTL Verilog, TCAD 2008