Assertion-based verification has been an integral part of modern-day design verification. Concurrent SVA is a powerful assertion language that expresses the definition of properties in a concise set of notations and rules; its use is very wide spread and is definitely encouraged. However, SVA is designed for a static world; it fails to easily address the use of delays and repetitions based on the values of unit variables (module, checker, interface); it cannot reference non-static class properties or methods; care should be taken when accessing large data structures, especially large dynamic data structures; sequence_match_item cannot directly modify unit variables; there are very strict rules on how property local variables are processed in the ORing and ANDing of sequences, and the flow through of those variables. It is important to note that those restrictions should not be viewed as a discount of SVA because SVA easily addresses most common cases of chip design requirements. In addition, the alternative presented in this article is only applicable for simulation, but definitely not for formal verification, as that is only supported by assertion languages (SVA, PSL).
This article first explains the concepts, and then by example, how a relatively simple assertion can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as vacuity or an error in the assertion. The article then provides examples that demonstrate how some of the SVA limitations can be overcome with the use of tasks, but yet maintain the spirit (but not vendor’s implementations) of SVA. Another possibility to handle these issues is to use checker libraries such as OVL, Go2UVM2; those checkers are not addressed in this article. Again, it is important to emphasize that this alternate solution with tasks should only be used when those difficult situations arise.
An assertion consists of 2 parts:
- The property: The property describes the body of the requirements, but not its initiation for simulation. The property can be emulated with an automatic task that when triggered, starts an independent thread that can span over one or more cycles.
- The assert statement: The assert statement is the mechanism that triggers the property at the clocking event. That action can be emulated with an always block that, at the clocking event, initiates the automatic task using the
fork/join_none statement; this is more like a fire-and-forget of an automatic thread of the property from its starting (attempt) point.
The Task Model
In modeling a property that contains an antecedent and a consequent, the task emulates the SVA antecedent with an
if statement that represents the attempt phase, and a
return statement to emulate an assertion vacuity when that
if statement is false. If the
if statement is true (i.e., successful attempt), then the task proceeds to emulate further sequence elements until it reaches the antecedent endpoint, but checking at each clocking event that the sequence is true. If it is false, a
return statement emulates vacuity.
At the successful completion of the antecedent the task proceeds to emulate the consequent. This process is similar to the steps used in the antecedent but it returns a failure message upon an error prior to exiting the task with a
return or a disable. The generic structure of the task is as follows:
The Assert Model
Below is a model of the assert statement. In this example,
task t_a2b_then_3c (discussed below) is triggered in parallel to other possible tasks using the clocking event
<font color="#8f499c">posedge</font> clk. // Emulation of the assert statements for all of the examples is expressed below:
EMULATING A SIMPLE ASSERTION
Consider the following SVA assertion:
Using that structure defined in section 1, the property for that assertion can be expressed as:
Simulation of the assertion with SVA and with the task emulation produced the following results:
DELAYS BASED ON UNIT VARIABLES
Consider the same assertion as above, but with a small variation:
What is desired in this assertion is having the delays be defined by dynamic values that are set in variables. SVA 1800’2017 does not allow delays or repeat operators to be defined dynamically, they must be static after elaboration. To circumvent this issue, SVA requires a convoluted counting method that does not clearly express the intent of the property, but is a workaround solution. In SVA, one must define in the property a set of local variables, then setting them up at the successful attempt, and then use those variables as counters. On top of these complexities, one must use in some cases the
first_match() operator to forcibly end the count. Below is a possible solution, which looks rather complex.
The code is much simpler represented using tasks, as shown below:
REPEATS BASED ON UNIT VARIABLES
Consider the same assertion as above, but with another small variation:
The above assertion is illegal because the range must be statically defined at elaboration. The following is a workaround.
Using tasks, the same can be expressed more simply as shown below:
CONCURRENT ASSERTIONS IN CLASSES
There are cases, such as in class monitors, where a set of concurrent assertions are useful because the data is available within those classes and in the interfaces (e.g., the virtual interface), but the verification occurs over a set of cycles. Concurrent assertions are illegal in classes. A workaround is to copy the class variables into the interfaces, and perform the assertions in those interfaces. However, the use of tasks alleviates this copying need. On the following page is a simple example that demonstrates the concept of how tasks can be used within classes to express concurrent assertions.
EMULATING A COMPLEX ASSERTION, DIFFICULT WITH SVA
A problematic issue in SVA is the flow-through of local variables when dealing with ORed sequences. Another issue is how local variables are handled when they are assigned and read in multiple ORed and ANDed threads. Consider these requirements that came from an actual example in the Verification Academy forums
The requirements for this model, as demonstrated in the figure below, are:
- Upon a rose of go, data is sent on a data bus
- Data is only valid when the vld signal is true
- The checksum chksum is on the data bus and is asserted upon the fall of go
- Following the initialization of the checker sum, a running sum with overflow is computed at every cycle vld is true
- In the chksum cycle, the checker sum must be compared against the chksum that appeared on the data bus
Figure 1: Requirements for Assertion
Assertions that Appear OK but Are Not!
An assertion that appears on the surface like it should work, but fails to compile, is shown below:
The issue with this property is that the local variable result does not flow out of the ORing of the two sequences in the consequent; the code fails to compile.
An alternate SVA solution is to put the error message within the function (option 1) along with embedding the result in the second sequence of the consequent, thus avoiding the above described issue; but this solution is in error, though it compiles OK. This is shown below:
The above assertion tries to express that upon a rose of go, sum=0. Then, at every clock cycle when vld==1, we compute the sum (local variable sum = sum+data). This process is repeated up to 100,000 times unless we get a fell of go, at which time we compare sum with the provided checksum from the data line. If there is a mismatch between the computed checksum and the provided checksum on the data line, the chek_sum function assigns a 0 to local variable result; this forces an assertion error, as it is the last term evaluated. The thinking here is that without this forcing of value, the SVA assertion will not exit as a failure. However, this is faulty logic because we have an ORing of two sequences in the consequent, and if one of those sequences fails, the assertion waits for a possibility that the second sequence may succeed with a match; thus it waits for 100,000 cycles.
A potential solution to avoid this waiting for all possibilities is to use one of the SVA property abort operators (accept_on, reject_on, sync_accept_on, sync_reject_on). That solution fails to compile because local variables cannot be referenced in the abort condition.
The SVA solution that works OK is shown below. It requires two assertions:
ap_check_msg_OK requires that upon a rose of go, a cheksum is calculated at every occurrence of vld. This operation is continued until the first occurrence of a fell of go (that is why the
first_match operator is needed). Thereafter a check is made to compare the presented checksum against what is dynamically calculated.
2. The above assertion requires that there must be at least one vld between a rose of go and a fell of go; however, that is not necessarily the requirements. The assertion on the following page addresses this case:
Note that even though SVA does provide a clear solution, the above discussion emphasizes some of the restrictions that can cause misunderstandings.
EMULATING THIS SVA ASSERTION WITH TASKS
Using tasks eliminates the issues of visibility of local variables by threads, and makes the code far more readable and understandable. The following code for the task demonstrates the concepts:
Concurrent SVA is very powerful language to express relatively straightforward properties in a concise and readable manner. SVA is also well supported in formal verification. However, SVA has limitations that causes the use of less expressive options, such as counters, to circumvent the language restrictions. An alternative solution that emulates how SVA operates conceptually (but not in tool implementations) helps resolve those issues, and in some cases, simplify the definition of assertions. That solution relies on automatic tasks that are triggered at every clocking event, thus allowing the full use of all the features of SystemVerilog; these features include automatic variables, loops (e.g., repeat, forever, while, for), return, disable, fork-join, and immediate assertions. Keep in mind that an assertion is just a statement that a property is true, regardless of implementation. Thus, implementing an assertion with tasks is acceptable; SVA is just a shorter notation that adapts well for most cases, but not all cases.
Acknowledgement: I thank my co-author Srinivasan Venkataramanan from verifworks for his valuable comments and expertise.
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448 ben@SystemVerilog.us
- verifworks.com github.com/go2uvm
Back to Top