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

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

PSL

• The Designer's Guide To PSL (ru)

---

Литература

• Литература
• IEEE Std 1850-2010

---

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

* VHDL * OS-VVM * Co-Simulation *

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

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

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

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.