After first "pass" assertion does not fire unless a failure occurs

SystemVerilog
1

Hi all, interesting problem here maybe you can help me figure it out.

I’ve got a simple connectivity check assertion:
(I’m running simulations with this on Cadence Incisive, not sure that it matters)


property connectivity_check(dsbl, clk, src, dest);
 @ (posedge clk) disable iff(dsbl)
  !$stable(src) |-> (src == dest);
endproperty

The assertion does pass when there are no failures found. The assertion itself according to the simulator seems to always be in one of two states:

“$finished”
“$inactive”

At the start of the simulation, the assertion begins in the “$inactive” state. The first time the assertion check passes, it enters the “$finished” state. In other assertion checks that I have seen, it is then supposed to return to “$inactive” shortly thereafter.

That’s not the case here. When my assertion above passes, it gets stuck in the “$finished” state. As a result, during every other part in the test that wiggles the assertion, it is still “$finished” and doesn’t increment the # of times the assertion fires. Thus in the end of test assertion reports, the simulator claims the assertion fired only once even if it was checking 1000 times.

I know the assertion isn’t simply dead because if I inject an error on the src, I can get the assertion to fail. This causes the assertion to return to the “$inactive” state. The next time the assertion hits a check and passes, it goes back to the “$finished” state and gets stuck again.

I’m honestly not sure if this is an error on my part or a simulator error. Hopefully somebody can give me a clue, thanks!

2

In reply to silverace99:

You will need to check your simulator’s documentation on how it reports coverage of assertions.

An implication can pass vacuously (antecedent/LHS is false), or non-vacuously (both antecedent and consequent/RHS are true). Typically a tool considers a implication property covered once it has passed non-vacuously .

3

In reply to dave_59:
What Dave wrote is correct. I am providing for you more infomation about the assertion states from my SVA Handbook 4th Edition, 2016.

Your specific assertion !$stable(src) |-> (src == dest); is checked at every cycle and its lifetime is only at that cycle; Thus, its possible states are all in that one time step and include ATTEMPTED, PASS, FAILED, ACTIVE, INACTIVE. Its possible outcomes are SUCCESS, FAILURE, DISABLED, KILLED.

Since this is a 1 cycle assertion, it can never enter the ACTIVE state.

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

1 Like
4

In reply to silverace99:

Not the best forum to discuss this, but this is how the tool works by default. There is a switch to disable this behavior and have it fire in every cycle.

5

Thanks for the supplemental information everyone :)

In reply to Tudor Timi:

In reply to silverace99:
Not the best forum to discuss this, but this is how the tool works by default. There is a switch to disable this behavior and have it fire in every cycle.

You see that’s what I was wondering…but in the same environment there are other assertions of a similar nature that seem to be working the way I would expect.

I’m having some trouble getting posting access on the cadence forums but I will see if I can pose the question there now that I’m more sure it’s not a design issue on my part. Thanks!

6

In reply to silverace99:

Hi all, interesting problem here maybe you can help me figure it out.
I’ve got a simple connectivity check assertion:
(I’m running simulations with this on Cadence Incisive, not sure that it matters)


property connectivity_check(dsbl, clk, src, dest);
@ (posedge clk) disable iff(dsbl)
!$stable(src) |-> (src == dest);
endproperty

The assertion does pass when there are no failures found. The assertion itself according to the simulator seems to always be in one of two states:
“$finished”
“$inactive”
At the start of the simulation, the assertion begins in the “$inactive” state. The first time the assertion check passes, it enters the “$finished” state. In other assertion checks that I have seen, it is then supposed to return to “$inactive” shortly thereafter.
That’s not the case here. When my assertion above passes, it gets stuck in the “$finished” state. As a result, during every other part in the test that wiggles the assertion, it is still “$finished” and doesn’t increment the # of times the assertion fires. Thus in the end of test assertion reports, the simulator claims the assertion fired only once even if it was checking 1000 times.
I know the assertion isn’t simply dead because if I inject an error on the src, I can get the assertion to fail. This causes the assertion to return to the “$inactive” state. The next time the assertion hits a check and passes, it goes back to the “$finished” state and gets stuck again.
I’m honestly not sure if this is an error on my part or a simulator error. Hopefully somebody can give me a clue, thanks!

Hi Silverace99,

Have you got the solution to your problem as I am also facing the same problem?

Regards
Neeraj

7

In reply to Neeraj Dahiy:

When my assertion above passes, it gets stuck in the “$finished” state

I have no idea as to what you’re talking about. At every clocking event there is an attempt at the property and based on the evaluation of the the first term of the property the simulator determines the state for that thread. Each attempted thread and its consequential evaluation is TOTALLY INDEPENDENT from other threads.
Thus, to say that “when my assertion above passes, it gets stuck in the “$finished” state” makes no sense. To say that “After first “pass” assertion does not fire unless a failure occurs” seems to say that a new assertion is not evaluated unless the new evaluation fails. This is very contradictory - no evaluation unless new evaluation???

Again, SVA requires a new evaluation at every clocking event!!

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
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
8

In reply to silverace99:

Some simulators implement an optimization, where new assertion attempts aren’t triggered unless the relevant signals change. This isn’t LRM compliant, as you get fewer executions of the actions blocks, but it will catch all the fails. You’ll have to look in the docs for your tool.

9

In reply to Tudor Timi:

I believe that that is not the problem because others assertions are working fine. And also internal signal for active state of assertion is working fine. In right moment is active and deactivates also in right moment. Ckeckers are working for cases when is more than 1 clock checker(not stuck in finished), but for one clock checker it’s always on finished, never inactive even if internal signal for active state of assertion is showing that is inactive.