Язык спецификации свойств

Язык спецификации свойств ( PSL ) — это темпоральная логика, расширяющая линейную темпоральную логику набором операторов, обеспечивающих как простоту выражения, так и повышение выразительных возможностей. PSL широко использует регулярные выражения и синтаксический сахар. Он широко используется в индустрии проектирования и проверки аппаратного обеспечения, где инструменты формальной проверки (например, проверка модели ) и/или инструменты логического моделирования используются для доказательства или опровержения того, что данная формула PSL применима к данной конструкции.

PSL изначально был разработан Accellera для определения свойств или утверждений о конструкции аппаратного обеспечения. С сентября 2004 года стандартизацией языка занимается рабочая группа IEEE 1850. В сентябре 2005 года был анонсирован стандарт IEEE 1850 для языка спецификации свойств (PSL).

Синтаксис и семантика [ править ]

PSL может выражать то, что если какой-то сценарий происходит сейчас, то другой сценарий должен произойти через некоторое время. Например, свойство «a запрос всегда должен в конечном итоге быть грант ed» можно выразить формулой PSL:

  always (request -> eventually! grant)

Объект «каждый запрос , за которым сразу следует Подтверждающий сигнал должен сопровождаться полным передача данных , где полная передача данных представляет собой последовательность, начинающуюся с сигнала начало , окончание сигналом конец , в котором в это время занято удержание» можно выразить формулой PSL:

  (true[*]; req; ack)  |=> (start; busy[*]; end)

След, удовлетворяющий этой формуле, показан на рисунке справа.

Темпоральные операторы PSL можно грубо разделить на операторы в стиле LTL и операторы в стиле регулярных выражений . Многие операторы PSL существуют в двух версиях: сильная версия обозначается суффиксом восклицательного знака ( ! ), и слабая версия. Сильная версия предъявляет требования на случай возникновения событий (т. е. требует, чтобы что-то сохранялось в будущем), а слабая версия этого не делает. Суффикс подчеркивания ( _ ) используется для различения инклюзивных и неинклюзивных требований. _а и Суффиксы _e используются для обозначения универсальных (всех) и экзистенциальных (существующих) требований. Точные временные окна обозначаются [n] и гибкий благодаря [м..н] .

Операторы в стиле SERE [ править ]

Наиболее часто используемый оператор PSL — это оператор «суффикс-импликация» (также известный как оператор «триггеров»), который обозначается |=> . Его левый операнд — это регулярное выражение PSL, а правый операнд — любая формула PSL (будь то в стиле LTL или в стиле регулярного выражения). Семантика r |=> p заключается в том, что в каждый момент времени i, когда последовательность моментов времени до i соответствует регулярному выражению r, путь от i+1 должен удовлетворять свойству p. Это показано на рисунках справа.

Регулярные выражения PSL имеют общие операторы конкатенации ( ; ), замыкание Клини ( * ) и объединение ( | ), а также оператор слияния ( : ), пересечение ( && ) и более слабая версия ( & ) и множество вариантов последовательного подсчета [*n] и последовательный подсчет, например [=n] и [->n] .

Оператор триггера существует в нескольких вариантах, показанных в таблице ниже.

Здесь песок t — регулярные выражения PSL, а p — формула PSL.

s \|=> t!	если есть совпадение s, то в суффиксе трассы есть совпадение t, t запускает цикл после окончания s, совпадение t должно дойти до конца
s \|-> t!	если есть совпадение s, то в суффиксе трассы есть совпадение t, t запускает тот же цикл, который заканчивается, совпадение t должно дойти до конца
s \|=> t	если есть совпадение s, то в суффиксе трассы есть совпадение t, t запускает цикл после окончания s, совпадение t может «застрять» в середине
s \|-> t	если есть совпадение s, то в суффиксе трассы есть совпадение t, t запускает тот же цикл, который заканчивается, совпадение t может «застрять» в середине

Операторы конкатенации, слияния, объединения, пересечения и их варианты показаны в таблице ниже.

Здесь песок t — регулярные выражения PSL.

`s ; t`	совпадение s, за которым следует совпадение t, t запускает цикл после окончания s
`s : t`	совпадение s, за которым следует совпадение t, t запускает тот же цикл, которым заканчивается s
`s \| t`	совпадение s или совпадение t
`s && t`	совпадение s и совпадение t, продолжительность обоих одинаковая
`s & t`	совпадение s и совпадение t, совпадения продолжительности могут быть разными
`s within t`	совпадение s внутри совпадения t, сокращение ([]; s; []) && t

Операторы для последовательных повторений показаны в таблице ниже.

Здесь s — регулярное выражение PSL.

`s[*i]`	я последовательные повторения s
`s[*i..j]`	между i и j последовательными повторениями s
`s[*i..]`	по крайней мере, я к последовательным повторениям s
`s[*]`	ноль или более последовательных повторений s
`s[+]`	одно или несколько последовательных повторений s

Операторы для непоследовательных повторений показаны в таблице ниже.

Здесь b — любое логическое выражение PSL.

`b[=i]`	i не обязательно последовательные повторения b, эквивалентно (!b[];b)[i]; !б[*]
`b[=i..j]`	не менее i и не более j, не обязательно последовательные повторения b, эквивалентно (!b[];b)[i..j]; !б[*]
`b[=i..]`	по крайней мере, я не обязательно последовательное повторение b, эквивалентно (!b[];b)[i..]; !б[*]
`b[->m]`	m не обязательно последовательные повторения b, заканчивающиеся на b, эквивалентно (!b[];b)[m]
`b[->m:n]`	не менее m и не более n, не обязательно последовательные повторения b, заканчивающиеся на b, эквивалентно (!b[];b)[m..n]
`b[->m..]`	по крайней мере, m не обязательно последовательных повторений b, заканчивающихся на b, эквивалентно (!b[];b)[m..]; !б[*]
`b[->]`	ярлык для b[->1], эквивалент (!b[*];b)

Операторы в стиле LTL [ править ]

Ниже приведен пример некоторых операторов PSL в стиле LTL.

Здесь п и q — любые формулы PSL.

`always p`	свойство p сохраняется в каждый момент времени
`never p`	свойство p не выполняется ни в какой момент времени
`eventually! p`	существует момент в будущем, когда p имеет место
`next! p`	существует следующий момент времени, и в этой точке выполняется p
`next p`	если существует следующий момент времени, то в этой точке выполняется p
`next![n] p`	существует n-й момент времени, и в этой точке выполняется p
`next[n] p`	если существует n-й момент времени, то в этой точке выполняется p
`next_e![m..n] p`	существует момент времени в пределах от m до n-го момента от текущего, в котором выполняется p.
`next_e[m..n] p`	если существует хотя бы n-й момент времени, то p имеет место в одной из m-й-n-й точек.
`next_a![m..n] p`	существует еще как минимум n моментов времени, и p выполняется во всех моментах времени между m-м и n-м включительно.
`next_a[m..n] p`	p выполняется во всех следующих моментах времени с m-го по n-й, сколько бы их ни существовало
`p until! q`	существует момент времени, когда выполняется q, и p сохраняется до этого момента времени
`p until q`	p сохраняется до момента времени, когда выполняется q, если таковой существует
`p until!_ q`	существует момент времени, когда выполняется q, а p сохраняется до этого момента и в этот момент времени
`p until_ q`	p сохраняется до момента времени, когда выполняется q, и в этот момент времени, если таковой существует
`p before! q`	p соблюдается строго до момента времени, когда соблюдается q, и в конечном итоге соблюдается p
`p before q`	p выполняется строго до момента времени, когда выполняется q; если p никогда не выполняется, то и q не выполняется.
`p before!_ q`	p выполняется до или в тот же момент времени, когда выполняется q, и p в конечном итоге выполняется
`p before_ q`	p выполняется до или в тот же момент времени, когда выполняется q; если p никогда не выполняется, то и q не выполняется.

Оператор выборки [ править ]

Иногда желательно изменить определение следующего момента времени , например, в проектах с многократной тактовой частотой или когда требуется более высокий уровень абстракции. Оператор выборки (также известный как оператор часов ), обозначаемый @ используется для этой цели. Формула п@ц где p — формула PSL и c Булевы выражения PSL выполняются на заданном пути, если p на этом пути, проецируемом на циклы, в которых c выполняется, как показано на рисунках справа.

Первое свойство гласит, что «каждый запрос , за которым сразу следует Подтверждающий сигнал должен сопровождаться полным передача данных , где полная передача данных представляет собой последовательность, начинающуюся с сигнала начало , окончание сигналом конец , в котором данные должны содержать не менее 8 раз:

  (true[*]; req; ack)  |=> (start; data[=8]; end)

Но иногда желательно рассматривать только случаи, когда указанные выше сигналы возникают в цикле, где clk высокий. Это изображено на втором рисунке, на котором, хотя формула

  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk

использует данные[*3] и [*n] — последовательное повторение, совпадающая трасса имеет 3 непоследовательных момента времени, где данные верны, но если рассматривать только те моменты времени, когда clk содержит моменты времени, когда удержание данных становится последовательным.

Семантика формул с вложенным @ немного тонка. Заинтересованного читателя отсылаем к [2].

Операторы прерывания [ править ]

В PSL есть несколько операторов для работы с усеченными путями (конечными путями, которые могут соответствовать префиксу вычисления). Усеченные пути возникают при проверке ограниченной модели из-за сброса и во многих других сценариях. Операторы прерывания определяют, как следует поступать в случае усечения пути. Они опираются на усеченную семантику, предложенную в [1].

Здесь p — любая формула PSL и b — любое логическое выражение PSL.

`p async_abort b`	либо p выполняется, либо p не нарушается до тех пор, пока не выполняется b; b распознается асинхронно
`p sync_abort b`	либо p выполняется, либо p не нарушается до тех пор, пока не выполняется b; б распознается синхронно
`p abort b`	эквивалент p async_abort b

Выразительная сила [ править ]

PSL включает в себя темпоральную логику LTL и расширяет ее выразительную силу до уровня омега-регулярных языков . Увеличение выразительной силы по сравнению с LTL, который обладает выразительной силой ω-регулярных выражений без звездочек, можно объяснить суффиксной импликацией , также известной как оператор триггера , обозначаемый «|->». Формула r |-> f , где r — регулярное выражение, а f — формула темпоральной логики, справедлива для вычисления w, если любой префикс w, соответствующий r, имеет продолжение, удовлетворяющее f . Другие операторы PSL, не относящиеся к LTL, — это оператор @ для указания проектов с многократным тактированием, операторы прерывания для работы с аппаратным сбросом и локальные переменные для краткости.

Слои [ править ]

PSL определяется на 4 уровнях: логический уровень , временной уровень , уровень моделирования и уровень проверки .

Логический уровень используется для описания текущего состояния проекта и формулируется с использованием одного из вышеупомянутых HDL.
Временной уровень состоит из темпоральных операторов, используемых для описания сценариев, охватывающих время (возможно, неограниченное количество единиц времени).
Уровень моделирования можно использовать для описания вспомогательных конечных автоматов процедурным способом.
Уровень проверки состоит из директив для инструмента проверки (например, для подтверждения того, что данное свойство является правильным, или для предположения , что определенный набор свойств является правильным при проверке другого набора свойств).

Языковая совместимость [ править ]

Язык спецификации свойств может использоваться с несколькими языками проектирования электронных систем (HDL), такими как:

VHDL (IEEE 1076)
Верилог (IEEE 1364)
СистемВерилог (IEEE 1800)
SystemC (IEEE 1666) от Open SystemC Initiative (OSCI) .

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

Ссылки [ править ]

1850–2005 — Стандарт IEEE для языка спецификации свойств (PSL) . 2005. doi : 10.1109/IEESTD.2005.97780 . ISBN 0-7381-4780-Х .
- МЭК 62531:2007 62531-2007 – МЭК 62531 Ред. 1 (2007–11) (IEEE Std 1850–2005): Стандарт языка спецификации свойств (PSL) . 2007. doi : 10.1109/IEESTD.2007.4408637 . ISBN 978-0-7381-5727-6 .
1850–2010 — Стандарт IEEE для языка спецификации свойств (PSL) . 2010. doi : 10.1109/IEESTD.2010.5446004 . ISBN 978-0-7381-6255-3 .
- МЭК 62531:2012 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Стандарт языка спецификации свойств (PSL) . 2012. doi : 10.1109/IEESTD.2012.6228486 . ISBN 978-0-7381-7299-6 .
Эйснер, Синди; Фисман, Дана ; Гавличек, Джон; Люстиг, Йоад; МакИсаак, Энтони; Ван Кампенхаут, Дэвид (2003). «Рассуждения с помощью временной логики об усеченных путях» (PDF) . Компьютерная проверка . Конспекты лекций по информатике. Том. 2725. с. 27. дои : 10.1007/978-3-540-45069-6_3 . ISBN 978-3-540-40524-5 .
Эйснер, Синди; Фисман, Дана ; Гавличек, Джон; МакИсаак, Энтони; Ван Кампенхаут, Дэвид (2003). «Определение оператора временных часов» (PDF) . Автоматы, языки и программирование . Конспекты лекций по информатике. Том. 2719. с. 857. дои : 10.1007/3-540-45061-0_67 . ISBN 978-3-540-40493-4 .

Внешние ссылки [ править ]

Книги по PSL [ править ]