PV3 ⊧ SimpleCARchecks if a given property holds on a given circuit model

Safety hardware model checker. Tool specifically for evaluating and extending the CAR (Complementary Approximate Reachability) framework. It can be used for unsafety checking, or bug-finding.

Application domain/field

• Model checking
• Hardware model checking
• Safety verification

Type of tool

Hardware model checker

Expected input

Hardware circuit model expressed as And-Inverter Graphs containing a single safety property

Format:

AIGER 1.9

Expected output

0 (SAFE), 1(UNSAFE) SimpleCar can also generate a counterexample if run with the option -e.

Internals

Uses Glucose as underlying SAT solver, AIGER for parsing and error checking.