SVA to catch a signal assertion during ACK phase

SystemVerilog
,
1

Hello,
I’m trying to write a SVA for the following scenario for a serial protocol.

  1. detect payload sequence: 010000
  2. detect intr assertion on [20:24] clock cycle (after the sequence in #1 above)
  3. if(intr) asserted, check for intr deassert in the following [1:3] clk cycles.
property intr_during_ack;
	@(negedge vclk) 
	 $fell(payload) |=> payload |=> !payload [*4] ##[20:24] $stable(intr) ##[1:3] $rose(intr) ##[10:13] payload;
endproperty
intr_during_ack_assert: assert property (intr_during_ack) $display("intr_during_ack: %0t ",$time);

The issue I’m seeing is, the assert above fails when $stable(intr) is not true.
What I want to achieve is, when $stable(intr) is not true, it should progress and check if $rose(intr) occurred.
Could you please help.

2

Why the $stable(intr)? The opposite of $stable is $changed.
Is this what you want?


/* 1. detect payload sequence: 010000
2. detect intr assertion on [20:24] clock cycle (after the sequence in #1 above)
3. if(intr) asserted, check for intr deassert in the following [1:3] clk cycles.*/

property intr_during_ack;
	@(negedge vclk) 
	 $rose(payload) ##1 !payload[*4] // detect payload sequence: 010000
              |->  ##[20:24] intr  // detect intr assertion on [20:24] clock cycle
                   ##[1:3] $fell(intr); // ntr deassert in the following [1:3] clk
// Why the "if(intr) asserted" since you want an intr after the 20:24? 
// Why the  $stable(intr)?? you did not mention that in your requirement. 
// AVOID multiple antecedents, a general guidelines. (e.g., a |=> b |=> )
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

Avoid multiple antecedents is a great input! thank you!
Why the $stable(intr)? The opposite of $stable is $changed. Is this what you want?
I’m trying to write this assert for the scenario where the packet is 38 vclk cycles long. intr can assert anytime during these 38 cycles.
The assert should capture only the packets where intr asserts between 20-24 cycles of vclk and clear in the following 3clks.
I want the assert to be inactive for the rest of the packets.

The property I wrote was asserting for all the packets, if I use $stable it asserts only for those packets where intr is not stable. But $stable led to other issues.

The property you gave me works perfectly for the packets where I’m expecting this behavior, however reports error for the rest of the packets. How can I disable the property for the packets where intr is stable? Could you please help.
Thank you again!

4

In reply to mannat:
DO you have access to a signal that identifies the start and end of a packet?
can you generate that signal? If you can, the solution is easy, add a pkt_on signal to enable the assertion.


// I want the assert to be inactive for the rest of the packets.
bit pkt_on; // generated by supporting logic
always @(posedge clk) 
  if(...) pkt_on<=1'b1; 

property intr_during_ack;
	@(negedge vclk) 
	 $rose(payload) ##1 pkt_on && !payload[*4] // detect payload sequence: 010000
              |->  ##[20:24] intr  // detect intr assertion on [20:24] clock cycle
                   ##[1:3] $fell(intr); // intr deassert in the following [1:3] clk
ap_intr_during_ack: assert property(intr_during_ack) pkt_on=1'b0;  // action block to reset 
                          else pkt_on=1'b0;  // action block to reset, pass or fail

Ben SystemVerilog.us