Assertion Count

SystemVerilog
, ,
1

I have written assertion to wait in same state st = a when cnt is less than 5.
but I have used always block to increment the cnt.
—Is there any other way to write this?
—Is there a way to write incrementing cnt inside property?

always @(posedge clk) begin
  if (rst)
     cnt = 0;
  else begin
     if(st == a)
       cnt = cnt +1;
     else
end

property cnt_p;
  @(posedge clk) disable iff (rst)
  (st == a)&&(cnt < 5) |-> (st == a);
endproperty
cnt_assert : assert(cnt_p);
2

In reply to Timus:

There is probably a better way to write your assertion, but the way you have written it, (st == a) has to be true just once, and the count is irrelevant.

3

In reply to dave_59:

Let’s say if I write it in a way such that
(st==a)&& (cnt=0) |->(st == a)&&(cnt < 5);
Si that antecedent is true just once… But still count cannot be irrelevant right??

4

In reply to Timus:

Only local variables are allowed to be modified inside property, so you need to call some method from property to increment the counter. you can try something like this -


module top();

bit clk;
int count;

always #1 clk = !clk;

initial begin
  repeat(10) @(posedge clk);
  $finish;
end

property cnt_p();
        //@(posedge clk) (1) |-> (1,count=count+1);
        @(posedge clk) (1) |-> (1,t_inc_counter());
endproperty

count_ap: assert property(cnt_p());

task automatic t_inc_counter();
 count++;
endtask

endmodule
5

In reply to Timus:

Your assertion reads like:

If in the cycle that both st equals a and cnt equals 0 then in the same cycle both st equals a and cnt is less than 5

In the cycle that the antecedent is true, the consequent will always be true.

It might help to explain your requirement in words rather than SystemVerilog code.

6

In reply to dave_59:
requirements are ambiguous. However,


// "I have written assertion to wait in same state st = A when cnt is less than 5."
// Reading into your requirements:
// When state goes into 'A', it shall stay in that state for a total of 5 cycle. 
// (i.e., for 4 more cycles)
// BTW, use upper case for states enumerations, it's a convention

property cnt_p;
  @(posedge clk) disable iff (rst)
  $rose(st == A) |-> ##1 st==A [*4] ##1 st !=A; // updated
endproperty
cnt_assert : assert(cnt_p);
7

In reply to ben@SystemVerilog.us:

The requirement is that FSM should wait in (st == A) till 5 clk cycles. If it by force or by mistake moves to next state it assertion should be triggered as error

8

In reply to Timus:
You mean, when the FSM enters in state A then it should stay (not wait)
in that state (st == A) for a total of 5 clk cycles. Afterwards the fsm goes to a different state.
My previous assertion does that.

 
// When state goes into 'A', it shall stay in that state for a total of 5 cycle. 
// (i.e., for 4 more cycles)
// 
 
property cnt_p;
  @(posedge clk) disable iff (rst)
  $rose(st == A) |-> ##1 st==A [*4] ##1 st !=A; // updated
endproperty
cnt_assert : assert(cnt_p);
9

In reply to Timus:
Following conditions are met in this assertion,
When rst is deasserted (when FSM comes out of reset) and st == a, then it should remain in this state for minimum 5 cycles.

You can remove $fell(rst), if for anytime st == a then it should be in this state for minimum 5 cycles.

  property cnt_p;
    @(posedge clk) disable iff (rst)
    $fell(rst) && (st == a) |=> $stable(st)[*4]; 
  endproperty
10

In reply to raja rathinam:

 // should not remove the $fell, but instead use the or

$fell(rst) && (st == a) or $rose(st==a) |=> $stable(st)[*4] ##1 $changed(st);
// to account for the change in the 6th cycle