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

SMT-based symbolic model checker for hardware design

Application domain/field

• Model checking
• SMT-based model checking
• Hardware design
• Bounded model checking

Type of tool

Model checker

Expected input

• Input files describing the hardware
• Verification problem (e.g. safety or LTL) or equivalence checking
• Depending on previous choice you may need to provide: Property (invariant or LTL property)

Format:

It supports many input formats including:

• CoreIR
• BTOR2
• Verilog
• SystemVerilog
• Symbolic Transition Systems (STS)
• Explicit states Transition Systems (ETS).

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.

Internals

CoSA supports many different analyses/verifications:

• Invariant properties
• LTL properties
• Equivalence checking
• Parametric (Invariant) model checking
• Fault analysis
• Automated lemma extraction

CoSA reduces all analyses to symbolic model-checking problems. Uses Yosys to support Verilog as input format. Uses PySMT, PyCoreIR

Comments

License: Modified BSD (3-clause BSD) license