PV3 CoSA: CoreIR Symbolic Analyzerchecks user-specified properties for hardware designs

SMT-based symbolic model checker for hardware design

Application domain/field

Type of tool

Model checker

Expected input


It supports many input formats including: Properties can be defined as a parameter or in some of the input formats mentioned above.

Expected output

Depends on the type of analysis that you do with the tool.


CoSA supports many different analyses/verifications: CoSA reduces all analyses to symbolic model-checking problems. Uses Yosys to support Verilog as input format. Uses PySMT, PyCoreIR


License: Modified BSD (3-clause BSD) license
Hardware LTL Model checking


Repository: https://github.com/cristian-mattarei/CoSA

Related papers

CoSA: Integrated Verification for Agile Hardware Design (FMCAD '18)

Last publication date

2 November 2018

Related tools

Pono: this tool was developed as the next generation of CoSA.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.