Assertion causes sim crash

I have setup an assertion and cover property like below, and the sim will crash due to running out of memory:

//-------------------------------------------------------
property desc_set_seq_push_eng_engOut_pull_tag;
@(posedge mem_clk) disable iff (mem_rst)
dec_push_desc_fifo_vld [= 3] |-> ##[1:500] dec_engine_core_desc_fifo_vld [= 2] ##[1:500]
dec_engine_output_desc_fifo_vld ##[1:500] dec_pull_desc_fifo_vld [= 5] ##[1:500] tag_fifo_vld;
endproperty

// assert property
chk_desc_seq: assert property(desc_set_seq_push_eng_engOut_pull_tag) else
`uvm_error($psprintf(“%m”), “Descriptor setup sequence failed”)

// cover peoperty
cov_desc_seq: cover property(desc_set_seq_push_eng_engOut_pull_tag);
//-------------------------------------------------------

Any ideas why the statements above are bad?

Thanks,
Richard

In reply to hctseng:
Your assertion has the following as an antecedent:
dec_push_desc_fifo_vld [= 3] |-> …
Note that

 
b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]

b[=2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]

  1. That means that at every clocking event you’ll have a successful attempt, and thus a new valid thread whenever dec_push_desc_fifo_vld == 0. Thus, there are way-way too many unnecessary threads and thus you will run out of memory. The solution, start the assertion when dec_push_desc_fifo_vld is true rather than falses or true.
  2. Also, the b[=n] causes a !b[*0:] at the end of the nth time, and this assertion can never succeed since all threads of the antecedent must be tested for a pass. However, the b[->1] is equivalent to: !b[*0:] ##1 b. POINT: Use the goto operator

,


property desc_set_seq_push_eng_engOut_pull_tag;
  @(posedge mem_clk) disable iff (mem_rst)
  dec_push_desc_fifo_vld ##1 dec_push_desc_fifo_vld [-> 2] |-> // <-------
       ##[1:500] dec_engine_core_desc_fifo_vld [= 2] 
       ##[1:500] dec_engine_output_desc_fifo_vld 
       ##[1:500] dec_pull_desc_fifo_vld [= 5] 
       ##[1:500] tag_fifo_vld;
endproperty
 

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


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thank you very much Ben. I read the SV LRM, and I still could not quite fully understand the difference between b[=n] and b[->n]. Could you please make an legal example both terms?

Richard

In reply to hctseng:

I am giving you 3 pages from my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448 that clearly explains these concepts with examples. I tend to use lots of examples in my book. Hopefully, that will clarify things for you.

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


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thank you Ben. This helps a lot. Appreciate your help!!

Just wondering what is the big difference between your 3rd edition and the 4th edition book? I have a coworker owns the 3rd edition, but I’m not sure if I should purchase the 4th edition for myself.

Richard

In reply to hctseng:
The 4th edition has

  1. Some clarifications and more examples
  2. Significant update to the SystemVerilog checker
  3. A new chapter on VERIFYING ASSERTIONS (using constrained-random tests, but not UVM)
    Some explanation on constraints. I covered a lot assertion verification examples in my posts
  4. A few more examples on the dictionary chapter.
  5. A new chapter on 1800’18 PREVIEW, but I covered a lot of that in my posts

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


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Cool thanks. I’ll go ahead to order a copy.

Richard