Checking sequences directly in SVA or is it better to use auxillary code?

SystemVerilog
, ,
1

If I want to check in simulation that a signal A is always followed by B what is the best choice. This is a randomised bench where the time between A and B is allowed to scale to mimic traffic elsewhere. Is it possible to create an assertion directly in RTL that can catch this?

assert @(posedge clk) A |-> ##[1:$] B;

I understand this will be weak in simulation since we cannot prove that for infinite lengths that B occurs.

Would it be better to create helper code and check that when B occurs, A had already previously occured?

2

In reply to cwcar:


// one or more A is satisfied with a single B
A |-> stong(##[1:$] B);
A |-> strong(B[->1]; 

// Every A is satisfied by its own B 
// Thus A....A ..  B...B
// See my paper on support logic in my signature.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to cwcar:

You can make you assertion strong with

assert property (@(posedge clk) A |-> strong (##[1:$] B) );

And this fails if B does not occur by the end of simulation.

Usually better to write

assert property (@(posedge clk) $rose(A) |-> strong (##[1:$] $rose(B)) );

But you need to have clearer requirements about A and B. What happens if they occur together? When is A allowed to be deasserted. You may have to break these up into seperate assertions