SymbiYosys (sby) Documentation

SymbiYosys (sby) is a front-end driver program for Yosys-based formal hardware verification flows. SymbiYosys provides flows for the following formal tasks:

• Bounded verification of safety properties (assertions)

• Unbounded verification of safety properties

• Generation of test benches from cover statements

• Verification of liveness properties

• Formal equivalence checking [TBD]

• Reactive Synthesis [TBD]

(Items marked [TBD] are features under construction and not available at the moment.)

• Installing
  • Prerequisites
  • Yosys, Yosys-SMTBMC and ABC
  • SymbiYosys
  • Yices 2
  • Z3
  • super_prove
  • Avy
  • Boolector
• Getting Started
  • First step: A simple BMC example
  • Selecting the right engine
  • Beyond bounded model checks
• Reference for .sby file format
  • Tasks section
  • Options section
  • Engines section
    • smtbmc engine
    • btor engine
    • aiger engine
    • abc engine
  • Script section
  • Files section
  • File sections
  • Pycode blocks
• Autotune: Automatic Engine Selection
  • Using Autotune
    • Example
  • Autotune Log Output
  • Configuring Autotune
  • Autotune Options
• Formal extensions to Verilog
  • SystemVerilog Immediate Assertions
  • SystemVerilog Functions
  • Liveness and Fairness
  • Unconstrained Variables
  • Global Clock
  • SystemVerilog Concurrent Assertions
• SystemVerilog, VHDL, SVA
  • Supported SVA Property Syntax
    • High-Level Convenience Features
    • Expressions in Sequences
    • Sequences
    • Properties
    • Clocking and Reset
• SymbiYosys License