PSL/IEEE Standard 1850-2010 for Property Specification Language (PSL)
- Литература
- IEEE Std 1850-2010
- Embedded PSL in VHDL (en)
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
1. Обзор
1.1 Возможность
Этот стандарт определяет язык свойств спецификации (PSL), который формально описывает поведение электронных систем. Этот стандарт специфицирует синтаксис и семантику для PSL, а также разъясняет, как PSL взаимодействует с различными стандартами языков описания электронных систем.
1.2 Назначение
Назначение этого стандарта заключается в том, чтобы предоставить четкий язык для формальной спецификации поведения электронных систем, который будет совместим с множеством языков описания электронных систем, включая IEEE Std 1076TM (VHDL®),1 IEEE Std 1364TM (Verilog®), IEEE Std 1800TM (SystemVerilog®), и IEEE Std 1666TM (SystemC®), способствуя общему потоку верификации и спецификации для проектов описанных на разных и смешанных языках.
Этот стандарт создает обновленный IEEE стандарт базирующийся на IEEE Std 1850-2005. Обновленный стандарт усовершенствует IEEE стандарт, адресные опечатки, незначительные технические вопросы и предполагаемого расширения непосредственно связанных свойств, для дальнейшего использования и облегчения моделирования.
1.2.1 Происхождение
Сложность проектов с очень большой степенью интеграции (VLSI) выросла до такого уровня, что традиционные подходы начали достигать своего предела, а издержки верификации достигли 60%-70% от ресурсов разработки. Потребность в более продвинутой методологии верификации, с улучшенной наблюдаемостью поведения проекта и улучшенной контролируемостью (способностью контроля) процесса верификации, стала критической. За последние 10 лет, методология, базирующаяся на понятии "свойств", была определена, как мощная парадигма верификации, которая способна обеспечить повышение производительности (эффективности), повышенное качество проекта, и значительно ускорить время выхода на рынок (time to market), увеличить число производителей (higher value to engineers?) и пользователей электронных продуктов. Свойства, используемые в данном контексте, являются краткие, декларативные/описательные (declarative), выразительные/ясные/точные (expressive) и однозначные спецификации желаемого поведения системы, которые используются для проведения процесса верификации. IEEE 1850 PSL стандартный язык для описания (спецификации) поведения электронной системы, используя свойства. PSL облегчает верификацию основанную на свойствах (property-based verification) с использованием как моделирования так и формальной верификации, что позволяет повысить эффективность функциональной верификации.
1.2.2 Мотивация
Обеспечение реализации проекта удовлетворяющей его спецификацию, является основным для верификации аппаратуры. Ключ к проекту и процессу верификации является законом спецификации. Исторически, процесс спецификации состоял из создания языкового описания набора требований к проекту. Эта форма спецификации неоднозначная, и во многих случаях неверифицируема в связи с отсутствием стандарта машинно-выполняемого представления. Кроме того, обеспечение, того чтобы все функциональные аспекты спецификации были адекватно верифицированы (т.е. покрыты), довольно проблематично.
IEEE PSL был создан, чтобы устранить эти недостатки. Это дает архитектуре проекта стандарт, означающий спецификацию свойств проекта используемых краткий синтаксис с простой формальной семантикой. Аналогичным образом, позволяется RTL-исполнителю определить цели проекта в проверяемых формах, пока разрешается верификации подтвердить, что выполнение окончено и его спецификация определена через динамическую ( моделирование) и статическую (формальную) верификацию. Более того, он предоставляет средства для определения качества процесса верификации, через создание полной функциональной модели построения на формально специфицированных свойствах. В дополнение, он предоставляет стандартные средства для аппаратуры проекта и инженера верификации при создании строгой и исполняемой машиной спецификации проекта.
1.2.3 Цели
PSL был специально создан для исполнения следующих общих аппаратных функциональных требований:
- Легко обучать, чиать и писать
- Краткий синтаксис
- Строго определенная формальная семантика
- Выразительная мощность, позволяющая специфицировать большие классы реальных проектов
- Известные эффективные алгоритмы моделирования, такие же как формальная верификация
1.3 Использование
PSL язык для формальной спецификации аппаратуры. Он используется для описания свойств, которые требуют поддержки в проекте под верификацию. PSL предоставляет средства для написания спецификаций, которые легко читаются и математически точны. Это предназначение используется для функциональной спецификации, с одной стороны, и как вход в программы функциональной верификации, с другой. Таким образом, спецификация PSL - это исполняемая спецификация для аппаратного проекта.
1.3.1 Функциональная спецификация
PSL может использоваться для выделения требований относительно общего поведения проекта, также как допущения о среде, в которой ожидается обработка проекта. PSL также может выделять внутреннее поведение требований и допущений, которые возникают в процессе обработки проекта. Доступными являются более эффективная функциональная верификация и продолжения обработки самого проекта.
Один из важных аспектов использования PSL - это использование для документации, как вместо, так и совместно с английской спецификацией. Спецификация PSL может описать простые инварианты (например: сигналы read_enable и
write_enable никогда не используются в одно время), также как многотактовое поведение (например: правильное поведение интерфейса с поддержкой протокола шины или правильное поведение конвейерных операций).
Спецификация PSL состоит из утверждений относительно свойства проекта под набором допущений. Свойство строится из трех видов элементов: Булевы выражения, которые описывают поведение в одно цикле; последовательные выражения, которые могут описывать многотактовое поведение; и временные операторы, которые описывают временные взаимоотношения между Булевыми выражениями и последовательностями. Например, Булево выражение в Verilog:
ena || enb
Это выражение описывает цикл, в котором, по крайней мере, один из сигналов ena и enb активен. Последовательное выражение PSL
{req; ack; !cancel}
описывает последовательность циклов, такую, что если req активен в первом цикле, ack активен во втором цикле, а cancel неактивен в третьем цикле. Следующее свойство получается, применяя временные операторы always и |=> к этим выражениям,
always {req;ack;!cancel} |=> (ena || enb)
это значит, что всегда (в каждом цикле), если встречается последовательность {req;ack;!cancel}, то либо ena, либо enb активен в течение цикла после окончания последовательности. Добавляя директиву assert следующей:
assert always {req;ack;!cancel} |=> (ena || enb);
завершается спецификация, указывая, что это свойство ожидается в проекте и что потребности это ожидания нужно верифицировать.
1.3.2 Функциональная верификация
PSL также может использоваться, как вход для программ верификации, как для верификации моделированием, так и для формальной верификации, используется проверка модели или теоретическое доказательство. Каждый вариант обсуждается в следующих пунктах.
1.3.2.1 Моделирование
Спецификация PSL также может использоваться для автоматического генерирования проверок поведения моделирования. Это может быть реализовано, например, прямой интеграцией проверок в программе моделирования; интерпретацией свойств PSL в тестовую автоматизированную программу, которая сопровождает симулятор; генерированием HDL контроллеров, которые моделируются рядом с проектом; или анализом путей пройденных во время моделирования.
Например, следующие PSL свойства:
Свойство 1: always (req -> next !req)
означает, что сигнал req пульсирующий сигнал, т.е. если он принимает высокие значения в одном цикле,то он примет низкие значения в следующем цикле. Такое свойство может быть легко проверенно, используя проверки моделирования, написанные на каком-нибудь HDL, который имеет функциональность конечного автомат (FSM), показанный на Рисунке 1.
|
|---|
| Рисунок 1—Простой FSM, который проверяет свойство 1 |
Для более сложных свойств, чем то что представлено на рисунке 1, писать вручную соответствующие проверки - это кропотливый труд, подверженный ошибкам, и содержание набора таких проверок для постоянно изменяющегося проекта - это очень трудоемкое задание. Вместо этого, спецификация PSL может использоваться, как вход для программы, которая автоматически генерирует проверки, поддающиеся моделированию.
Хотя в принципе, все свойства PSL могут быть проверены при окончание моделирования, исполнение проверок, часто, значительно проще для подмножеств, называемых простые подмножества PSL. Неформально, в этих подмножествах, состав временных свойств ограничен для обеспечения того, что бы время двигалось вперед слева направо через свойство, как это делается на временной диаграмме. (Смотрите 4.4.4 для формального понимания простых подмножеств.)
Например, свойство
Свойство 2: always (a -> next[3] b)
которое означает, что если a принимает значения, то b примет значение через три цикла, принадлежит простому подмножеству, потому что a появляется слева от b в свойстве и, также, появляется слева от b на временной диаграмме любой поведенческой модели, что не нарушает свойство. Рисунок 2 показывает пример такой временной диаграммы.
|
|---|
| Рисунок 2—Вариант удовлетворяющий свойство 2 |
Пример свойства не принадлежащего этому подмножеству
Свойство 3: always ((a && next[3] b) -> c)
которое значит, что если a принимает значение и b принимает значение через три цикла, то c принимает значение в том же цикле, что и a. Это свойство не принадлежит простому подмножеству, потому что хотя c появляется справа от a и b в свойстве, он появляется слева от b и a на временной диаграмме, и это не нарушает свойство. Рисунок 3 показывает пример такой временной диаграммы.
|
|---|
| Рисунок 3 3—Вариант, удовлетворяющий свойство 3 |
1.3.2.2 Формальная верификация
PSL это расширение стандарта временной логики Линейной временной логике (LTL) и Вычисляемого логического дерева (CTL). Спецификация в PSL фундаментального языка (соответственно, PSL дополнительного ветвления) может быть скомпилирована в виде чистого LTL (соответственно, CTL), возможно с некоторым вспомогательным HDL- кодом, известным, как спутник.
3. Определения, сокращения и аббревиатуры
<-- For the purposes of this document, the following terms and definitions apply. The IEEE Standards Diction- ary: Glossary of Terms & Definitions should be referenced for terms not defined in this clause.6 --> Цели этого документа - текущие термины и определения. IEEE словарь стандартов: Cловарь терминов и определений должен ссылаться на условия неопределенные в этом пункте.6
3.1 Определения (Definitions)
Этот подпункт определяет термины, используемые в этом стандарте.
утверждение (assertion): значит, что данное свойство требуется выполнить и указать программе функциональной верификации, чтобы убедиться, что оно выполняется.
допущение (assumption): значит, что проект ограничен данным свойством и программе функциональной верификации указывается учитывать только тот путь, на котором данное свойство выполняется.
асинхронное свойство (asynchronous property): Свойство, временной контекст которого эквивалентен значению Правда.
поведение (behavior): Путь.
Булевы (выражения) (Boolean (expression)): Выражения, которые принимают на выходе логические значения.
проверка (checker): Вспомогательный процесс (обычно применяемый, как конечный автомат), который проверяет моделирование проекта и сообщения об ошибках, когда утвержденное свойство не выполняется. Проверка может быть представлена в том же HDL-коде, что и проект или в какой-либо другой форме, которая может ссылаться на моделирование проекта.
завершение (completes): Термин используемый для определения последнего цикла пути, который удовлетворяет последовательности выражений или свойств.
вычисленный путь (computation path): Правопреемство состояний проекта, такое что проект может актуально переходить из каждого состояния на пути к его преемнику.
ограничение (constraint): Состояние ( обычно для входного сигнала), которое ограничивает набор поведений, которые следует рассматривать. Ограничение может представлять реальные требования (т.е. временные требования) в среде, в которой используется проект, или может представлять искусственные ограничения (т.е. настройки режима) наложенные в порядке разделения задания функциональной верификации.
счетчик (count): Число или диапазон.
зона покрытия (coverage): Мера возникновения определенного поведения в течение (обычно динамическое) функциональной верификации и поэтому расчет сложности (динамического) процесса функциональной верификации.
цикл (cycle): Оценочный цикл.
описания (describes): Термин, используемый для определения набора поведений, для которого Булевы выражения, последовательные выражения или выполняемые свойства.
проект (design): Модель кусочка аппаратуры, описанная на некотором языке описания аппаратуры (HDL). Проект типично включает в себя набор входов, выходов, элементов состояния и комбинационных функций, которые рассчитывают следующие состояние и выходы из текущего состояния и входов.
поведение проекта (design behavior): Рассчитанный путь для данного проекта.
динамическая верификация (dynamic verification): Процесс верификации, такой как моделирование, в котором свойство проверяется отдельно, конечные поведения проекта, которые обычно получаются динамическим проведением проекта через конечное число оценочных циклов. В общем, динамическая верификация не дает вывода о выполняющемся свойстве поведения, через которое свойство еще не было проверено.
оценка (evaluation): Процесс проведения проекта итеративным принятием значений на его входы, рассчитывая его следующие состояния и выходные значения, время опережения, и назначение переменных состояний и выходов своих следующих значений.
оценочный цикл (evaluation cycle): Одна итерация оценочного процесса. На одном оценочном цикле, состояние проекта пересчитывается ( и может быть изменено).
расширения (данного пути) (extension (of a given path)): Путь, который начинается с точного правопреемства состояний в данном пути.
- False — Интерпритация определённых значений определённых типов в HDL языках. В SystemVerilog и Verilog стилях, битовые значения 1’b0, 1 ’bx, и 1’bz интерпретируются как логическое значение False. В VHDL стиле, значения STD.Standard.Boolean’(False) и STD.Standard.Bit’(‘0’), также как значения IEEE.std_logic_1164.std_logic’( ‘0’), IEEE.std_logic_1164.std_logic’(‘L’), IEEE.std_logic_1164.std_logic’(‘X’), и IEEE.std_logic_1164.std_logic’(‘Z’) все интерпретируются как логическое значение False. В SystemC стиле, значение 'false' типа bool и любой литерал типа integer с числовым значением 0 интерпретируется как значение False. В GDL стиле, значение типа Boolean 'false' и значение типа bit 0B оба интерпретируются как логическое значение False.
конечный диапазон (finite range): Диапазон с большой конечной границей.
формальная верификация (formal verification): Процесс функциональной верификации, в котором анализ дизайна и выхода свойства логически разъясняет о выполняемое свойство для все поведений проекта. Если свойство продекларировано значение "правда" программой формальной верификации, моделирование не может сделать его значение "ложным". Если свойство не выполняется для каждого поведения, то процесс формальной верификации должен предоставить специфический контрпример свойства, если это возможно.
функциональная верификация (functional verification): Процесс подтверждения того, что для данного проекта и данного набора ограничений, свойство, которое требует выполнение в этом проекте, действительно выполняется в соответствие с данными ограничениями.
исполнение (holds): Термин используемый для разъяснения значения Булевых выражений, последовательных выражений или свойств.
обязательное исполнение(holds tightly): Термин используемый для разъяснения значения последовательных выражений. Последовательные выражения оцениваются на конечной стадии (поведение).
живучие свойства (liveness property): Свойства, которые указывают на случайность, которая не ограничена во времени. Грубо говоря, живучие свойства утверждает, что что-то “хорошее” в конечном счете произошло. Более формально, живучие свойство - это свойство, для которого любая конечная стадия может быть продолжена до стадии удовлетворения свойства. Например, свойство “когда-либо сигнал req принимает значение, сигнал ack принимает значение через некоторое время” это живучие свойство.
логический тип (logic type): Тип данных HDL, который включает значения, которые интерпретируются, как логические значения. Логический тип, также, включает значения, которые не интерпретируются, как логические значения. Как логический тип, обычно, представляет многозначную логику.
логическое значение (logical value): Значение из набора {True, False}.
проверка на модели (model checking): Тип формальной верификации.
число (number): Неотрицательное целочисленное значение, и статично подсчитанное выражение полученное, как выражение.
(occurs): Термин используемый для индикации того, что Булево выражение выполняется в данном цикле.
occurrence (of a Boolean expression): Цикл, в котором выполняется Булево выражение.
Стадия (путь) (path): Правопреемственность состояний проекта, ???
positive count: A positive number or a positive range.
positive number: A number that is greater than zero (0).
positive range: A range with a low bound that is greater than zero (0).
prefix (of a given path): A path of which the given path is an extension.
property: A collection of logical and temporal relationships between and among subordinate Boolean expressions, sequential expressions, and other properties that in aggregate represent a set of behaviors.
range: A series of consecutive numbers, from a low bound to a high bound, inclusive, such that the low bound is less than or equal to the high bound. In particular, this includes the case in which the low bound is equal to the high bound. Also, a pair of statically computable integer expressions specifying such a series of consecutive numbers, where the left expression specifies the low bound of the series, and the right expression specifies the high bound of the series. A range may describe a set of values or a variable number of cycles or event repetitions.
restriction: A statement that the design is constrained by the given sequential expression and a directive to functional verification tools to consider only paths on which the given sequential expression holds.
safety property: A property that specifies an invariant over the states in a design. The invariant is not necessarily limited to a single cycle, but it is bounded in time. Loosely speaking, a safety property claims that “something bad” does not happen. More formally, a safety property is a property for which any path violating the property has a finite prefix such that every extension of the prefix violates the property. For example, the property, “whenever signal req is asserted, signal ack is asserted within 3 cycles” is a safety property.
sequence: A sequential expression that may be used directly within a property or directive.
sequential expression: A finite series of terms that represent a set of behaviors. sequential extended regular expression: A form of sequential expression, and a component of a sequence.
starts: A term used to identify the first cycle of a path that satisfies a sequential expression.
strictly before: Before, and not in the same cycle as.
strong operator: A temporal operator, the non-negated use of which usually creates a liveness property.
temporal expression: An expression that involves one or more temporal operators.
temporal operator: An operator that represents a temporal (i.e., time-oriented) relationship between its operands.
terminating condition: A Boolean expression, the occurrence of which causes a property to complete.
terminating property: A property that, when it holds, causes another property to complete.
- True: Интерпритация определённых значений определённых типов в HDL языках.
- В SystemVerilog и Verilog стилях, битовые значение 1'b1 интерпретируется как логическое значение True.
- В VHDL стиле, значения STD.Standard.Boolean'(True), STD.Standard.Bit'('1'), IEEE.std_logic_1164.std_logic'('1'), и IEEE.std_logic_1164.std_logic'('H') интерпретируются как логическое значение True.
- В SystemC стиле, значение 'true' типа bool и любой литерал типа integer с ненулевым числовым значением интерпретируется как логическое значение True.
- В GDL стиле, значение типа Boolean 'true' и значение типа bit 1B интерпретируются как логическое значение True.
unknown value: A value of a (multi-valued) logic type, other than 0 or 1.
weak operator: A temporal operator, the non-negated use of which does not create a liveness property.
3.2 Acronyms and abbreviations
- ABV — assertion-based verification
- BNF — extended Backus-Naur Form
- cpp — C pre-processor
- CTL — computation tree logic
- EDA — electronic design automation
- FL — Foundation Language
- FSM — finite state machine
- GDL — General Description Language
- HDL — hardware description language
- iff — if and only if
- LTL — linear-time temporal logic
- PSL — Property Specification Language
- OBE — Optional Branching Extension
- RTL — Register Transfer Level
- SERE — Sequential Extended Regular Expression
- VHDL — VHSIC Hardware Description Language
- VHSIC — Very High Speed Integrated Circuit
4.1.1 Слои (Layers)
PSL состоит из четырёх слоёв: булевый (Boolean), временной (temporal), верификационный (verification), и модельный (modeling).
4.1.1.1 Булевый слой (Boolean layer)
Булевый слой используется для создания выражений, которые, в свою очередь, используются другими слоями. Хотя этот слой содержит выражения над многими типами, он называется как булевый слой, потому что он является поставщиком булевых (логических) выражений для основы (сердца) языка — временнОго слоя. Выражения булевого слоя выполняются в едином (одиночном) цикле выполнения.
4.1.1.2 ВременнОй слой (Temporal layer)
Временной слой является основой языка; он используется для описания свойств проекта. Он называется временным, потому что, в дополнение к простым свойствам, таким как "сигналы a и b являются взаимноисключающими", он может также описывать свойства включающие сложные временные отношения между сигналами, например "если сигнал c устанавливается, тогда сигнал d должен установиться прежде, чем сигнал e установится, но не позже более восьми периодов синхросигнала". ВременнЫе выражения выполняются в течении серии циклов выполнения.
4.1.1.3 Верификационный слой (Verification layer)
Верификационный слой используется для того чтобы сказать верификационному инструменту (САПР), что делать с свойствами описанными во временном слое. Например, верификационный слой включает директивы, которые говорят инструменту (САПР) чтобы верифицировал (verify) то, что свойство удерживает (hold) или проверил (check) то, что заданная последовательность покрыта некоторым тестирующим случаем.
4.1.1.4 Моделирующий слой (Modeling layer)
Моделирующий слой (Modeling layer) используется для моделирования поведения входов проекта (для инструментов (САПР), таких как инструменты (САПР) для формальной верификации, которые не используют тестов) и для моделирования дополнительной аппаратуры, которая не является частью проекта, но необходима для верификации.
4.1.2 Стили/Варианты (Flavors)
PSL идёт с пятью вариантами/стилями (flavors): один для каждого HDL языка SystemVerilog, Verilog, VHDL, SystemC, и GDL. Синтаксис каждого варианта (стиля) соответствует синтаксису соответствующего HDL языка в ряде конкретных областей — данный стиль PSL совместим с соответствующим синтаксисом HDL-языка в этой области.
| Слой | HDL | ||||
|---|---|---|---|---|---|
| SystemVerilog | Verolog | VHDL | SystemC | GDL | |
| Булевый |  |
|
|
|
|
| Модельный | |
|
|
|
|
| Временной | i:j | i:j | i to j | i:j | i..j |
4.2 Lexical structure
This subclause defines the identifiers, keywords, operators, macros, and comments used in PSL.
4.2.1 Идентификаторы (Identifiers)
Идентификаторы в PSL состоят из символа латинского алфавита, за которым следует ноль или более символов латинского алфавита; каждый последующий символ алфавита может по желанию предшествовать одному символу подчеркивания. Например:
mutex Read_Transaction L_123
PSL идентификаторы являются чувстительными к регистру в SystemVerilog, Verilog, и SystemC вариантах/стилях и не чувствительными к регистру в VHDL и GDL вариантах.
4.2.2 Ключевые слова
A |
sequence |
anda |
async_abort |
U |
G |
const |
vprop |
within |
- a and is a keyword only in the VHDL flavor; see the flavor macro AND_OP (4.3.2.6).
- b is is a keyword only in the VHDL flavor; see the flavor macro DEF_SYM (4.3.2.9).
- c not is a keyword only in the VHDL flavor; see the flavor macro NOT_OP (4.3.2.6).
- d or is a keyword only in the VHDL flavor; see the flavor macro OR_OP (4.3.2.6).
- e to is a keyword only in the VHDL flavor; see the flavor macro RANGE_SYM (4.3.2.7).
4.2.3 Операторы
4.2.3.1 Операторы HDL языка
Для заданного стиля PSL, операторы основного HDL языка имеют наивысший преоритет. В частности это включает логические, арифметические операторы и операторы отношения языка HDL. Логические операции HDL языка для отрицания, конъюнкции и дизъюнкции булевых (логических) значений могут использоваться в PSL для отрицания, конъюнкции и дизъюнкции свойств. В таких приложениях, эти операторы имеют их обычный приоритет и ассоциативность, как если бы PSL свойства,....
4.2.3.2 Foundation Language (FL) operators
Various operators are available in PSL. Each operator has a precedence relative to other operators. In general, operators with a higher relative precedence are associated with their operands before operators with a lower relative precedence. If two operators with the same precedence appear in sequence, then the operators are associated with their operands according to the associativity of the operators. Left-associative operators are associated with operands in left-to-right order of appearance in the text; right-associative operators are associated with operands in right-to-left order of appearance in the text.
| Operator class | Associativity | Operators | |
|---|---|---|---|
| (highest precedence)
HDL operators |
|||
| Union operator | left | union | |
| Clocking operator | left | @ | |
| SERE repetition operators | left | [* ] [+] [= ] [-> ] | |
| Sequence within operator | left | within | |
| Sequence AND operators | left | & | && |
| Sequence OR operator | left | | | |
| Sequence fusion operator | left | : | |
| Sequence concatenation operator | left | ; | |
| FL termination operator | left | abort sync_abort |
async_abort |
| FL occurrence operators | right | next* | eventually! |
| X X! | F | ||
| FL bounding operators | right | U | W |
| until* | before* | ||
| Sequence implication operators | right | |-> | |=> |
| Boolean implication operators | right | -> | <-> |
| FL invariance operators (lowest precedence) |
right | always G |
never |
NOTE—The notation next* represents the next family of operators, which includes the operators next, next!, next_a, next_a!, next_e, next_e!, next_event, next_event!, next_event_a!, and next_event_e!. The notation until* represents the until family of operators, which includes the operators until, until!, until_, and until!_. The notation before* represents the before family of operators, which includes the operators before, before!, before_, and before!_.7
4.2.3.2.1 Union operator
Для любого стиля PSL, FL опрератор со следующим наибольшим приоритетом после HDL опрераторов является тот, который используется для обозначения недетерминированного выражения:
union union оператор
Оператор union является лево-ассоциативным.
4.2.3.2.2 Clocking operator
For any flavor of PSL, the FL operator with the next highest precedence is the clocking operator, which is used to associate a clock expression with a property or sequence:
@ clock event
The clocking operator is left-associative.
4.2.3.2.3 SERE операторы повторов (repetition operators)
Для любого стиля PSL, FL операторы со следующим наибольшим приоритетом являются операторами повторов, которые используются для создания последовательных расширенных регулярных выражений (Sequential Extended Regular Expressions — SEREs). Эти операторы следующие:
[* ] последовательное повторение (consecutive repetition) [+] последовательное повторение (consecutive repetition) [= ] не последовательное повторение (non-consecutive repetition) [-> ] goto repetition
SERE операторы повторения являются лево-ассоциативными.
4.2.3.2.4 Sequence within operator
For any flavor of PSL, the FL operator with the next highest precedence is the sequence within operator, which is used to describe behavior in which one sequence occurs during the course of another, or within a time-bounded interval:
within sequence within operator
The sequence within operator is left-associative.
4.2.3.2.5 Sequence conjunction operators
For any flavor of PSL, the FL operators with the next highest precedence are the sequence conjunction operators, which are used to describe behavior consisting of parallel paths. These operators are as follows:
& non-length-matching sequence conjunction && length-matching sequence conjunction
Sequence conjunction operators are left-associative.
4.2.3.2.6 Sequence disjunction operator
For any flavor of PSL, the FL operator with the next highest precedence is the sequence disjunction operator, which is used to describe behavior consisting of alternative paths:
| sequence disjunction
The sequence disjunction operator is left-associative.
4.2.3.2.7 Sequence fusion operator
For any flavor of PSL, the FL operator with the next highest precedence is the sequence fusion operator, which is used to describe behavior in which a later sequence starts in the same cycle in which an earlier sequence completes:
: sequence fusion
The sequence fusion operator is left-associative.
4.2.3.2.8 Sequence concatenation operator
For any flavor of PSL, the FL operator with the next highest precedence is the sequence concatenation operator, which is used to describe behavior in which one sequence is followed by another:
; sequence concatenation
The sequence concatenation operator is left-associative.
4.2.3.2.9 FL termination operators
For any flavor of PSL, the FL operators with the next highest precedence are the FL termination operators, which are used to describe behavior in which a condition causes both current and future obligations to be canceled:
sync_abort immediate termination of current and future obligations, synchronous with the clock async_abort immediate termination of current and future obligations, independent of the clock abort equivalent to async_abort
The FL termination operators are left-associative.
4.2.3.2.10 FL occurrence operators
For any flavor of PSL, the FL operators with the next highest precedence are those used to describe behavior in which an operand holds in the future. These operators are as follows: eventually! the right operand holds at some time in the indefinite future
next* the right operand holds at some specified future time or range of future times
FL occurrence operators are right-associative.
4.2.3.2.11 Bounding operators
For any flavor of PSL, the FL operators with the next highest precedence are those used to describe behavior in which one property holds in some cycle or in all cycles before another property holds. These operators are as follows:
until* the left operand holds at every time until the right operand holds before* the left operand holds at some time before the right operand holds
FL bounding operators are right-associative.
4.2.3.2.12 Suffix implication operators
For any flavor of PSL, the FL operators with the next highest precedence are those used to describe behavior consisting of a property that holds at the end of a given sequence. These operators are as follows:
|-> overlapping suffix implication |=> non-overlapping suffix implication
The suffix implication operators are right-associative.
NOTE—The FL Property {r} (f) is an alternative form for (and has the same semantics as) the FL Property {r} |-> f.
4.2.3.2.13 Logical implication operators
For any flavor of PSL, the FL operators with the next highest precedence are those used to describe behavior consisting of a Boolean, a sequence, or a property that holds if another Boolean, sequence, or property holds. These operators are as follows:
-> logical IF implication <-> logical IFF implication
The logical IF and logical IFF implication operators are right-associative.
4.2.3.2.14 FL invariance operators
For any flavor of PSL, the FL operators with the next highest precedence are those used to describe behavior in which a property does or does not hold, globally. These operators are as follows:
always the right operand holds, globally never the right operand does NOT hold, globally
FL occurrence operators are right-associative.
4.2.3.3 Optional Branching Extension (OBE) operators
| Operator class | Associativity | Operators | |
|---|---|---|---|
| (highest precedence) HDL operators |
|||
| OBE occurrence operators | left | AX AG AF A [ U ] |
EX EG EF E [ U ] |
| Boolean implication operators (lowest precedence) |
right | -> | <-> |
4.2.3.3.1 OBE occurrence operators
For any flavor of PSL, the OBE operators with the next highest precedence after the HDL operators are those used to specify when a subordinate property is required to hold, if the parent property is to hold. These operators include the following:
AX on all paths, at the next state on each path AG on all paths, at all states on each path AF on all paths, at some future state on each path EX on some path, at the next state on the path EG on some path, at all states on the path EF on some path, at some future state on the path A[U] on all paths, in every state up to a certain state on each path E[U] on some path, in every state up to a certain state on that path
The OBE occurrence operators are left-associative.
4.2.3.3.2 OBE implication operators
For any flavor of PSL, the OBE operators with the next highest precedence are those used to describe behavior consisting of a Boolean or a property that holds if another Boolean or property holds. These operators are:
-> logical IF implication <-> logical IFF implication
The logical IF and logical IFF implication operators are right-associative.
4.2.4 Macros
PSL provides macro processing capabilities that facilitate the definition of properties. SystemC, VHDL, and GDL flavors support cpp pre-processing directives (e.g., #define, #ifdef, #else, #include, and #undef). SystemVerilog and Verilog flavors support Verilog compiler directives (e.g., `define, `ifdef, `else, `include, and `undef). All flavors also support PSL macros %for and %if, which can be used to conditionally or iteratively generate PSL statements. The cpp or Verilog compiler directives shall be interpreted first, and PSL %if and %for macros shall be interpreted second.
4.2.4.1 The %for construct
4.2.4.2 The %if construct
4.2.5 Комментарии
PSL обеспечивает возможность вставки комментариев в PSL спецификацию. Для каждого стиля, возможность комментариев совместима с тем, что обеспечивается соответсвующией средой PSL.
Для SystemC, SystemVerilog, и Verilog стиля, оба варианта блочных комментариев (/* .... */) и (// .... <eol>) поддерживается. (<eol> — конец строки)
Для стиля VHDL, поддерживается комментарии (-- .... <eol>).
Для стиля GDL, оба блочных стилей комментариев поддерживаются: (/* .... */) и (-- .... <eol>).
4.3 Syntax
4.3.1 Conventions
| Flavor Macro | SystemVerilog | Verilog | VHDL | SystemC | GDL |
|---|---|---|---|---|---|
| AND_OP | && | && | and | && | & |
| OR_OP | || | || | or | || | | |
| NOT_OP | ! | ! | not | ! | ! |
| RANGE_SYM | : | : | to | : | .. |
| MIN_VAL | 0 | 0 | 0 | 0 | null |
| MAX_VAL | $ | inf | inf | inf | null |
| LEFT_SYM | [ | [ | ( | [ | ( |
| RIGHT_SYM | ] | ] | ) | ] | ) |
| DEF_SYM | = | = | is | = | := |
4.4 Semantics
The following subclauses introduce various general concepts related to temporal property specification and explain how they apply to PSL.
