PV3 ⊧ VCEGARchecks user-specified safety properties for Verilog programs

VCEGAR is a tool for checking safety properties (assertions) of Verilog programs

Application domain/field

• Safety verification
• Verilog
• Predicate abstraction
• Hardware model checking
• Model checking
• Counterexample-guided abstraction refinement (CEGAR)

Type of tool

Model checker

Expected input

• Verilog description
• Property

Format:

• Verilog description: Verilog
• Property: CTL?

Expected output

Property holds or a counterexample showing how the property is violated.

Internals

Uses predicate abstraction and a refinement loop (CEGAR).