Question

The purpose of the assume statement is to allow properties to be considered as assumptions for formal analysis as well as for dynamic simulation tools. When a property is assumed, the tools constrain the environment so that the property holds.

For formal analysis, there is no obligation to verify that the assumed properties hold. An assumed property can be considered as a hypothesis to prove the asserted properties.

For simulation, the environment must be constrained such that the properties that are assumed shall hold. Like an assert property, an assumed property must be checked and reported if it fails to hold. There is no requirement on the tools to report successes of the assumed properties.

Additionally, for random simulation, biasing on the inputs provides a way to make random choices. An expression can be associated with biasing as shown below

expression dist { dist_list } ; // from Annex A.1.9

Distribution sets and the dist operator are explained in Section 12.4.4.

The biasing feature is only useful when properties are considered as assumptions to drive random simulation. When a property with biasing is used in an assertion or coverage, the dist operator is equivalent to inside operator, and the weight specification is ignored. For example,

a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
property proto
    @(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty

This is equivalent to:

a1_assertion:assert property req inside {0, 1} ;
property proto_assertion
    @(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty

In the above example, signal req is specified with distribution in assumption a1, and is converted to an equivalent assertion a1_assertion.

It should be noted that the properties that are assumed must hold in the same way with or without biasing. When using an assume statement for random simulation, the biasing simply provides a means to select values of free variables, according to the specified weights, when there is a choice of selection at a particular time.

Consider an example specifying a simple synchronous request - acknowledge protocol, where variable req can be raised at any time and must stay asserted until ack is asserted. In the next clock cycle both req and ack must be de-asserted.

Properties governing req are:

property pr1;
    @(posedge clk) !reset_n |-> !req; //when reset_n is asserted (0),keep req 0
endproperty

property pr2;
    @(posedge clk) ack |=> !req; // one cycle after ack, req must be de-asserted
endproperty

property pr3;
    @(posedge clk) req |-> req[*1:$] ##0 ack; // hold req asserted until
    // and including ack asserted
endproperty

Properties governing ack are:

property pa1;
    @(posedge clk) !reset_n || !req |-> !ack;
endproperty

property pa2;
    @(posedge clk) ack |=> !ack;
endproperty

When verifying the behavior of a protocol controller which has to respond to requests on req, assertions assert_req1 and assert_req2 should be proven while assuming that statements a1, assume_ack1, assume_ack2 and assume_ack3 hold at all times.

a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
assume_ack1:assume property (pr1);
assume_ack2:assume property (pr2);
assume_ack3:assume property (pr3);
assert_req1:assert property (pa1)
    else $display("\n ack asserted while req is still de-asserted");
assert_req2:assert property (pa2)
    else $display("\n ack is extended over more than one cycle");

Note that assume does not provide an action block, as the actions for an assumption serve no purpose.