Язык Спецификации Свойств (PSL): Обзор и Операторы
Property Specification Language
Язык спецификации свойств (PSL) – формальная логика для верификации аппаратного обеспечения. Используется в IEEE 1850, Accellera для проверки дизайнов.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Язык спецификации свойств (PSL) — это темпоральная логика, расширяющая линейную темпоральную логику набором операторов, обеспечивающих простоту выражения и повышение выразительной силы. PSL активно использует регулярные выражения и синтаксический сахар. Он широко применяется в индустрии разработки и верификации аппаратного обеспечения, где формальные инструменты верификации (например, проверка моделей) и/или инструменты логического моделирования используются для доказательства или опровержения справедливости заданной формулы PSL для конкретной схемы. PSL был изначально разработан компанией Accellera для спецификации свойств или утверждений об аппаратных проектах. Начиная с сентября 2004 года, стандартизация языка осуществлялась в рабочей группе IEEE 1850. В сентябре 2005 года был опубликован стандарт IEEE 1850 для языка спецификации свойств (PSL).
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design. PSL was initially developed by Accellera for specifying properties or assertions about hardware designs. Since September 2004 the standardization on the language has been done in IEEE 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.
Операторы типа LTL
Ниже приведен пример некоторых операторов в стиле LTL языка PSL. Здесь и – любые формулы PSL. Свойство p истинно в каждой точке времени. Свойство p ложно в любой точке времени. Существует будущая точка времени, в которой p истинно. Существует следующая точка времени, и p истинно в этой точке. Если существует следующая точка времени, то p истинно в этой точке. Существует n-я точка времени, и p истинно в этой точке. Если существует n-я точка времени, то p истинно в этой точке. Существует точка времени, находящаяся на расстоянии от m до n шагов от текущей, в которой p истинно. Если существует по крайней мере n шагов, то p истинно хотя бы в одной из точек от m до n шага. Существует по крайней мере n дополнительных шагов, и p истинно во всех точках времени между m-м и n-м шагами включительно. p истинно во всех следующих точках от m до n шагов, если таковые существуют. Существует точка времени, в которой q истинно, и p истинно до этой точки. p истинно до точки времени, в которой q истинно, если такая точка существует. Существует точка времени, в которой q истинно, и p истинно до этой точки и в этой точке. p истинно до точки времени, в которой q истинно, и в этой точке, если такая точка существует. p истинно строго перед точкой времени, в которой q истинно, и p в конечном итоге истинно. p истинно строго перед точкой времени, в которой q истинно, если p никогда не истинно, то и q тоже не истинно. p истинно до или в момент времени, в котором q истинно, и p в конечном итоге истинно. p истинно до или в момент времени, в котором q истинно, если p никогда не истинно, то и q тоже не истинно.
Below is a sample of some LTL style operators of PSL. Here and are any PSL formulas. property p holds on every time point property p does not hold on any time point there exists a future time point where p holds there exists a next time point, and p holds on this point if there exists a next time point, then p holds on this point there exists an n th time point, and p holds on this point if there exists an n th time point, then p holds on this point there exists a time point, within m th to n th from the current where p holds. if there exists at least n th time points, then p holds on one of the m th to n th points. there exists at least n more time points and p holds in all the time points between the m th to the n th, inclusive. p holds on all the next m th through n th time points, however many exist there exists a time point where q holds, and p hold up until that time point p holds up until a time point where q hold, if such exists there exists a time point where q holds, and p holds up until that time point and in that time point p holds up until a time point where q holds, and in that time point, if such exists p holds strictly before the time point where q holds, and p eventually holds p holds strictly before the time point where q holds, if p never holds, then neither does q p holds before or at the same time point where q holds, and p eventually holds p holds before or at the same time point where q holds, if p never holds, then neither does q
Выразительная сила
PSL включает в себя временную логику LTL и расширяет ее выразительную силу до омега-регулярных языков. Увеличение выразительной силы по сравнению с LTL, которая обладает выразительной мощностью звездных свободных ω-регулярных выражений, обусловлено суффиксной импликацией, также известной как оператор триггеров, обозначаемый "|>". Формула r |> f, где r – регулярное выражение, а f – формула временной логики, истинна для вычисления w, если любой префикс w, соответствующий r, имеет продолжение, удовлетворяющее f. Другими операторами PSL, не входящими в LTL, являются оператор @ для спецификации синхронизированных по нескольким тактам конструкций, операторы прерывания для обработки аппаратных сбросов и локальные переменные для лаконичности.
PSL subsumes the temporal logic LTL and extends its expressive power to that of the omega regular languages. The augmentation in expressive power, compared to that of LTL, which has the expressive power of the star free ω regular expressions, can be attributed to the suffix implication, also known as the triggers operator, denoted "| >". The formula r | > f where r is a regular expression and f is a temporal logic formula holds on a computation w if any prefix of w matching r has a continuation satisfying f. Other non LTL operators of PSL are the @ operator, for specifying multiply clocked designs, the abort operators, for dealing with hardware resets, and local variables for succinctness.
Слои
PSL определяется в 4 слоях: булевом слое, временном слое, слое моделирования и слое верификации. Булевый слой используется для описания текущего состояния разрабатываемой схемы и выражается с помощью одного из вышеупомянутых языков описания аппаратуры (HDL). Временной слой состоит из временных операторов, используемых для описания сценариев, развивающихся во времени (возможно, на неограниченном количестве временных шагов). Слой моделирования может использоваться для описания вспомогательных конечных автоматов процедурным способом. Слой верификации состоит из директив для инструмента верификации (например, для утверждения корректности заданного свойства или для предположения корректности определенного набора свойств при верификации другого набора свойств).
PSL is defined in 4 layers: the Boolean layer, the temporal layer, the modeling layer and the verification layer. The Boolean layer is used for describing a current state of the design and is phrased using one of the above mentioned HDLs. The temporal layer consists of the temporal operators used to describe scenarios that span over time (possibly over an unbounded number of time units). The modeling layer can be used to describe auxiliary state machines in a procedural manner. The verification layer consists of directives to a verification tool (for instance to assert that a given property is correct or to assume that a certain set of properties is correct when verifying another set of properties).