Check once signal occurency between two occurrence of another signal

SystemVerilog
,
1

I need help in writing an assertion to check that signal b occurs once between two pulse of signal “a”

I tried with

`assert_clk_reset_n (a |=> ( b [-> 1] ##[0:$] a ))

but my assertion doesn’t fail if two consecutive a pulse occurs without b

2

In reply to alexkidd84:

Hi,

Could you please post the complete assertion? Is that a macro?Is it sensitive to clock? Need some information to solve your query?

3

In reply to Anudeep J:

something was missing obviously:

assert property (@(posedge clk) disable iff (!reset_n) arg) (a |=> ( b [-> 1] ##[0:$] a ))
4

In reply to alexkidd84:

you need to specify consequent as strong sequence for it to fail if a asserts twice without b toggling in between.

assert property (@(posedge clk) disable iff (!reset_n) arg) (a |=> strong( b [-> 1] ##[0:$] a ))
5

In reply to rohitk:

mmmh nope, it doesn’t work yet

6

In reply to alexkidd84:

Try:

$rose(a) |=> strong(!a throughout b[->])

Please take below as constructive feedback:

For faster help with SVA related queries it helps a lot if you show full compiling code with input traces - as failures are trace dependent and it is sub-optimal to ask others to recreate the trace that you already have

Srini
www.verifworks.com

7

In reply to Srini @ CVCblr.com:

In reply to alexkidd84:
Try:
$rose(a) |=> strong(!a throughout b[->])
Please take below as constructive feedback:
For faster help with SVA related queries it helps a lot if you show full compiling code with input traces - as failures are trace dependent and it is sub-optimal to ask others to recreate the trace that you already have
Srini
www.verifworks.com

Thanks for the suggestion and the solution Srini!