# Concurrent Assertion :: After ' a ' is True . ' b ' Should Never be True till end of Simulation **URL:** \ **Category:** SystemVerilog\ **Tags:** SystemVerilog, Concurrent-Assertion-After--a--is-True---b--Should-Never-be-True-till-end-of-Simulation\ **Created:** [February 10, 2022, 6:06am UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046 "2022-02-10T06:06:31Z")\ **Posts on this page:** 6\ **Page:** 1
**Author:** ![hisingh](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/h/97f17d/32.png) [@hisingh](https://verificationacademy.com/forums/u/hisingh)\ **Post date:** [February 10, 2022, 6:06am UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/1 "2022-02-10T06:06:31Z")
Hi all , I coded the following :: ```verilog bit clk , a , b ; property ab ; @( posedge clk ) a |=> always !b ; endproperty initial forever #5 clk = ! clk ; initial begin // ' b ' is NEVER True after ' a ' is True at T : 5 // #4 ; a = 1 ; #10 ; a = 0 ; #10 ; a = 0 ; #50 ; #5 ; $finish() ; end a_property : assert property ( ab ) else $display(" TIME : %0t AB FAIL " , $time ) ; c_property : cover property ( ab ) $display(" TIME : %0t AB PASS " , $time ) ; ``` My expectation was that the assertion would pass as there was No b , however I observe No O/P i.e Incomplete Assertion . Any suggestions ? ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [February 10, 2022, 9:24pm UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/2 "2022-02-10T21:24:25Z")
_In reply to [hisingh](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046):_ If the **strong** or **weak** operator is omitted, then the evaluation of the sequence\_expr (interpreted as a property) _depends on the assertion statement in which it is used._ If the assertion statement is **assert property** or **assume property** , then the _sequence\_expr is evaluated as **weak** (sequence\_expr)_. Otherwise, the sequence\_expr is evaluated as **strong** (sequence\_expr). Thus, ```verilog a |=> always strong(!b) ``` ---
**Author:** ![hisingh](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/h/97f17d/32.png) [@hisingh](https://verificationacademy.com/forums/u/hisingh)\ **Post date:** [February 12, 2022, 7:09am UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/3 "2022-02-12T07:09:40Z")
_In reply to [ben@SystemVerilog.us](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/2):_ Ben , I tried using ```verilog a |=> always strong(!b) ``` However I still don’t see the assertion Pass display . ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [February 12, 2022, 8:19pm UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/4 "2022-02-12T20:19:29Z")
_In reply to [hisingh](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/3):_ Ran the assertion below. Because there no failure, the error count is zero. At the end of simulation the tool reports the Active count. It canot report the pass action block because the assertion is not finished, and is in the active state. ```verilog property ab ; @( posedge clk ) a |=> always !b; endproperty ap_always : assert property (@(posedge clk) a |=> s_always[1:10000] !b) else $display(" TIME : %0t AB FAIL " , $time ); ac_always : cover property (ab); ``` ---
**Author:** ![hisingh](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/h/97f17d/32.png) [@hisingh](https://verificationacademy.com/forums/u/hisingh)\ **Post date:** [February 13, 2022, 9:36am UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/5 "2022-02-13T09:36:30Z")
_In reply to [ben@SystemVerilog.us](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/4):_ Got it . So I would have to use an appropriate unbounded delay ---
**Author:** ![dave\_59](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/dave_59/32/4499_2.png) [@dave\_59](https://verificationacademy.com/forums/u/dave_59)\ **Post date:** [February 14, 2022, 8:37pm UTC](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/6 "2022-02-14T20:37:06Z")
_In reply to [hisingh](https://verificationacademy.com/forums/t/concurrent-assertion-after-a-is-true-b-should-never-be-true-till-end-of-simulation/40046/5):_ There are a couple of issues in play here. The main issue is that dynamic simulation cannot consistently prove that a safety property like **always** or a liveness property like **eventually** will definitively pass or fail, only static formal analysis can do that. For a bounded **strong** sequence, a dynamic simulation can trigger a failure if the sequence does not reach its endpoint by the end of simulation. But all you can say for an unbounded sequence is that it has been started and still active, but it can never reach an endpoint. How this gets reported is tool specific. This Mentor/Siemens EDA sponsored public forum is not for discussing tool specific usage or issues. Please read your tool’s user manual or contact your tool vendor directly for support.