hello everyone , i have two questions
what is the use of always in SVA? can i use always in concurrent assertion?
and the second question that i want to know the difference between
assume (s_eventually !req) and assume (s_eventually always !req);
thanks
Per 1800’2023:16.12.11 Always property
Weak always
always property_expr
A property always property_expr evaluates to true if, and only if, property_expr holds at every current or future clock tick.
Thus, if I write:
initial ap_once: assert property(@(posedge clk) req[->1]);
// From start of sim, check that req occurs, and do it once.
// But
initial ap_once: assert property(@(posedge clk) always
$rose(req) |-> ##[1:3] ack);
// Then at every clocking event the property ($rose(req) |-> ##[1:3] ack) is attempted.
// In 1800: implicit form:
implicit_always: assert property(p);
// Explicit form: (and equivalent)
initial explicit_always: assert property(always p);
Note: the always needs a leading clocking event.
// NOT OK, missing leading clocking event in the always
initial ap_req_pulse: assert property(always(@(posedge clk) req |=> !req));
// OK
initial ap_ack_pulse: assert property(@(posedge clk) always(ack |=> !ack));
```quote]
and the second question that i want to know the difference between
assume (s_eventually !req) and assume (s_eventually always !req);
[/quote]
1800: 16.12.13 Eventually property
1800 is confusing in its explanation, I agree.
https://www.perplexity.ai/search/explain-to-me-in-simple-terms-oDaVSDNiRqqR_DUQxjLvmw
did a good job:
Let's break down the differences between these SystemVerilog properties in simple terms:
## Property p2: s_eventually a
This property states that "a" will become true at some point and then stay true forever after.
- It's looking for a specific moment when "a" becomes true and remains true for all future clock ticks.
- Once "a" becomes true, it must never become false again for this property to hold.
- This is often used to check for conditions that, once met, should persist indefinitely.
## Property p3: s_eventually always a
This property is more flexible and states that "a" will be true infinitely often, but not necessarily continuously.
- It allows "a" to toggle between true and false over time.
- As long as "a" keeps becoming true at various points in the future, this property holds.
- For finite simulations, it checks if "a" is true at the very last clock tick (if there's at least one tick).
## Key Differences
**Persistence vs. Recurrence:**
- p2 requires "a" to become permanently true at some point.
- p3 only requires "a" to keep occurring as true, even if it becomes false in between.
**Flexibility:**
- p3 is more lenient, allowing "a" to fluctuate between true and false.
- p2 is stricter, demanding "a" to stabilize at true permanently.
**Finite Simulation Behavior:**
- In finite simulations, p3 focuses on the final clock tick.
- p2 still requires finding a point where "a" becomes and stays true.
These properties are useful for different verification scenarios. p2 is ideal for checking conditions that should stabilize, while p3 is better for recurring events or conditions that may toggle over time.
Citations:
[1] https://en.wikipedia.org/wiki/SystemVerilog
[2] https://insights.sigasi.com/tech/systemverilog.ebnf/
[3] https://www.design-reuse.com/articles/10907/using-systemverilog-assertions-in-rtl-code.html
[4] https://www.youtube.com/watch?v=4g2EmIptwNY
[5] https://www.accellera.org/images/resources/videos/systemverilog-design-tutorial-2015.pdf
[6] https://verificationacademy.com/forums/t/question-about-system-verilog-property-statement/38377
[7] https://www.systemverilog.io/verification/sva-basics/
[8] https://fpga.mit.edu/6205/_static/F23/documentation/1800-2017.pdf