Module implementing Bounded Model Checking for the verification of AIGER circuits. Currently only supports bad state detection (Circuits with one output that is 1 iff the circuit is in a bad state).
Install the requirements with pip install -r requirements.txt.
- Bound Model Checking:
python3 modelcheckers/BoundedModelChecker.py <path-to-aiger-circuit> <bound> - Model Checking:
python3 modelcheckers/UnboundedModelChecker.py <path-to-aiger-circuit>
python3 modelcheckers/BoundedModelChecker.py benchmarks/texas.PI_main%5E02.E.aag 10python3 modelcheckers/UnboundedModelChecker.py benchmarks/vis.emodel.E.aag