How to write the assertions

SystemVerilog
1

there is a requirement that b should be asserted after that and a is asserted and de-asserted ( there can be any number of clocks between b and a) and a can be asserted and de-asserted any number of times

please let me know how to write assertion for that.

2

In reply to srbeeram:
Rephrasing the requirements:

[list=1]
Following a new “b” signal “a” is asserted after any number of cycles. This is then followed by the signal “a” being deasserted after any number of cycles.


ap: assert property(
    @(posedge clk) $rose(b) |-> a[->1] ##1 !a[->1]);

Note: b[->1] is equivalent to:
!b[*0:$] ##1 b

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Thanks Ben for providing the answer. the answer you provide will give error if a is not asserted. but I dont need error if a is not asserted. please let me know how I can change the assertion for that.

4

In reply to srbeeram:
You need to qualify your requirements. you wrote:

there is a requirement that b should be asserted after that and a is asserted and de-asserted ( there can be any number of clocks between b and a) and a can be asserted and de-asserted any number of times

I interpret this to mean: Following a new “b” signal “a” is asserted after any number of cycles. This is then followed by the signal “a” being deasserted after any number of cycles.

ap: assert property(
    @(posedge clk) $rose(b) |-> a[->1] ##1 !a[->1]);  
ap_same: assert property(
    @(posedge clk) $rose(b) |-> !a[*0:$] ##1 a ##1 a[*0:$] ##1 !a);
ap_same2: assert property(
    @(posedge clk) $rose(b) |-> !a[*0:$] ##1 a[*1:$] ##1 !a);
// above assertions says 
// "b" should be asserted, after that "a" is asserted some time later and then 
// "a" is de-asserted in any number of cycles. 
// Note: b[->1] is equivalent to: !b[*0:$] ##1 b

You now say

the answer you provide will give error if a is not asserted. but I don’t need error if a is not asserted.

Your 2nd requirement contradicts the first that says after that and a is asserted and de-asserted. What is the relationship between “b” and “a”?
You can draw it, for example:


     |   |   |  ....   |   |   ....   |   |   |   |   |   |   |   |   |   | 
b    0   1   X  ...X   X   X   ...X   X   X   X   X   X   X   X   X   X   X    
a    X   0   0  ...0   1   1   ...1   0   X   X   X   X   X   X   X   X   X
property <---------------------------->

If you cannot express your requirements in English, you certainly cannot write an assertion for it.

Ben SystemVerilog.us