Circular Assume-Guarantee Verification with SBY

The acyclic assume-guarantee rule requires one of the modules to be provable independently of other modules. In practice, this is not always possible. In fact, the correctness of most modules require some assumption on their inputs which are provided by other modules.

In general, it is very useful to be able to reason in an assume-guarantee way, and to prove each module’s assertion separately, by assuming the other module’s assertion. Ideally, we would like to obtain a rule of the following form:

where, as before, $\text{top}\setminus\text{subm}$ is obtained from $\text{top}$ by removing the submodule $\text{subm}$, so that the output pins of subm are non-deterministic. $\textsf{G}$ stands for the temporal operator “globally”, and means that the given property holds at all time points.

Unfortunately, this rule is not sound. We give an example below where a wrong property can be deduced if this rule is used. We then show how to fix this rule and derive a sound assume-guarantee rule allowing apparently circular reasoning.

Example showing that the above rule is unsound

Consider the following design. The top module cyclic receives has a register and output y which it passes to subm as input, and which it updates using the output of subm. The main specification is toplevel_guarantee and says that y should be odd at all times.

module cyclic(
    input logic clk,
    output logic [4:0] y
);
  logic [4:0] sy;

  subm s(.clk(clk), .x(y), .y(sy));

  always_ff @(posedge clk) begin
    y <= (sy < 29) ? sy + 2 : sy;
    `ifdef AG_CHECK_TOP
    toplevel_assume: assume(sy[0]);
    toplevel_guarantee: assert(y[0]);
    `endif
    `ifdef MONOLITHIC 
    assert(y[0]);
    `endif
  end
endmodule

module subm (
    input clk,
    input logic [4:0] x,
    output logic [4:0] y
);

  always_ff @(posedge clk) begin
    y <= (x < 29) ? x + 2 : x;
    `ifdef AG_CHECK_SUBM
    subm_assume: assume(x[0]);
    subm_guarantee: assert(y[0]);
    `endif
  end
endmodule

This is clearly wrong, since if the initial value of cyclic/y is 0, the property does not hold. Moreover, y will always remain even in this case. Such a counterexample can be generated as follows.

sby -f cyclic_wrong.sby monolithic

Nevertheless, we can “prove” that this property holds using the unsound rule above.

Let us check each module separately.

sby -f acyclic_wrong.sby check_top
sby -f acyclic_wrong.sby check_subm

Here, the check_subm task just loads the module with subm as the top module, while check_top loads cyclic as the top module but applies a cutpoint at subm/y before flattening, so disconnecting the submodule entirely. You can inspect the configuration file cyclic_wrong.sby (see also the acyclic rule for a detailed explanation of cutpoints).

Both verification tasks pass! What happened? We did prove something, but just not what we intended. The above rule actually implies that $\text{top} \models P\Leftrightarrow Q$, which holds here. In fact, subm/y is odd iff cyclic/y is odd, but this does not imply that these signals are always odd. In fact, both are odd if and only if the initial value of cyclic/y is odd. But because the initial value is not defined, here, it is considered nondeterministic and the property actually fails.

The situation is depicted below. Each module satisfies its specification provided that the other module satisfies its specification.

graph LR
  P((P)) --> Q((Q))
  Q --> P
  style P fill:#f9f,stroke:#333
  style Q fill:#bbf,stroke:#333

Sound Circular Assume-Guarantee Reasoning

The above error is known as circular reasoning, and is a common pitfall in mathematics. Can we still somehow assume something about the other module while proving each module? Fortunately yes, and the solution is to use induction over time.

The idea is simple: we can break circularity by assuming that the property of module A holds up to time $t-1$ when proving module B at time $t$, and vice versa. This means that at $t=0$, we must establish both properties independently. And at $t>0$, we can only rely on an assumption on the other module at the previous time step $t-1$.

We get the following sound circular assume-guarantee rule.

Here, in both premises, a property is asserted at the first time step, and then all times assuming the other property holds at the previous time point. One could strengthen the assumption and assume the other property at all previous time points by writing $\textsf{G}($\textsf{past}(\textsf{H} Q) \Rightarrow P)$ using the “historically” modality. This is also sound and can facilitate difficult proofs by strengthening the assumption.

This rule, however, only applies to sequential circuits and thus cannot be applied to combinational ones as in the example of the first section.

Note that the first conjunct in each premise corresponds to the base case of induction and is required. In fact, if we omit it, the rule is not sound for the same reason as for the first rule: e.g. if both $P$ and $Q$ are false at all times, then omitting the first conjunct, both premises would pass.

The relation between assumptions and guarantees is illustrated in the figure below. Notice that there is no more circularity.

graph TB
  subgraph Cyclic["Cyclic"]
    direction TB
    Pass[P at t-1]
    P[P at t]
  end

  subgraph Subm_["Subm"]
    direction TB
    Qass[Q at t-1]
    Q[Q at t]
  end

  Pass -.-> Q
  Qass -.-> P

  linkStyle 0 stroke:#666,stroke-width:1.5px,stroke-dasharray:5 5
  linkStyle 1 stroke:#666,stroke-width:1.5px,stroke-dasharray:5 5

  style P fill:#f99,stroke:#333
  style Q fill:#99f,stroke:#333
  style Pass fill:#f99,stroke:#333
  style Qass fill:#99f,stroke:#333

This can be modeled as follows; see also cyclic.sv.

module cyclic(
    input logic clk,
    output logic [4:0] y
);
  logic [4:0] sy;

  subm s(.clk(clk), .x(y), .y(sy));

  initial begin
    y = 1;
    // Base case: Assert P at t=0
    `ifdef AG_CHECK_TOP
    toplevel_guarantee_base: assert(y[0]);
    `endif
  end

  always_ff @(posedge clk) begin
    y <= (sy < 29) ? sy + 2 : sy;
    `ifdef AG_CHECK_TOP
    toplevel_assume: assume($past(sy[0])); // Assume Q held at t-1
    toplevel_guarantee: assert(y[0]);      // Assert P at t
    `endif
    `ifdef MONOLITHIC 
    assert(y[0]);
    `endif
  end
endmodule

module subm (
    input clk,
    input logic [4:0] x,
    output logic [4:0] y
);
  // Base case: Assert Q at t=0
  initial begin
    y = 1;
    `ifdef AG_CHECK_SUBM
    subm_guarantee_base: assert(y[0]);
    `endif
  end

  // Inductive step: Assume P held at t-1, assert Q at t
  always_ff @(posedge clk) begin
    y <= (x < 29) ? x + 2 : x;
    `ifdef AG_CHECK_SUBM
    subm_assume: assume($past(x[0])); // Assume P held at t-1
    subm_guarantee: assert(y[0]);     // Assert Q at t
    `endif
  end
endmodule

We can check both premises separately, using the cyclic.sby configuration file:

[tasks]
check_top
check_subm
monolithic

[options]
mode prove

[engines]
smtbmc

[script]
read -noverific
check_top:
read -define AG_CHECK_TOP=1 
read -sv cyclic.sv
prep -top cyclic
cutpoint subm/y
--
check_subm:
read -define AG_CHECK_SUBM=1 
read -sv cyclic.sv
prep -top subm
--
monolithic:
read -define MONOLITHIC=1
read -sv cyclic.sv
prep -top cyclic
--
[files]
cyclic.sv

Here, we had to annotate the assumptions and verification conditions in the source code but we only enabled these annotations in the respective tasks thanks to the use of macros.

You can run both tasks with:

sby -f cyclic.sby

If you want to check the property monolithically, run

sby -f cyclic.sby monolithic

Redundant Base Case

The above model can actually be simplified by removing the base case. Indeed, due to the semantics of SystemVerilog assertions, the base case is checked within the always_ff block.

First, note that Yosys encodes $past(y) by generating a register. The initial value of this register is artbirary (nondeterministic), and at each cycle, the register is updated with the previous value of y.

Furthermore, assert and assume statements inside always_ff blocks use values of signals sampled in the preponed region, that is, their values correspond to the stable values of the previous cycle (before the non-blocking assignment (NBA) region). So the values of y and sy in the first cycles are as below (assume x=0 at all times):

Here, step 0 is the initial step where the always block has not been yet executed. Step 1 corresponds to the first positive edge of clk, and the first execution of the always block. The assume and assertion still see the previous stable values of y and sy as per the semantics of SystemVerilog. From step 2 onwards, the value of sy relates to the input x, and the value y to sy.

The above semantics can sometimes cause confusion since signals values in simulation results show post-NBA values (stable values at the current cycle).

Now, look at what happens on step 1. We have

assume($past(sy[0]));
assert(y[0]);

The assume does not relate to any useful signal value since the initial value (shown as nondet above) of the register $past(y) does not propagate to any other signal. During this check, assume($past(y[0])) forces this value to be 1 without any logical consequence on y. The model checker will then check the assertion assert(y[0]) alone, which is precisely the base case of the induction since this sampled value is equal to the initial value.

We still leave the base case above since this is harmless, and make the induction argument more explicit.