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

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.
Hardware Model checking

Links

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.