Assertions

In reply to Mechanic:
I’ll take these questions as a teaching moment opportunity by asking you questions to reflect on the answers. You may use 1800’2017 and possibly a simulator to arrive at the answers you’ll learn more by digging through the language than for me to just feeding you the answers. Don’t take this as mean, but rather a teaching moment.

  1. frame should go low within 2 to 5 clocks
    a)frame_|->##[2:5] $fell(frame_)
    b)s_eventually[2:5] $fell(frame_)
    Does both the properties(a ,b) are same ? if yes then that is the importance of S_eventually operator apart from strong property.
  1. what is the purpose of an antecedent?
  2. what is the definition of the s_eventually?
    Is it a sequence or a property?
  3. what is the meaning of the “s_”
  4. when is it desirable to define a consequent as “strong”?
  1. request must be true until grant is true (non overlapping)
    req until gnt; == req[*1:$]##1gnt; ?
  1. what is the definition of the “until”?
  1. request must be true until and including clock tick grant is true (overlapping)
    req until_with gnt; == req[*1:$]##0gnt;?

look it up.

If the above properties are correct then what is the importance of eventually,until,until_with operator.

SVA is rich in options