5

Here is a spec: If signal a is asserted then it must be asserted till signal b is asserted and then it should de-assert on next clock edge. I'm reading through 16.9.9 of LRM (as well as http://www.testbench.in/AS_06_SEQUENCES.html) and the way I understood it, above mentioned spec can be written as

   property a2b_notA;
        @(posedge clk) ($rose (a) ##0 (a throughout b)) |=> (~a);
   endproperty
   a_a2b_notA: assert property (a2b_notA);

However this fails immediately on second clock edge after starting, and I can't figure out why.

AndresM
  • 1,293
  • 10
  • 19
wisemonkey
  • 571
  • 3
  • 15
  • 29

1 Answers1

16

You're correct in wanting to use the throughout operator for your assertion, but the code you wrote has some problems. Let's look at it piece by piece.

Whenever I write an assertion I pay attention to the natural language description of what I want to check. In your case, we know we want to trigger when a goes from 0 to 1. Everything that happens afterwards is the behavior that we want to check, so it should be on the right hand side of an implication operator:

$rose(a) |-> ... something ...

The way you wrote your assertion, it would only trigger checks if the throughout sequence also happened after rose(a). This would cause you to ignore bad behavior.

The next piece of the puzzle is "a must stay high until b is asserted". Here we'll use the throughout operator. The sequence "until b is asserted" is expressed as b [->1]. This is equivalent to !b [*] ##1 b. Our sequence should thus be a throughout b [->1].

The throughout sequence will end when b goes high. At this point we need to check that a goes low on the next cycle: ##1 !a. I've used logical negation here because I find it clearer than bitwise negation, but the result should be the same.

Putting it all together, the whole property should be:

$rose(a) |-> (a throughout b [->1]) ##1 !a;

I've used overlapping implication here because b could already be high when a goes high, in which case I'm assuming that a should go low immediately on the next cycle. If not, you can fiddle with the details yourself.

You can find a working example on EDAPlayground.

Tudor Timi
  • 7,453
  • 1
  • 24
  • 53
  • Thanks, I understood throughout wrongly. I thought just writing `throughout b` takes care of until `b` fails. And thanks for tip about deciding antecedent and precedent – wisemonkey Jun 08 '15 at 18:30
  • Thanks, @Tudor. The example works fine but I didn't get why you used "b[->1]" ? Since the goto repetition operator represents non-consecutive repetitions, so I understand b must be high for exactly 1 clock cycle when a is high. Can we do something like : `a[*0:$] |-> b [*0:$] ##1 !a` or `b within a` – sharvil111 Oct 02 '15 at 04:53
  • @sharvil111 The property you wrote doesn't do what the OP asked. Yours matches as many occurrences of `a` as possible and then it matches as many matches of `b`. When you're writing SVAs, I find it best to stay as close to the natural description as possible. `b [->1]` means "wait until `b` goes high". – Tudor Timi Oct 03 '15 at 16:50
  • Ok tried with a pseudo code, and got it. Thanks for clarification @Tudor. – sharvil111 Oct 05 '15 at 03:40
  • @TudorTimi can I use $rose(a)|-> (a throughtout ([1:$]~b ##1 b))? – Rottenengg Nov 17 '17 at 01:35
  • 1
    @Rottenengg `[1:$]~b` isn't legal syntax. Do you mean `~b [*1:$]`? If so (rewriting the property as `(a throughout (~b [*1:$] ##1 b))`), you're skipping a clock cycle where you don't check if `a` is high in the consequent. This isn't a big deal, due to the fact that the consequent (`$rose(a)`) already required `a` to be high in that particular cycle. You still need to end the property with `##1 !a`, otherwise you're not checking the requirement that "it should de-assert on next clock edge [after b goes high]". – Tudor Timi Nov 17 '17 at 07:55
  • @TudorTimi Yes. Can we use $rose(a) |-> s_eventually(b) ##1 !a? .Also, do we get a syntax error if we write like [*1:$] b i.e variable on right in consecutive or goto or non-consecutive operators? – Rottenengg Nov 17 '17 at 12:13
  • 1
    @Rottenengg `s_eventually(b)` doesn't say anything about `a`, that it stays high during that time. `[*1:$] b` would also work instead of `[->b]`, but the two aren't equivalent in all cases. The first one will match multiple times on a trace like `!b !b b b`, whereas the second for will only match on the first occurrence of `b` and stop there. Since the sequence is being used as a consequent in an implication property, the first time `[*1:$] b` matches, the entire property will also complete and no further evaluations will be started. – Tudor Timi Nov 17 '17 at 13:19
  • @TudorTimi Hey tudor, can you tell me like what conditions do we have to check for cache coherence? My plan is to perform protocol verification(MESI), and to check write serialization and write propagation. – Rottenengg Nov 21 '17 at 04:14
  • @Rottenengg Unfortunately, that's something I don't know how to answer and it's also out of the scope of this StackOverflow question. Try posting this question in a more specialized forum. – Tudor Timi Nov 21 '17 at 07:54
  • What's the difference between `$rose(a) |-> (a throughout b [->1]) ##1 !a;` and `$rose(a) |-> ((a throughout b [->1]) |=> !a);`? Will those assertions behave in the same way? – Ilan Biala Oct 21 '18 at 23:06
  • 1
    @IlanBiala In natural language, the first one says "after I see `a` rise, then I want to see `a` stay high until `b` goes high and see `a` go low immediately after. The second one says `after I see `a` rise, then if I see `a` staying high until `b` goes high, then I want to see `a` go low immediately after. The second form allows for `a` not staying high until `b`. If this is the case, the second implication vacuously passes, leading to the entire property passing. They are not equivalent. – Tudor Timi Oct 22 '18 at 08:02