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

Type of tool

Hardware model checker

Expected input

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



Expected output

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


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


Related papers

Last publication date

18 July 2018

Related tools

SimpleCAR is a rewrite of CARChecker.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.