All engineers who attend our courses are invited to send their questions to us in the weeks and months that follow the course, as they learn to apply the knowledge they gained during the few days of the course. The problem we're looking at here came from an email from an antendee, and he described his need to verify an interface that is simple to describe but harder to check.
SystemVerilog Assertions (SVA) have helped in verifying many designs and for some groups they have driven the adoption of SystemVerilog. They work particularly well on complex control logic with many states; the sort of code that is hard to exercise completely in simulation. They can also be useful for providing robust specifications of interface behaviour, a place where differences in interpretation can lead to hard-to-find bugs. However, the effective use of SVA is distinctly non-trivial. The grammar and syntax of SVA can be hard to penetrate, and even when you know the grammar it can be hard to create a property that you are sure describes your desired behaviour.
We assume readers are familiar with the basics of SVA.
Two blocks communicate using a pair of wires, consisting of a request (REQ) and a grant (GRA). Requester asserts REQ to issue a request, which may happen in consecutive clock cycles. When Granter has completed the work associated with a request, it asserts GRA. Again, this may be in consecutive cycles. Granter can maintain four outstanding requests, and there must be two or more cycles between a request and its corresponding grant.
It's the second part of the specification that presents the problem; how do we allow for overlapping activity in our assertion? Leaving aside the spacing of REQ and GRA, a simple property such as this
assert property (REQ |-> ##[1:4] GRA);
is not going to handle the situation, as we can see here:
The first of the two expected GRA pulses will cause the completion of two evaluations of the property, each started on the REQ pulse.
To deal with this, we need to solve two problems:
(You don't hear that very often...)
The first problem has to be solved by adding some external code to count requests and grants. This is very simple:
bit [1:0] req_num, gra_num; always @(posedge clock) begin if (reset) begin req_num = 0; gra_num = 0; end else begin if (req) req_num++; if (gra) gra_num++; end end
As the maximum number of outstanding requests is four, it's convenient to use a two-bit counter.
The second problem means that we have to be able to identify each evaluation of the property; to put it another way, each assertion thread must be unique somehow. To do this, we make use of SVA's facility for local variables in properties. A variable declared in a property is created anew each time an assertion evaluation starts, and thus each evaluation can be distinct. For example:
property data_pipe; logic [31:0] v; ( $rose(load), v = data_in ) |=> ##[1:10] (done && (data_out == v)); endproperty
Notice the comma-separated lists of actions at each stage in the property; when the first item is found to be true, the list of actions that follow is performed. This mechanism can be used to record the values that are used in the evaluation of the property, and these values can then be passed out for use in functional coverage.
In our example, each time a REQ occurs, we save the value of the satellite REQ counter in a local variable and use that to search for a grant that matches:
property req_gra_check; bit [1:0] num; (req, num = req_num) |-> ##[2:$] gra && (num == gra_num) ); endproperty
Thus when a REQ is seen, the number is recorded. This then implies that two or more cycles later GRA must be asserted and the satellite grant counter have reached the correct value.
This is not adequate, however. Our specification says that the correctly-numbered GRA must occur two cycles after the REQ to which it refers. Our property does not currently include this behaviour, as there is no specification of what can or should occur during the delay of two or more cycles. To this end, I must add to the property the requirement that during the delay, if GRA is asserted, the grant counter must not have the number corresponding to the request we are following in this thread. Got that? Luckily, the code is easier than the text (a major plus for SVA there):
property req_gra_check; bit [1:0] num; (req, num = req_num) |-> !(gra && (num == gra_num))[*2] ##[1:$] gra && (num == gra_num) ); endproperty
This now says that on a request with count N, grant N must be inactive for two cycles, before going active later. The repetition number $ means "end of simulation", and you must think very carefully if this is appropriate. Our example property will never fail if grant N never occurs.
This property is OK, but it does not deal with the other part of the requirement, that there be no more than four outstanding requests. How can we deal with that? Remember that our satellite counter loops through the values one to four. We can simply write that if request N occurs, grant N should occur before another request N:
property req_gnt_check; bit [1:0] num; (req, num = req_num) |-> ( ##1 !(req && (req_num==num))[*1:$] ) intersect ( !(gra && (num == gra_num))[*2] ##[1:$] gra && (num == gra_num) ); endproperty
Notice the use of the intersect operator. This length-matching sequence "and" allows us to specify that the two operands must start and finish in the same cycle. Thus, however long it takes for the grant N to occur, there must not be another request N during the whole of that time. If one occurs, the property fails to hold.
We have shown how some useful features of SVA can help create a property that describes our stated behaviour. We have also illustrated that SystemVerilog properties require a great deal of thought and attention in their development. They make it possible to define unambiguous specifications of behaviour, but they also make it possible to write a property that has little to do with the behaviour you thought it had.
This is a serious issue: how can we make sure that an assertion of even this moderate complexity is correct and complete? It is a question that is asked in almost every SystemVerilog course we run. There are no really good answers, alas. Following much discussion with course attendees, we have come to some conclusions about how assertions get used in a real project:
A new generation of tools is beginning to appear that use formal methods and various forms of fault modelling to identify possible broken-ness in your design that would not be caught by any of your assertions. Of course, they can't say whether your design is actually broken because they don't know the specification you're working to, but they will help in identifying areas of your design and testbench where checking is weak.
Even though SystemVerilog Assertions can be hard to write and harder to debug, we consider that assertion-based verification is A Good Thing. It presents another weapon in the armoury of the team attempting to produce, correctly, ever more complex devices to ever tighter timescales.
Click here to download source code accompanying this article and this page in PDF.
In exchange for these downloads, we will ask you to enter some personal details. To read about how we use your details, click here. On the registration form you will be asked whether you want us to send you further information concerning other Doulos products and services in the subject area concerned.
Your comments are welcome - send email