The Designer's Guide To PSL

What is PSL?

PSL is an abbreviation for Property Specification Language. A property is a boolean-valued fact about a design-under-test. Right now, PSL works alongside a design written in VHDL or Verilog, but in future PSL may be extended to work with other languages. Properties written in PSL may be embedded within the HDL code as comments or may be placed in a separate file alongside the HDL code.

Properties are used to create assertions. An assertion is an instruction to a verification tool to prove that a given property holds. The verification tool could be a simulator (dynamic verification) or a model checker that constructs a mathematical proof of a property (static formal verification).

Properties can play a number of different roles in verification:

• Monitors that dynamically check the state of the design during simulation
• Constraints that define legal sequences of input vectors for simulation
• Functional coverage points that allow the completeness of simulation to be measured
• Assertions to be proved by static formal property checkers
• Assumptions to be made by static formal property checkers when proving assertions

Properties in PSL are composed of boolean expressions written in the host language (VHDL or Verilog) together with temporal operators and sequences native to PSL. The boolean expressions enable PSL to sample the state of the HDL design at a particular point in time, whilst the temporal operators and sequences describe the relationship between states over time. What PSL brings to the underlying HDL is the ability to describe temporal relationships clearly and concisely.

With future extension in mind, PSL also allows expressions to be written in a neutral formal called GDL (for General Description Language) in addition to VHDL and Verilog.

Assertion Based Verification

Writing assertions concurrently with the RTL design and keeping these assertions closely tied to the RTL code has been found to bring significant benefits in both the design and verification processes for digital hardware. The primary benefit is that assertions help to detect more functional bugs, detect them earlier in the process and detect them closer to their original cause. This leads in turn to fewer bugs remaining undetected into production, shorter verification timescales and faster debugging.

A secondary benefit is that the very act of formulating and writing assertions can give the designer a better understanding of the design, and hence uncover bugs in the specification or else avoid introducing bugs into the design in the first place. Once written, bound to the RTL code and proven, assertions play the role of formal comments. Unlike conventional comments, assertions are executable and continue to monitor the design for functional correctness long after they’ve ceased being the focus of attention.

Assertions bring the possibility of increased metrication to the verification process. Assertions directly increase observability of the state of the design during verification. By measuring and controlling the density of assertions and logging assertion passes as well as failures, it is possible to bring some science to the task of knowing when functional verification is complete.

Finally, the introduction of PSL as a standard property language provides a low cost, low risk way of bringing immediate benefits to the design and verification process, yet at the same time opens the door to the introduction of new verification tools such as static property checkers.

The Development of PSL/Sugar

PSL was chartered by the Functional Verification Technical Committee of Accellera. After a process in which donations from a number of sources were evaluated, the Sugar language from IBM was chosen as the basis for PSL. The Language Reference Manual for PSL version 1.01 was released in April 2003. PSL Version 1.1 is currently under development as of February 2004.

Sugar began as an internal development within IBM, where the CTL formalism (Computation Tree Logic) was used to express properties for model checking. The raw CTL notation allows the concise expression of temporal relationships, but was found hard to write and read by non-specialists. Sugar was developed to provide syntactic sugaring on top of CTL, i.e. a layer of user-friendly syntax to hide the more obscure notation. Sugar was subsequently extended to support sequential regular expressions, an extension of the regular expressions familiar to Unix and Perl programmers into the time domain, which provided an alternative form of syntactic sugaring. An implementation of dynamic property checking during simulation was added, and finally the underlying semantic foundation was migrated from CTL to LTL (Linear-time Temporal Logic), because the latter was considered more suitable for simulation and accessible to a wider audience.

PSL currently provides the raw CTL and LTL operators, together with two forms of syntactic sugaring: the temporal operators of the Foundation Language (FL), and Sequential Extended Regular Expressions (SERE). The semantics of each are formally defined in the PSL Language Reference Manual.

The PSL standard is currently owned by Accellera. The PSL/Sugar Consortium is a complementary organisation that exists to facilitate the adoption of PSL by the user community.

The Structure of PSL

The PSL language is formally structured into four distinct layers: the boolean, temporal, verification and modelling layers. The verification and temporal layers have a native syntax of their own, whereas the modelling and boolean layers borrow the syntax of the underlying HDL. Thus PSL is said to come in three flavours: VHDL, Verilog and GDL. The flavour directly determines the syntax used for the boolean and modelling layers and also has a small influence on the syntax of the temporal layer.

The boolean layer consists of boolean expressions containing variables and operators from the underlying language. Formally, the boolean layer consists of any expression that is allowed as the condition in an if statement in the underlying language. As such, expressions in the boolean layer are evaluated at a single point in time.

(a &   (a-1)) == 0         // Verilog flavour
(a and (a-1)) =  0         -- VHDL flavour

The temporal layer forms the major part of the PSL language. As well as including expressions from the boolean layer, expressions in the temporal layer may include temporal operators and Sequential Extended Regular Expressions or SEREs. It is usual for temporal expressions to be sampled on a clock. PSL is intended for designs with synchronous timing.

(always req -> next (ack until grant)) @clk

The verification layer consists of verification directives together with syntax to group PSL statements and bind them to HDL modules. A verification directive is an instruction to a tool to tell it what to do with a property. The principle verification directives are assert (the tool should attempt to prove the property), assume (the tool may assume the given property is true) and cover (the tool should measure how often the given property occurs during simulation).

assert (always req -> ack) @clk;

Verification directives such as the one above can be embedded in the HDL code as comments. Alternatively, verification directives can be grouped into verification units, or vunits, and placed in a separate file. There are actually three kinds of verification unit, with the vunit being the most general, the vprop containing nothing but assertions, and the vmode containing anything but assertions. A verification unit can be explicitly bound to an HDL module or design unit.

vunit my_properties(myVerilog.instance.name) {
  assert (always req -> ack) @ clk;
  assume (never req && reset)@ clk;
}

The modelling layer allows extra code fragments from the underlying language to be included with the properties to augment what is possible using PSL alone. For example, the modelling layer could be used to calculate the expected value of an output.

The modelling layer includes some additional language constructs and convenience functions. For example, the prev() function returns the value of an expression in the previous cycle. Currently, these functions are only part of the Verilog flavour modelling layer, but most tools unofficially support VHDLflavoured versions too.

PSL keywords are case sensitive. As you've probably noticed above, statements are terminated by a semi-colon ;.

Simple Properties

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

assert always CONDITION;

However, this form of property is not particularly useful, since it is vulnerable to race hazards. It is more common to introduce a sampling event or clock.

assert (always CONDITION) @(posedge clk);

It is also possible to define a default clock and thus avoid the need to repeat the explicit clock operator @ in every single assertion.

default clock = (posedge clk);
assert always CONDITION;

It is more common still for a property to take the form of an implication, with a pre-condition that must be satisfied before the main condition is checked.

assert always PRECONDITION -> CONDITION;

This asserts that whenever PRECONDITION holds, CONDITION must hold in the same cycle. The symbol -> denotes logical implication.

It is common (though not essential) for the precondition and condition within the assertion to each take the form of temporal sequences enclosed in braces.

assert always {a;b} |-> {c;d};

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 suffix implication, meaning that if the first sequence holds, the second sequence must hold also, 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 mid-way through the matching of a temporal sequence.

assert (always ({a;b} |-> {c;d} abort reset))
                              @(posedge clk);

When the reset goes true, the obligation for the suffix implication to hold is removed, whether or not there has been a partial match between the property and the actual state of the design.

Temporal Logic

The temporal operators of the foundation language provide syntactic sugaring on top of the LTL operators. These temporal operators include always, never, next, until and before, amongst others. The meaning of these operators is quite intuitive, but there are a few surprises.

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

assert always req -> next grant;

means that whenever the HDL signal req is true, the HDL signal grant must be true in the following cycle. The meaning of a cycle will typically be specified either by defining 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 grant in any cycle other than the immediately following cycle. Also, it says nothing about the value of grant when req is false. It only says that whenever req is true, it must be the case that grant is true in the very next cycle.

The next operator can take a number of cycles as an argument, enclosed in square brackets, as in:

assert always req -> next[2] (grant);

This means that whenever req is true, grant must be true two cycles later. It says nothing about the value of grant 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 were true for three consecutive cycles, say, so must grant be true for three consecutive cycles, but with a latency of two cycles. If this assertion is implemented as a simulation check, it would be re-triggered every time req is true, such that concurrent invocations of the simulation check are effectively pipelined.

The meaning of the until operator is a bit more subtle:

assert always req -> next (ack until grant);

This asserts that whenever req is true, ack is true in the following cycle and ack remains true until the first subsequent cycle in which grant is true. There is no obligation on the value of ack in the cycle in which grant goes true, nor in any subsequent cycles (unless the check is re-triggered by req going true once more). If req goes true and then grant goes true in the following cycle, ack need not go true at all. On the other hand, there is no obligation for grant to ever go true following a req, in which case ack would have to remain true indefinitely.

The cycle in which the left-hand operand to until is first required to hold is determined by the context in which that operator appears. In the example above, the obligation for ack to be true begins in the cycle after req is true. Once again, the always operator requires that the temporal expression shall hold in every cycle, and hence concurrent invocations of the check are pipelined.

Finally, the before operator:

assert always req -> next (ack before grant);

This asserts that whenever req is true, ack must be true at least once in the period starting in the following cycle and ending in the last cycle before grant is true. There are no obligations on the value of ack in the cycle in which req goes true, nor in the cycle in which grant goes true. There is no obligation for grant to ever go true following a req, in which case ack need not go true either. In other words, following a req both ack and grant could remain false indefinitely.

Strong Operators and Liveness Properties

Consider the following assertion:

assert always req -> eventually! ack;

This asserts that whenever req is true, ack must go true at some future cycle, but there is no upper limit on the time by which ack is required to go true. This is known as a liveness property. Liveness properties are characterised by the fact that they do not possess a finite counter-example, and hence in principle they cannot be disproved by simulation. However, liveness properties can in principle be proved or disproved by static model checking tools. Properties that do possess finite counter-examples are known as safety properties.

Liveness properties are written in PSL using strong operators, all of which include an exclamation mark in their name. There exist strong forms of several temporal operators, including next!, until! and before!. For example:

assert always req -> next (ack until! grant);

This means that whenever req is true, ack is true in the following cycle, ack remains true until the first subsequent cycle in which grant is true and grant must go true eventually.

Non-negated strong operators always create liveness properties, but you might care to ponder the fact that:

not eventually! (not P)

is actually formally equivalent to

always P

Sequences

The sequence, which is the syntactic equivalent of the timing diagram, often provide the most convenient way to write properties in PSL, with time advancing as we move from left to right through the text. The Sequential Extended Regular Expression or SERE (which rhymes with beer) permits a compact abbreviation for many common timing relationships.

Consider the following assertion:

assert always {a;b} |-> {c;d};

As was explained above, the semicolon operator moves forward one cycle, whilst the suffix implication operator |-> means that the first sequence must always be followed by the second with an overlap of one cycle. (There is an alternative suffix implication operator |=> which requires that the two sequences do not overlap.)

SEREs permit longer sequences and families of related sequences to be written in a compact notation. For example:

• {a[*2]} means {a;a}
• {a[+]} means {a;a;...;a} with a repeated one or more times
• {a[*]} means {a;a;...;a} with a repeated zero of more times
• {[*]} matches any sequence whatsoever
• {a[=2]} means {[*];a;[*];a;[*]}, i.e. non-consecutive repetition
• {a[*1 to 3]} means {a} or {a;a} or {a;a;a}

There are also several operators that work with whole sequences:

• {seq1} | {seq2} means that one or the other sequence must hold
• {seq1} & {seq2} means that both sequences must hold
• {seq1} && {seq2} means that both must hold and be of equal length

Semantics

The semantics of PSL are declarative rather than imperative, meaning that PSL allows you to describe and reason about an abstract succession of states in such a way as to be equally applicable for generating simulation checkers, for formal proof and for documentation. Unlike some other current property languages, the definition of PSL is not tied to the idea of a checker implemented as a finite state machine executing in monotonically increasing simulation time. Indeed, it is possible to write PSL properties that cannot be implemented efficiently as simulation checkers. Those properties that can be implemented as efficient finite state machine automata are said to belong to the simple subset of PSL. Most practical properties fall in the simple subset.

The semantics of the temporal layer are defined by considering all possible paths through all possible states of a design. A PSL property is said to hold in a particular cycle if it matches (depending on the meaning of the temporal operator in question) a path starting with the current cycle and extending a finite or infinite number of cycles into the future. In other words, to see if a particular property holds, you should choose a particular cycle to start from and then peer forward into the future, comparing the actual state of the design with the obligations imposed by the temporal operators. For a typical PSL property (i.e. one that uses the always operator), this rule applies equally and independently for every cycle.

The semantics of SEREs is defined somewhat differently by considering the set of all possible sequences that can be generated from a particular SERE. For example, the SERE {a[+]} generates the sequences {a}, {a;a}, {a;a;a},... A SERE is said to hold tightly on a finite path if the sequence of states that constitute that path belongs to the set of sequences generated by the SERE. In other words, a SERE that matches a particular finite sequence of states is said to hold tightly over that path, whereas a property is said to hold in a particular cycle if it matches a finite or infinite sequence of states, looking forward in time starting from that cycle.

More PSL?

Learn more about PSL and using PSL to improve your verification process. Consider attending Assertion-Based Verification with PSL. Or, if you are ready to learn some advanced VHDL or Verilog then consider the new improved Expert VHDL or Expert Verilog classes now including PSL.

Источник

• The Designer's Guide To PSL