A feature where SystemVerilog really shines for hardware verification is its assertion language. Making it easy to specify complex requirements in a clear and easily understandable way, coupled with the fact that they can be used for both simulation and formal verification, means that *SVA*s are the complete package.

A question I got from a colleague a little while back was "How do I do overlapped implication in an *e* temporal expression? You know, like *SystemVerilog*'s '|->' operator.". He hit the nail on the head with that one; there is no such operator in *e*, but surely we can figure something out.

Let's start with the basics. Here is what an overlapped implication property looks like in *SystemVerilog*:

```
overlapped_implication: assert property (
@(posedge clk)
antecedent |-> consequent
);
```

Whenever the first condition is true (called the antecedent) then the second condition (called the consequent) must also be true.

Digging around in the *e* LRM I got the idea of using a combination of the* detach* operator, together with the *true match variable repeat* operator (which is fancy talk for ~[range]). Here's what I came up with:

```
<'
expect overlapped_implication is @antecedent => detach({@consequent; ~[1]});
'>
```

The way it works is that *detach* sort of spawns a parallel evaluation of the second TE. The second TE will evaluate to true whenever *@consequent* has happened once. Putting it all together would read: whenever *@antecedent* happens, make sure that *@consequent* already happened once. This is all fine and dandy on paper, but when doing a test run I was surprised to see the *SVA* firing without any error message from the *expect*. Continuing the simulation also caused the *expect* to trigger, but one clock cycle later. Strange?

Well not so strange after all. The gotcha here is that the '=>' operator includes an additional clock cycle between the execution of the left hand side and of the right hand side (because it is equivalent to non-overlapped implication). What we actually described in our *expect* is: whenever *@antecedent* happens, make sure that at the next clock cycle *@consequent* already happened once. This explains why we only saw it triggering one clock cycle later. While we could live with this approach and just put a nice error message that hints to look at the previous clock cycle for the source of the error, this feels like only half of a solution. There has to be a better way!

Breaking out the old Boolean algebra textbook (or in our case Wikipedia) we are reminded that logical implication is just another logical operation, which means we can also express it using **and**, **or** and **not**. The equivalent form of *"p implies q*" is "

*". This is easily expressed as a TE:*

**not**p**or**q```
<'
// @antecedent implies @consequent
expect overlapped_implication is not @antecedent or @consequent;
'>
```

The only disadvantage here is that it isn't instantly apparent to a not so math savvy person reading the code that what we have is an implication, but this can be easily fixed with a comment.

You can find both forms of the temporal expression, including some *SystemVerilog* code to test them, on the blog's SourceForge repository.

See you next time!

## No comments:

## Post a Comment