SVA- How we can write property such that it will check OUT_BITS increment and decrement

[rupeshblr]

There are below Input signals- mon_count, count, Enable
and output signal - OUT_BITS ( initial value 8’b100000000 i.e 128 )

How to write property to check the below scenario ?

** if (mon_count < count) and Enable = 1 then OUT_BITS should increment like 11000000 (i.e 198) again sample at mon_clk if (mon_count < count) OUT_BITS should 11100000 (i.e 224) like it can reach upto 8’b11111111 but if (mon_count > count ) it should do the decrement like (OUT_BITS is 10000000 then OUT_BITS should decrement to 01000000) . it will so on.

Any leads

[ben2]

In reply to rkg_:

Write 2 assertions, one for the increment and one for the decrement.
If you know anything about SVA, then you would know about the implications operators.
To learn SVA you need to write a model and also study the language.
Ben

[rupeshblr]

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for suggestion.

Is it correct way ?

property out_bits_incr_prpty;
		@(negedge refclk_output) disable iff(!reset)
		(monclk_count <  count) |=> (out_bits > ($past(out_bits, 1) );
	endproperty
/* check the out bits decrement */
property out_bits_decr_prpty;
		@(negedge refclk_output) disable iff(!en_reset)
		(negclk_count > count) |=> (out_bits < ($past(out_bits, 1));
	endproperty

please correct me if i am wrong

[ben2]

In reply to rkg_:
Your requirements are ambiguous, do you want an increment/decrement by 1 or
do you want a shift left/right. Also what about the rollover?
bit[3:0] a=4’b1111;
a + 1’b1 == 4’b0000;

// ** if (mon_count < count) and Enable = 1 then OUT_BITS should increment like 11000000 (i.e 198) 
// again sample at mon_clk if (mon_count < count) OUT_BITS should 11100000 (i.e 224) like it can reach upto 8'b11111111
//  but if (mon_count > count ) it should do the decrement like (OUT_BITS is 10000000 
// then OUT_BITS should decrement to 01000000) . it will so on.
property out_bits_incr_prpty;
  @(negedge refclk_output) disable iff(!reset)
  (monclk_count <  count) && Enable|=> out_bits == $past(out_bits) + 1'b1;
   // was: (out_bits > ($past(out_bits, 1) );
endproperty 
/* check the out bits decrement */
property out_bits_decr_prpty;
  @(negedge refclk_output) disable iff(!en_reset)
  (negclk_count > count) && Enable|=> out_bits == $past(out_bits) - 1'b1; 
  // was: (out_bits < ($past(out_bits, 1));
endproperty

[rupeshblr]

In reply to ben@SystemVerilog.us:

HI,

I don’t want incr/decr by 1.

its should be like if (mon_count < count ) out_bits should get increment like from 10000000 to 11000000 like so on and if mon_count > count out_bits should be decrement like from 10000000 to 01000000 and so on

And It should not rollover means out_bits will not toggles once it reach to 11111111 or 00000000.

[ben2]

In reply to rkg_:

So your increment / decrement for a 4-bit “a” is

    bit[3:0] a;
    a = {1'b1, a[3:1]}; // increment, 1'b1 concat with a right shift by 1
    a = {a[2:0], 1'b0}; // deccrement, shift left by 1 with concat of 0  
property out_bits_incr_prpty;
  @(negedge refclk_output) disable iff(!reset)
  (monclk_count <  count) && Enable|=> 
      out_bits == {1'b1, $past(out_bits[3:1])};
   // was: (out_bits > ($past(out_bits, 1) );
endproperty 
/* check the out bits decrement */
property out_bits_decr_prpty;
  @(negedge refclk_output) disable iff(!en_reset)
  (negclk_count > count) && Enable|=> 
       out_bits == {$past(out_bits[2:0]), 1'b0)}; 
  // was: (out_bits < ($past(out_bits, 1));
endproperty

[rupeshblr]

In reply to ben@SystemVerilog.us:

HI Ben,

Thanks for suggestion.

[rupeshblr]

In reply to rkg_:

Hi Ben,

i can see decr_property get trigger when monclk_cout < i_count and same incr_property get trigger when monclk_count >= i_count

Code :

property prog_out_fll_incr_prpty;
		@(negedge  refclk_sig_d1) disable iff(!i_en_fll)
		(monclk_count < i_count) |=> (o_prog_out_fll == {1'b1,$past(o_prog_out_fll[7:1])} );
	endproperty


property prog_out_fll_decr_prpty;
		@(negedge  refclk_sig_d1) disable iff(!i_en_fll)
                                              
		(monclk_count >= i_count) |=> (o_prog_out_fll == {1'b0,$past(o_prog_out_fll[7:1])}) ;
	endproperty

Waveform :

assertion incr — Postimages

Am i doing any mistake ?

[ben2]

In reply to rkg_:
You have the proper tools to evaluate the correctness of your assertions.
The concepts look good, but you understand your requirements.
Ben

[rupeshblr]

In reply to ben@SystemVerilog.us:

I have proper tool (cadence ).

My only concern is why its triggering the property where antecedent is not meeting criteria.

[ben2]

In reply to rkg_:

I don’t know if those solid values are Xs for monclk_count at sampling times, but if Xs it should not trigger.
For things like that, you can add debugging signals. For example

  event e_p, e_m;
always @(negedge  refclk_sig_d1)  begin 
	if(monclk_count < i_count)  -> e_m; 
 	if(monclk_count >= i_count) -> e_p; 

Offhand, things look OK, I seriously doubt that the vendor is making such a silly mistake.

[rupeshblr]

In reply to ben@SystemVerilog.us:

In reply to rkg_:
So your increment / decrement for a 4-bit “a” is

bit[3:0] a;
a = {1'b1, a[3:1]}; // increment, 1'b1 concat with a right shift by 1
a = {a[2:0], 1'b0}; // deccrement, shift left by 1 with concat of 0  
property out_bits_incr_prpty;
@(negedge refclk_output) disable iff(!reset)
(monclk_count <  count) && Enable|=> 
out_bits == {1'b1, $past(out_bits[3:1])};
// was: (out_bits > ($past(out_bits, 1) );
endproperty 
/* check the out bits decrement */
property out_bits_decr_prpty;
@(negedge refclk_output) disable iff(!en_reset)
(negclk_count > count) && Enable|=> 
out_bits == {$past(out_bits[2:0]), 1'b0)};  //before
out_bits == {$past(1'b0,out_bits[3:1])};   // modified 
// was: (out_bits < ($past(out_bits, 1));
endproperty

Hi Ben,
it will work only on below sequence only:
for DECR :- 10000000 → 01000000 → 00100000 … so on
for incr :- 10000000 → 11000000 → 11100000

This assertion will not work on below
For DECR:- 11000000 → 10100000 → 10010000 → 10001000 …etc
for incr :- 10100000 → 10110000 → 10111000

Any suggestion

[ben2]

In reply to rkg_:

I may have misunderstood your requirements, but the shift left/right was what I interpreted from your posts.
You need to clearly define the requirements and implement the code accordingly.
You have the right concepts.
If the increment /decrement is ccmplex use a function call from the sequence_match_item e. G,

 
function bit dec(logic[your _range]:
  ... // your decrement algorithm 
 return value; //
endfunction 

property out_bits_decr_prpty;
  @(negedge refclk_output) disable iff(!en_reset)
  bit v;
  (negclk_count > count) && Enable|=> 
       (1, v=dec(out_bits)) ##0 v;
       //mout_bits == {$past(out_bits[2:0]), 1'b0)};  //before
       //out_bits == {$past(1'b0,out_bits[3:1])};   // modified 
  // was: (out_bits < ($past(out_bits, 1));
endproperty

[rupeshblr]

In reply to ben@SystemVerilog.us:

Hi Ben

Here my intention is sar_mask should retain the value at every every function call . will it work ?

fll_out_bits changes at every negedge sampled_monclk and my function should get called at every negedge sampled_monclk and same time assertion should get trigger

function bit incr_decr (logic [7:0]fll_out_bits , logic [7:0]mon_clk_count, logic [7:0]counts);
 bit[7:0] sar_mask = 8'b10000000;
//INCR
begin
if (mon_clk_count < counts)
begin 
  fll_out_bits = fll_out_bits | (sar_mask >>1);
 sar_mask = sar_mask >> 1'b1;
end
//DECR
else if (mon_clk_counts >= counts)
begin
 fll_out_bits = (fll_out_bits & !(sar_mask)) | (sar_mask >> 1)
 sar_mask = sar_mask >> 1'b1;
end
return fll_out_bits ;
end
endfunction 


property out_bits_decr_prpty;
  bit v;
  @(negedge  sampled_monclk) disable iff(!en_fll)
  
  1'b1 |=> (1, v=incr_decr(fll_out_bits ,monclk_count, i_count)) ##0 v;
endproperty

Error :
Unexpected identifier ‘sar_mask’ after completed expression

[rupeshblr]

In reply to rkg_:

And below is the algorithm for property but not sure how to implement this .
Algorithm :

1. calculate the index of fll_out_bits where 1’b1 is present (eg. if fll_out_bits 10100000 (big endian )then index should be 5 in this case)
2. for incr : (index-1 = 5-1 = 4) so position 4 should be 1 and rest other position value should be same like previous ( e.g 10110000)
3. for decr : if input is 10100000 (index -1 = 5-1 = 4) so position 4 should be 1 and (index) position 5 will be 0 and rest should be same e.g(10010000)

I hope , I am able to explain the algorithm.

if above code (i have mixed incr and decr) looks good then i don’t need to write code for above algorithm but if not work i have to implement this .

Could you please help

[ben2]

In reply to rkg_:
Perhaps someone else can help you. You need to experiment with the function using testbench and randomized numbers, perhaps single-step it if needed.
Ben

[rupeshblr]

In reply to ben@SystemVerilog.us:

Hi,

function bit[7:0] incr (logic [7:0]fll_out_bits ,logic [7:0] sar_mask, logic [8:0]mon_clk_count, logic [8:0]counts);
//INCR
begin
  $display ("time %t ,INCR: , fll_out_bits= %b , mon_clk_count = %d, counts= %d, sar_mask = %d ", $time, fll_out_bits, mon_clk_count, counts, sar_mask); 
  fll_out_bits = fll_out_bits | (sar_mask >>1);
  $display ("time %t ,INCR: , fll_out_bits= %b , " , $time, fll_out_bits ); 
 
return fll_out_bits ;
end
endfunction 
 
function bit[7:0] decr (logic [7:0]fll_out_bits ,logic [7:0] sar_mask, logic [8:0]mon_clk_count, logic [8:0]counts);
begin
  $display ("time %t ,DECR: , fll_out_bits= %b , mon_clk_count = %d, counts= %d, sar_mask = %d ", $time, fll_out_bits, mon_clk_count, counts, sar_mask); 
 
 fll_out_bits = (fll_out_bits & !(sar_mask)) | (sar_mask >> 1);
 $display ("time %t ,DECR: , fll_out_bits= %b , " , $time, fll_out_bits ); 
 
return fll_out_bits ;
end
endfunction 
 
property out_bits_incr_prpty;
  bit v;
 @(posedge monclk_output) disable iff (!i_en_fll)
 $rose (sampled_monclk)  |->  ((monclk_count < i_count), v=incr(o_prog_out_fll, sar_mask ,monclk_count, i_count) , $display ( "time %d FUNC VALUE value of incr =%d", $time, v)) ;
endproperty

property out_bits_decr_prpty;
  bit v;
 
@(posedge monclk_output) disable iff (!i_en_fll)
 $rose (sampled_monclk)  |->  ((monclk_count >= i_count), v=decr(o_prog_out_fll, sar_mask ,monclk_count, i_count) , $display ( "time = %d,FUNC VALUE value of decr =%d", $time,v)) ;
endproperty

function is being called 1st time at 1417 (which is posedge of sampled monclk) but i am getting message from inside function at 0 time onwards. and why its printing INCR and DECR both at the same time from both the function since i am calling function at different condition.

time =                 1417,FUNC VALUE value of decr =0

My intention function should get called only posedage of sampled_output and when sampled monclk goes 0

output :

time             0.000 ns ,INCR: , fll_out_bits= 10010000 , mon_clk_count =   0, counts= 256, sar_mask = 128 
time             0.000 ns ,INCR: , fll_out_bits= 11010000 , 
time             0.000 ns ,DECR: , fll_out_bits= 10010000 , mon_clk_count =   0, counts= 256, sar_mask = 128 
time             0.000 ns ,DECR: , fll_out_bits= 01000000 , 
time             2.000 ns ,INCR: , fll_out_bits= 10010000 , mon_clk_count =   0, counts= 256, sar_mask = 128 
time             2.000 ns ,INCR: , fll_out_bits= 11010000 , 
time            32.000 ns ,DECR: , fll_out_bits= 10000000 , mon_clk_count =   0, counts= 256, sar_mask = 128 
time            32.000 ns ,DECR: , fll_out_bits= 01000000 , 
time            32.000 ns ,INCR: , fll_out_bits= 10000000 , mon_clk_count =   0, counts= 256, sar_mask = 128 
time            32.000 ns ,INCR: , fll_out_bits= 11000000 , 
time           134.000 ns ,DECR: , fll_out_bits= 10000000 , mon_clk_count =   1, counts= 256, sar_mask = 128 
time           134.000 ns ,DECR: , fll_out_bits= 01000000 , 
time           134.000 ns ,INCR: , fll_out_bits= 10000000 , mon_clk_count =   1, counts= 256, sar_mask = 128 
time           134.000 ns ,INCR: , fll_out_bits= 11000000 , 
time           137.000 ns ,DECR: , fll_out_bits= 10000000 , mon_clk_count =   2, counts= 256, sar_mask = 128 
time           137.000 ns ,DECR: , fll_out_bits= 01000000 , 
time           137.000 ns ,INCR: , fll_out_bits= 10000000 , mon_clk_count =   2, counts= 256, sar_mask = 128 
time           137.000 ns ,INCR: , fll_out_bits= 11000000 , 
time           140.000 ns ,DECR: , fll_out_bits= 10000000 , mon_clk_count =   3, counts= 256, sar_mask = 128 

BUT FUNCTION is being called at 1417

time =                 1417,FUNC VALUE value of decr =0
 $rose (sampled_monclk)  |->  ((monclk_count < i_count), v=incr(o_prog_out_fll, sar_mask ,monclk_count, i_count) , $display ( "time %d FUNC VALUE value of incr =%d", $time, v)) ;
                                             |
xmsim: *E,ASRTST  (time 1416500 PS) Assertion top.dut.u_assert_ip.AP_OUT_BITS_INCR_PRPTY has failed (1 cycles, starting 1416500 PS)
time          1417.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   0, counts= 256, sar_mask =  64 
time          1417.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          1417.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   0, counts= 256, sar_mask =  64 
time          1417.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          1417.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   0, counts= 256, sar_mask =  64 
time          1417.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          1417.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   0, counts= 256, sar_mask =  64 
time          1417.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          1422.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   0, counts= 256, sar_mask =  64 
time          1422.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          2697.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   1, counts= 256, sar_mask =  64 
time          2697.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          2697.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   1, counts= 256, sar_mask =  64 
time          2697.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          2701.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   2, counts= 256, sar_mask =  64 
time          2701.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          2701.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   2, counts= 256, sar_mask =  64 
time          2701.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          2705.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   3, counts= 256, sar_mask =  64 
time          2705.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          2705.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   3, counts= 256, sar_mask =  64 
time          2705.000 ns ,INCR: , fll_out_bits= 01100000 , 
time          2709.000 ns ,DECR: , fll_out_bits= 01000000 , mon_clk_count =   4, counts= 256, sar_mask =  64 
time          2709.000 ns ,DECR: , fll_out_bits= 00100000 , 
time          2709.000 ns ,INCR: , fll_out_bits= 01000000 , mon_clk_count =   4, counts= 256, sar_mask =  64 
time          2709.000 ns ,INCR: , fll_out_bits= 01100000 , 

Could anyone see any thinf wrong ?

[ben2]

In reply to rkg_:
I don’t see anything wrong, but I am seen what you want me to see; maybe there are other places where you call the function. If the antecedent fails, the consequent is not triggered. The true action block may be triggered though because a vacuously true condition is true.

EDA Playground

module m; 
  bit a=0, clk; 
  
  initial forever #10 clk = !clk;
  ap: assert property(@(posedge clk) a |-> 1) $display("%t Test vacuous true a=", $realtime, $sampled(a));  
   
  initial begin
    repeat (6) begin   
      @(posedge clk);
      $display("%t a= ", $realtime, a);
      a<= !a;     
    end ;     
    $finish;
  end
endmodule
//--------
# KERNEL:                   10 a= 0
# KERNEL:                   10 Test vacuous true a=0
# KERNEL:                   30 a= 1
# KERNEL:                   30 Test vacuous true a=1
# KERNEL:                   50 a= 0
...

Things you can do:

• Use the debugging tool of the simulator. Some tools have a thread viewer that traces what is going on.
• Write a simple model with a function call and see how your simulator handles that.
• Check your action block

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
2. Free books: Component Design by Example https://rb.gy/9tcbhl
   Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3. Papers:

• Understanding the SVA Engine,
  Verification Horizons
• SVA Alternative for Complex Assertions
  https://verificationacademy.com/news/verification-horizons-march-2018-issue
• SVA in a UVM Class-based Environment
  https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

[ben2]

In reply to ben@SystemVerilog.us:

Check with your tool vendor for switches you can set for the assertion action block. Most vendors provide switches to enable you to set the assertion action for concurrent assertion starts, failures, passes, and antecedent matches.
In your case, it looks like a vacuous pass triggers the action block, but you can turn that option off.

Ben

[rupeshblr]

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for suggestion .

Could anyone tell, what is the syntax error here ? I am getting the compilation error.

property out_bits_incr_prpty;
  bit[7:0] v;
//  @(posedge monclk_output) disable iff(!i_en_fll)
@(posedge sampled_monclk) disable iff (!i_en_fll)
  ##1  1   |->   if (monclk_count < i_count)
   v=incr(o_prog_out_fll, sar_mask ,monclk_count, i_count) ##0 v 
  else
   v=decr(o_prog_out_fll, sar_mask ,monclk_count, i_count)  ##0 v ;
endproperty