Open Source Projects

YosysHQ members have created and contributed to world class Open Source projects. Here are some of the projects that are being maintained by members of our team.

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.

The version of Yosys that is included in Tabby CAD Suite also includes industrial-strength SystemVerilog and VHDL front-ends.

SymbiYosys (SBY) is a front-end for Yosys-based formal verification flows with support for

  • Unbounded and bounded verification of safety properties

  • Unbounded verification of liveness properties

  • Reachability-check and bounds-detection for cover properties

  • Additional attributes for management of unconstrained signals

  • Synchronous, asynchronous, and multi-clock designs, resets and latches

SymbiYosys integrates with state-of-the-art SMT solvers and HW model checkers

mcy is a new tool to help digital designers and project managers understand and improve testbench coverage. If you have a testbench, and it fails, you know you have a problem. But if it passes, you know nothing if you don’t know what your testbench is actually testing for.

A refreshed Python toolbox for building complex digital hardware.

Despite being faster than schematics entry, hardware design with Verilog and VHDL remains tedious and inefficient for several reasons. The event-driven model introduces issues and manual coding that are unnecessary for synchronous circuits, which represent the lion's share of today's logic designs.

To address those issues, we have developed the nMigen FHDL, a library that replaces the event-driven paradigm with the notions of combinatorial and synchronous statements, has arithmetic rules that make integers always behave like mathematical integers, and most importantly allows the design's logic to be constructed by a Python program.

nextpnr aims to be a vendor neutral, timing driven, FOSS FPGA place and route tool.

Currently nextpnr supports a range of FPGAs including Lattice iCE40 and ECP5 devices.

Project IceStorm aims at documenting the bitstream format of Lattice iCE40 FPGAs and providing simple tools for analyzing and creating bitstream files. The IceStorm flow (Yosys, Arachne-pnr, and IceStorm) is a fully open source Verilog-to-Bitstream flow for iCE40 FPGAs.

The focus of the project is on the iCE40 LP/HX 1K/4K/8K chips. (Most of the work was done on HX1K-TQ144 and HX8K-CT256 parts.) The iCE40 UltraPlus parts are also supported, including DSPs, oscillators, RGB and SPRAM. iCE40 LM, Ultra and UltraLite parts are not yet supported.

Project Trellis enables a fully open-source flow for ECP5 FPGAs using Yosys for Verilog synthesis and nextpnr for place and route. Project Trellis itself provides the device database and tools for bitstream creation.

PicoRV32 is a CPU core that implements the RISC-V RV32IMC Instruction Set. It can be configured as RV32E, RV32I, RV32IC, RV32IM, or RV32IMC core, and optionally contains a built-in interrupt controller.

riscv-formal is a framework for formal verification of RISC-V processors. riscv-formal specifies a common trace port interface (RVFI) that must be implemented by the processor under test, and includes a set of processor-independent formal properties that can be applied to any processor that implements the RVFI specification.

CXXRTL is a high-performance simulation back-end for Yosys. It writes optimized C++ code that simulates the design. The generated code requires a driver program that instantiates the design, toggles its clock, and interacts with its ports. CXXRTL also supports replacing parts of the design with black boxes implemented in C++.