[SVA] signal rise and stay stable -> how to write an assertion?

[Altera_Forum]

Hi All, 

 How can I write an assertion for a signal, which should rise within between 10 to 20 cycles and stay stable (HIGH) until the assertion will be disabled?  Thank you!

[Altera_Forum]

Best to write a counter to count the number of cycles signal is high, then assert the counter when the signal goes low. 

  Int cnt; Always @(posedge clk) begin If signal = 1'b0 cnt = 0; Else cnt = cnt + 1; End; Assert property ( @(posedge clk) $fell(sig) |-> (cnt >= 10 && cnt <= 20); )

[Altera_Forum]

Thank you Tricky for your response, but actually I wanted something else... Probably I did not explain myself well...  

 Actually, I wanted to assert/check the following scenario: 1) some event (let's name it event1) happens in TestBench  2) since this event, the signal should rise within between 10 to 20 cycles (if the signal rises after 11 cycles it's OK, if after 19 cycles it's also OK) 3) once the signal rises, it should stay stable (no changes in the signal) utill another event (let's name it event2) in the TestBench happens  Here is how I would check that the signal rises within 10 to 20 cycles after event1 happens (is this correct?): assert property ((posedge clk) (event1) $rose(signal) );  But how can I add the check what the signal is stable after it's rose and until the assertion is disabled (the check should be disabled when event2==1'b1)?  Could I write it in the following way?  assert property (@(posedge clk) $rose(event1) $rose(signal)); assert property (@(posedge clk) disable iff (event2==1'b1) $rose(signal) |-> $stable(signal));   How to write the above as a single assertion?  Thank you!

[Altera_Forum]

The more complicated your assertion, the harder your simulator has to work on every cycle to check an assertion. If you have a multi cycle assertion, you could have several overlapping assertions, which just adds load to your cpu. And if you ever get into formal verification, your prove time will just explode, if the assertion works at all. 

 Ideally you want assertions that are as simple as possible, ideally a |-> b. If necessary, you should write auxiliary code to achieve this, rather than putting the code in the assertion.  My example can easily be adapted to check for property 2), possibly as a sequence with your first line in your example code.  For 3), you could just write.   Assert property (@(posedge clk) $rose(event2) |=> $fell(signal) )   I am not a regular user of sva. Sva is also something very few FPGA engineers will be using. You might get better answers at the mentor verification academy forum.

[Altera_Forum]

"SVA is also something very few FPGA engineers will be using" - why? FPGA engineers still need to write TestBench... it should be much easier to write assertions than going to waveform each time and check behavior of all the signals there...

[Altera_Forum]

Most FPGA engineers are happy writing immediate assertions (using assert statement without a property), but SVA is another thing, and comes under the verification topic. Most FPGA engineers are happy writing a testbench that gives them a waveform and/or writing a self checking testbench. These can be done without SVA/PSL. As the syntax is nothing like standard RTL, it is outside the comfort zone for most, and is often the preserve of verification engineers, or people that work on ASICs. Im not sure about Modelsim, But I know that the cheapest versions of ActiveHDL and Xilinx Xsim do not support SVA (XSim just ignores SVA, ActiveHDL needs a more expensive licence).  

 And as I pointed out earlier, assertions can be a CPU killer when badly written.

[Altera_Forum]

Thanks for sharing your thoughts!  

 BTW, what's the difference between the# #1:3a and a[1:3] syntax?