Язык спецификации свойств ( PSL ) - это темпоральная логика, расширяющая линейную темпоральную логику с помощью ряда операторов как для простоты выражения, так и для повышения выразительной силы. PSL широко использует регулярные выражения и синтаксический шугаринг. Он широко используется в индустрии проектирования и верификации оборудования, где используются формальные инструменты верификации (такие как проверка модели ) и / или инструменты логического моделирования , чтобы доказать или опровергнуть, что данная формула PSL верна для данной конструкции.
Первоначально PSL был разработан Accellera для определения свойств или утверждений о конструкции оборудования. С сентября 2004 года стандартизация языка проводилась в рабочей группе IEEE 1850. В сентябре 2005 г. был объявлен стандарт IEEE 1850 для языка спецификации свойств (PSL).
Синтаксис и семантика [ править ]
PSL может выразить, что если какой-то сценарий произойдет сейчас, то другой сценарий должен произойти через некоторое время. Например, свойство « запрос всегда в конечном итоге должен быть удовлетворен » может быть выражено формулой PSL:
всегда (запрос -> в конце концов! грант)Свойство «каждый запрос , который сразу же следует Ack сигнал, должно сопровождаться полной передачей данных , где полная передача данных представляет собой последовательность , начиная с сигналом началом , заканчивая сигналом конца , в котором занят держит в то же время» может быть выражается формулой PSL:
(true [*]; req; ack) | => (начало; занято [*]; конец)След, удовлетворяющий этой формуле, показан на рисунке справа.
Временные операторы PSL можно грубо разделить на операторы в стиле LTL и операторы в стиле регулярных выражений . Многие операторы PSL представлены в двух версиях: сильная версия, обозначенная суффиксом восклицательного знака ( ! ), И слабая версия. Сильная версия делает требование к неожиданностям (т.е. требует , чтобы что - то будет держать в будущем), в то время как слабая версия не делает. Подчеркивание суффикс ( _ ) используется для дифференциации включительно против не включены требований. An _A и _e суффиксы используются для обозначения универсальной(все) против экзистенциальных (существующих) требований. Окна точного времени обозначаются [n], а гибкие - [m..n] .
Операторы в стиле SERE [ править ]
Наиболее часто используемый оператор PSL - это оператор "суффикс-импликация" (также известный как оператор "триггеры"), который обозначается | => . Его левый операнд - это регулярное выражение PSL, а его правый операнд - это любая формула PSL (будь то в стиле LTL или в стиле регулярного выражения). Семантика r | => p состоит в том, что в каждую временную точку i, такую, что последовательность временных точек до i составляет соответствие регулярному выражению r, путь от i + 1 должен удовлетворять свойству p. Это проиллюстрировано на рисунках справа.
Регулярные выражения PSL имеют общие операторы для конкатенации ( ; ), Клини замыкание ( * ), и объединение ( | ), а также оператор слияния ( : ), пересечения ( \ & \ & ) и более слабой версии ( \ & ), а также множество вариантов для последовательного подсчета [* n] и последовательного подсчета, например [= n] и [-> n] .
Есть несколько вариантов оператора триггера, которые показаны в таблице ниже.
Здесь s и t - регулярные выражения PSL, а p - формула PSL.
с | => т! | если есть совпадение s, то есть совпадение t на суффиксе трассы,
|
с | -> т! | если есть совпадение s, то есть совпадение t на суффиксе трассы,
|
с | => т | если есть совпадение s, то есть совпадение t на суффиксе трассы,
|
с | -> т | если есть совпадение s, то есть совпадение t на суффиксе трассы,
|
Операторы конкатенации, слияния, объединения, пересечения и их варианты показаны в таблице ниже.
Здесь s и 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..] | как минимум i до последовательных повторений s |
s[*] | ноль или более последовательных повторений s |
s[+] | одно или несколько последовательных повторений s |
Операторы для непоследовательных повторов показаны в таблице ниже.
Здесь b - любое логическое выражение PSL.
b[=i] | я не обязательно последовательные повторения b,
|
b[=i..j] | не менее i и не более j, необязательно последовательных повторений b,
|
b[=i..] | по крайней мере я не обязательно последовательные повторения b,
|
b[->m] | m не обязательно последовательные повторения b, заканчивающиеся на b,
|
b[->m:n] | не менее m и не более n не обязательно последовательных повторений b, заканчивающихся на b,
|
b[->m..] | по крайней мере m не обязательно последовательных повторений b, заканчивающихся на b,
|
b[->] | ярлык для b [-> 1],
|
Операторы в стиле LTL [ править ]
Ниже приведен пример некоторых операторов PSL в стиле LTL.
Здесь p и 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 @ c, где p - формула PSL, а c - логические выражения PSL, выполняются на заданном пути, если p на этом пути проецируется на циклы, в которых выполняется c , как показано на рисунках справа.
Первые государства собственности , что «каждый запрос , который сразу же следует Ack сигнал, должен сопровождаться полной передачей данных , где полная передача данных представляет собой последовательность , начиная с сигналом началом , заканчивая сигналом конца , в котором данные должны занимать по меньшей мере , 8 раз:
((true [*]; req; ack) | => (начало; данные [= 8]; конец)Но иногда желательно рассматривать только те случаи, когда вышеуказанные сигналы возникают в цикле с высоким 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;
|
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 . Другими не-LTL операторами PSL являются @оператор для определения многочастотных схем, операторы прерывания для работы с аппаратным сбросом и локальные переменные для краткости.
Слои [ править ]
PSL определяется на 4 уровнях: логический уровень , временной уровень , уровень моделирования и уровень проверки .
- Логический слой используется для описания текущего состояния конструкции и сформулирован с помощью одного из указанных выше ЛВПА.
- Височной слой состоит из временных операторов , используемых для описания сценариев , которые с течением времени продолжительности (возможно , в течение неограниченного количества единиц времени).
- Моделирования слой может быть использован для описания вспомогательных машин состояний в процедурном порядке.
- Уровень проверки состоит из директив для средства проверки (например, чтобы утверждать, что данное свойство является правильным, или предполагать, что определенный набор свойств является правильным при проверке другого набора свойств).
Совместимость языков [ править ]
Язык спецификации свойств может использоваться с несколькими языками проектирования электронных систем (HDL), такими как:
- VHDL (IEEE 1076)
- Verilog (IEEE 1364)
- SystemVerilog (IEEE 1800)
- SystemC (IEEE 1666) от Open SystemC Initiative (OSCI) .
Когда PSL используется вместе с одним из вышеуказанных HDL, его логический уровень использует операторы соответствующего HDL.
Ссылки [ править ]
- 1850-2005 - Стандарт IEEE для языка спецификации свойств (PSL) . 2005. DOI : 10,1109 / IEEESTD.2005.97780 . ISBN 0-7381-4780-X.
- МЭК 62531: 2007 62531-2007 - МЭК 62531 Ред. 1 (2007-11) (IEEE Std 1850-2005): Стандарт языка спецификации свойств (PSL) . 2007. DOI : 10,1109 / IEEESTD.2007.4408637 . ISBN 978-0-7381-5727-6.
- 1850-2010 - Стандарт IEEE для языка спецификации свойств (PSL) . 2010. DOI : 10,1109 / IEEESTD.2010.5446004 . ISBN 978-0-7381-6255-3.
- IEC 62531: 2012 62531-2012 - IEC 62531: 2012 (E) (IEEE Std 1850-2010): Стандарт языка спецификации свойств (PSL) . 2012. DOI : 10,1109 / IEEESTD.2012.6228486 . ISBN 978-0-7381-7299-6.
- Эйснер, Синди; Фисман, Дана; Гавличек, Джон; Люстиг, Йоад; МакИсаак, Энтони; Ван Кэмпенхаут, Дэвид (2003). «Рассуждения с временной логикой на усеченных путях» (PDF) . Компьютерная проверка . Конспект лекций по информатике. 2725 . п. 27. DOI : 10.1007 / 978-3-540-45069-6_3 . ISBN 978-3-540-40524-5.
- Эйснер, Синди; Фисман, Дана; Гавличек, Джон; МакИсаак, Энтони; Ван Кэмпенхаут, Дэвид (2003). «Определение оператора временных часов» (PDF) . Автоматы, языки и программирование . Конспект лекций по информатике. 2719 . п. 857. DOI : 10.1007 / 3-540-45061-0_67 . ISBN 978-3-540-40493-4.
Внешние ссылки [ править ]
- Рабочая группа IEEE 1850
- Объявление IEEE, сентябрь 2005 г.
- Accellera
- Учебное пособие по языку спецификации свойств
- Руководство для дизайнеров по PSL
Книги на PSL [ править ]
- Использование PSL / Sugar для формальной и динамической проверки, 2-е издание, Бен Коэн, Аджита Кумари, Шринивасан Венкатараманан
- Практическое введение в PSL, Синди Эйснер, Дана Фисман
