PV3 ⊧ SimpleCARchecks if a given property holds on a given circuit modelSafety 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.
- Model checking
- Hardware model checking
- Safety verification
Type of toolHardware model checker
Expected inputHardware circuit model expressed as And-Inverter Graphs containing a single safety property
Expected output0 (
SimpleCar can also generate a counterexample if run with the option