The book provides detailed descriptions of all the language features of SVA, accompanied by step-by-step examples of how to employ them to construct powerful and reusable sets of properties. The book also shows how SVA fits into the broader System Verilog language, demonstrating the ways that assertions can interact with other System Verilog components.
The reader new to hardware verification will benefit from general material describing the nature of design models and behaviors, how they are exercised, and the different roles that assertions play. The port connections are made according to the implicit connection rules in module dataAdd.
The purpose of the bind statement is to add code in a place without actually modifying that code where it is added. Customarily, once the design is implemented, the design code is maintained with rigor and discipline to minimize code changes. During the verification phase, either verification engineers or designers themselves add code for monitoring the behavior of the design.
The bind statement is ideal for that purpose, as the monitoring code can be added or removed without affecting the design code.
This method is nonintrusive and efficient. Less frequently, code is also added to temporarily fix a bug in the design code, or work around a deficiency.
Once proven to work correctly, the patch is removed and the design code is fixed by actually modifying the code to retain the modified behavior permanently. The bind statement can appear either in a module, an interface or in a compilation-unit scope. It binds a source instance to one or more target instances. When the source instance is bound, it behaves as if it were instantiated in the target instance. Based on this premise, semantic correctness check of the bound instance is performed.
The source instance can be a module, interface, program, or a checker instance, while the target instance can be a module or an interface instance.
More than one source instance can be bound to the same target instance. The following example illustrates binding a checker to a module instance. The generate looping constructs provide a clean way to write such repetitive code, as shown below.
Here, for is a generate loop construct which defines a generate scheme for repeating the body of the loop. The index used in the looping control must be an elaboration time constant, generally consisting of constant literals or parameters. Conventionally, the generate loop iterations are configured based on the elaboration-time parameters.
The looping scheme is processed during the elaboration phase to unroll the generate block as many times as the loop condition holds true. Each iteration of the loop creates an instance of the generate block.
After processing, the generate loop is completely replaced by the unrolled code, leaving no looping code for run time execution. The looping index must be declared as genvar. This declaration must exist prior to using the index and its use is confined within the body of the loop.
Also, it is treated like a localparam and can only be used in places where a localparam can be used. A reference to the genvar index outside the loop is illegal. Another generate scheme uses a conditional if clause. In this scheme, one of the alternative blocks gets selected, based on the condition. Again, the condition of if must consist of elaboration time constants.
At the elaboration time, the condition is evaluated, resulting in the selection of one of the alternative blocks. After elaboration, only the body of the selected block remains. For more than one alternative blocks, a generate case statement is often used as shown below. The use of naming the block is that the contents of the block can be identified and referenced with the block name.
For the case of looping generate block, the name of the generate block instance is tagged with the index, like an array. In contrast, the contents of an unnamed generate block cannot be referenced from the outside. In any case, a generate block creates a scope. The references, when legal, to the contents must be made as hierarchical references following the normal scoping rules.
For complex situations, generate constructs can be nested. There is no restriction on the depth of nesting. The generate block can contain most of the description items, including assertions, properties, and sequences. Disallowed items are stand-alone blocks containing procedural statements.
Syntactically, the generate looping for-loop and conditional if-else and case constructs are similar to the corresponding procedural statements. What distinguishes one from the other is that a generate construct can only appear outside any procedural code, while a procedural statement can only appear inside procedural code.
Optionally, the generate code can be enclosed within generate - endgenerate keywords for clear demarcation from the rest of the code. An example of using generate - endgenerate is shown below.
They cannot appear inside any procedural code. SystemVerilog supplies many constructs to fulfill designer and testbench writer requirements for reducing the time to write tests and catching bugs early on in the design cycle.
These constructs do not exist in isolation. While one can see the operations of individual constructs, understanding the interactions between the constructs is rather complex.
In particular, the order in which the activities must take place is the crux of event semantics underlying the operational semantics of the language constructs. We can see the necessity of ordering events from the following simple example. Thereafter, the assertion evaluation continues and may report other failing attempts. Subexpressions 82 3 Assertion Statements 10 20 30 40 50 60 70 80 90 clk a Fig.
Multiclocked properties are relatively rare, and we postpone their description until Chap. For now, we assume that the subexpressions of the assertion property expression do not modify the clock.
Since concurrent assertions are clocked, the main assertion clock must be present in the assertion. This clock either should be explicitly specified or inferred from the context: from an event control in the surrounding always or initial procedure, or from the default clocking. We discuss in detail clock inference rules in Sects. All signal values participating in the property expression are sampled at the assertion clock tick only, and their values between the clock ticks are completely ignored.
For example, the assertion a1: assert property posedge clk a ; passes for the signal waveforms shown in Fig. Although a is low between time 55 and 65, this is considered to be a glitch and is ignored, because the values of a are sampled on posedge clk, i.
The role of a clock in concurrent assertions is to convert the continuous time into the discrete one. This is important since SVA temporal operators are defined for discrete time. The clocking event follows standard SystemVerilog semantics, and it is based on the clock signal changes: posedge clk triggers when clk becomes 1, negedge clk triggers when clk becomes 0, clk triggers when clk changes value, and edge clk triggers when clk changes to 0 or to 1.
Gated Clock An assertion clock may be gated see Sect. For example, the following assertion has a gated clock which is active only when en is high: a3: assert property posedge clk iff en a ; 2 clk and edge clk behave the same way when clk is of type bit, but they behave differently when the type is logic.
For example, this assertion passes in the case shown in Fig. Global Clocking SystemVerilog provides the capability to specify one clocking event in the entire elaborated model as the primary system clock, called also global clock.
This is done with a global clocking declaration, which is a special form of clocking block declaration. Figure 3. Such a reference appears in line 7. Global clocking name is optional, and GCLK could be omitted in our example.
A common purpose of declaring a global clock is to specify the primary clock for formal verification. The ticks of the primary clock are at the finest granularity of time in a formal model, and the global clock is assumed to tick forever.
Global clocking in formal verification is discussed in Chap. For consistency with simulation, it 10 20 30 40 50 60 70 80 clk en a Fig. Nevertheless, the simulator is not required to check this property of the global clock. In the presence of global clocking, a number of sampled value functions may be used that are synchronized to the global clock.
These are discussed in Sect. Global clock use cases are provided in subsequent chapters. It means that concurrent assertions use the values of signals at the beginning of the simulation step in which the clocking event occurs. Assertion value sampling makes concurrent assertions insensitive to simulation glitches. The assertion body is evaluated using values collected in the Preponed region. The action blocks are executed in the Reactive region.
One should be aware of this peculiarity of concurrent assertions to correctly analyze their behavior in timing diagrams and simulation traces. Since the assertion action blocks are executed in the Reactive region, the signal values used in the action blocks may be inconsistent with the sampled values of the signals used in the assertion.
Example 3. Below, we reuse the example from Sect. The pass action of assertion a2 executes at time 10, 30, 50, 70, 90, , and Its fail action executes at time , , and As an example, consider assertion status at time Assertion a2 samples values of signals a and b in the Preponed region, that is before the value of a changes.
Yes, it is 0 that is printed, not 1 because the action 3. The message is misleading, since the assertion uses the old value of a, while its action block uses the new one! Other exceptions will be covered in subsequent chapters. Sampling of the main reset is explained in detail in Sect. The value of the main assertion reset is not sampled in concurrent assertions.
If the main assertion clock is explicitly specified, disable iff should immediately follow it. If the assertion clock is omitted, disable iff should be the first operator in the assertion body. There may be at most one disable iff operator in the whole assertion. If at any point prior to completion of an assertion evaluation attempt the reset is high or becomes high, then the evaluation attempt is discarded. Such attempts are called disabled.
The reset is asynchronous, in the sense that it is monitored at every time-step, and not only at the ticks of the assertion clock. Therefore, it also makes it sensitive to simulation glitches. In this example, there are three assertion evaluation attempts beginning at times 20, 40, and 70 that satisfy the antecedent signal req.
The last attempt is normal, and it succeeds because ack is received in two cycles after req is issued. Refer to Chap. Its evaluation goes on evaluating regardless of the occurrence of the clock tick of the associated assertion.
An example of disable iff. Detect the occurrence of clock posedge clk , since sequence ack and assertion a1 evaluations are activated by the clock. Start a new attempt for sequence ack. Determine whether there is a match for sequence ack. Start a new attempt for assertion a1. Resume evaluation of the previous attempts for this clock tick.
For an attempt of a1 resulting in a failure, schedule the action block execution in the Re-Active queue of the Reactive region. For an attempt of a1 resulting in a success, report a success. Execute action blocks. These steps are taken in specific regions. Each region contributes to the execution of concurrent assertions as shown in Fig. Normally, the detection of an assertion clock occurs in the Active region.
What sets a concurrent assertion apart from an immediate assertion is that the former is 3. Consequently, its evaluation resumes at the arrival of the clock and gets suspended at the end of the time slot in which the clock occurs. Beside the clock, the new attempts of procedural concurrent assertions are bound to the procedural context in which they are specified.
Assertion a1 is standalone, and therefore it has an implicit always operator. Its performance in simulation may be poor if req is asserted and no gnt is asserted for a long time if ever. Simulation performance efficiency is discussed in detail in Sect. In this example, we assumed that the request remains pending until granted. Example 5. A device must be available infinitely many times. The device availability is indicated by high value of the ready signal. It expresses the notion of fairness.
Fairness indicates that some resource eventually becomes available, as in Example 4. The absence of fairness is called starvation, the situation when the requested resource is never available: Imagine a car waiting at an intersection forever on the red light when the traffic lights are broken.
We get back to the notions of fairness and starvation in Chap. In simulation, of course, this assertion cannot be verified it cannot fail because simulation will end in a finite number of clock ticks. The above definitions with obvious modifications apply also to the way property truth is determined in clock tick i. For example, p and q is true in clock tick i iff both p and q are true in clock tick i.
In the special case of Boolean properties, it is possible to rewrite Boolean property connectives in a different way. Since Boolean expressions in this case may also be considered as Boolean properties, both operators may be applied to them.
Similarly, e1 or e2 is equivalent to e2 e2, but not e is equivalent to! The following expression is syntactically illegal: a and b c.
The operator , however expects both its operands to be Boolean expressions. What does not always p mean? Solution: According to the definition of property not, this property is true iff always p is false, which means that p is false at least in one clock tick. Reset rst must be asserted during the first two cycles. A more elegant way to write the same property is described in Sect. See Sect. What is the meaning of always p and always q?
Solution: According to the definition of property and this property is true iff both p and q hold in each clock tick, that is, the original property is equivalent to always p and q.
Discussion: always p or always q is not equivalent to always p or q. Consider a case when p holds in all odd clock ticks, and q holds in all even ticks.
Then always p or q is true, whereas always p or always q is false. It follows that property p until q is true iff the property p is true in every clock tick until but not including the first clock tick where q is true. See Fig. If q never happens p should be true forever.
Note that p until q does not mean that p cannot be true starting from the clock tick when q becomes true.
It only means that p does not have to be true after q becomes true for the first time. Also, the operator until is nonoverlapping: p does not have to be true when q becomes true for the first time though, of course, p may be true at this moment.
See Exercise 4. Example 4. Table 4. Solution: initial a1: assert property posedge clk! There cannot be a read before the first write: Solution: initial a2: assert property posedge clk! Write a restriction saying that initially all bus drivers are disconnected have a high impedance value.
Write the following assertion: rdy should be low while rst is active. What do the following properties mean? Discuss the usage of the always operator in assertions. What is the meaning of the following assertion note that it does not belong to an initial procedure? What is the meaning of the following properties?
Chapter 5 Basic Sequences A sequence works in a way a collection never can. We considered Boolean properties as the simplest building block. SVA provides sequences as more elaborate building blocks for properties. Since the simplest sequence is a Boolean expression, we could say that properties are built not from Boolean expressions, but from sequences. Sequence is a rule defining a series of values in time. A sequence does not have a truth value, it has one initial point and zero or more match, or tight satisfaction points.
Like properties, sequences are clocked. If the clock is not written explicitly, we assume that the sequence inherits this clock from the property to which it belongs. When a sequence is applied to a specific trace, it defines zero or more finite fragments on this trace starting at the sequence initial point and ending in its tight satisfaction points.
We will call the length of a trace fragment defined by a sequence match simply the length of the sequence match. In the following sections, we define the sequence match separately for each kind of a sequence.
Before we proceed to the accurate definitions, we informally illustrate the notion of a sequence on the following example. Sequence a [] b defines the following scenario: a is followed by b in one or two clock ticks. Let the initial point of this sequence be clock tick 2.
Then this sequence has a match if a is true in clock tick 2 and either b is true in clock tick 3 or b is true in clock tick 4. Thus, the following matching outcomes are possible: 1. In this case, the sequence has no match.
In this case, the sequence has a single match at clock tick 3. In this case, the sequence has a single match at clock tick 4. In this case, the sequence has two matches, or two tight satisfaction points: 3 and 4. In case 1 it defines zero fragments, in case 2 it defines one fragment, , in case 3 it also defines one fragment, , and in case 4 it defines two fragments, We numerate clock ticks with integer numbers starting with 0. In diagrams, we designate trace fragments defined by sequence matches with ovals.
The sequence and property operators described in this chapter are summarized in Table 5. They are grouped by their precedence, from highest to lowest. Additional sequence operators are covered in Chap. This sequence has a match or a tight satisfaction point at its initial point if e is true. Otherwise, it does not have any satisfaction points at all. The initial fragment of the trace of signals a and b is shown in Table 5.
Table 5. For initial points 1 and 2 there are no sequence matches. Sequence s should not admit an empty match the notion of empty match is explained below in this section. This definition is applicable only to sequential properties in the context of assertions or assumptions. In the context of cover statements, the definition of sequential property is different, as explained in Chap. Except for Chap. Although it is not easy to understand the full meaning and the rationale of the definition of a sequential property at this point, because we have not yet described the SVA constructs in which all nuances of this definition come into play, we need this definition now to build properties from sequences.
We will explain some of its aspects here, while the other aspects will become clear to the reader only later. Consider the most important special case of this definition: if a sequence has at least one match, then the corresponding sequential property is true. The entire definition is broader since it allows in some cases sequential properties to be true even if their sequences do not have any match.
Indeed, in this case the fact that sequence s does not have any match on a trace fragment of length L witnesses its inability to have any match. We will call such sequences bounded sequences. It is easy to see that all Boolean sequences are bounded, as all their matches are one clock cycle long. Sequence a [] b informally described in Example 5. Solution: This sequence can only have matches of length 2 or 3, and its match upper bound L D 3: if this sequence does not have a match on a trace fragment of three clock cycles, it does not have matches at all.
So, what is the nature of unbounded sequences? They should admit arbitrary long matches. Examples of unbounded sequences are provided in Sect. Another point to be clarified is the notion of empty match. The match is empty if the trace fragment it defines is empty. We will provide examples of empty match in Sects. Note that a Boolean sequence cannot have an empty match. It either has a match of size 1 if its Boolean expression is true, or it does not have matches at all.
Pay attention to the clock tick where the truth value of a sequential property is defined. The truth value of sequential property s corresponds to the initial point of sequence s, and not to the point of its tight satisfaction. Let a be true in clock tick 2, and false in all other clock ticks, and b be true in clock tick 3, and false in all other clock ticks. Then sequential property a [] b is true in clock tick 2 not 3!
Since Boolean sequences are bounded, Boolean sequential property e is true iff Boolean sequence e has a match, that is, when e is true. We come to the conclusion that Boolean sequential properties are exactly Boolean properties we described in Sect. Therefore, sequential properties generalize Boolean properties, and it is possible to define all property operators from Chap.
In other words, a finite trace matches r 1 s iff it can be split into two adjacent fragments, the first one matching r, and the second one matching s. If both operands of sequence concatenation are bounded sequences, its result is also bounded.
What is the meaning of a 1 b, where a and b are Boolean expressions? Solution: Let the initial point be clock tick i. Sequence a 1 b has a match iff a is true in clock tick i and b is true in clock tick i C 1.
Sequence a 1 b may have only one tight satisfaction point, in clock tick i C 1. Therefore, this sequence means that b immediately follows a. Discussion: Tight satisfaction of sequence a 1 b does not depend on the value of b in clock tick i and on the value of a in clock tick i C 1. Although this looks obvious, this is a source of confusion for many people who erroneously believe that t for this sequence match b must become true for the first time in clock tick i C 1.
Write a sequence capturing the following scenario: request req, immediately followed by retry rtry, immediately followed by acknowledgment ack. Write the following sequence: request req followed by acknowledgment ack in two cycles.
To match, the corresponding Boolean expression should be true. Recall Sect. So, the desired sequence may be written as req 1 1 1 ack. There is a special syntax to capture this situation: r n s n must be a nonnegative elaboration time integral constant.
We will call this interval between two sequences in clock cycles delay not to be confused with the delay operator in SystemVerilog. Using this syntax, the sequence from Example 5. With the exception of Boolean sequential properties, top-level sequential properties are relatively rare in assertions and assumptions, and they are normally used to specify reset sequences. Reset rst must be initially high and be low in clock tick Solution: initial a1: assert property posedge clk rst 20!
What does the following assertion mean? Hence, a must be true in each clock tick, and b must be true starting form clock tick 1. With numerous exercises, ranging in depth and difficulty, the book is also suitable as a text for students. The book provides detailed descriptions of all the language features of SVA,.
Get Sva Books now! This book is the result of the deep involvementof the authors in the development of EDA tools, SystemVerilog Assertion standardization, and many years of practical experience. One of the goals of this book is to expose the oral knowhow circulated among design and veri? This book provides a hands-on, application-oriented guide to the language and methodology of both SystemVerilog Assertions and SystemVerilog Functional Coverage.
Readers will benefit from the step-by-step approach to functional hardware verification using SystemVerilog Assertions and Functional Coverage, which will enable them to uncover hidden and hard to find bugs, point.
This book describes in detail all required technologies and methodologies needed to create a comprehensive, functional design verification strategy and environment to tackle the toughest job of guaranteeing first-pass working silicon.
The author first outlines all of the verification sub-fields at a high level, with just enough depth to allow. SystemVerilog language consists of three categories of features -- Design, Assertions and Testbench. Author : Brian Bailey Publisher: Intl. We sincerely hope that the readers? Formal Verification FV enables a designer to directly analyze and mathematically explore the quality or other aspects of a Register Transfer Level RTL design without using simulations.
This can reduce time spent validating designs and more quickly reach a final design for manufacturing. Building on a basic knowledge of SystemVerilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes at Intel and other companies. After reading this book, readers will be prepared to introduce FV in their organization and effectively deploy FV techniques to increase design and validation productivity.
0コメント