Counting number of events on clock a, while clock o is forbidden

In reply to ben@SystemVerilog.us:

replacing the implication operator will make the program to expect a valid start on each clock cycle. thats what i think, and also i get 5/6 errors now, right from the beginning of the simulation.

In reply to Jadoon:


Use the implication operator after the rst
$rose(rst) |=> (a[->4]) intersect !o[*]) ##1 a[->1]

In reply to ben@SystemVerilog.us:

Seems I got the answer, using two assertions:


$rose(rst) |=> (a[->4] intersect !o[*]) ##1 a[->1] ##0 o==1'b1; 

$rose(rst) |=> o[->1] ##0 a==1'b1 ##1 a ~^ o[*1000]; 

First assertion forbids O for 4 events of A, followed by 5th A with O.
Second assertion checks for O and expects A that time. It is to catch the violation:
rst…a…a…a…a…o…a

It is followed by the XNOR pattern. Just one question, I tried this assertion with the range a ~^ o[*1:$] and it didn’t worked. Can you refer to some detailed reading material for the reason behind it?

thanks a ton.

In reply to Jadoon:


//in my previous code with the TB I have 
 // Let k==5
  ap_AsFrom: assert property(@(posedge clk)  		                            
      (($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |-> 
                                                    o==1'b1 ##1 a ~^ o[*1000]); 
And that worked. By now you got the needed cpncepts.  Test my code.


In reply to ben@SystemVerilog.us:

Now that I conclude my work, I thank this forum and especially Ben for the help. I got lots of ideas and cleared many concepts here. Bottom line is, in SVAs there are many way to do a single task.

A few of things that I learned during this whole process, in order of priority.

  1. No matter how clear we are, still we need to formally define the requirements.
  2. Divide and conquer rule works here, so we should divide the requirements into smaller parts and then proceed.
  3. There are important similarities/differences in various SVA operators, better to learn and use them carefully.
  4. Lastly but the most importantly, its always better to be in the company of people who know better and who care a lot. ;)

Ciao.