Verification Languages:Property Specification Languages

Property Specification Languages

Use of property based veriﬁcation [4] is increasing among the design and veriﬁcation community. As mentioned before, there are two major methods in property based veriﬁcation: ABV and FV. CTL that was described in the pervious section is a property language which is used only in formal veriﬁcation. On the other hand, PSL [4] is a standard assertion language and a language for description of properties. It is used by engineers to specify functional properties of logic designs.

A property is a Boolean valued fact about a design-under-test and PSL is designed to capture design properties in an executable, formal, unambiguous manner. It uses many of the underlying HDL operators and expression syntax to build necessary Boolean expressions in properties. On top of that, when required, PSL deﬁnes its own syntax, (separate from HDLs) to build complex temporal relationships among the Boolean expressions.

In contrast, an assertion is a conditional statement that checks for a speciﬁc behavior and displays a message if it occurs. Assertions are generally used as monitors looking for bad behaviors, but may be used to create an alert for a desired behavior. Assertions are added during veriﬁcation to monitor conditions that are otherwise hard to check using simulation and sometimes, they are used to simplify the debugging of complex design problems. Assertion monitors can be considered as internal hardware test points that wait for a particular problem to occur and then alert the designer when it does. In these cases, assertions are used to improve the ability of observing bugs once they are triggered by a simulation vector.

Application of PSL for formal veriﬁcation is similar to that for CTL described in the previous subsection. So in this section, we focus on PSL as an assertion language. It is important to note that all assertions can be used as properties for a formal veriﬁcation tool. In this section that follows we ﬁrst show all components of a typical PSL assertion to give an overview of this language. Then we will describe the details of PSL.

Components of a PSL Assertion

The general structure of a PSL assertion is shown in a simple property in Figure 92.7. The subsections that follow, describe various parts of this structure.

Various pieces that comprise a complete PSL assertion are described in the following subsections.

Label

Label is optional for every assertion. It is a recommended practice to use a meaningful name for assertions. It helps in identifying failures, success reports coming from a PSL tool.

Verification Directive

It is also possible for users to specify an action to be executed when an assertion passes or a possibly different action to be executed when the assertion fails. PSL has a set of constructs to build complex properties. A property itself is a declaration and a veriﬁcation tool does not know what to do with it unless told otherwise. A veriﬁcation directive sits on top of a property and instructs a tool whether the property should be checked to satisfy or it should never be true.

Occurrence Operators

Occurrence operators as part of the temporal layer are means to specify “when to check for a property.” PSL supports the following occurrence operators:

• always

• never

• eventually!

• next

The always operator is the most frequently used one and it speciﬁes that the property expression which follows it should be checked every clock.

Property to be Checked

The property to be checked forms the core of PSL which allows properties to be declared and then used in an assertion or simply speciﬁes the complete property in the assertion itself as shown in Figure 92.7. Later, we will describe this part in more details.

Clocking Event

Properties can be either clocked or unclocked. A clock for a property can be speciﬁed in the property deﬁnition as shown in Figure 92.7. The symbol @ is used to specify clocking while any Boolean expression can be used for it. PSL also allows a default clock speciﬁcation as given below:

PSL Flavors

In the previous sections PSL assertions that we showed used syntax that was similar to Verilog. However, this is not necessarily a requirement of PSL. PSL is a multiﬂavored, multilayered language. A ﬂavor is the syntax used in a property that may be of VHDL or Verilog. This syntax dictates the syntax for the Boolean expressions, clocking and in general, the way a property is written. Properties shown below have VHDL and Verilog ﬂavors of the same.

VHDL_Prop: assert always not (busy1 and busy2) @(rising_edge(clk)); Verilog_Prop: assert always ~(busy1 & busy2) @(posedge clk);

PSL Layers

In Figure 92.7, a PSL assertion is shown. Different layers are distinguished in this assertion. All properties in PSL are structured. They have Boolean, temporal, veriﬁcation, and modeling layers. The details of these layers are described in a later section. Here, we will merely discuss the categorization of these layers.

The Boolean layer forms a Boolean expression that becomes part of a property. An example for the Boolean layer is “not (ack1 and ack2);”. This example property states that ack1 and ack2 should not be asserted simultaneously. The second layer in PSL is the temporal layer that consists of sequential extended regular expression (SERE) and properties. An example for this layer is “{req;busy[*1:10];ack};”, which is a sequence of three Boolean expressions. In this layer, the timing of the expressions is expressed. Using this sequence, a property can be formed such as “reset |=> {req;busy[*1 to 10];ack}”. The next layer is the veriﬁcation layer that constructs a property. An example for this layer is “assert (reset |=>

{req;busy[*1 to 10];ack});”, which uses the property we just formed. This layer applies the veriﬁcation directive (assert) to the deﬁned property.

The modeling layer is used for formal veriﬁcation. This layer associates PSL properties with a hardware model we are verifying. Other alternatives such as ﬁle name may also be used for this association.

Property Expressions

Speciﬁcation of properties in PSL can be as simple as a Boolean equation that is true for just one clock cycle or can be a complex temporal SERE that is constructed from multiple Boolean expressions in multiple cycles. So we only use Boolean layer and temporal layer to build a property and then a veriﬁcation directive from the veriﬁcation layer converts this property into an assertion. The next two subsections describe property expressions as Boolean layer and temporal layer.

Boolean Layer

The Boolean layer consists of Boolean expressions containing variables and operators from the underlying language. All expressions that can be used as a condition in the underlying language can be used for

Boolean expressions of the Boolean layer. Two simple Boolean expressions in Verilog and VHDL languages are shown below, respectively:

(a & b) == 0 (a and b) = 0

As shown, at the Boolean layer, PSL looks very similar to the underlying HDL. This characteristic of PSL is often referred to as language neutrality.

Temporal Layer

The temporal operators of PSL sit on top of the LTL operators. These temporal operators include always, never, next, until, and before, among others, and are described later.

The Boolean layer forms the core of PSL and the real power of PSL comes from its temporal layer. The term temporal refers to the design behavior expressed as a series of Boolean expressions over multiple clock cycles. To support this, PSL has two major components in the temporal layer: sequences and properties. Sequences are built from basic Boolean expressions and sequence operators such as repetition operators. Properties are built on the top of sequences and can include Boolean expressions, sequences, and other properties.

Sequences

It is necessary for an assertion language to be able to express design behavior over multiple clocks. PSL supports SEREs to meet this requirement. PSL provides an easy and familiar way for engineers to capture sequential behavior. The syntax is derived from standard UNIX regular expressions and hence the name SERE. The ﬁrst and foremost requirement of any temporal sequence is a quick way to move time forward. PSL uses SERE concatenation to achieve this. This operator is represented with a semicolon.

For example, this pseudo-code: {a;b} describes the following behavior:

• a being high in the current clock tick,

• wait until the next clock tick (t + 1) and

• check for b being high.

The curly brackets around the sequence mark the beginning and ending of a SERE. In real life, the delay between two such expressions can be

• More than one

• A range

• Not necessarily occurring in contiguous clock cycles

PSL supports all these requirements via its repetition operators. There are three types of SERE repetition operators, which are consecutive repetition operator, nonconsecutive repetition operator, and GOTO repetition operator. These operators are discussed below.

a. Consecutive repetition operator

The consecutive repetition operator is used to specify that a signal must be asserted continuously for n

clocks. The following example states that busy signal is asserted for three clocks.

We can also specify a range for a SERE with a MIN and MAX speciﬁcations as shown below:

Few notes on the ranges:

• Both MIN and MAX have to be constants.

• Both have to be natural numbers (³0).

• MIN can be set to 0.

• MAX can be set to the keyword inf to indicate inﬁnity.

The following SEREs show several possible repetition operators. They all start when signal req is asserted. In the very next clock, busy is asserted. The number of clocks that this signal (busy) remains asserted is different in the properties shown. For all four properties, the sequence ﬁnishes when an ack is seen after a desired number of busy.

Property Prop_1 states that when req is asserted, signal busy can be asserted two clocks later and then signal ack should be asserted. Property Prop_2 states that when req is asserted, signal busy can be asserted between 0 to 100 clocks later and then, signal ack should be asserted. Property Prop_3 states that when req is asserted, signal busy can be asserted between 2 and inﬁnity clocks later and then, signal ack should be asserted. Property Prop_4 states that when req is asserted, signal busy should be asserted at least 1 clock later and then signal ack should be asserted.

b. Nonconsecutive repetition operator

To have a repetition in which occurrences of the repeated expression or sequence needs not to be contiguous, a nonconsecutive repetition operator can be used. PSL uses the “=” symbol to denote nonconsecutive repetitions. The examples in the previous section with a nonconsecutive repetition are shown below:

c. GOTO repetition operator

The GOTO repetition operator is used to go to the nth repetition of the Boolean expression that it follows and immediately after the occurence of that last repetition, checks for the next expression in the sequence. The intermediate repetitions may be nonconsecutive. This is referred to as GOTO repetition in PSL and is

represented with the “->” symbol. The examples in the previous section with a GOTO repetition are shown below:

In the above, property Prop_1 states that when req is asserted, we go to the second repetition of the busy signal and immediately after the occurrence of that signal, ack should be asserted.

SEREs within Operator

To construct a SERE in which one sequence’s start and end points are fully contained within the other sequence, the SERE within operator can be used. In the following example,

Sere1 within Sere2

sere1’s start point should be after sere2 and its end point should be before that of sere2.

Compound SERE Operators

Repetition operators give the ability to build basic SEREs in PSL. In contrast, compound SERE operators combine two or more sequences and describe complex sequences. PSL provides the following operators for building compound SEREs.

• Fusion operator (:)

• SERE nonlength matching AND (&)

• SERE length-matching AND (&&)

• SERE OR operator (|)

Table 92.4 shows all formats of SEREs and their descriptions.

Occurrence Operators

In addition to sequences, temporal (occurrence) operators are used in temporal layer to construct temporal properties. PSL provides several operators to specify when to check for a property. In the PSL LRM, these are referred to as “simple FL properties” (FL stands for foundation language) and in this section, they are termed as “occurrence operators” for clarity.

The temporal operators sit on top of the LTL operators. These temporal operators include always, never, next, until, and before, among others. The meaning of these operators is clear, but there are a few exceptions.

The always operator states that its operand holds in every single cycle, while the never operator states that its operand fails to hold in every single cycle. The next operator states that its operand holds in the cycle that immediately follows. Hence the assertion

assert always req -> next acknowledge;

means that whenever the HDL signal req is true, the HDL signal acknowledge must be true in the following cycle. The meaning of a cycle will typically be speciﬁed either by deﬁning a default clock or by including the clocking operator @ within the property. Note that when req is true, this assertion says nothing about the value of acknowledge in any cycle other than the following cycle. It also says nothing about the value of acknowledge when req is false. In this case, true is returned as result. This assertion only says that whenever req is true, it must be the case that acknowledge is true in the very next cycle.

This assertion means that whenever req is true, acknowledge must be true two cycles later. It says nothing about the value of acknowledge one cycle after req is true. An interesting feature of this assertion is that it must hold in every single cycle, such that if req was true for three consecutive cycles, then acknowledge must be true for three consecutive cycles, but with a latency of two cycles.

For the meaning of the until operator consider the following example:

This property states that whenever req is true, busy is true in the following cycle and busy remains true until the ﬁrst cycle in which acknowledge is true. When acknowledge goes true, the value of busy is not important. This is the same for any subsequent cycles. If req goes true and then acknowledge goes true in the following cycle, busy needs not to go true at all.

For the before operator consider the following example:

This property states that whenever req is true, busy must be true at least once in the period starting in the following cycle and ending in the last cycle before acknowledge is true.

Table 92.5 shows all temporal operators in PSL and their descriptions.

Suffix Implication Operators

In a class of design properties, a property/sequence is expected to hold only after a condition occurs. This is also referred to as an implication operator. Sufﬁx implication operators in PSL can either be of

the overlapping sufﬁx implication operator (|->) type or of the nonoverlapping sufﬁx implication operator (|=>) type.

In the overlapping sufﬁx implication operator, the condition is checked in the same clock as the precondition occurs. For example, to describe a property in an arbiter as “whenever there is a process using resource (indicated by busy1), the other process should be free (busy2 should be low),” we can have this assertion:

The above property describes that once a process asserts the req signal, the next clock cycle shall make the arbiter to assert ack signal.

Verification Directives

Veriﬁcation directives are used to direct a veriﬁcation tool to check for the validity of properties. Without veriﬁcation directives, a veriﬁcation tool does not know what to do when an assertion passes or which action to be executed when the assertion fails. PSL supports the following directives:

• assert

• assume

• assume_guarantee

• cover

• restrict

• restrict_guarantee

• fairness

• strong_fairness

Among these, assert and cover are the most frequently used directives in simulation-based veriﬁcation methods. Other directives are mostly used in formal veriﬁcation. The assert directive instructs the tool to check whether the property is satisﬁed and if not, to report a failure. The cover directive checks if the sequence was satisﬁed during veriﬁcation. PSL allows labeling of such directives, and it is a good coding style to use descriptive labels for them.

Other directives are described in Table 92.6.

Operator Precedence

The precedence of PSL operators, used above, is shown in Table 92.7.

Specification of Properties in PSL

In PSL, a property forms the top-level part of an assertion. A property can comprise sequences and Boolean expressions that are combined using various property operators described in this section.

The simplest form of property in PSL takes the form of a combinational Boolean condition that must be continuously true.

The sequence {a; b} holds if a holds in a cycle and b holds in the following cycle. The symbol | -> placed between the two sequences denotes sufﬁx implication, meaning that if the ﬁrst sequence holds, the second sequence must also hold, with the two sequences overlapping by a single cycle.

Finally, it is common for properties to include a terminating condition (such as a reset), which will cause the property to be abandoned through the matching of a temporal sequence.

This property states that when the reset signal is asserted, condition evaluation is removed.

Verification Units

PSL is a property language that talks about the design and needs to be linked to a design unit for a tool to check if the design meets the requirements as described by PSL properties. PSL supports a set of

veriﬁcation units as containers of properties so that a set of properties can be linked to a design. Of these,

vunit is the most commonly used and is described below.

Using vunit

A vunit is used as a container for PSL properties. In a property, there are various signals used in the basic Boolean expressions that are expected to exist in a design. The link to the design under test occurs via an argument to the vunit speciﬁcation. These properties can be either bound to a design module or an instance of a module.

Built-In Functions

PSL provides some of the most commonly used functions that can be used inside property expressions. Table 92.8 shows these functions and their descriptions.

The fourth layer in PSL is a modeling layer that is described in the next subsection.

Modeling Layer

The modeling layer is used for formal veriﬁcation. This layer associates PSL properties with a hardware model that is being veriﬁed. For this association, we can use similar ﬁle names for the model and the property set. For example, a model’s ﬁle name may be File1.vhd and its associated property set may be File2.psl. Other alternatives may also be possible.

As with the Boolean layer, the modeling layer comes in the underlying language format. PSL format in this layer deﬁnes design hierarchies and model correspondences. Different formats are used for VHDL and Verilog.

An Example: SAYEH ALU

In this section, we use SAYEH ALU as our example for veriﬁcation. We will show various parts of properties that are needed for this example. This ALU is a 16-bit combinational logic. Its data inputs are 16-bit A and B and its data output is aluout. The ALU, shown in Figure 92.8, has control inputs that determine the function it performs. In addition, the cin input is its carry input used in arithmetic operations. Control outputs of this unit are zout and cout that are the zero and carry ﬂags, respectively.

ALU function control inputs control its transparency, logic and arithmetic functions. For readability of Verilog code of the ALU, Verilog deﬁnitions shown in Figure 92.9 are used for functions of the ALU. The ALU has nine function control inputs, and only one is active at any one time.

Figure 92.10 shows the complete Verilog code of the ALU. Ports of the ArithmeticUnit module are deﬁned as described above. The complete description of this ALU consists of an always block that is sensitive to the input ports of this module. To guarantee that this module is combinational and therefore avoid latches, all ALU outputs are set to their inactive values at the beginning of the always block of Figure 92.10.

Figure 92.11 shows several properties that are written in PSL for our ALU example. When this ALU is being used, we do not expect its control inputs to be asserted simultaneously. For example, AandB and AorB cannot both be 1 at the same time. The ﬁrst property shown in Figure 92.11 checks this. The next seven properties shown in this ﬁgure check the output of the ALU output (aluout) to have the correct functionality when its corresponding function control input is active.

In the property set shown, two properties check that if cin is 0, then the ALU output is the sum of the two inputs if AaddB is 1 and subtraction of the two if AsubB is 1. Another property shown veriﬁes that cout is affected when add or subtract operation is being done. The next to last property in Figure 92.11 says that if aluout is 0, zout must always be 0, which is of course the way this ALU has to function. The last property veriﬁes that if add or subtract operation is being done and the data on A is 0 and data on B is all 1s (FFFF) and cin is 1, then we will deﬁnitely have a carry output.

Conclusions

In this chapter we discussed formal veriﬁcation, assertions, CTL and PSL. CTL is a mathematical form of expressing properties, while PSL which we discussed was for assertion veriﬁcation. We talked about use of assertion languages for speciﬁcation of properties. The ABV methodology compares the implementation of a design against its speciﬁed assertions. Assertions are written in a standard property language such as PSL. The PSL property language was described in this section.

Search This Blog

Integrated circuit course