YosysHQ Tool Documentation

Yosys

Yosys is a framework for RTL synthesis and more. It currently has extensive Verilog-2005 support and provides a basic set of synthesis algorithms for various application domains. Yosys is the core component of most our implementation and verification flows.

• Yosys manual

• Yosys command reference

SBY

SBY is a front-end for Yosys-based formal verification flows for safety properties, liveness properties, and reachability. Different engines offer a variety of solving methods in order to find the fastest solution.

• SBY reference manual

• Supported engines

MCY

MCY uses Yosys to provide mutation coverage of testbenches. By using built-in equivalence checking, the common problem with equivalent mutations can be avoided, and 100% coverage can be targeted.

• MCY reference manual

EQY

EQY is a tool to provide Yosys-based equivalence checking for formal verification.

• EQY reference manual

Formal Off-the-Shelf VIP

• riscv-formal is a framework for formal verification of RISC-V processors.

• SVA-AXI4-FVIP is a set of SVA properties that can be used to verify modules implementing any of the AXI4 and AXI4-Lite manager, subordinate, or interconnect interfaces.