Question on assume() for liveness example

SystemVerilog
,
1

I have a verilog module below to be fed into yosys-smtbmc formal verification tool.

Code retrieved from yosys-smtbmc webpage

assume(axis_valid);

But I found out that with and without the above line does not affect the SMT solver result. WHY ?

module liveness(input clk, input axis_valid, output axis_ready);

	wire [7:0] maxcnt = $anyconst;
	reg [9:0] count1 = 0, count2 = 0;
	reg state2 = 0;

	reg expect_axis_valid = 0;

	always @(posedge clk) begin
		//if (expect_axis_valid)
		//	assume(axis_valid);
		expect_axis_valid <= axis_valid && !axis_ready;
	end

	always @(posedge clk) begin
		if (!axis_valid || (axis_valid && axis_ready)) begin
			count1 <= 0;
			count2 <= 0;
			state2 <= 0;
			axis_ready <= 0;
		end else
		if (axis_valid) begin
			if (!state2) begin
				count1 <= count1 + 3;
				if (count1 > maxcnt)
					state2 <= 1;
			end else begin
				count2 <= count2 + 1;
				if (count2*2 > count1)
					axis_ready <= 1;
			end
		end
	end

	integer timeout = 0;

	always @(posedge clk)
		if (axis_valid && !axis_ready)
			timeout <= timeout + 1;
		else
			timeout <= 0;

	assert property (timeout < 1000);

	always @* begin
		if (!state2)
			assert(count2 == 0);
		assert(3*timeout - 3*count2 == count1);
		assert(count1 <= maxcnt+6);
		assert(2*count2 <= count1+4);
	end
endmodule
2

In reply to feiphung:

When you write “assume(axis_valid);” the formal verification tool makes axis_valid ==1 for all analyses, meaning that it does not change. If your assertions pass with that signal being 1 or 0, then you would not have a negative report from the tool; thus, the above line does not affect the SMT solver result.
The “assume” defines conditions that should not be considered.
Should your model fail when that input is 0?
Ben Ben@systemverilog.us

3

In reply to ben@SystemVerilog.us:

expect_axis_valid <= axis_valid && !axis_ready;

How would this above line work with the if and assume() just before it ?

	always @(posedge clk) begin
		if (expect_axis_valid)
			assume(axis_valid);
		expect_axis_valid <= axis_valid && !axis_ready;
	end
4 
 
module liveness(input clk, input axis_valid, output axis_ready); 
 // How would this above line work with the if and assume() just before it ?
  always @(posedge clk) begin
	if (expect_axis_valid)
		assume(axis_valid);
	expect_axis_valid <= axis_valid && !axis_ready;
   end

FIrst, let’s understand the assume statement

The immediate assume statement specifies that its expression is assumed to hold. For example, immediate assume statements can be used with formal verification tools to specify assumptions on design inputs that constrain the verification computation. When used in this way, they specify the expected behavior of the
environment of the design as opposed to that of the design itself. In simulation, an immediate assume may behave as an immediate assert to verify that the environment behaves as assumed. A simulation tool shall provide the capability to check the immediate assume statement in this way.

So what is your immediate assume say?
if (expect_axis_valid), same as if ($sampled(axis_valid && !axis_ready) is true,
then the assume(axis_valid) says that for formal verification the input axis_valid need not be switched to zero in the current cycle. In simulation, under those conditions, axis_valid is true in the current cycle.

So what does that all mean? My guess is that the formal verification tool will not test the case of axis_valid==0 in the cycle following the case when axis_valid==1 and the output axis_ready==0. This is because we told the tool that following the cycle when expect_axis_valid==1 the input axis_valid is always true; thus no need to test THAT condition.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

5

In reply to ben@SystemVerilog.us:

Thanks Ben.

	always @* begin
		if (!state2)
			assert(count2 == 0);
		assert(3*timeout - 3*count2 == count1);
		assert(count1 <= maxcnt+6);
		assert(2*count2 <= count1+4);
	end

I am still wondering about the last three assertions ?

Do you have any comments ?

6

In reply to feiphung:

Assertions should be based on requirements, and not on actual code.
You need to refer to the requirements to determine if those assertions make sense.
Ben Ben@systemverilog.us