Awesome Open Source
Awesome Open Source

.. figure:: :align: center

CoSA: CoreIR Symbolic Analyzer SMT-based symbolic model checker for hardware design.

======================== Overview

CoSA supports a variety of input formats:

  • CoreIR_
  • BTOR2_
  • Verilog (with Yosys)
  • SystemVerilog (with Verific)
  • 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

======================== Installation

  1. pip3 install cosa to install CoSA, and its dependencies i.e., PySMT, PyCoreIR, and PyVerilog_

  2. pysmt-install --msat to install MathSAT5_ solver (it provides interpolation support), or pysmt-install --cvc4 for CVC4_ and pysmt-install --z3 for Z3_ and pysmt-install --btor for Boolector_

  3. pysmt-install --env to show the environment variables that need to be exported

Software requirements:

  • Python3_ -- Full support requires Python3.6 or higher, however running without the CoreIR_ inputs should work on older Python 3 versions
  • Pip3_: package manager -- easiest way to install CoSA. On Debian: apt-get update; apt-get install python3-pip.
  • Cmake_ and a standard C++ compiler for CoreIR_ / PyCoreIR_
  • Yosys_ needs to be installed in order to support Verilog as an input format
  • Verific_ binaries or Yosys built with Verific library in order to support SystemVerilog as an input format [Commercial Tool]

.. _BTOR2: .. _Boolector: .. _Cmake: .. _CoreIR: .. _CVC4: .. _ETS: .. _Git: .. _Icarus Verilog: .. _MathSAT5: .. _Pip3: .. _PyCoreIR: .. _PySMT: .. _Python3: .. _PyVerilog: .. _STS: .. _Verific: .. _Yosys: .. _Z3:

======================== Installation from Source

  • Install Git_
  • git clone
  • cd CoSA
  • pip3 install -e .

Pip will automatically install the Python dependencies. To install Yosys for Verilog support, follow the instructions here <>_.

Note: If running in a Python virtualenv, pip will install the CoSA script in ~/.local/bin, so be sure it's added to your PATH with export PATH=~/.local/bin:$PATH.

To run tests (tests include Veriog models and thus require Yosys):

  • nosetests tests

======================== Usage

To start playing with the tool, you can run:

  1. CoSA -h shows the helper with command options

  2. CoSA -i examples/counters/counters.json --verification simulation -k 7 generates a system execution with depth 7

  3. CoSA -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 Bitvector

  4. CoSA --problem examples/counter/problem.txt --prefix trace performs liveness (GF) and finally (F) checking on the counter.json model using the problem definition

  5. CoSA --problem examples/fold-constants/problem.txt performs equivalence checking using lemmas

For more information, please refer to the CoSA user manual_.

.. _CoSA user manual:

======================== Docker

  1. install Docker with your package manager e.g., sudo apt-get install docker

  2. build the Docker image: cd docker/ubuntu_1604 && docker build -t ubuntu-cosa .

  3. run the Docker image: docker run -i -t ubuntu-cosa /bin/bash

======================== License

CoSA is released under the modified BSD (3-clause BSD) License.

If you use CoSA in your work, please consider citing the following publication:

.. code::

@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} }

======================== Build Status

.. image:: :target:

Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
python (45,333
verilog (215
systemverilog (55
model-checking (17
formal-methods (14
formal-verification (14

Find Open Source By Browsing 7,000 Topics Across 59 Categories