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

Last commit date

21 December 2020

Related papers

Last publication date

18 July 2018

Related tools

SimpleCAR is a rewrite of CARChecker.

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.