I would like to write the following in SVA (SystemVerilog Assertion) format.
signal a should never be 2 until it attains the value 1
How can we do that?
Asked
Active
Viewed 149 times
2
Shashank V M
- 2,279
- 13
- 47
vineeshvs
- 155
- 2
- 8
-
4Sorry, I cant help it, this triggers immediately: *"Four shalt thou not count, neither count thou two, excepting that thou then proceed to three."* – Oldfart Sep 22 '19 at 07:42
-
1... *Five is right out!* – Dave Tweed Sep 22 '19 at 13:16
-
1For the clueless: http://www.montypython.net/scripts/HG-handgrenade.php – dave_59 Sep 25 '19 at 10:37
2 Answers
5
property p;
@(posedge clk) (A != 2) until (A == 1);
endproperty
assert property (p);
dave_59
- 7,557
- 1
- 14
- 26
-
Another related question: I want to generate the counter-example for this property. When I try `assert property (not(p))` for that purpose, it says syntax error. Is there an issue with using `not` with `until`? – vineeshvs Sep 25 '19 at 14:04
-
Another doubt: How can I write the following in SVA? `not(a until b)` without using `until` or `s_until`. – vineeshvs Sep 25 '19 at 15:14
-
1
-
Okay. What would be the recommended way if we want to negate such a property? The objective here is to get the counterexample corresponding to the property (hence the negation). – vineeshvs Sep 26 '19 at 06:43
-
4
2
Such a condition requires a state machine, and cannot be done with simple assertions alone. You need to build the state machine, and then make an assertion that certain transitions cannot occur within that state machine.
Dave Tweed
- 168,369
- 17
- 228
- 393
-
Do you mean state machine in the Verilog design or state machine in the SVA property (is that possible)? – vineeshvs Sep 23 '19 at 06:13
-
2