Просмотр исходного текста страницы PSL/IEEE Standard 1850-2010 for Property Specification Language (PSL)

{{PSL TOC}}


== 1. Обзор ==

=== 1.1 Возможность ===

<!--
This standard defines the property specification language (PSL), which formally describes electronic system
behavior. This standard specifies the syntax and semantics for PSL and also clarifies how PSL interfaces
with various standard electronic system design languages.
-->
Этот стандарт определяет язык свойств спецификации (PSL), который формально описывает поведение электронных систем. Этот стандарт специфицирует синтаксис и семантику для PSL, а также разъясняет, как PSL взаимодействует с различными стандартами языков описания электронных систем.

===1.2 Назначение===

<!--
The purpose of this standard is to provide a well-defined language for formal specification of electronic
system behavior, one that is compatible with multiple electronic system design languages, including IEEE
Std 1076TM (VHDL®),1 IEEE Std 1364TM (Verilog®), IEEE Std 1800TM (SystemVerilog®), and IEEE Std
1666TM (SystemC®), to facilitate a common specification and verification flow for multi-language and
mixed-language designs.
-->
Назначение этого стандарта заключается в том, чтобы предоставить четкий язык для формальной спецификации поведения электронных систем, который будет совместим с множеством языков описания электронных систем, включая IEEE Std 1076TM (VHDL®),1 IEEE Std 1364TM (Verilog®), IEEE Std 1800TM (SystemVerilog®), и IEEE Std 1666TM (SystemC®), способствуя общему потоку верификации и спецификации для проектов описанных на разных и смешанных языках.    

<!--
This standard creates an updated IEEE standard based upon IEEE Std 1850-2005. The updated standard will
refine IEEE standard, addressing errata, minor technical issues, and proposed extensions specifically related
to property reuse and improved simulation usability.
-->
Этот стандарт создает обновленный IEEE стандарт базирующийся на IEEE Std 1850-2005. Обновленный стандарт усовершенствует IEEE стандарт, адресные опечатки, незначительные технические вопросы и предполагаемого расширения непосредственно связанных свойств, для дальнейшего использования и облегчения моделирования.
       
==== 1.2.1 Происхождение ====

<!--
The complexity of Very Large Scale Integration (VLSI) has grown to such a degree that traditional
approaches have begun to reach their limitations, and verification costs have reached 60%–70% of
development resources. The need for advanced verification methodology, with improved observability of
design behavior and improved controllability of the verification process, has become critical. Over the last
decade, a methodology based on the notion of “properties” has been identified as a powerful verification
paradigm that can assure enhanced productivity, higher design quality, and, ultimately, faster time to market
and higher value to engineers and end-users of electronics products. Properties, as used in this context, are
concise, declarative, expressive, and unambiguous specifications of desired system behavior that are used to
guide the verification process. IEEE 1850 PSL is a standard language for specifying electronic system
behavior using properties. PSL facilitates property-based verification using both simulation and formal
verification, thereby enabling a productivity boost in functional verification.
-->
Сложность проектов с очень большой степенью интеграции (VLSI) выросла до такого уровня, что традиционные подходы начали достигать своего предела, а издержки верификации достигли 60%-70% от ресурсов разработки. Потребность в более продвинутой методологии верификации, с улучшенной наблюдаемостью  поведения проекта и улучшенной контролируемостью (способностью контроля) процесса верификации, стала критической. За последние 10 лет, методология, базирующаяся на понятии "свойств", была определена, как мощная парадигма верификации, которая способна обеспечить повышение производительности (эффективности), повышенное качество проекта, и значительно ускорить время выхода на рынок (time to market), увеличить число производителей (higher value to engineers?) и пользователей электронных продуктов. Свойства, используемые в данном контексте, являются краткие, декларативные/описательные (declarative), выразительные/ясные/точные (expressive) и однозначные спецификации желаемого поведения системы, которые используются для проведения процесса верификации. IEEE 1850 PSL стандартный язык для описания (спецификации) поведения электронной системы, используя свойства. PSL облегчает верификацию основанную на свойствах (property-based verification) с использованием как моделирования так и формальной верификации, что позволяет повысить эффективность функциональной верификации.

====1.2.2 Мотивация====

<!--
Ensuring that a design’s implementation satisfies its specification is the foundation of hardware verification.
Key to the design and verification process is the act of specification. Yet historically, the process of
specification has consisted of creating a natural language description of a set of design requirements. This
form of specification is both ambiguous and, in many cases, unverifiable due to the lack of a standard
machine-executable representation. Furthermore, ensuring that all functional aspects of the specification
have been adequately ''verified'' (that is, covered) is problematic.
-->
Обеспечение реализации проекта удовлетворяющей его спецификацию, является  основным для верификации аппаратуры. Ключ к проекту и процессу верификации является законом спецификации. Исторически, процесс спецификации состоял из создания языкового описания набора требований к проекту. Эта форма спецификации неоднозначная, и во многих случаях неверифицируема в связи с отсутствием стандарта машинно-выполняемого представления. Кроме того, обеспечение, того чтобы все функциональные аспекты спецификации были адекватно ''верифицированы'' (т.е. покрыты), довольно проблематично.           

<!--
The IEEE PSL was developed to address these shortcomings. It gives the design architect a standard means
of specifying design properties using a concise syntax with clearly-defined formal semantics. Similarly, it
enables the RTL implementer to capture design intent in a verifiable form, while enabling the verification
engineer to validate that the implementation satisfies its specification through ''dynamic'' (that is, simulation)
and ''static'' (that is, formal) verification means. Furthermore, it provides a means to measure the quality of the
verification process through the creation of functional coverage models built on formally specified
properties. In addition, it provides a standard means for hardware designers and verification engineers to
create a rigorous and machine-executable design specification.
-->
IEEE PSL был создан, чтобы устранить эти недостатки. Это дает архитектуре проекта стандарт, означающий спецификацию свойств проекта
используемых краткий синтаксис с простой формальной семантикой. Аналогичным образом, позволяется RTL-исполнителю определить цели проекта в проверяемых формах, пока разрешается верификации подтвердить, что выполнение окончено и его спецификация определена через ''динамическую'' ( моделирование) и статическую (формальную) верификацию. Более того, он предоставляет средства для определения качества процесса верификации, через создание полной функциональной модели построения на формально специфицированных свойствах. В дополнение, он предоставляет стандартные средства для аппаратуры проекта и инженера верификации при создании строгой и исполняемой машиной спецификации проекта.

====1.2.3 Цели====

<!--
PSL was specifically developed to fulfill the following general hardware functional specification
requirements:
-->
PSL был специально создан для исполнения следующих общих аппаратных функциональных требований:
* Легко обучать, чиать и писать
* Краткий синтаксис
* Строго определенная формальная семантика
* Выразительная мощность, позволяющая специфицировать большие классы реальных проектов
* Известные эффективные алгоритмы моделирования, такие же как формальная верификация

===1.3 Использование===

<!--
PSL is a language for the formal specification of hardware. It is used to describe properties that are required
to hold in the design under verification. PSL provides a means to write specifications that are both easy to
read and mathematically precise. It is intended to be used for functional specification on the one hand and as
input to functional verification tools on the other. Thus, a PSL specification is an executable specification of
a hardware design.
-->
PSL язык для формальной спецификации аппаратуры. Он используется для описания свойств, которые требуют поддержки в проекте под верификацию. PSL предоставляет средства для написания спецификаций, которые легко читаются и математически точны. Это предназначение используется для функциональной спецификации, с одной стороны, и как вход в программы функциональной верификации, с другой. Таким образом, спецификация PSL - это исполняемая спецификация для аппаратного проекта.
      
====1.3.1 Функциональная спецификация====

<!--
PSL can be used to capture requirements regarding the overall behavior of a design, as well as assumptions
about the environment in which the design is expected to operate. PSL can also capture internal behavioral
requirements and assumptions that arise during the design process. Both enable more effective functional
verification and reuse of the design.
-->
PSL может использоваться для выделения требований относительно общего поведения проекта, также как допущения о среде, в которой ожидается обработка проекта. PSL также может выделять внутреннее поведение требований и допущений, которые возникают в процессе обработки проекта. Доступными являются более эффективная функциональная верификация и продолжения обработки самого проекта.

<!--    
One important use of PSL is for documentation, either in place of or along with an English specification. A
PSL specification can describe simple invariants (for example, signals <code>read_enable</code> and
<code>write_enable</code> are never asserted simultaneously) as well as multi-cycle behavior (for example, correct
behavior of an interface with respect to a bus protocol or correct behavior of pipelined operations).
-->
Один из важных аспектов использования PSL - это использование для документации, как вместо, так и совместно с английской спецификацией. Спецификация PSL может описать простые инварианты (например: сигналы <code>read_enable</code> и
<code>write_enable</code> никогда не используются в одно время), также как многотактовое поведение (например: правильное поведение интерфейса с поддержкой протокола шины или правильное поведение конвейерных операций).  
 
<!--
A PSL specification consists of ''assertions'' regarding ''properties'' of a design under a set of ''assumptions''. A
''property'' is built from three kinds of elements: ''Boolean expressions'', which describe behavior over one cycle;
''sequential expressions'', which can describe multi-cycle behavior; and ''temporal operators'', which describe
temporal relationships among Boolean expressions and sequences. For example, consider the following
Verilog Boolean expression:
-->
Спецификация PSL состоит из ''утверждений'' относительно ''свойства'' проекта под набором ''допущений''. ''Свойство'' строится из трех видов элементов: ''Булевы выражения'', которые описывают поведение в одно цикле; ''последовательные выражения'', которые могут описывать многотактовое поведение;  и ''временные операторы'', которые описывают временные взаимоотношения между Булевыми выражениями и последовательностями. Например, Булево выражение в Verilog:

 ena || enb

<!--
This expression describes a cycle in which at least one of the signals <code>ena</code> and <code>enb</code> are asserted. The PSL
sequential expression
-->
Это выражение описывает цикл, в котором, по крайней мере, один из сигналов <code>ena</code> и <code>enb</code> активен. Последовательное выражение PSL

 {req; ack; !cancel}

<!--
describes a sequence of cycles, such that req is asserted in the first cycle, <code>ack</code> is asserted in the second
cycle, and <code>cancel</code> is deasserted in the third cycle. The following property, obtained by applying the
temporal operators <code>always</code> and <code>|=></code> to these expressions,
-->
описывает последовательность циклов, такую, что если <code>req</code> активен в первом цикле, <code>ack</code> активен во втором цикле, а <code>cancel</code>  неактивен  в третьем цикле. Следующее свойство получается, применяя временные операторы <code>always</code> и <code>|=></code> к этим выражениям,

 always {req;ack;!cancel} |=> (ena || enb)

<!--
means that always (that is, in every cycle), if the sequence <code>{req;ack;!cancel}</code> occurs, then either <code>ena</code>
or <code>enb</code> is asserted one cycle after the sequence ends. Adding the directive <code>assert</code> as follows:
-->
это значит, что всегда (в каждом цикле), если встречается последовательность <code>{req;ack;!cancel}</code>, то либо <code>ena</code>, либо <code>enb</code> активен в течение цикла после окончания последовательности. Добавляя директиву <code>assert</code> следующей:   

 assert always {req;ack;!cancel} |=> (ena || enb);

<!--
completes the specification, indicating that this property is expected to hold in the design and that this
expectation needs to be verified.
-->
завершается спецификация, указывая, что это свойство ожидается в проекте и что потребности это ожидания нужно верифицировать.
  
====1.3.2 Функциональная верификация====

<!--
PSL can also be used as input to verification tools, for both verification by simulation, as well as formal
verification using a model checker or a theorem prover. Each of these is discussed in the subclauses that
follow.
-->
PSL также может использоваться, как вход для программ верификации, как для верификации моделированием, так и для формальной верификации, используется проверка модели или теоретическое доказательство. Каждый вариант обсуждается в следующих пунктах.

=====1.3.2.1 Моделирование=====

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

<!--  
For instance, the following PSL property:
-->
Например, следующие PSL свойства:

 Свойство 1: always (req -> next !req)

<!--
states that signal <code>req</code> 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.
-->
означает, что сигнал <code>req</code> пульсирующий сигнал, т.е. если он принимает высокие значения в одном цикле,то он примет низкие значения в следующем цикле. Такое свойство может быть легко проверенно, используя проверки моделирования, написанные на каком-нибудь HDL, который имеет функциональность конечного автомат (FSM), показанный на Рисунке 1. 

{| align=center
! [[Файл:Std psl fig01.png|300px]]
|-
!Рисунок 1—Простой FSM, который проверяет свойство 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.
-->
Для более сложных свойств, чем то что представлено на рисунке 1, писать вручную соответствующие проверки - это кропотливый труд, подверженный ошибкам, и содержание набора таких проверок для постоянно изменяющегося проекта - это очень трудоемкое задание. Вместо этого, спецификация PSL может использоваться, как вход для программы, которая автоматически генерирует проверки, поддающиеся моделированию.

<!--     
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
-->
Хотя в принципе, все свойства PSL могут быть проверены при окончание моделирования, исполнение проверок, часто, значительно проще для подмножеств, называемых ''простые подмножества'' PSL. Неформально, в этих подмножествах, состав временных свойств ограничен для обеспечения того, что бы время ''двигалось вперед'' слева направо через свойство, как это делается на временной диаграмме. (Смотрите 4.4.4 для формального понимания простых подмножеств.)

Например, свойство 

 Свойство 2: always (a -> next[3] b)

<!--
which states that, if <code>a</code> is asserted, then <code>b</code> is asserted three cycles later, belongs to the simple subset, because
<code>a</code> appears to the left of b in the property and also appears to the left of <code>b</code> 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.
-->
которое означает, что если <code>a</code> принимает значения, то <code>b</code> примет значение через три цикла, принадлежит простому подмножеству, потому что <code>a</code> появляется слева от <code>b</code> в свойстве и, также, появляется слева от <code>b</code> на временной диаграмме любой поведенческой модели, что не нарушает свойство. Рисунок 2 показывает пример такой временной диаграммы.  

{| align=center
! [[Файл:Std psl fig02.png|400px]]
|-
! Рисунок 2—Вариант удовлетворяющий свойство 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 <code>c</code> is asserted (in the same cycle as
<code>a</code>). This property does not belong to the simple subset, because although <code>c</code> appears to the right of <code>a</code> and <code>b</code> in
the property, it appears to the left of <code>b</code> in <code>a</code> timing diagram that is not a violation of the property. Figure 3
shows an example of such a timing diagram.
-->
Пример свойства не принадлежащего этому подмножеству

 Свойство 3: always ((a && next[3] b) -> c)

которое значит, что если <code>a</code> принимает значение и <code>b</code> принимает значение через три цикла, то <code>c</code> принимает значение в том же цикле, что и <code>a</code>. Это свойство не принадлежит простому подмножеству, потому что хотя <code>c</code> появляется справа от <code>a</code> и <code>b</code> в свойстве, он появляется слева от <code>b</code> и <code>a</code> на временной диаграмме, и это не нарушает свойство. Рисунок 3 показывает пример такой временной диаграммы.    

{| align=center
! [[Файл:Std psl fig03.png|400px]]
|-
! Рисунок 3 3—Вариант, удовлетворяющий свойство 3
|}

=====1.3.2.2 Формальная верификация=====

<!--
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''.
-->
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) ===

<!--
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.
-->
'''утверждение (assertion)''': значит, что данное свойство требуется выполнить и указать программе функциональной верификации, чтобы убедиться, что оно выполняется. 

<!--
'''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.
-->
'''допущение (assumption)''': значит, что проект ограничен данным свойством и программе функциональной верификации указывается учитывать только тот путь, на котором данное свойство выполняется.  

<!--
'''asynchronous property''': A property whose clock context is equivalent to True.
-->
'''асинхронное свойство (asynchronous property)''': Свойство, временной контекст которого эквивалентен значению Правда.

<!-- 
'''behavior''': A path.
-->
'''поведение (behavior)''': Путь.

<!--
'''Boolean (expression)''': An expression that yields a logical value.
-->
'''Булевы (выражения) (Boolean (expression))''': Выражения, которые принимают на выходе логические значения.

<!--
'''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.
-->
'''проверка (checker)''': Вспомогательный процесс (обычно применяемый, как конечный автомат), который проверяет моделирование проекта и сообщения об ошибках, когда утвержденное свойство не выполняется. Проверка может быть представлена в том же HDL-коде, что и проект или в какой-либо другой форме, которая может ссылаться на моделирование проекта.  

<!--
'''completes''': A term used to identify the last cycle of a path that satisfies a sequential expression or property.
-->
'''завершение (completes)''': Термин используемый для определения последнего цикла пути, который удовлетворяет последовательности выражений или свойств.

<!--
'''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.
-->
'''вычисленный путь (computation path)''': Правопреемство состояний проекта, такое что проект может актуально переходить из каждого состояния на пути к его преемнику. 

<!--
'''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.
-->
'''ограничение (constraint)''': Состояние ( обычно для входного сигнала), которое ограничивает набор поведений, которые следует рассматривать. Ограничение может представлять реальные требования (т.е. временные требования) в среде, в которой используется проект, или может представлять искусственные ограничения (т.е. настройки режима) наложенные в порядке разделения задания функциональной верификации.       
 
<!--
'''count''': A number or range.
-->
'''счетчик (count)''': Число или диапазон.

<!--
'''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.
-->
'''зона покрытия (coverage)''': Мера возникновения определенного поведения в течение (обычно динамическое) функциональной верификации и поэтому расчет сложности (динамического) процесса функциональной верификации.     

<!--
'''cycle''': An evaluation cycle.
-->
'''цикл (cycle)''': Оценочный цикл.

<!--
'''describes''': A term used to identify the set of behaviors for which Boolean expression, sequential expression,
or property holds.
-->
'''описания (describes)''': Термин, используемый для определения набора поведений, для которого Булевы выражения, последовательные выражения или выполняемые свойства.  

<!--
'''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)''': Модель кусочка аппаратуры, описанная на некотором языке описания аппаратуры (HDL). Проект типично включает в себя набор входов, выходов, элементов состояния и комбинационных функций, которые рассчитывают следующие состояние и выходы из текущего состояния и входов.  

<!--
'''design behavior''': A computation path for a given design.
-->
'''поведение проекта (design behavior)''': Рассчитанный путь для данного проекта.

<!--
'''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.
-->
'''динамическая верификация (dynamic verification)''': Процесс верификации, такой как моделирование, в котором свойство проверяется 
отдельно, конечные поведения проекта, которые обычно получаются динамическим проведением проекта через конечное число оценочных циклов. В общем, динамическая верификация не дает вывода о выполняющемся свойстве поведения, через которое свойство еще не было проверено.

<!--    
'''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)''': Процесс проведения проекта итеративным принятием значений на его входы, рассчитывая его следующие состояния и выходные значения, время опережения, и назначение переменных состояний и выходов своих следующих значений.   

<!--
'''evaluation cycle''': One iteration of the evaluation process. At an evaluation cycle, the state of the design is
recomputed (and may change).
-->
'''оценочный цикл (evaluation cycle)''': Одна итерация оценочного процесса. На одном оценочном цикле, состояние проекта пересчитывается ( и может быть изменено). 

<!--
'''extension (of a given path)''': A path that starts with precisely the succession of states in the given path.
-->
'''расширения (данного пути) (extension (of a given path))''': Путь, который начинается  с точного правопреемства состояний в данном пути.

<!-- 
* '''False''': An interpretation of certain values of certain data types in an HDL. In the SystemVerilog and Verilog flavors, the single bit values 1’b0, 1 ’bx, and 1’bz are interpreted as the logical value False. In the VHDL flavor, the values STD.Standard.Boolean’(False) and STD.Standard.Bit’(‘0’), as well as the values IEEE.std_logic_1164.std_logic’( ‘0’), IEEE.std_logic_1164.std_logic’(‘L’), IEEE.std_logic_1164.std_logic’( ‘X’), and IEEE.std_logic_1164.std_logic’(‘Z’) are all interpreted as the logical value False. In the SystemC flavor, the value 'false' of type bool and any integer literal with a numeric value of 0 are interpreted as the logical value False. In the GDL flavor, the Boolean value 'false' and bit value 0B are both interpreted as the logical value False.
-->

* '''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.
-->
'''конечный диапазон (finite range)''': Диапазон с большой конечной границей.

<!--
'''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.
-->
'''формальная верификация (formal verification)''': Процесс функциональной верификации, в котором анализ дизайна и выхода свойства логически разъясняет о выполняемое свойство для все поведений проекта. Если свойство продекларировано значение "правда" программой формальной верификации, моделирование не может сделать его значение "ложным". Если свойство не выполняется для каждого поведения, то процесс формальной верификации должен предоставить специфический контрпример свойства, если это возможно.

<!--
'''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.
-->
'''функциональная верификация (functional verification)''': Процесс подтверждения того, что для данного проекта и данного набора ограничений, свойство, которое требует выполнение в этом проекте, действительно выполняется в соответствие с данными ограничениями.  

<!--
'''holds''': A term used to talk about the meaning of a Boolean expression, sequential expression, or property.
-->
'''исполнение (holds)''': Термин используемый для разъяснения значения Булевых выражений, последовательных выражений или свойств.

<!--
'''holds tightly''': A term used to talk about the meaning of a sequential expression. Sequential expressions are
evaluated over finite paths (behavior).
-->
'''обязательное исполнение(holds tightly)''': Термин используемый для разъяснения значения последовательных выражений. Последовательные выражения оцениваются на конечной стадии (поведение). 

<!--
'''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.
-->
'''живучие свойства (liveness property)''': Свойства, которые указывают на случайность, которая не ограничена во времени. Грубо говоря, живучие свойства утверждает, что что-то “хорошее” в конечном счете произошло. Более формально, живучие свойство - это свойство, для которого любая конечная стадия может быть продолжена до стадии удовлетворения свойства. Например, свойство “когда-либо сигнал req принимает значение, сигнал ack принимает значение через некоторое время” это живучие свойство. 

<!--
'''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.
-->
'''логический тип (logic type)''': Тип данных HDL, который включает значения, которые интерпретируются, как логические значения. Логический тип, также, включает значения, которые не интерпретируются, как логические значения. Как логический тип, обычно, представляет многозначную логику.

<!--
'''logical value''': A value in the set {True, False}.
-->
'''логическое значение (logical value)''': Значение из набора {True, False}.

<!--
'''model checking''': A type of formal verification.
-->
'''проверка на модели (model checking)''': Тип формальной верификации.

<!--
'''number''': A non-negative integer value, and a statically computable expression yielding such a value.
-->
'''число (number)''': Неотрицательное целочисленное значение, и статично подсчитанное выражение полученное, как выражение.

<!--
'''occurs''': A term used to indicate that a Boolean expression holds in a given cycle.
-->
''' (occurs)''': Термин используемый для индикации того, что Булево выражение выполняется в данном цикле.

<!--
'''occurrence (of a Boolean expression)''': A cycle in which the Boolean expression holds.
-->
'''occurrence (of a Boolean expression)''': Цикл, в котором выполняется Булево выражение.

<!--
'''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.
-->
'''стадия (путь) (path)''': Правопреемственность состояний проекта, ??? 

<!--
'''positive count''': A positive number or a positive range.
-->
'''положительный счетчик (positive count)''': Положительное число или положительный диапазон.

<!--
'''positive number''': A number that is greater than zero (0).
-->
'''положительное число (positive number)''': Число, которое больше нуля (0).

<!--
'''positive range''': A range with a low bound that is greater than zero (0).
-->
'''положительный диапазон (positive range)''': Диапазон с нижней границей большей нуля (0).

<!--
'''prefix (of a given path)''': A path of which the given path is an extension.
-->
'''префикс (данной стадии) (prefix (of a given path))''': Стадия в которую расширяется данная стадия.

<!--
'''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.
-->
'''свойство (property)''': Набор логических и временных взаимоотношений между и среди подчиненных Булевых выражений, последовательных выражений и других свойств, которые в совокупности представляют набор поведений.

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

<!--
'''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.
-->
'''ограничение (restriction)''': Утверждение, что проект ограничивается данным последовательным выражением, и директива программе функциональной верификации рассматривать только стадию, на которой выполняется данное последовательное выражение.  

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

<!--
'''sequence''': A sequential expression that may be used directly within a property or directive.
-->
'''последовательность (sequence)''': Последовательное выражение, которое может напрямую использоваться в течение свойства или директивы.

<!--
'''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.
-->
'''последовательное выражение (sequential expression)''': Законченный набор терминов, который представляет набор поведений.

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

<!--
'''starts''': A term used to identify the first cycle of a path that satisfies a sequential expression.
-->
'''начало (starts)''': Термин используемый для идентификации первого цикла пути, который удовлетворяет последовательное выражение. 

<!--
'''strictly before''': Before, and not in the same cycle as.
-->
'''строго перед (strictly before)''': Перед, и не в этом же цикле.

<!--
'''strong operator''': A temporal operator, the non-negated use of which usually creates a liveness property.
-->
'''сильный оператор (strong operator)''': Временной оператор, неотрицательное использование которого, обычно, создает живучие свойства.

<!--
'''temporal expression''': An expression that involves one or more temporal operators.
-->
'''временное выражение (temporal expression)''': Выражение, которое включает один или более временных операторов.

<!--
'''temporal operator''': An operator that represents a temporal (i.e., time-oriented) relationship between its
operands.
-->
'''временной оператор (temporal operator)''' Оператор, который представляет временные ( т.е. ориентированные во времени) взаимоотношения между операндами.

<!--
'''terminating condition''': A Boolean expression, the occurrence of which causes a property to complete.
-->
'''условие завершения (terminating condition)''': Булево выражение, появление которого, приводит к завершению свойства.

<!--
'''terminating property''': A property that, when it holds, causes another property to complete.
-->
'''свойство завершения (terminating property)''': Свойство, выполнение которого, приводит к завершению другого свойства.

<!-- 
True: An interpretation of certain values of certain data types in an HDL. In the SystemVerilog and Verilog
flavors, the single bit value 1'b1 is interpreted as the logical value True. In the VHDL flavor, the values
STD.Standard.Boolean'(True), STD.Standard.Bit'('1'),
IEEE.std_logic_1164.std_logic'('1'), and IEEE.std_logic_1164.std_logic'('H')
interpreted as the logical value True. In the SystemC flavor, the value 'true' of type bool and any integer
literal with a non-zero numeric value are interpreted as the logical value True. In the GDL flavor, the Boolean value 'true' and bit value 1B are both interpreted as the logical value True.
-->
* '''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.
-->
'''неизвестное значение (unknown value)''': Значение (многозначного) логического типа, отличное от 0 и 1.

<!--
'''weak operator''': A temporal operator, the non-negated use of which does not create a liveness property.
-->
'''слабый оператор (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) =====

<!-- The Boolean layer is used to build expressions that are, in turn, used by the other layers. Although it contains
expressions of many types, it is known as the Boolean layer because it is the supplier of Boolean
expressions to the heart of the language—the temporal layer. Boolean layer expressions are evaluated in a
single evaluation cycle.
-->
Булевый слой используется для создания выражений, которые, в свою очередь, используются другими слоями. Хотя этот слой содержит выражения над многими типами, он называется как булевый слой, потому что он является поставщиком булевых (логических) выражений для основы (сердца)  языка — временнОго слоя. Выражения булевого слоя выполняются в едином (одиночном) цикле выполнения.

===== 4.1.1.2 ВременнОй слой (Temporal layer) =====
<!-- 
The temporal layer is the heart of the language; it is used to describe properties of the design. It is known as
the temporal layer because, in addition to simple properties, such as “signals a and b are mutually
exclusive,” it can also describe properties involving complex temporal relations between signals, such as, “if
signal c is asserted, then signal d shall be asserted before signal e is asserted, but no more than eight clock
cycles later.” Temporal expressions are evaluated over a series of evaluation cycles.
-->
Временной слой является основой языка; он используется для описания свойств проекта. Он называется временным, потому что, в дополнение к простым свойствам, таким как "сигналы a и b являются взаимноисключающими", он может также описывать свойства включающие сложные временные отношения между сигналами, например "если сигнал c устанавливается, тогда сигнал d должен установиться прежде, чем сигнал e установится, но не позже более восьми периодов синхросигнала". ВременнЫе выражения выполняются в течении серии циклов выполнения.

===== 4.1.1.3 Верификационный слой (Verification layer) =====

<!-- The verification layer is used to tell the verification tools what to do with the properties described by the
temporal layer. For example, the verification layer contains directives that tell a tool to verify that a property
holds or to check that a specified sequence is covered by some test case.
-->
Верификационный слой используется для того чтобы сказать верификационному инструменту (САПР), что делать с свойствами описанными во временном слое. Например, верификационный слой включает директивы, которые говорят инструменту (САПР) чтобы верифицировал (verify) то, что свойство удерживает (hold) или  проверил (check) то, что заданная последовательность покрыта некоторым тестирующим случаем.

===== 4.1.1.4 Моделирующий слой (Modeling layer) =====

<!-- The modeling layer is used to model the behavior of design inputs (for tools, such as formal verification
tools, which do not use test cases) and to model auxiliary hardware that is not part of the design, but is
needed for verification.
-->
Моделирующий слой (Modeling layer) используется для моделирования поведения входов проекта (для инструментов (САПР), таких как инструменты (САПР) для формальной верификации, которые не используют тестов) и для моделирования дополнительной аппаратуры, которая не является частью проекта, но необходима для верификации.

==== 4.1.2 Стили/Варианты (Flavors) ====

<!-- PSL comes in five flavors: one for each of the hardware description languages SystemVerilog, Verilog,
VHDL, SystemC, and GDL. The syntax of each flavor conforms to the syntax of the corresponding HDL in
a number of specific areas—a given flavor of PSL is compatible with the corresponding HDL’s syntax in
those areas.
-->
PSL идёт с пятью вариантами/стилями (flavors): один для каждого HDL языка SystemVerilog, Verilog, VHDL, SystemC, и GDL. Синтаксис каждого варианта (стиля) соответствует синтаксису соответствующего HDL языка в ряде конкретных областей — данный стиль PSL совместим с соответствующим синтаксисом HDL-языка в этой области.

{| class=standard align=center
|+ Влияние стиля на слои PSL
!rowspan=2| Слой ||colspan=5 | HDL
|-
!  SystemVerilog || Verolog || VHDL || SystemC || GDL
|-
| Булевый || {{V|16px}} || {{V|16px}} || {{V|16px}} || {{V|16px}} || {{V|16px}} 
|-
| Модельный  || {{V|16px}} || {{V|16px}} || {{V|16px}} || {{V|16px}} || {{V|16px}} 
|-
| Временной || i:j || i:j || i to j || i:j ||  i..j
|-
 
|}

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

<!--
This subclause defines the identifiers, keywords, operators, macros, and comments used in PSL.
-->
Этот подпункт определяет идентификаторы, ключевые слова, операторы, макросы и комментарии, используемые в PSL.
 
==== 4.2.1 Идентификаторы (Identifiers) ====

<!-- Identifiers in PSL consist of an alphabetic character, followed by zero or more alphanumeric characters;
each subsequent alphanumeric character may optionally be preceded by a single underscore character.
-->
Идентификаторы в PSL состоят из символа латинского алфавита, за которым следует ноль или более символов латинского алфавита; каждый последующий символ алфавита может по желанию предшествовать одному символу подчеркивания. Например:

 mutex
 Read_Transaction
 L_123

<!-- PSL identifiers are case-sensitive in the SystemVerilog, Verilog, and SystemC flavors and case-insensitive in
the VHDL and GDL flavors.
-->
PSL идентификаторы являются чувстительными к регистру в SystemVerilog, Verilog, и SystemC вариантах/стилях и не чувствительными к регистру в VHDL и GDL вариантах.

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

{|
|<poem> A
 E
 next!
 rose
AF
 EF
 next_a
AG
 EG
 next_a!
</poem>
| <poem> sequence
AX
abort
 EX
 next_e
 stable
always
 ended
 next_e!
string
</poem>
| <poem>anda
 eventually!
 next_event
 strong
assert
 next_event!
 sync_abort
assume
 F
 next_event_a
</poem>
| <poem>async_abort
fairness
 next_event_a!
 toe
before
 fell
 next_event_e
before!
 for
 next_event_e!
</poem>
| <poem> U
before!_
 forall
 nondet
 union
before_
 nondet_vector
 until
bitvector
 bit
</poem>
| <poem> G
 notc
 until!
boolean
 numeric
 until!_
hdltype
until_
clock
 onehot
</poem>
| <poem>const
 in
 onehot0
 vmode
countones
 inf
 ord
 vpkg
cover
 inherit
</poem>
| <poem> vprop
isb
 property
 vunit
default
 isunknown
 prev
W
report
mutable
</poem>
| <poem> within
restrict
restrict!
never
 X
next
 X!</poem>
|}

*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 языка =====
<!-- 
For a given flavor of PSL, the operators of the underlying HDL have the highest precedence. In particular,
this includes logical, relational, and arithmetic operators of the HDL. The HDL’s logical operators for
negation, conjunction, and disjunction of Boolean values may be used in PSL for negation, conjunction, and
disjunction of properties as well. In such applications, those operators have their usual precedence and
associativity, as if the PSL properties that are operands produced Boolean values of a type appropriate to the
logical operators native to the HDL.
-->
Для заданного стиля PSL, операторы основного HDL языка имеют наивысший преоритет. В частности это включает логические, арифметические операторы и операторы отношения языка HDL. Логические операции HDL языка для отрицания,  конъюнкции и дизъюнкции булевых (логических) значений могут использоваться в PSL для отрицания, конъюнкции и дизъюнкции свойств. В таких приложениях, эти операторы имеют их обычный приоритет и ассоциативность, как если бы PSL свойства,....

===== 4.2.3.2 Операторы фундаментального языка =====

<!--
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.
-->
Различные операторы доступны в PSL. Каждый оператор имеет приоритет по отношению к другим операторам. В общем операторы с большим приоритетом получают доступ к свои операндам, раньше, чем операнды с меньшим приоритетом. Если два оператора имеют одинаковый приоритет и появляются в последовательности, то они получают доступ к свои операндам в соответствие с ассоциативностью операторов. Лева-ассоциативные оператор получает доступ к своим операндам слева на право в порядке появления в тексте, право-ассоциативные операторы получают доступ к своим операндам справа на лева в порядке появления в тексте.   
 
{| class=standard align=center
|+ Таблица приоритетов и ассоциативности двух операторов фундаментального языка  
|-
! Оператор класс || Ассоциативность ||colspan=2| Операторы
|-
| ''(наивысший приоритет)''

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

<!--
For any flavor of PSL, the FL operator with the next highest precedence after the HDL operators is that used to indicate a non-deterministic expression:

 union   union operator

The union operator is left-associative.
-->
Для любого стиля PSL, FL оператор со следующим наибольшим приоритетом после HDL операторов является тот, который используется для обозначения недетерминированного выражения:

 union   union оператор

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

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

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

 @   clock event

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

====== 4.2.3.2.3 SERE операторы повторов (repetition operators) ======

<!-- For any flavor of PSL, the FL operators with the next highest precedence are the repetition operators, which
are used to construct Sequential Extended Regular Expressions (SEREs). These operators are as follows:
-->
Для любого стиля PSL, FL операторы со следующим наибольшим приоритетом являются операторами повторов, которые используются для создания последовательных расширенных регулярных выражений (Sequential Extended Regular Expressions — SEREs). Эти операторы следующие:

 [* ]   последовательное повторение (consecutive repetition)
 [+]    последовательное повторение (consecutive repetition)
 [= ]   не последовательное повторение (non-consecutive repetition)
 [-> ]  goto repetition

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

====== 4.2.3.2.4 Последовательный предельный оператор ======

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

<!--
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.
-->
Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, в котором операнды используются в будущем. Это следующие операторы: 
eventually! правый операнд выполняется через некоторое время в неопределенном будущем
 next*     правый операнд выполняется в некотором специфицированном будущем времени или диапазоне будущего времени
операторы местонахождения фундаментального языка право-ассоциативные.

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

<!--
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:
-->
Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые описывают поведение, в котором одно свойство выполняется в некотором цикле или во всех циклах перед выполнением следующего слова. Это следующие операторы:

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

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

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

<!--
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:
-->
Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, состоящего из свойства, которое выполняется в конце данной последовательности. Это следующие операторы:

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

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

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

<!--
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:
-->
Для любого варианта PSL, операторый фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, состоящего из Булевых выражений, последовательности или свойства, которое выполняется, если выполняется другое Булево выражение, последовательность или свойство.  

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

<!--
The logical IF and logical IFF implication operators are right-associative.
-->
Операторы логической импликации право-ассоциативные.

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

<!--
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:
-->
Для любого варианта PSL, операторы фундаментального языка со следующим наивысшим приоритетом те, которые используются для описания поведения, в котором выполняется или не выполняется глобально. 

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

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

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

{| class=standard align=center
|+ Таблица 3—OBE оператор, приоритет и ассоциативность
|-
! Класс оператора || Ассоциативность ||colspan=2| Операторы
|-
| (наивысший приоритет)<br/>HDL операторы || || ||
|-
| OBE операторы местонахождения ||left ||  AX AG AF<br/> A [ U ] || EX EG EF <br/>E [ U ]
|-
| Операторы Булевой импликации<br/>(низший приоритет) || right || -> || <->
|}

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

<!--
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:
-->
Для любого варианта PSL, OBE операторы являются следующими операторами с наивысшим приоритетом, после HDL операторов, они используются для указания, когда подчиненное свойство должно выполняться, если выполняется старшее свойство. Это следующие операторы:   

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

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

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

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

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

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

==== 4.2.4 Макросы ====

<!--
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.
-->
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.4.1 Конструкция %for =====

===== 4.2.4.2 Конструкция %if =====

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

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

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

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

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


=== 4.3 Синтаксис ===

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

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

=== 4.4 Семантика ===

<!--
The following subclauses introduce various general concepts related to temporal property specification and
explain how they apply to PSL.
-->
Следующие подпункты представляют различные общие концепции связанные со спецификацией временных свойств и пояснения того, как они применяются в PSL.  

==== 4.4.1 Временная оценка против не временной оценки ====

== NEW ==