...an SMT-based symbolic model checker for hardware design.
CoSA supports a variety of input formats:
- CoreIR
- BTOR2
- Verilog
- SystemVerilog
- Symbolic Transition System (STS)
- Explicit states Transition System (ETS)
and verifications:
- Invariant Properties
- Linear Temporal Logic (LTL) Properties
- Proving capabilities
- Equivalence Checking
- Parametric (Invariant) Model Checking
- Fault Analysis
- Automated Lemma Extraction
pip3 install cosa
to install CoSA, and its dependencies i.e., PySMT, PyCoreIR, and PyVerilogpysmt-install --msat
to install MathSAT5 solver (it provides interpolation support), orpysmt-install --cvc4
for CVC4 andpysmt-install --z3
for Z3pysmt-install --env
to show the environment variables that need to be exported
Software requirements:
- CoreIR needs to be installed in order to support CoreIR as input format
- Icarus Verilog needs to be installed in order to support Verilog as input format
- Verific binaries (i.e.,
verific
) and Icarus Verilog need to be installed in order to support SystemVerilog as input format
To start playing with the tool, you can run:
CoSA -h
shows the helper with command optionsCoSA -i examples/counters/counters.json --simulate -k 7
generates a system execution with depth 7CoSA -i examples/counters/counters.json --safety -p "!(count0.a.out = 5_16)" -k 7
performs reachability model checking with property count0.a.out != 5 as a 16-bit BitvectorCoSA --problem examples/counter/problem.txt --prefix trace
performs liveness (GF) and finally (F) checking on the counter.json model using the problem definitionCoSA --problem examples/fold-constants/problem.txt
performs equivalence checking using lemmas
For more information, please refer to the CoSA user manual.
- install Docker with your package manager e.g.,
sudo apt-get install docker
- build the Docker image:
cd docker/ubuntu_1604 && docker build -t ubuntu-cosa .
- run the Docker image:
docker run -i -t ubuntu-cosa /bin/bash
pip3 install -e .
to install CoSA from the sourcenosetests tests
to run the tests
CoSA is released under the modified BSD (3-clause BSD) License.
If you use CoSA in your work, please consider citing the following publication:
@inproceedings{DBLP:conf/fmcad/MattareiMBDHH18, author = {Cristian Mattarei and Makai Mann and Clark Barrett and Ross G. Daly and Dillon Huff and Pat Hanrahan}, title = {{CoSA: Integrated Verification for Agile Hardware Design}}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2018, Austin, Texas, USA, October 30 - November 2, 2018.}, publisher = {{IEEE}}, year = {2018} }