Handshake with two different clocks

SystemVerilog
, , , ,
1

Hi,

Write an assertion for the following scenario:

req asserts at negedge of clk1 and ack will occur after clk2 is generated (triggered by req). For ack to be asserted clk2 has to be toggling for a minimum of 4 clock cycles. Ack occurs at posedge of clk2.

Here is my solution and I see a vacuous pass, please help!

@(negedge clk1) $rose(req) ##1 @(posedge clk2) !ack[*4:$] ##1 ack;

Thanks

Edit: I see vacuous pass if I use implication(|->), but this assertion fails.

2

In reply to foxtrot:

Without an implication, the assertion fails on every negedge clk1 where req does not rise.

With an implication, you get a vacuous pass every time req rises but the sequence for ack does not succeed. That is probably what you want to happen. A non-vacuous pass is required for the assertion to be considered covered.

3

In reply to dave_59:

I have tried this as well, but it’s a vacuous pass even when ack rises after say 4 or 6 clk2 cycles.
How do I fix it?

@(negedge clk1) $rose(req) |-> @(posedge clk2) !ack[*4:$] ##1 ack;
4

In reply to foxtrot:

…but it’s a vacuous pass even when ack rises after say 4 or 6 clk2 cycles.

Vacuity occurs only if the antecedent $rose(req)==0.
Keep in mind that at every clocking event (i.e., the @(negedge clk1)) you have an attempt at the property, and if in the cycles af$ter the successful $rose(req) you have no more rose, then those attempts are vacuous. Maybe what you see are those vacuous threads.
However, the attempt with a successful $rose(req) can finish in one of the possible ways:
PASS, FAIL, INCOMPLETE (if at end of simulation ack never occurred).
Try the following


ap_reqack: assert property(@(negedge clk1) $rose(req) |-> 
          @(posedge clk2) !ack[*4:$] ##1 ack) $display("%t PASS", $realtime);
          else $display("%t FAIL", $realtime);

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:
5

In reply to ben@SystemVerilog.us:

In reply to foxtrot:
Vacuity occurs only if the antecedent $rose(req)==0.
Keep in mind that at every clocking event (i.e., the @(negedge clk1)) you have an attempt at the property, and if in the cycles af$ter the successful $rose(req) you have no more rose, then those attempts are vacuous. Maybe what you see are those vacuous threads.

Right, I have just one rising edge of req now. As I said earlier that solution did not work for me. It’s a vacuous pass even though req and ack are asserted at right time.

6

In reply to foxtrot:
It would really help to show a complete example showing the behavior you are seeing and describing what you would like to see instead.