Assume-Guarantee Proofs for SystemVerilog with Yosys/SBY

While model checking is a powerful tool to verify properties of a design, one often encounters models that are too large or complex for model checking. This can also be the case when verifying SystemVerilog modules with formal verification tools such a sby.

In such difficult cases, a good strategy is to use assume-guarantee reasoning to break the problem into smaller pieces. This basically consists in removing one or more submodules, and replacing them by assumptions on their outputs. There are several assume-guarantee reasoning rules, and one must be careful in choosing the right rule and rigorously respecting the setting of the rule.

In this note, we will present two rules. We start with the simplest one, called the acyclic rule, and then we will present the circular rule which is slightly more involved.

In the future, we will also present a circular assume-guarantee rule for liveness properties (such as general LTL - PSL properties).

Requirements

This document assumes that the reader has basic knowledge of SystemVerilog and its assertion language. Moreover, we will be using the sby verification tool from YosysHQ.

The easiest way to obtain all dependencies is to install the OSS CAD suite.

References

A good starting point for assume-guarantee verification rules is the following book chapter.