The Designer's Guide To PSL/ru — различия между версиями
Valentin (обсуждение | вклад) (→Temporal Logic) |
Valentin (обсуждение | вклад) (→Временная логика) |
||
| Строка 238: | Строка 238: | ||
means that whenever the HDL signal <code>req</code> is true, the HDL signal <code>grant</code> 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 <code>req</code> is true, this assertion says nothing about the value of <code>grant</code> in any cycle other than the immediately following cycle. Also, it says nothing about the value of <code>grant</code> when <code>req</code> is false. It only says that whenever <code>req</code> is true, it must be the case that <code>grant</code> is true in the very next cycle. | means that whenever the HDL signal <code>req</code> is true, the HDL signal <code>grant</code> 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 <code>req</code> is true, this assertion says nothing about the value of <code>grant</code> in any cycle other than the immediately following cycle. Also, it says nothing about the value of <code>grant</code> when <code>req</code> is false. It only says that whenever <code>req</code> is true, it must be the case that <code>grant</code> is true in the very next cycle. | ||
--> | --> | ||
| − | означает, что когда бы HDL-сигнал <code>req</code> не принимал значение "правда", HDL-сигнал <code>grant</code> должен принимать значение "правда" в следующем цикле. | + | означает, что когда бы HDL-сигнал <code>req</code> не принимал значение "правда", HDL-сигнал <code>grant</code> должен принимать значение "правда" в следующем цикле. Цикл имеет типичное представление обозначенное часами по умолчанию или включая оператор времени с течением свойства. Следует отметить, что когда <code>req</code> принимает значение "правда", то это утверждение ничего не говорит о значении <code>grant</code> в любом другом цикле,кроме последующего. Также ничего не говорит о значении <code>grant</code>, когда <code>req</code> принимает значение "ложь". Это говорит лишь о том, что когда бы <code>req</code> не принимало значение "правда", всегда найдется случай, в котором <code>grant</code> примет значение "правда" уже на следующем цикле. |
| + | |||
| + | <!-- | ||
The <code>next</code> operator can take a number of cycles as an argument, enclosed in square brackets, as in: | The <code>next</code> operator can take a number of cycles as an argument, enclosed in square brackets, as in: | ||
| + | --> | ||
| + | Оператор <code>next</code> может использовать число циклов,как аргумент, заключенный в квадратные скобки: | ||
assert always req -> next[2] (grant); | assert always req -> next[2] (grant); | ||
| + | <!-- | ||
This means that whenever <code>req</code> is true, <code>grant</code> must be true two cycles later. It says nothing about the value of <code>grant</code> one cycle after <code>req</code> is true. An interesting feature of this assertion is that it must hold in every single cycle, such that if <code>req</code> were true for three consecutive cycles, say, so must <code>grant</code> 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 <code>req</code> is true, such that concurrent invocations of the simulation check are effectively pipelined. | This means that whenever <code>req</code> is true, <code>grant</code> must be true two cycles later. It says nothing about the value of <code>grant</code> one cycle after <code>req</code> is true. An interesting feature of this assertion is that it must hold in every single cycle, such that if <code>req</code> were true for three consecutive cycles, say, so must <code>grant</code> 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 <code>req</code> is true, such that concurrent invocations of the simulation check are effectively pipelined. | ||
| + | --> | ||
| + | Это значит, что когда бы <code>req</code> не принимал значение "правда", <code>grant</code> примет, также, значение "правда" через два цикла. Это ничего не говорит, о значении <code>grant</code> через один цикл, после того, как <code>req</code> приняло значение "правда". Интересная особенность этого утверждения заключается в том, что оно имеет место в каждом отдельном цикле, так если бы <code>req</code> имел значение "правда" три подряд цикла, то и <code>grant</code> должен держать значение "правда" три цикла, но с задержкой в два цикла. Если это утверждение реализовать,как проверку моделирования, то оно будет повторно вызываться каждый раз когда, <code>req</code> будет принимать значение "правда", таким образом эти одновременные вызовы проверки моделирования являются эффективным конвейером. | ||
| + | <!-- | ||
The meaning of the <code>until</code> operator is a bit more subtle: | The meaning of the <code>until</code> operator is a bit more subtle: | ||
| + | --> | ||
| + | Смысл оператора <code>until</code> немного более хитрый: | ||
assert always req -> next (ack until grant); | assert always req -> next (ack until grant); | ||
| + | <!-- | ||
This asserts that whenever <code>req</code> is true, <code>ack</code> is true in the following cycle and <code>ack</code> remains true until the first subsequent cycle in which <code>grant</code> is true. There is no obligation on the value of <code>ack</code> in the cycle in which <code>grant</code> goes true, nor in any subsequent cycles (unless the check is re-triggered by <code>req</code> going true once more). If <code>req</code> goes true and then <code>grant</code> goes true in the following cycle, <code>ack</code> need not go true at all. On the other hand, there is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> would have to remain true indefinitely. | This asserts that whenever <code>req</code> is true, <code>ack</code> is true in the following cycle and <code>ack</code> remains true until the first subsequent cycle in which <code>grant</code> is true. There is no obligation on the value of <code>ack</code> in the cycle in which <code>grant</code> goes true, nor in any subsequent cycles (unless the check is re-triggered by <code>req</code> going true once more). If <code>req</code> goes true and then <code>grant</code> goes true in the following cycle, <code>ack</code> need not go true at all. On the other hand, there is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> would have to remain true indefinitely. | ||
| + | --> | ||
| + | Это утверждает, что когда бы <code>req</code> не принимал значение "правда", <code>ack</code> принимает значение "правда" в следующем цикле и остается в этом значении до первой последовательности циклов, в которых <code>grant</code> принимает значение "правда". Нету обязательного значения <code>ack</code> в цикле, в котором <code>grant</code> принимает значение "правда",ни для какой последовательности циклов (кроме проверки,вызываемой <code>req</code> более одного раза). Если <code>req</code> принимает значение "правда", и затем <code>grant</code> принимает это же значение в следующем цикле, то <code>ack</code> вообще не должен принимать значение "правда". С другой стороны, не существует обязательств для <code>grant</code> когда-либо принимать значение "правда" следуя за <code>req</code>, в это случае <code>ack</code> будет иметь значение "правда" неопределенное время. | ||
| + | <!-- | ||
The cycle in which the left-hand operand to <code>until</code> is first required to hold is determined by the context in which that operator appears. In the example above, the obligation for <code>ack</code> to be true begins in the cycle after <code>req</code> 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. | The cycle in which the left-hand operand to <code>until</code> is first required to hold is determined by the context in which that operator appears. In the example above, the obligation for <code>ack</code> to be true begins in the cycle after <code>req</code> 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: | + | Цикл, в котором левый операнд <code>until</code> вызывается первым, определен контекстом, в котором этот оператор появился. В пример выше, <code>ack</code> должен принимать значение "правда" в цикле, после того, как <code>req</code> примет значение "правда". |
| + | <!-- | ||
| + | Finally, the <code>before</code> operator: | ||
| + | --> | ||
| + | И, оператор <code>before</code>: | ||
assert always req -> next (ack before grant); | assert always req -> next (ack before grant); | ||
| + | <!-- | ||
This asserts that whenever <code>req</code> is true, <code>ack</code> must be true at least once in the period starting in the following cycle and ending in the last cycle before <code>grant</code> is true. There are no obligations on the value of <code>ack</code> in the cycle in which <code>req</code> goes true, nor in the cycle in which <code>grant</code> goes true. There is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> need not go true either. In other words, following a <code>req</code> both <code>ack</code> and <code>grant</code> could remain false indefinitely. | This asserts that whenever <code>req</code> is true, <code>ack</code> must be true at least once in the period starting in the following cycle and ending in the last cycle before <code>grant</code> is true. There are no obligations on the value of <code>ack</code> in the cycle in which <code>req</code> goes true, nor in the cycle in which <code>grant</code> goes true. There is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> need not go true either. In other words, following a <code>req</code> both <code>ack</code> and <code>grant</code> could remain false indefinitely. | ||
| + | --> | ||
| + | Смысл заключается в том, что когда бы <code>req</code> не принимал значение "правда", <code>ack</code> должен принять значение "правда" по крайней мере один раз в период, начиная со следующего цикла и заканчивая последним циклом,перед тем, как <code>grant</code> примет значение "правда". Не существует обязательного значения для <code>ack</code> ни в цикле, в котором <code>req</code> принимает значение "правда", ни в цикле, в котором <code>grant</code> принимает значение "правда". Не существует никаких правил, по которым <code>grant</code> должен, когда-либо принимать значение "правда", следуя за <code>req</code>, в это случае <code>ack</code>, также, не должен принимать этого значения. Другими словами, следуя за <code>req</code>, и <code>ack</code>, и <code>grant</code> могут оставаться в значении "ложь" неопределенное время. | ||
==Strong Operators and Liveness Properties== | ==Strong Operators and Liveness Properties== | ||
Версия 20:26, 17 сентября 2013
- 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. вкус напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
Язык 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 чувствительны к регистру. Как вы уже могли заметить, операторы разделяются ;.
Простые свойства
Простейшая форма свойства в PSL представляет собой комбинационное булево условие, которое должно быть непрерывно правдивым.
assert always CONDITION;
Однако, эта форма свойств практически не используется, т.к. является уязвимой для многих возможных рисков. Наиболее основным является представление разделенных событий или часов.
assert (always CONDITION) @(posedge clk);
Также возможно определить часы по умолчанию и таким образом избежать потребности в повторении явного оператора времени @ для каждого отдельного утверждения.
default clock = (posedge clk); assert always CONDITION;
Основным, для свойств, остается принятие формы импликации, с предварительным условием, которое должно быть выполнено до того, как основное условие будет проверено.
assert always PRECONDITION -> CONDITION;
Утверждение PRECONDITION должно поддерживаться всегда, CONDITION должно поддерживаться в этом же цикле. Символ -> обозначает логическую импликацию.
В общем (хотя это и необязательно) для предварительного условия и основного условия, в пределах утверждения, используется форма временной последовательности заключенной в фигурные скобки.
assert always {a;b} |-> {c;d};
Последовательность {a;b} удерживается в цикле, если a, и имеет место в следующем цикле, если b. Символ |->, находящийся между двумя последовательностями, обозначает окончание импликации, это значит, что если первая последовательность удерживается, то вторая также удерживается, две последовательности совмещаются одним циклом.
В итоге для свойств включающих временные условия (таких как сброс), которые могут прерывать свойства в любой момент временной последовательности.
assert (always ({a;b} |-> {c;d} abort reset))
@(posedge clk);
Когда сброс принимает значение правда, обязательство удержания окончания импликации удаляется, и проверяется наличие совпадений между свойством и актуальным состоянием проекта.????
Временная логика
Временные операторы фундаментального языка предоставляют syntactic sugaring для верхнего уровня LTL-операторов. Эти временные операторы включают в себя always, never, next, until and before, среди прочих. О значении операторов можно догадаться интуитивно, но здесь есть некоторые сюрпризы.
Оператор always выполняется, если его операнды выполняются в каждом отдельном цикле, в то время как оператор never выполняется, если его операнд не выполняется в каждом отдельном цикле. Оператор next выполняется, если его операнд выполняется в цикле, который немедленно следует, после текущего. Следовательно утверждение
assert always req -> next grant;
означает, что когда бы HDL-сигнал req не принимал значение "правда", HDL-сигнал grant должен принимать значение "правда" в следующем цикле. Цикл имеет типичное представление обозначенное часами по умолчанию или включая оператор времени с течением свойства. Следует отметить, что когда req принимает значение "правда", то это утверждение ничего не говорит о значении grant в любом другом цикле,кроме последующего. Также ничего не говорит о значении grant, когда req принимает значение "ложь". Это говорит лишь о том, что когда бы req не принимало значение "правда", всегда найдется случай, в котором grant примет значение "правда" уже на следующем цикле.
Оператор next может использовать число циклов,как аргумент, заключенный в квадратные скобки:
assert always req -> next[2] (grant);
Это значит, что когда бы req не принимал значение "правда", grant примет, также, значение "правда" через два цикла. Это ничего не говорит, о значении grant через один цикл, после того, как req приняло значение "правда". Интересная особенность этого утверждения заключается в том, что оно имеет место в каждом отдельном цикле, так если бы req имел значение "правда" три подряд цикла, то и grant должен держать значение "правда" три цикла, но с задержкой в два цикла. Если это утверждение реализовать,как проверку моделирования, то оно будет повторно вызываться каждый раз когда, req будет принимать значение "правда", таким образом эти одновременные вызовы проверки моделирования являются эффективным конвейером.
Смысл оператора until немного более хитрый:
assert always req -> next (ack until grant);
Это утверждает, что когда бы req не принимал значение "правда", ack принимает значение "правда" в следующем цикле и остается в этом значении до первой последовательности циклов, в которых grant принимает значение "правда". Нету обязательного значения ack в цикле, в котором grant принимает значение "правда",ни для какой последовательности циклов (кроме проверки,вызываемой req более одного раза). Если req принимает значение "правда", и затем grant принимает это же значение в следующем цикле, то ack вообще не должен принимать значение "правда". С другой стороны, не существует обязательств для grant когда-либо принимать значение "правда" следуя за req, в это случае ack будет иметь значение "правда" неопределенное время.
Цикл, в котором левый операнд until вызывается первым, определен контекстом, в котором этот оператор появился. В пример выше, ack должен принимать значение "правда" в цикле, после того, как req примет значение "правда".
И, оператор before:
assert always req -> next (ack before grant);
Смысл заключается в том, что когда бы req не принимал значение "правда", ack должен принять значение "правда" по крайней мере один раз в период, начиная со следующего цикла и заканчивая последним циклом,перед тем, как grant примет значение "правда". Не существует обязательного значения для ack ни в цикле, в котором req принимает значение "правда", ни в цикле, в котором grant принимает значение "правда". Не существует никаких правил, по которым grant должен, когда-либо принимать значение "правда", следуя за req, в это случае ack, также, не должен принимать этого значения. Другими словами, следуя за req, и ack, и grant могут оставаться в значении "ложь" неопределенное время.
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.
