Basic doubt regarding SV assertion

SystemVerilog
,
1

Hi,

I am new to SVA and want to write one plain assertion with the requirement as follows:

There are 2 signals - req and ack.
Between two consecutive assertions of req, ack should be asserted only once.

Please help in writing this simple assertion.
Should i use throughout, first_match or, within operator?

I am confused.

Thanks,
Ashish

2

sequence s1
//syntax to detect 2 consicutive req signals
endsequence

sequence s2
//syntax to detect one ack signal
endsequence

property check;
@(posedge clk) $rose(req) → s2 within s1;
endproperty

assert property(check)
else
$error(“assert failed”)

//the above mentioned syntax could be one option.
//or

sequence s3
//syntax to detect first req followed by an ack and then again req
endsequence

property check1;
@(posedge clk) $rose(req) → s3;
endproperty

assert property(check1)
else
$error(“assert failed”);

//you can try this one also
//if I am wrong please feel free to correct me

Thanks,
Naresh