PSL/IEEE Standard 1850-2010 for Property Specification Language (PSL)

Ссылки сюда (20) →

PSL

• The Designer's Guide To PSL (ru)

---

Литература

• Литература
• IEEE Std 1850-2010
• Embedded PSL in VHDL (en)

Введение в PSL

• 1. Introduction (en)
• 2. Basic Temporal Properties (en)
• 3. Some Philosophy (en)
• 4. Weak vs. Strong Temporal Operators (en)
• 5. SERE Style (en)

---

• Словарь терминов
• Дневник
• История проекта

* VHDL * OS-VVM * Co-Simulation *

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): Положительное число или положительный диапазон.

положительное число (positive number): Число, которое больше нуля (0).

положительный диапазон (positive range): Диапазон с нижней границей большей нуля (0).

префикс (данной стадии) (prefix (of a given path)): Стадия в которую расширяется данная стадия.

свойство (property): Набор логических и временных взаимоотношений между и среди подчиненных Булевых выражений, последовательных выражений и других свойств, которые в совокупности представляют набор поведений.

диапазон (range): Набор последовательных чисел, от нижней до верней границы, включительно, такой, что нижняя граница меньше или равна верхней. В частности, это предполагает случай, в котором нижняя граница эквивалентна верхней. Также, пара статически подсчитанных целочисленных выражений представляются, как наборы последовательных чисел, где левая выражения является нижней границей, а правое выражение верхней границей набора. Диапазон может описывать набор значении и переменное число циклов или повторяющихся событий.

ограничение (restriction): Утверждение, что проект ограничивается данным последовательным выражением, и директива программе функциональной верификации рассматривать только стадию, на которой выполняется данное последовательное выражение.

защищенное свойство (safety property): Свойство, которое указывает инвариантность по состояниям в проекте. Инвариантность - это необязательно ограниченность в один цикл, но ограниченность по времени. Грубо говоря, защищенное свойство показывает, что ничего “плохого” не произошло. Более формально, защищенное свойство - это свойство, для которого любая стадия имеющая навязывающееся свойство получает конечный префикс, такой ,что каждое расширение префикса навязывается свойству. Например, свойство “когда-либо сигнал req принимает значение, сигнал ack принимает значение через три цикла”, является защищенным свойством.

последовательность (sequence): Последовательное выражение, которое может напрямую использоваться в течение свойства или директивы.

последовательное выражение (sequential expression): Законченный набор терминов, который представляет набор поведений.

последовательные регулярно расширяемые выражения (sequential extended regular expression): Форма последовательных выражений и компонентов последовательностей.

начало (starts): Термин используемый для идентификации первого цикла пути, который удовлетворяет последовательное выражение.

строго перед (strictly before): Перед, и не в этом же цикле.

сильный оператор (strong operator): Временной оператор, неотрицательное использование которого, обычно, создает живучие свойства.

временное выражение (temporal expression): Выражение, которое включает один или более временных операторов.

временной оператор (temporal operator) Оператор, который представляет временные ( т.е. ориентированные во времени) взаимоотношения между операндами.

условие завершения (terminating condition): Булево выражение, появление которого, приводит к завершению свойства.

свойство завершения (terminating property): Свойство, выполнение которого, приводит к завершению другого свойства.

• 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): Значение (многозначного) логического типа, отличное от 0 и 1.

слабый оператор (weak operator): Временной оператор, неотрицательное использование которого не создает живучего свойства.

3.2 Сокращения и аббревиатуры

• ABV — утверждения, базирующиеся на верификации
• BNF — расширенная форма Бакуса-Наура
• cpp — C препроцессор
• CTL — вычисляемое логическое дерево
• EDA — авторматизация проектирования
• FL — фундаметальный язык
• FSM — конечный автомат
• GDL — общий язык описания
• HDL — язык описания аппаратуры
• iff — если, и только если
• LTL — линейная временная логика
• PSL — язык спецификации свойств
• OBE — дополнительное расширение ветвления
• RTL — уровень регистровых передач
• SERE — последовательное расширенное регулярное выражение
• VHDL — VHSIC язык описания аппаратуры
• VHSIC — высоко скоростная интегральная схема

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-языка в этой области.

Влияние стиля на слои PSL

Слой	HDL
	SystemVerilog	Verolog	VHDL	SystemC	GDL
Булевый
Модельный
Временной	i:j	i:j	i to j	i:j	i..j

4.2 Лексическая структура

Этот подпункт определяет идентификаторы, ключевые слова, операторы, макросы и комментарии, используемые в PSL.

4.2.1 Идентификаторы (Identifiers)

Идентификаторы в PSL состоят из символа латинского алфавита, за которым следует ноль или более символов латинского алфавита; каждый последующий символ алфавита может по желанию предшествовать одному символу подчеркивания. Например:

mutex
Read_Transaction
L_123

PSL идентификаторы являются чувстительными к регистру в SystemVerilog, Verilog, и SystemC вариантах/стилях и не чувствительными к регистру в VHDL и GDL вариантах.

4.2.2 Ключевые слова

A  E  next!  rose AF  EF  next_a AG  EG  next_a!

sequence AX abort  EX  next_e  stable always  ended  next_e! string

anda  eventually!  next_event  strong assert  next_event!  sync_abort assume  F  next_event_a

async_abort fairness  next_event_a!  toe before  fell  next_event_e before!  for  next_event_e!

U before!_  forall  nondet  union before_  nondet_vector  until bitvector  bit

G  notc  until! boolean  numeric  until!_ hdltype until_ clock  onehot

const  in  onehot0  vmode countones  inf  ord  vpkg cover  inherit

vprop isb  property  vunit default  isunknown  prev W report mutable

within restrict restrict! never  X next  X!

• 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 Операторы фундаментального языка

Различные операторы доступны в PSL. Каждый оператор имеет приоритет по отношению к другим операторам. В общем операторы с большим приоритетом получают доступ к свои операндам, раньше, чем операнды с меньшим приоритетом. Если два оператора имеют одинаковый приоритет и появляются в последовательности, то они получают доступ к свои операндам в соответствие с ассоциативностью операторов. Лева-ассоциативные оператор получает доступ к своим операндам слева на право в порядке появления в тексте, право-ассоциативные операторы получают доступ к своим операндам справа на лева в порядке появления в тексте.

Таблица приоритетов и ассоциативности двух операторов фундаментального языка

Оператор класс	Ассоциативность	Операторы
(наивысший приоритет) HDL операторы
Оператор объединения	left	union
Оператор времени	left	@
SERE повторяющийся оператор	left	[* ] [+] [= ] [-> ]
Последовательный предельный оператор	left	within
Последовательный оператор И	left	&	&&
Последовательный оператор ИЛИ	left	|
Последовательный оператор слияния	left	:
Последовательный оператор конкатенации	left	;
Операторы прерывания фундаментального языка	left	abort sync_abort	async_abort
Операторы фундаментального языка, указывающие местонахождение	right	next*	eventually!
		X X!	F
Операторы фундаментального языка, показывающие границы	right	U	W
		until*	before*
Последовательный оператор импликации	right	|->	|=>
Булевы операторы импликации	right	->	<->
Неизменные операторы фундаментального языка (низший приоритет)	right	always G	never

Примечание - Обозначение next* представляет семейство next-операторов, которое включает операторы: next, next!,
next_a, next_a!, next_e, next_e!, next_event, next_event!, next_event_a! и
next_event_e!. Обозначение until* представляет семейство until-операторов, которое включает операторы: until,
until!, until_ и until!_. Обозначение before* представляет семейство before-операторов, которое включает операторы: before, before!, before_, and before!_.7

4.2.3.2.1 Объединительные операторы

Для любого стиля PSL, FL оператор со следующим наибольшим приоритетом после HDL операторов является тот, который используется для обозначения недетерминированного выражения:

union   union оператор

Оператор union является лева-ассоциативным.

4.2.3.2.2 Операторы времени

Для любого варианта PSL, оператор фундаментального языка со следующим наивысшим приоритетом - это оператор времени, который используется для связи временного выражения со свойством или последовательностью:

@   clock event

Временной оператор лева-ассоциативный.

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 Последовательный предельный оператор

Для любого варианта PSL, оператор фундаментального языка со следующим наивысшим приоритетом - это последовательный предельный оператор, который используется для описания поведения, в котором одна последовательность появляется в ходе другой, или в пределах интервала ограниченного временем.

within    последовательность within оператор

Последовательный предельный оператор лева-ассоциативный.

4.2.3.2.5 Последовательные операторы конъюнкции

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетов - это последовательные операторы конъюнкции, которые описывают поведение состоящие из параллельных стадий. Это следующие операторы:

&    последовательная конъюнкция без сопоставления длинны
&&   последовательная конъюнкция с сопоставлением длины

Последовательные операторы конъюнкции лева-ассоциативные.

4.2.3.2.6 Последовательный оператор дизъюнкции

Для любого варианта PSL, оператор фундаментального языка со следующим наивысшим приоритетом - это последовательный оператор дизъюнкции, который используются для описания поведения состоящего из альтернативных стадий:

|    последовательная дизъюнкция

Последовательный оператор дизъюнкции лева-ассоциативный.

4.2.3.2.7 Последовательный оператор слияния

Для любого варианта PSL, оператор фундаментального языка со следующим наивысшим приоритетом - это последовательный оператор слияния, который используется для описания поведения, в котором более поздняя последовательность начинает выполняться в том же цикле, в котором заканчивает выполняться более ранняя.

:    последовательное слияние

Последовательный оператор слияния лева-ассоциативный.

4.2.3.2.8 Последовательный оператор конкатенации

Для любого варианта PSL, оператор фундаментального со следующим наивысшим приоритетом - это последовательный оператор конкатенации, который используется, чтобы описывать поведение, в котором одна последовательность следует за другой:

;    последовательная конкатенация

Последовательный оператор конкатенации лева-ассоциативный.

4.2.3.2.9 Операторы прерывания фундаментального языка

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом - это операторы прерывания фундаментального языка, которые используются для описания поведения, в котором условие вызывает текущие и будущие процессы, которые будут прерваны:

sync_abort    немедленное завершение текущего и следующего процесса, синхронизовано по времени
async_abort   немедленное прерывание текущего и следующего процесса, независт от времени
abort         эквивалентно to async_abort

Операторы прерывания фундаментального языка лева-ассоциативные.

4.2.3.2.10 Операторы местонахождения фундаментального языка

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, в котором операнды используются в будущем. Это следующие операторы: eventually! правый операнд выполняется через некоторое время в неопределенном будущем

next*     правый операнд выполняется в некотором специфицированном будущем времени или диапазоне будущего времени

операторы местонахождения фундаментального языка право-ассоциативные.

4.2.3.2.11 Граничные операторы

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые описывают поведение, в котором одно свойство выполняется в некотором цикле или во всех циклах перед выполнением следующего слова. Это следующие операторы:

until* левый операнд выполняется в любое время до выполнения правого операнда before* левый операнд выполняется через некоторое время после выполнения правого

Граничные операторы фундаментального языка право-ассоциативные.

4.2.3.2.12 Суффиксные операторы импликации

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, состоящего из свойства, которое выполняется в конце данной последовательности. Это следующие операторы:

|->    суффиксная импликация с перекрытием
|=>    суффиксная импликация без перекрытия

Операторы суффиксной импликации право-ассоциативные.

Примечание - Свойство фундаментального языка {r} (f) - это альтернативная форма (и имеет такую же семантику) для свойства фундаментального языка {r} |-> f.

4.2.3.2.13 Операторы логической импликации

Для любого варианта PSL, операторый фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, состоящего из Булевых выражений, последовательности или свойства, которое выполняется, если выполняется другое Булево выражение, последовательность или свойство.

->    логическая IF импикация
<->   логическая IFF импликация

Операторы логической импликации право-ассоциативные.

4.2.3.2.14 Операторы неизменности фундаментального языка

Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, в котором выполняется или не выполняется глобально.

always   правый операнд выполняется глобально
never    правый операнд не выполняется глобально

Операторы неизменности фундаментального языка право-ассоциативные.

4.2.3.3 Операторы дополнительного расширенного ветвления (OBE)

Таблица 3—OBE оператор, приоритет и ассоциативность

Класс оператора	Ассоциативность	Операторы
(наивысший приоритет) HDL операторы
OBE операторы местонахождения	left	AX AG AF A [ U ]	EX EG EF E [ U ]
Операторы Булевой импликации (низший приоритет)	right	->	<->

4.2.3.3.1 OBE операторы местонахождения

Для любого варианта PSL, OBE операторы являются следующими операторами с наивысшим приоритетом, после HDL операторов, они используются для указания, когда подчиненное свойство должно выполняться, если выполняется старшее свойство. Это следующие операторы:

AX    на всех путях, на следующем состоянии каждого пути
AG    на всех путях, на каждом состоянии любого пути
AF    на всех путях, на некотором будущем состоянии каждого пути
EX    на некотором пути, на следующем состоянии пути
EG    на некотором пути, на всех состояния пути
EF    на некотором пути , на некотором будущем состоянии пути
A[U]  на всех путях, в каждом состоянии до определенного состояния пути
E[U]  на некотором пути, в каждом состоянии до определенного состояния пути

OBE операторы местонахождения лева-ассоциативные.

4.2.3.3.2 OBE операторы импликации

Для любого варианта PSL, OBE операторы со следующим наивысшим приоритетом, это те которые используются для описания поведения, состоящего из Булевых выражений или свойства, которое выполняется, если Булево выражение или другое свойство выполняется. Это следующие операторы:

->   логическая IF импликация
<->  логическая IFF импликация

Операторы логической IF и логической IFF импликации право-ассоциативные.

4.2.4 Макросы

PSL предоставляет возможность обработки макросов, которые помогают в определении свойств. SystemC, VHDL и GDL варианты поддерживают cpp препроцессорные директивы (т.е. #define, #ifdef, #else, #include и #undef). SystemVerilog и Verilog поддерживают директивы Verilog компилятора (т.е. `define, `ifdef, `else, `include и `undef). Все варианты, также поддерживают PSL макросы %for и %if, которые могут использоваться для условно или итеративно генерированного PSL утверждения. Компилированные директивы Verilog или cpp должны быть интерпретированы первыми, макросы PSL %if и %for должны быть интепретированы вторыми

4.2.5 Комментарии

PSL обеспечивает возможность вставки комментариев в PSL спецификацию. Для каждого стиля, возможность комментариев совместима с тем, что обеспечивается соответсвующией средой PSL.

Для SystemC, SystemVerilog, и Verilog стиля, оба варианта блочных комментариев (/* .... */) и (// .... <eol>) поддерживается. (<eol> — конец строки)

Для стиля VHDL, поддерживается комментарии (-- .... <eol>).

Для стиля GDL, оба блочных стилей комментариев поддерживаются: (/* .... */) и (-- .... <eol>).

4.3 Синтаксис

4.3.1 Соответствия

Операнд	SystemVerilog	Verilog	VHDL	SystemC	GDL
И	&&	&&	and	&&	&
ИЛИ	||	||	or	||	|
НЕ	!	!	not	!	!
ДИАПАЗОН	:	:	to	:	..
МИНИМАЛЬНОЕ ЗНАЧЕНИЕ	0	0	0	0	null
МАКСИМАЛЬНОЕ ЗНАЧЕНИЯ	$	inf	inf	inf	null
ЛЕВАЯ ГРАНИЦА	[	[	(	[	(
ПРАВАЯ ГРАНИЦА	]	]	)	]	)
ПРИСВАИВАНИЕ	=	=	is	=	:=

4.4 Семантика

Следующие подпункты представляют различные общие концепции связанные со спецификацией временных свойств и пояснения того, как они применяются в PSL.