Question on assume() for liveness example

SystemVerilog
,
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