SVA Assertion

SystemVerilog
,
1

Hi,

clk
pc0
pc1
pc2
pc3
pop

I need to write an assertion to catch error scenario.
Condition : on clk edge any one of the pc0/1/2/3/ trigger to high for one clock cycle. After few cycles(currently,spec didn’t mention how many clocks) pop should be high for one clock cycle.
Suppose,if PC0 is high , In between PC0 high ----> pop high PC1/2/3 signals should go high.
if PC1 is high , In between PC1 high ----> pop high PC0/2/3 signals should go high.
This pc0/1/2/3 are triggered based on the read data match from ahb.

can someone help me how do I make it.
Please let me know if any info is still required.

-Regards,
-Raja.

2

In reply to sraja:

Can you write your description in the form:

If (this_condition_happens) then (this condition must happen)
If (this_condition_happens) then (this condition must not happen)

3

In reply to dave_59:

In reply to sraja:
Can you write your description in the form:

HI Dave,

  1. if (PC0 == 1) then after some clock cycles (pop == 1)
  2. PC1,PC2,PC3 signals shouldnot goto high in between condition 1.(i.e in between $rose(PC0) and $rose(pop).

Hope this is clear.

-Regards,
-Sravan.

4

In reply to sraja:
That is better. Originally you wrote that pop should go hight for one cycle. You did not specify what should happen if more than one of PC0…PC3 goes high at the same time. And you did not specify if PC0 could go high again before pop goes high. Here’s an assertion that should work for what you wrote:

  property grant_follows_request(req,gnt);
      @(posedge clk) $rose(req) |-> s_eventually !gnt ##1 gnt ##1 !gnt;
   endproperty
   property in_between(r0,r1,r2,r3,gnt);
      @(posedge clk) $rose(r0) |=> !r1&&!r2&&!r3 until gnt;
   endproperty 

   A1 :assert property ( grant_follows_request(pc0,pop) );
   A2 :assert property ( in_between(pc0,pc1,pc2,pc3,pop) );

You’ll need to repeat these assertions for PC1…PC3.

5

In reply to dave_59:

Yeah sure i will make it clear.
Thank you.Its working…