Войти
Язык спецификации свойств (PSL ) - это темпоральная логика, расширяющая линейная темпоральная логика с набором операторов для простоты выражения и повышения выразительной силы. PSL широко использует регулярные выражения и синтаксический шугаринг. Он широко используется в индустрии проектирования и проверки аппаратного обеспечения, где для подтверждения используются инструменты формальной проверки (например, проверка модели ) и / или инструменты логического моделирования. или опровергнуть, что данная формула PSL верна для данного дизайна.
PSL изначально был разработан Accellera для указания свойств или утверждений о конструкции оборудования. С сентября 2004 года стандартизация языка была проведена в рабочей группе IEEE 1850. В сентябре 2005 г. был объявлен стандарт IEEE 1850 для языка спецификации свойств (PSL).
PSL может выразить, что если какой-то сценарий произойдет сейчас, то другой сценарий должен случится некоторое время спустя. Например, свойство «запрос всегда должен в конечном итоге быть предоставлен» может быть выражено формулой PSL:
всегда (запрос ->в конечном итоге! Грант)
Свойство «каждый запрос, который сразу за ним следует сигнал подтверждения, за которым следует полная передача данных, где полная передача данных представляет собой последовательность, начинающуюся с сигнала start, заканчивающуюся сигналом end, в которой занято пока удерживается "может быть выражено формулой PSL:
(true [*]; req; ack) | =>(start; busy [*]; end)
Трасса, удовлетворяющая этой формуле, приведено на рисунке справа.
простая трассировка, удовлетворяющая (true [*]; req; ack) | =>(start; busy [*]; end)
временные операторы PSL могут быть грубо классифицированы в стиле LTL операторы и операторы в стиле регулярных выражений. Многие операторы PSL представлены в двух версиях: сильная версия, обозначенная суффиксом восклицательного знака (!), И слабая версия. Сильная версия предъявляет требования к вероятности (т.е. требует, чтобы что-то сохранялось в будущем), а слабая - нет. Суффикс подчеркивания (_) используется для различения инклюзивных и не включающих требований. Суффиксы _a и _e используются для обозначения универсальных (всех) и экзистенциальных (существующих) требований. Окна точного времени обозначаются [n], а гибкие - [m..n].
Наиболее часто используемый оператор PSL - это оператор «суффикс-импликации» (также известный как оператор «триггеры»), который обозначается | =>. Его левый операнд - это регулярное выражение PSL, а его правый операнд - это любая формула PSL (будь то в стиле LTL или в стиле регулярного выражения). Семантика r | =>p состоит в том, что в каждый момент времени i, такой, что последовательность моментов времени до i составляет соответствие регулярному выражению r, путь от i + 1 должен удовлетворять свойству p. Это проиллюстрировано на рисунках справа.
путь, удовлетворяющий r триггерам p двумя неперекрывающимися способами 
путь, удовлетворяющий r триггерам p двумя перекрывающимися способами 
путь, удовлетворяющий r триггерам p 'тремя способами Регулярные выражения PSL имеют общие операторы для конкатенации (;), замыкания Клини (*) и объединения (|), а также оператора для объединения (:), пересечения (\ \ ) и более слабую версию (\ ), а также множество вариантов для последовательного подсчета [* n] и последовательного подсчета, например [= n] и [->n].
Есть несколько вариантов оператора триггера, которые показаны в таблице ниже.
Здесь s и t - регулярные выражения PSL, а p - формула PSL.
с | =>т! | если есть совпадение s, то есть совпадение t в суффиксе трассы,
|
s | ->t! | если есть совпадение s, то есть совпадение t в суффиксе трассы,
|
s | =>t | если есть совпадение s, то есть совпадение t в суффиксе трассы,
|
s | ->t | если есть совпадение s, то есть совпадение t на суффиксе трасса,
|
Операторы конкатенации, слияния, объединения, пересечения и их варианты показаны в таблице ниже.
Здесь s и t - регулярные выражения PSL.
с; t | соответствие s, за которым следует совпадение t, t запускает цикл после того, как s заканчивается |
s: t | соответствие s, за которым следует совпадение t, t запускает тот же цикл, который заканчивается s |
с | t | совпадение s или совпадение t |
s t | совпадение s и совпадение t, продолжительность обоих имеет одинаковую длину |
s t | совпадение s и совпадение t, продолжительность совпадений может быть различной |
s в пределах t | совпадений s в пределах совпадения t, сокращение ([*]; s; [*]) (t) |
Показаны операторы для последовательных повторений в таблице ниже.
Здесь s - регулярное выражение PSL.
s [* i] | i последовательных повторений s |
s [* i..j] | от i до j последовательных повторений s |
s [* i..] | не менее i до последовательных повторений s |
s [*] | ноль или более последовательных повторений s |
s [+] | одно или более последовательных повторений s |
Операторы для не- последовательные повторы показаны в таблице ниже.
Здесь b - любое логическое выражение PSL.
b [= i] | i не обязательно последовательные повторения b,
|
b [= i..j] | не менее i и не более j, не обязательно последовательные повторения b,
|
b [= i..] | по крайней мере i не обязательно последовательные повторения b,
|
b [->m] | m не обязательно последовательные повторения b, заканчивающиеся на b,
|
b [->m: n] | не менее m и не более n не обязательно последовательных повторений b, оканчивающихся на b,
|
b [->m..] | не менее m не обязательно последовательных повторений b, заканчивающихся на b,
|
b [->] | ярлык для b [->1],
|
Ниже приведен пример некоторых операторов PSL в стиле LTL.
Здесь p и q - любые формулы PSL.
всегда p | свойство p сохраняется в каждой временной точке |
никогда p | свойство p не сохраняется ни в какой временной точке |
в конечном итоге! 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 до! q | существует момент времени, в котором q удерживается, и p удерживается до этого момента времени |
p, пока q | p не удерживается до момента времени, в котором q удерживается, если таковой существует |
p до! _ q | существует момент времени, в котором q сохраняется, а p сохраняется до этого момента времени, а в этом моменте времени |
p до_ q | p сохраняется до момента времени, в котором q сохраняется, и в этом момент времени, если он существовал |
p до! q | p выполняется строго до момента времени, в котором выполняется q, и в конечном итоге p выполняется |
p до того, как q | p выполняется строго до момента времени, в котором выполняется q, если p никогда не выполняется, то и q |
p до! _ q | p выполняется до или в тот же момент времени, когда q выполняется, а p в конечном итоге сохраняет |
p before_ q | p выполняется до или в тот же момент времени, где q выполняется, если p никогда не выполняется, то и q |
Иногда желательно изменить определение следующей временной точки, например, в многочастотных проектах или когда требуется более высокий уровень абстракции. Для этой цели используется оператор выборки (также известный как оператор часов), обозначенный @. Формула p @ c, где p - формула PSL, а логические выражения ca PSL сохраняются на заданном пути, если p на этом пути проецируется на циклы, в которых выполняется c, как показано на рисунках справа.
путь и формула, показывающие необходимость в операторе выборки Первое свойство гласит, что «каждый запрос, за которым сразу следует сигнал подтверждения, должен сопровождаться полной передачей данных, где полная передача данных - это последовательность, начинающаяся с сигнала start, заканчивающаяся сигналом end, в которой данные должны удерживаться не менее 8 раз:
((true [*]; req; ack) | =>(start; data [= 8]; end)
Но иногда желательно рассматривать только случаи, когда указанные выше сигналы возникают в цикле, где clk высокий. Это изображено на втором рисунке. в котором, хотя формула
((true [*]; req; ack) | =>(start; data [* 3]; end) @ clk
использует data [* 3] и [* n] - последовательное повторение, соответствующая трасса имеет 3 непоследовательных временных точки, в которых хранятся данные, но при рассмотрении только временных точек, в которых сохраняется clk, временные точки, в которых удерживаются данные, становятся последовательный.
путь и формула, показывающие эффект операции выборки r @ Семантика формул с вложенным @ немного тонкая. Заинтересованным читателям отсылаем к [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), такие как:
Когда PSL используется вместе с одним из вышеуказанных HDL, его логический уровень использует операторы соответствующего HDL.
