2
\$\begingroup\$

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?

\$\endgroup\$
3
  • 4
    \$\begingroup\$ Sorry, I cant help it, this triggers immediately: "Four shalt thou not count, neither count thou two, excepting that thou then proceed to three." \$\endgroup\$
    – Oldfart
    Commented Sep 22, 2019 at 7:42
  • 1
    \$\begingroup\$ ... Five is right out! \$\endgroup\$
    – Dave Tweed
    Commented Sep 22, 2019 at 13:16
  • 1
    \$\begingroup\$ For the clueless: montypython.net/scripts/HG-handgrenade.php \$\endgroup\$
    – dave_59
    Commented Sep 25, 2019 at 10:37

2 Answers 2

5
\$\begingroup\$
property p;
  @(posedge clk) (A != 2) until (A == 1);
endproperty

assert property (p);
\$\endgroup\$
5
  • \$\begingroup\$ 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? \$\endgroup\$
    – vineeshvs
    Commented Sep 25, 2019 at 14:04
  • \$\begingroup\$ Another doubt: How can I write the following in SVA? not(a until b) without using until or s_until. \$\endgroup\$
    – vineeshvs
    Commented Sep 25, 2019 at 15:14
  • 1
    \$\begingroup\$ You cannot use parenthesis () with property expressions. \$\endgroup\$
    – dave_59
    Commented Sep 25, 2019 at 16:56
  • \$\begingroup\$ 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). \$\endgroup\$
    – vineeshvs
    Commented Sep 26, 2019 at 6:43
  • 4
    \$\begingroup\$ Assert property ( not p) \$\endgroup\$
    – dave_59
    Commented Sep 26, 2019 at 6:45
2
\$\begingroup\$

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.

\$\endgroup\$
2
  • \$\begingroup\$ Do you mean state machine in the Verilog design or state machine in the SVA property (is that possible)? \$\endgroup\$
    – vineeshvs
    Commented Sep 23, 2019 at 6:13
  • 2
    \$\begingroup\$ I just showed a very simple assertion. \$\endgroup\$
    – dave_59
    Commented Sep 25, 2019 at 9:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.