Acyclic Assume-Guarantee Verification with SBY

Consider the following module acyclic that can be found in acyclic.sv.

module acyclic(x, z); 
  input logic [4:0] x;
  output logic [4:0] z;
  logic [4:0] y;

  subm s(.x(x), .y(y));
  always_comb begin
    z = (y < 13) ? y : y-2;
    acyclic_assert1: assert(z >= 2);
  end
endmodule

module subm (
    input logic [4:0] x,
    output logic [4:0] y
);
    always_comb begin
      y = (x > 2) ? x : 5'd 2;
      subm_assert1: assert (y >= 2);
    end
endmodule

The module takes as input x and produces z that is asserted to be at least 2. The correctness of this assertion both depends on the submodule subm which takes x and provides y, and on the blocking update of z which depends on y inside the combinational block of acyclic.

Let us look at the circuit computed by Yosys (with this script):

One can identify the input signal x on the left, the output signal z on the right, and the element labeled subm is the submodule instance. There is also a $check cell corresponding to the assertion acyclic_assert1.

The above circuit is displayed before flattening, which means that the subm module is kept separate. And here is the flattened full circuit, with the content of subm:

This circuit is of course small enough so that both assertions can be proven monolithically:

  sby -f acyclic.sby monolithic

You can inspect the monolithic task in the acyclic.sby configuration file. This simply loads the Verilog module with acyclic as top module, and applies the smtbmc engine in prove mode (which applies the k-induction algorithm).

Acyclic Assume-Guarantee Rule

But let us explain now the acyclic assume-guarantee rule and show how to apply it here. The acyclic rule allows us to prove the assertion of subm independently first, and then proving the assertion of the top module (module acyclic here) using the assertion of subm as an assumption, and immediately deduce that the overall system satisfies the top module’s assertion:

This is an inference rule, where $\text{subm} \vDash P$ means the submodule satisfies property $P$ (here, subm_assert1), and $\text{top} \setminus \text{subm} \vDash P \Rightarrow Q$ means that the top module without the submodule satisfies $Q$ provided that $P$ holds. That is, when proving $Q$ (here acyclic_assert1), $P$ is used as an assumption. If both these premises are proven, then we can deduce that $Q$ (here acyclic_assert1) holds as well, $P$ is used as an assumption.

Here, cutting off the submodule simply consists in disconnecting its output pins, and thus, in our case, in assigning the signal acyclic/y arbitrary non-deterministic values rather than values computed by subm. We will show below how to do this. The advantage of doing this is to reduce the state space to be analyzed since we are analyzing just the internal logic of the top module, and we are analyzing subm separately.

Note that sby’s distribution contains an “abstraction” example where the internal logic of a module is replaced by its properties. This is of course similar in spirit while we present this idea with explicitly given assume-guarantee reasoning rules.

Checking the Submodule

Checking the submodule subm is the easy part: run

  sby -f acyclic.sby check_subm

The configuration described in acyclic.sby for the task check_subm is equivalent to the following .sby file:

[tasks]
check_subm

[options]
mode prove

[engines]
smtbmc

[script]
read -formal acyclic.sv
hierarchy -top subm

[files]
acyclic.sv

Thus, we just load the file and choose subm as the top module, and check its assertion. When this module is verified in isolation, the input x is unconstrained, so we are indeed checking that all possible inputs to subm satisfy the assertion.

Checking the Top Module

Let us now check the second premise with sby. The idea is to replace the submodule subm with its specification, and check the top module. We could do this by a syntactic transformation, as follows:

module acyclic(x, z); 
  input logic [4:0] x;
  output logic [4:0] z;
  logic [4:0] y;

  always_comb begin
    z = (y < 13) ? y : y-2;
    subm_assume1: assume(y >= 2);
    acyclic_assert1: assert(z >= 2);
  end
endmodule

Here, we removed the instance of subm altogether, which resulted in signal y to be undriven. We then added the assumption subm_assume1 which constrains y to satisfy the property y >= 2 which we previously proved on subm. Here, y can of course take arbitrary values which are not possible under subm (such as $y = 2$ when $x > 2$). However, this general assumption on the outputs of subm is sufficient to prove our property on the top module.

The schematic of the resulting circuit is given below.

One can see that there is no driver for wire y. But there is an additional $check cell corresponding to the subm_assume1 constraining y to satisfy y >= 2.

While rewriting the models in this way is possible using macros, this might render the source code difficult to read and maintain, and might be error prone. The tool sby allows one to do the above transformation within the configuration script, without modifying the source code at all. We proceed as follows:

• Convert the assert cell of subm into an assume cell using the chformal command,
• Prepare the model (invoke RTL synthesis) with the prep command,
• Disconnect the wire y from its drivers (but keep the assume cell) using the cutpoint command. There is one subtlety here since we need the name of the flattened signal corresponding to y. After flattening applied by prep, a flattened signal name becomes <top_module>/<instance_name>.<signal_name>, so here acyclic/s.y. The script below contains log commands to check the new signal name.

These steps can be performed with the following commands in the script section:

[script]
check_top:
chformal -assert -assert2assume subm/subm_assert1
prep
cutpoint acyclic/s.y

# check that there is indeed a unique signal of the name acyclic/s.y
select -assert-count 1 acyclic/s.y
# Visual double-check: List all the wires that end with the suffix y into the file ../props.txt:
tee -a ../props.txt log The y wires:
tee -a ../props.txt select w:*y -list
--

The select -assert-count command checks that there exists indeed a single signal with name acyclic/s.y. We further use the select command to list all signal names ending with y for debugging or for manually checking all signals ending with y. This check is important to ensure that the cutpoint command does what we expect it to do.

One can visualize the synthesized circuit after the cutpoint by the following commands:

opt_clean -purge
show -format svg

Here, the first line removes unused cells that became disconnected due to cutpoint. We get the following circuit.

Here, the signal y is now driven by a $anyseq cell representing a non-deterministic value in a formal verification context. Moreover, the $check cell below is the assume statement, and the $check cell on the right is the assertion.

This circuit is equivalent to the one we obtained manually by removing the instance of subm in the source code, but with an additional explicit $anyseq cell driving s.y. This method must be preferred when possible.

Flatten/Prep Before Cutpoint

Why flatten before applying cutpoint? If we apply cutpoint before flattening, then the assume will also be cut and thus no longer constrain the top module’s y wire.

The following circuit was obtained by cutting the output y of subm (wire subm/y) before flattening (with this script).

The component above is subm is now fully disconnected from the top module acyclic below. One can see that the assume cell stays above. An attempt to verify the component below will fail since the assumption does not apply in this component.

To see this, run

sby -f acyclic.sby check_top_fails

Acyclicity

An important point to remember for this rule is that while the proof of the top module can depend on the properties proven by subm, the proof for subm cannot depend on the properties proven by the top module. This is why we call this rule acyclic. In general, it is possible to prove the assertions of a submodule subm1 independently (not depending on the correctness of other assertions), use their properties assertions for proving another submodule subm2, and use both assertions as assumptions when proving the top module. This chain is sound as long as there is no circular assumptions.

There is no automatic check of absence of circular reasoning. A sound circular reasoning rule is presented next.