Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

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


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


  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]

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


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.


  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


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

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

   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