jix.one

Yosys

Tagged formal-verification, hardware, sat

Yosys and associated YosysHQ projects form an open-source hardware synthesis and formal verification toolchain. In 2022 I strarted contributing to some of these projects and now co-maintain the formal verification part of YosysHQ’s tooling, making good use of my background in SAT and SMT solving.

The simplest way to try it out is the OSS CAD Suite which provides pre-built binaries including lots of optional-but-recommended dependencies.

The SBY Documentation is a good start if you want to learn how to use Yosys for formal verification.