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 аббревиатура от Язык описания свойств спецификации (Property Specification Language). Свойство здесь понимается, как логические данные, выраженные булевыми значениями (boolean-valued fact), о текущем тестируемом проекте. В настоящее время PSL работает с моделью описанной на VHDL или Verilog, но в будущем рамки PSL могут быть расширены для работы с другими языками. Свойства, описанные в PSL, могут быть встроены в HDL-описание, как комментарии или могут быть размещены в отдельном файле отдельно от HDL-описания.
Свойства (Properties) используются для создания утверждений (assertions). Утверждения — это инструкция для программы верификации, служащая для подтверждения того, что данное свойство поддерживается программой (that a given property holds 
). Программа верификации может быть симулятором (динамическая верификация) или программой проверки модели, которая строит математическое доказательство свойства (статическая формальная верификация).
Свойства могут играть большое количество ролей в верификации:
- Мониторы (Monitors), которые динамически проверяют состояние проекта в течение моделирования
- Ограничения (Constraints), которые устанавливают правильные (допустимые) последовательности входных векторов при моделировании
- Функциональное покрытие точек, которое позволяет оценить полноту моделирования
-
Утверждения (Assertions) доказываются программами проверки (checkers - спец. ПО) статических формальных свойств
- Предположения (Assumptions) делаются программами проверки статических формальных свойств в процессе доказательства утверждений.
Свойства в PSL складываются из булевых выражений, написанных на хост-языке (VHDL или Verilog), и временных операторов и последовательностей родных для PSL. Булевы выражения позволяют PSL выделять состояния HDL-проекта в определенный момент времени, в то время как временные операторы и последовательности описывают взаимосвязь между состояниями во времени. Что PSL привносит в лежащий в основание HDL, это возможность описывать временные взаимоотношения просто и кратко. С дальнейшим развитием, PSL также будет воспринимать выражения, описанные с помощью нейтрального формального языка GDL (General Description Language — Язык Общего Описания), в дополнение к VHDL и Verilog.
Утверждения базирующиеся на верификации
Написание утверждений происходит одновременно с разработкой RTL-модели и размещаются эти утверждения в близкой связи с RTL-кодом, что предназначено для привнесения значительных преимуществ в проект и в процессы верификации для цифрового оборудования. Первое преимущество заключается в том, что утверждения помогают обнаружить большее количество функциональных ошибок, обнаружить их на более ранних стадиях и определить наиболее возможную причину их появления. Это приводит к уменьшению числа не выявленных ошибок в продукте, к уменьшению сроков верификации и более быстрой отладке.
Второе преимущество заключается в том, что сам процесс формулирования и написания утверждении может дать разработчику возможность лучше понять проект и, следовательно, выявить ошибки в спецификации или, иначе говоря, не позволить ошибкам попасть в проект на первых порах. Однажды написанные, связанные с RTL-кодом и доказанные, утверждения играют роль формальных комментариев (спецификации). В отличие от обычных комментариев, утверждения выполняемы и непрерывно отслеживают проект на функциональную правильность, намного после того, как они оказывались в центре внимания.
Утверждения привносят возможность увеличенной измеряемости (контролируемости) в процесс верификации. Утверждения непосредственно увеличивают наблюдаемость состояния проекта во время верификации. Измеряя и контролируя плотность (частоту срабатывания) утверждений и регистрируя выполнение утверждений, так же как и ошибок, возможно привнести некоторые зная (некоторую определённость - science) в задачу определения момента, когда функциональная верификация выполнена.
В заключение, внедрение PSL, в качестве стандарта языка свойств, обеспечит дешевый и надежный путь привнесения незамедлительных преимуществ в разработку проекта и процесс верификации, также становится возможным использование новых программ верификации, таких как программы статической проверки свойств.
Развитие PSL/Sugar
PSL был впервые использован Functional Verification Technical Committee of Accellera. После процесса, в котором все возможные источники были оценены, язык Sugar из IBM был выбран в качестве базисного для PSL. The Language Reference Manual для PSL версии 1.01 был выпущен в апреле 2003-го. PSL версии 1.1, по состоянию на февраль 2004, находится в разработке.
Sugar взял свое начало, развиваясь внутри IBM, где CTL формализм (Computation Tree Logic — Вычисляемое Логическое Дерево) использовался для выражения свойств проверки модели. Сырые CTL обозначения позволяли использовать краткие выражения временной взаимосвязи, но были достаточно тяжелы для чтения и написания не специалистами. Sugar был разработан, чтобы обеспечить syntactic sugaring на верхнем уровне CTL, т.е. уровень с более удобным для пользователя синтаксисом, для того чтобы скрыть сложные обозначения. Впоследствии Sugar был расширен для поддержки последовательных регулярных выражений, расширение регулярных выражений близки для программистов Unix и Perl во временной области, что представляет собой альтернативную форму "syntactic sugaring". Была добавлена реализация проверки динамических свойств во время моделирования, и в итоге, лежащий в основе семантический фундамент перешел от CTL к LTL (Linear-time Temporal Logic — Линейная Временная Логика), т.к. позднее он был признан более удобным для моделирования и более доступным для широкой аудитории.
в настоящее время PSL предоставляет сырые CTL и LTL операторы вместе с двумя формами syntactic sugaring: временные операторы Foundation Language (FL) и Sequential Extended Regular Expressions (SERE). Семантика каждого вормально представлена в PSL Language Reference Manual.
Стандарт PSL принадлежит Accellera. The PSL/Sugar Consortium дополнительная организация, которая существует для популяризации PSL в сообществе пользователей.
Структура PSL
Язык PSL официально структурирован в четыре отдельных уровня: булевый уровень,временной,уровень верификации и уровень моделирования. Слой верификации и временной слой имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом говорят,что PSL сочетает три вкуса:VHDL, Verilog and GDL. вкус напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
Булевый уровень состоит из булевых выражений, включающих в себя переменные и операторы основополагающего языка. Формально, булевый уровень состоит из выражений, которые представляют собой условия для оператора if сновополагающего языка. Как таковые, выражения булевого уровня оцениваются в определенный момент времени.
(a & (a-1)) == 0 // Verilog flavour (a and (a-1)) = 0 -- VHDL flavour
Временной уровень формирует основную часть языка PSL. Временной уровень может включать в себя, как выражения из булевого уровня,так и временные операторы и последовательные расширенные регулярные выражения или SEREs. Для временных выражений, как обычно, применяется выборка по часам. PSL предназначен для моделирования в реальном времени.
(always req -> next (ack until grant)) @clk
Уровень верификации состоит из директив верификации и синтаксиса,позволяющего группировать PSL-операторы и связывать их с HDL-модулями. Директивы верификации- это инструкции программе, которые поясняют, что делать со свойствами. Принцип директив верификации следующий: assert (программа должна попытаться доказать свойство), assume (программа может предположить, что данное свойство справедливо) и cover (программа должна подсчитать, как часто используется свойство во время моделирования).
assert (always req -> ack) @clk;
Директивы верификации, такие как приведены выше, могут быть встроены в HDL-код, как комментарии. С другой стороны, директивы верификации могут быть сгруппированы в блоках верификации или vunits, и размещаться в отдельном файле. Существует три вида блоков верификации, vunit является наиболее общим, vprop не содержит ничего, кроме утверждений, vmode может содержать не только утверждения. Блок верификации может быть ясно связан с HDL-модулем или блоком проекта.
vunit my_properties(myVerilog.instance.name) {
assert (always req -> ack) @ clk;
assume (never req && reset)@ clk;
}
Уровень моделирования позволяет дополнительным фрагментам кода, из основополагающего языка, включаться в свойства и расширять их, что делает возможным использовать PSL отдельно. Например, уровень моделирования может использоваться для расчета ожидаемых выходных значений.
Уровень моделирования включает некоторые дополнительные языковые конструкции и удобные функции. Например, функция prev() возвращает значение выражения прошлого цикла. В настоящее время эти функции только часть уровня моделирования со вкусом Verilog, большинство программ, неофициально, поддерживают версии со вкусом VHDL.
Ключевые слова PSL чувствительны к регистру. Как вы уже могли заметить, операторы разделяются ;.
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.
