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 лет, методология, базирующаяся на понятие "свойства", была определена, как мощная парадигма верификации, которая способна обеспечивать повышение продуктивности, улучшить качество проекта, и значительно ускорить время производства, увеличить число производителей и пользователей электронных продуктов. Свойства, используемые в данном контексте, краткие, декларативные, определяющие выражение и недвусмысленную спецификацию желаемого поведения системы, которая для проведения процесса верификации. IEEE 1850 PSL языковой стандарт для спецификации поведения электронных систем, используя свойства. PSL способствует верификации базирующейся на свойствах, используя верификацию моделирования и формальную верификацию, тем самым позволяет повысить продуктивность в функциональной верификации.

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 Simulation

A PSL specification can also be used to automatically generate checks of simulated behavior. This can be done, for example, by directly integrating the checks in the simulation tool; by interpreting PSL properties in a testbench automation tool that drives the simulator; by generating HDL monitors that are simulated alongside the design; or by analyzing the traces produced during simulation.

For instance, the following PSL property:

Property 1: always (req -> next !req)

states that signal req is a pulsed signal, i.e., if it is high in some cycle, then it is low in the following cycle. Such a property can be easily checked using a simulation checker written in some HDL that has the functionality of the finite state machine (FSM) shown in Figure 1.

Figure 1—A simple (deterministic) FSM that checks Property 1

For properties more complicated than the property shown in Figure 1, manually writing a corresponding checker is painstaking and error-prone, and maintaining a collection of such checkers for a constantly changing design under development is a time-consuming task. Instead, a PSL specification can be used as input to a tool that automatically generates simulatable checkers.

Although in principle, all PSL properties can be checked for finite paths in simulation, the implementation of the checks is often significantly simpler for a subset called the simple subset of PSL. Informally, in this subset, composition of temporal properties is restricted to ensure that time moves forward from left to right through a property, as it does in a timing diagram. (See 4.4.4 for the formal definition of the simple subset.)

For example, the property

Property 2: always (a -> next[3] b)

which states that, if a is asserted, then b is asserted three cycles later, belongs to the simple subset, because a appears to the left of b in the property and also appears to the left of b in the timing diagram of any behavior that is not a violation of the property. Figure 2 shows an example of such a timing diagram.

Figure 2—A trace that satisfies Property 2

An example of a property that is not in this subset is the property

Property 3: always ((a && next[3] b) -> c)

which states that, if a is asserted and b is asserted three cycles later, then c is asserted (in the same cycle as a). This property does not belong to the simple subset, because although c appears to the right of a and b in the property, it appears to the left of b in a timing diagram that is not a violation of the property. Figure 3 shows an example of such a timing diagram.

Figure 3—A trace that satisfies Property 3

1.3.2.2 Formal verification

PSL is an extension of the standard temporal logics Linear-Time Temporal Logic (LTL) and Computation Tree Logic (CTL). A specification in the PSL Foundation Language (respectively, the PSL Optional Branching Extension) can be compiled down to a formula of pure LTL (respectively, CTL), possibly with some auxiliary HDL code, known as a satellite.

3. Definitions, acronyms, and abbreviations

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

3.1 Определения (Definitions)

This subclause defines the terms used in this standard.

утверждение (assertion): A statement that a given property is required to hold and a directive to functional verification tools to verify that it does hold.

assumption: A statement that the design is constrained by the given property and a directive to functional verification tools to consider only paths on which the given property holds.

asynchronous property: A property whose clock context is equivalent to True.

behavior: A path.

Boolean (expression): An expression that yields a logical value.

checker: An auxiliary process (usually constructed as a finite state machine) that monitors simulation of a design and reports errors when asserted properties do not hold. A checker may be represented in the same HDL code as the design or in some other form that can be linked with a simulation of the design.

completes: A term used to identify the last cycle of a path that satisfies a sequential expression or property.

computation path: A succession of states of the design, such that the design can actually transition from each state on the path to its successor.

constraint: A condition (usually on the input signals) that limits the set of behaviors to be considered. A constraint may represent real requirements (e.g., clocking requirements) on the environment in which the design is used, or it may represent artificial limitations (e.g., mode settings) imposed in order to partition the functional verification task.

count: A number or range.

coverage: A measure of the occurrence of certain behavior during (typically dynamic) functional verification and, therefore, a measure of the completeness of the (dynamic) functional verification process.

cycle: An evaluation cycle.

describes: A term used to identify the set of behaviors for which Boolean expression, sequential expression, or property holds.

design: A model of a piece of hardware, described in some hardware description language (HDL). A design typically involves a collection of inputs, outputs, state elements, and combinational functions that compute next state and outputs from current state and inputs.

design behavior: A computation path for a given design.

dynamic verification: A verification process such as simulation, in which a property is checked over indi- vidual, finite design behaviors that are typically obtained by dynamically exercising the design through a finite number of evaluation cycles. Generally, dynamic verification supports no inference about whether the property holds for a behavior over which the property has not yet been checked.

evaluation: The process of exercising a design by iteratively applying values to its inputs, computing its next state and output values, advancing time, and assigning to the state variables and outputs their next values.

evaluation cycle: One iteration of the evaluation process. At an evaluation cycle, the state of the design is recomputed (and may change).

extension (of a given path): A path that starts with precisely the succession of states in the 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: A range with a finite high bound.

formal verification: A functional verification process in which analysis of a design and a property yields a logical inference about whether the property holds for all behaviors of the design. If a property is declared true by a formal verification tool, no simulation can show it to be false. If the property does not hold for all behaviors, then the formal verification process should provide a specific counterexample to the property, if possible.

functional verification: The process of confirming that, for a given design and a given set of constraints, a property that is required to hold in that design actually does hold under those constraints.

holds: A term used to talk about the meaning of a Boolean expression, sequential expression, or property.

holds tightly: A term used to talk about the meaning of a sequential expression. Sequential expressions are evaluated over finite paths (behavior).

liveness property: A property that specifies an eventuality that is unbounded in time. Loosely speaking, a liveness property claims that “something good” eventually happens. More formally, a liveness property is a property for which any finite path can be extended to a path satisfying the property. For example, the prop- erty “whenever signal req is asserted, signal ack is asserted some time in the future” is a liveness property.

logic type: An HDL data type that includes values that are interpreted as logical values. A logic type may also include values that are not interpreted as logical values. Such a logic type usually represents a multi-val- ued logic.

logical value: A value in the set {True, False}.

model checking: A type of formal verification.

number: A non-negative integer value, and a statically computable expression yielding such a value.

occurs: A term used to indicate that a Boolean expression holds in a given cycle.

occurrence (of a Boolean expression): A cycle in which the Boolean expression holds.

path: A succession of states of the design, whether or not the design can actually transition from one state on the path to its successor.

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

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

Слой	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  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 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.

Table 2—FL operator precedence and associativity

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

Table 3—OBE operator precedence and associativity

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.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.