The Designer's Guide To PSL/ru
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Содержание |
Что такое PSL?
PSL аббревиатура от Язык описания свойств спецификации. Свойство здесь понимается,как логические данные,выраженные булевыми значениями, о текущем тестируемом проекте. В настоящее время PSL работает с моделью описанной на VHDL или Verilog, но в будущем рамки PSL могут быть расширены для работы с другими языками. Свойства описанные в PSL могут быть встроены в HDL-описание,как компонент,или могут быть размещены в отдельном, от HDL-описания, файле.
Свойства используются для создания утверждений. Утверждения - это инструкция для программы верификации, служащая для подтверждения того,что данное свойство поддерживается программой. Программой верификации может быть симулятор (динамическая верификация) или контроллер модели, который строит математическое доказательство свойства (статическая формальная верификация).
Свойства могут играть большое количество ролей в верификации:
- Динамическая проверка состояния проекта в течение моделирования
- Ограничения, которые устанавливают правильную последовательность входного вектора моделирования
- Функциональное количество точек,которое позволяет выполнить полное моделирования
- Утверждения доказываются статическими формальными свойствами контроллера
- Предположения делаются статическими формальными свойствами контроллера,в процессе доказательства утверждений
Свойства в PSL складываются из булевых выражений, написанных на хост-языке (VHDL или Verilog), и временных операторов и последовательностей родных для PSL. Булевы выражения позволяют PSL выделять состояния HDL-описания в определенный момент времени,в то время как временные операторы и последовательности описывают взаимосвязь между состояниями по времени. Что PSL привносит в лежащий в основание HDL, это возможность описывать временные взаимоотношения просто и кратко. С дальнейшим развитием, PSL, также, будет воспринимать выражения описанные с помощью нейтрального формального языка GDL ( Язык Общего Описания), в дополнение к VHDL и Verilog.
Утверждения базирующиеся на верификации
Написание утверждений происходить одновременно с разработкой RTL-модели и поддерживает эти утверждения в близкой связи с RTL-кодом,что предназначено для привнесения значительных преимуществ в проект и процессы верификации для цифрового оборудования. Первое преимущество заключается в том,что утверждения помогают обнаружить большее количество функциональных ошибок, выявить их на более ранних процессах и определить наиболее возможную причину их появления. Это приводить к уменьшению числа не выявленных ошибок и продукте,к уменьшению сроков верификации и более быстрой обработке.
Второе преимущество заключается в то, что сам процесс формулировки и написания утверждения может дать разработчику возможность лучше понять проект и, следовательно, выявить ошибки в спецификации или не позволить ошибкам попасть в проект на первых порах. Однажды написанные, связанные с RTL-кодом и доказанные, утверждения играют роль официального комментария. В отличие от обычного комментария, утверждения выполняемы и продолжают отслеживать функциональную правильность проекта, намного после того,как они оказывались в центре внимания.
Утверждения привносят возможность введения метрической системы в процесс верификации. Утверждения на прямую увеличивают возможность отслеживания состояния проекта во время верификации. Измеряя и контролируя плотность утверждения 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.???
В заключение, внедрение PSL, как стандартного языка свойств, предполагает небольшие затраты, путь привнесения незамедлительных преимуществ в проект и процесс верификации, также открывается дверь во внедрение новых программ верификации, таких как статический контроллер свойств.
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.
