# Clocking event in Concurrent Assertions

**URL:** <https://verificationacademy.com/forums/t/clocking-event-in-concurrent-assertions/51725>\
**Category:** SystemVerilog\
**Tags:** Clocking-event-sva, SVA, SystemVerilog, assertion\
**Created:** [September 5, 2026, 3:55pm UTC](https://verificationacademy.com/forums/t/clocking-event-in-concurrent-assertions/51725 "2026-09-05T15:55:41Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![AGS91](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/a/f475e1/32.png) [@AGS91](https://verificationacademy.com/forums/u/AGS91)\
**Post date:** [September 5, 2026, 3:55pm UTC](https://verificationacademy.com/forums/t/clocking-event-in-concurrent-assertions/51725/1 "2026-09-05T15:55:41Z")

</div>

Hi All,

Generally, the clocking event of concurrent assertion is actually a clock signal

```verilog
property sva1;
 @(posedge clk) <property_expression1>;
endproperty

```

In rare cases where I want to check for **FSM state transition** one could use `ps_state` as the clocking event **which would trigger**  **sva2 only when state changes**.

```verilog
property sva2;
 @(ps_state) <property_expression2>;
endproperty

```

From **LRM perspective the above code is perfectly legal**

On comparing the above two properties my understanding is that using `@(posedge clk)` the property would execute numerous times in a simulation **even when there is no transition** in `ps_state`.

Such unnecessary attempts are avoided in `sva2` which I feel could be possibly better from a tool perspective

I was specifically looking to hear from people with hands-on experience using formal tools whether the `sva2` is legal in a formal testbench ?

Are there any disadvantages with using `ps_state` as a clocking event of a concurrent assertion ?

Regards,

AGS

---

<div class="post-metadata">

**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:** [September 8, 2026, 8:39pm UTC](https://verificationacademy.com/forums/t/clocking-event-in-concurrent-assertions/51725/2 "2026-09-08T20:39:21Z")

</div>

The problem is when your \<_property\_expression_\> contains a reference to `ps_state`. Because of sampling semantics, it will have the old state, not the new state.

You could put your assertion into an implication

```
$changed(ps_state) |-> <property_expression> ;

```

---

<div class="post-metadata">

**Author:** ![AGS91](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/a/f475e1/32.png) [@AGS91](https://verificationacademy.com/forums/u/AGS91)\
**Post date:** [September 9, 2026, 5:15am UTC](https://verificationacademy.com/forums/t/clocking-event-in-concurrent-assertions/51725/3 "2026-09-09T05:15:01Z")

</div>

Hi Dave,

Yes, when using `ps_state` as clocking event I call a subroutine to return the new `ps_state` and use it as part of `property_expression`

From SV LRM perspective above logic works as per intention.

I was curious whether it would work / considered legal for formal tb as well