The Designer's Guide To PSL/ru
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Содержание |
Что такое PSL?
PSL аббревиатура от Язык описания свойств спецификации (Property Specification Language). Свойство здесь понимается, как логические данные, выраженные булевыми значениями (boolean-valued fact), о текущем тестируемом проекте. В настоящее время PSL работает с моделью описанной на VHDL или Verilog, но в будущем рамки PSL могут быть расширены для работы с другими языками. Свойства, описанные в PSL, могут быть встроены в HDL-описание, как комментарии или могут быть размещены в отдельном файле отдельно от HDL-описания.
Свойства (Properties) используются для создания утверждений (assertions). Утверждения — это инструкция для программы верификации, служащая для подтверждения того, что данное свойство поддерживается программой (that a given property holds 
). Программа верификации может быть симулятором (динамическая верификация) или программой проверки модели, которая строит математическое доказательство свойства (статическая формальная верификация).
Свойства могут играть большое количество ролей в верификации:
- Мониторы (Monitors), которые динамически проверяют состояние проекта в течение моделирования
- Ограничения (Constraints), которые устанавливают правильные (допустимые) последовательности входных векторов при моделировании
- Функциональное покрытие точек, которое позволяет оценить полноту моделирования
-
Утверждения (Assertions) доказываются программами проверки (checkers - спец. ПО) статических формальных свойств
- Предположения (Assumptions) делаются программами проверки статических формальных свойств в процессе доказательства утверждений.
Свойства в PSL складываются из булевых выражений, написанных на хост-языке (VHDL или Verilog), и временных операторов и последовательностей родных для PSL. Булевы выражения позволяют PSL выделять состояния HDL-проекта в определенный момент времени, в то время как временные операторы и последовательности описывают взаимосвязь между состояниями во времени. Что PSL привносит в лежащий в основание HDL, это возможность описывать временные взаимоотношения просто и кратко. С дальнейшим развитием, PSL также будет воспринимать выражения, описанные с помощью нейтрального формального языка GDL (General Description Language — Язык Общего Описания), в дополнение к VHDL и Verilog.
Утверждения базирующиеся на верификации
Написание утверждений происходит одновременно с разработкой RTL-модели и размещаются эти утверждения в близкой связи с RTL-кодом, что предназначено для привнесения значительных преимуществ в проект и в процессы верификации для цифрового оборудования. Первое преимущество заключается в том, что утверждения помогают обнаружить большее количество функциональных ошибок, обнаружить их на более ранних стадиях и определить наиболее возможную причину их появления. Это приводит к уменьшению числа не выявленных ошибок в продукте, к уменьшению сроков верификации и более быстрой отладке.
Второе преимущество заключается в том, что сам процесс формулирования и написания утверждении может дать разработчику возможность лучше понять проект и, следовательно, выявить ошибки в спецификации или, иначе говоря, не позволить ошибкам попасть в проект на первых порах. Однажды написанные, связанные с RTL-кодом и доказанные, утверждения играют роль формальных комментариев (спецификации). В отличие от обычных комментариев, утверждения выполняемы и непрерывно отслеживают проект на функциональную правильность, намного после того, как они оказывались в центре внимания.
Утверждения привносят возможность увеличенной измеряемости (контролируемости) в процесс верификации. Утверждения непосредственно увеличивают наблюдаемость состояния проекта во время верификации. Измеряя и контролируя плотность (частоту срабатывания) утверждений и регистрируя выполнение утверждений, так же как и ошибок, возможно привнести некоторые зная (некоторую определённость - science) в задачу определения момента, когда функциональная верификация выполнена.
В заключение, внедрение PSL, в качестве стандарта языка свойств, обеспечит дешевый и надежный путь привнесения незамедлительных преимуществ в разработку проекта и процесс верификации, также становится возможным использование новых программ верификации, таких как программы статической проверки свойств.
Развитие PSL/Sugar
PSL был впервые использован Functional Verification Technical Committee of Accellera. После процесса, в котором все возможные источники были оценены, язык Sugar из IBM был выбран в качестве базисного для PSL. The Language Reference Manual для PSL версии 1.01 был выпущен в апреле 2003-го. PSL версии 1.1, по состоянию на февраль 2004, находится в разработке.
Sugar взял свое начало, развиваясь внутри IBM, где CTL формализм (Computation Tree Logic — Вычисляемое Логическое Дерево) использовался для выражения свойств проверки модели. Сырые CTL обозначения позволяли использовать краткие выражения временной взаимосвязи, но были достаточно тяжелы для чтения и написания не специалистами. Sugar был разработан, чтобы обеспечить syntactic sugaring на верхнем уровне CTL, т.е. уровень с более удобным для пользователя синтаксисом, для того чтобы скрыть сложные обозначения. Впоследствии Sugar был расширен для поддержки последовательных регулярных выражений, расширение регулярных выражений близки для программистов Unix и Perl во временной области, что представляет собой альтернативную форму "syntactic sugaring". Была добавлена реализация проверки динамических свойств во время моделирования, и в итоге, лежащий в основе семантический фундамент перешел от CTL к LTL (Linear-time Temporal Logic — Линейная Временная Логика), т.к. позднее он был признан более удобным для моделирования и более доступным для широкой аудитории.
в настоящее время PSL предоставляет сырые CTL и LTL операторы вместе с двумя формами syntactic sugaring: временные операторы Foundation Language (FL) и Sequential Extended Regular Expressions (SERE). Семантика каждого вормально представлена в PSL Language Reference Manual.
Стандарт PSL принадлежит Accellera. The PSL/Sugar Consortium дополнительная организация, которая существует для популяризации PSL в сообществе пользователей.
Структура PSL
Язык PSL официально структурирован в четыре отдельных уровня (layers - слоя): булевый уровень (boolean), временной (temporal), уровень верификации (verification) и уровень моделирования (modelling). Уровень верификации и временной уровень имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом говорят, что PSL сочетает три «вкуса»/«привкуса» (flavour): VHDL, Verilog и GDL. «Вкус» напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
Булевый уровень состоит из булевых выражений, включающих в себя переменные и операторы основополагающего языка. Формально, булевый уровень состоит из выражений, которые представляют собой условия для оператора if базового языка. Как таковые, выражения булевого уровня оцениваются в определенный момент времени.
(a & (a-1)) == 0 // Verilog flavour (a and (a-1)) = 0 -- VHDL flavour
Временной уровень формирует основную часть языка PSL. Временной уровень может включать в себя, как выражения из булевого уровня, так и временные операторы и последовательные расширенные регулярные выражения или SEREs (SERE, Sequential Extended Regular Expression). Для временных выражений, как обычно, применяется выборка по тактовому сигналу (синхросигналу). PSL предназначен для описания синхронных схем.
(always req -> next (ack until grant)) @clk
Уровень верификации состоит из директив верификации и синтаксических конструкций, позволяющих группировать PSL-операторы и связывать их с HDL-модулями. Директивы верификации — это инструкции программе, которые поясняют, что делать со свойствами. Принцип директив верификации следующий: assert (программа должна попытаться доказать свойство), assume (программа может предположить, что данное свойство истинно) и cover (программа должна подсчитать, как часто используется свойство во время моделирования).
assert (always req -> ack) @clk;
Директивы верификации, такие как приведены выше, могут быть встроены в HDL-код, как комментарии. С другой стороны, директивы верификации могут быть сгруппированы в блоках верификации или vunits, и размещаться в отдельном файле. Существует три вида блоков верификации, vunit является наиболее общим, vprop не содержит ничего, кроме утверждений, vmode может содержать не только утверждения. Блок верификации может быть ясно связан с HDL-модулем или блоком проекта.
vunit my_properties(myVerilog.instance.name) {
assert (always req -> ack) @ clk;
assume (never req && reset)@ clk;
}
Уровень моделирования позволяет дополнительным фрагментам кода, из базового языка, включаться в свойства и расширять их, что делает возможным использовать PSL отдельно (самостоятельно). Например, уровень моделирования может использоваться для расчета ожидаемых выходных значений.
Уровень моделирования включает некоторые дополнительные языковые конструкции и удобные функции. Например, функция prev() возвращает значение выражения прошлого цикла. В настоящее время эти функции только часть уровня моделирования со «вкусом» Verilog, большинство программ, неофициально, поддерживают версии со «вкусом» VHDL.
Ключевые слова PSL чувствительны к регистру. Как вы уже могли заметить, операторы разделяются ;.
Простые свойства
Простейшая форма свойства в PSL представляет собой комбинационное булево условие, которое должно быть непрерывно правдивым.
assert always CONDITION;
Однако, эта форма свойств практически не используется, т.к. является уязвимой для многих возможных рисков. Наиболее основным является задания выборки событий или синхросигнала.
assert (always CONDITION) @(posedge clk);
Также возможно определить синхросигнал по умолчанию и, таким образом, избежать потребности в повторении явного оператора синхросигнала @ для каждого отдельного утверждения.
default clock = (posedge clk); assert always CONDITION;
Часто для свойств применяется форма импликации, которая включает предварительное условие, которое должно быть выполнено до того, как основное условие будет проверено.
assert always PRECONDITION -> CONDITION;
Данное утверждение означает, что всякий раз, когда выполняется предусловие PRECONDITION, условие CONDITION должно удовлетворяться в том же цикле. Символ -> обозначает логическую импликацию.
В общем (хотя это и необязательно) для предварительного условия и основного условия, в пределах утверждения, используется форма временной последовательности заключенной в фигурные скобки.
assert always {a;b} |-> {c;d};
Последовательность {a;b} выполняется, если условие a верно в текущем цикле, а b b — в следующем. Символ |->, находящийся между двумя последовательностями, обозначает суффиксную импликацию (suffix implication), это значит, что если первая последовательность выполняется, то вторая также должна выполняться, причем две последовательности пересекаются в одном цикле.
И наконец, для свойств, включающих условие остановки (таких как сброс (reset)), при активации которого прервётся проверка свойства в любой момент временной последовательности.
assert (always ({a;b} |-> {c;d} abort reset))
@(posedge clk);
Когда reset принимает значение истины, обязательство удержания окончания импликации удаляется, и проверяется наличие совпадений между свойством и актуальным состоянием проекта.????
Данное выражение утверждает, что при появлении сигнала reset снимаются все обязательства по выполнению условия, независимо от того, насколько свойство соответствует действительности.
Временная логика
Временные операторы фундаментального языка предоставляют syntactic sugaring для верхнего уровня LTL-операторов. Эти временные операторы включают в себя always, never, next, until and before, среди прочих. О значении операторов можно догадаться интуитивно, но здесь есть некоторые сюрпризы.
Оператор always выполняется, если его операнды выполняются в каждом отдельном цикле, в то время как оператор never выполняется, если его операнд не выполняется в каждом отдельном цикле. Оператор next выполняется, если его операнд выполняется в цикле, который немедленно следует, после текущего. Следовательно утверждение
assert always req -> next grant;
означает, что когда бы HDL-сигнал req не принимал значение "правда", HDL-сигнал grant должен принимать значение "правда" в следующем цикле. Цикл имеет типичное представление обозначенное часами по умолчанию или включая оператор времени с течением свойства. Следует отметить, что когда req принимает значение "правда", то это утверждение ничего не говорит о значении grant в любом другом цикле,кроме последующего. Также ничего не говорит о значении grant, когда req принимает значение "ложь". Это говорит лишь о том, что когда бы req не принимало значение "правда", всегда найдется случай, в котором grant примет значение "правда" уже на следующем цикле.
Оператор next может использовать число циклов,как аргумент, заключенный в квадратные скобки:
assert always req -> next[2] (grant);
Это значит, что когда бы req не принимал значение "правда", grant примет, также, значение "правда" через два цикла. Это ничего не говорит, о значении grant через один цикл, после того, как req приняло значение "правда". Интересная особенность этого утверждения заключается в том, что оно имеет место в каждом отдельном цикле, так если бы req имел значение "правда" три подряд цикла, то и grant должен держать значение "правда" три цикла, но с задержкой в два цикла. Если это утверждение реализовать,как проверку моделирования, то оно будет повторно вызываться каждый раз когда, req будет принимать значение "правда", таким образом эти одновременные вызовы проверки моделирования являются эффективным конвейером.
Смысл оператора until немного более хитрый:
assert always req -> next (ack until grant);
Это утверждает, что когда бы req не принимал значение "правда", ack принимает значение "правда" в следующем цикле и остается в этом значении до первой последовательности циклов, в которых grant принимает значение "правда". Нету обязательного значения ack в цикле, в котором grant принимает значение "правда",ни для какой последовательности циклов (кроме проверки,вызываемой req более одного раза). Если req принимает значение "правда", и затем grant принимает это же значение в следующем цикле, то ack вообще не должен принимать значение "правда". С другой стороны, не существует обязательств для grant когда-либо принимать значение "правда" следуя за req, в это случае ack будет иметь значение "правда" неопределенное время.
Цикл, в котором левый операнд until вызывается первым, определен контекстом, в котором этот оператор появился. В пример выше, ack должен принимать значение "правда" в цикле, после того, как req примет значение "правда".
И, оператор before:
assert always req -> next (ack before grant);
Смысл заключается в том, что когда бы req не принимал значение "правда", ack должен принять значение "правда" по крайней мере один раз в период, начиная со следующего цикла и заканчивая последним циклом,перед тем, как grant примет значение "правда". Не существует обязательного значения для ack ни в цикле, в котором req принимает значение "правда", ни в цикле, в котором grant принимает значение "правда". Не существует никаких правил, по которым grant должен, когда-либо принимать значение "правда", следуя за req, в это случае ack, также, не должен принимать этого значения. Другими словами, следуя за req, и ack, и grant могут оставаться в значении "ложь" неопределенное время.
Сильные операторы и живучие свойства
Заострим внимание на следующем утверждении:
assert always req -> eventually! ack;
Когда бы req не принимал значение "правда", ack должен принимать значение "правда" в будущем цикле, но это не является верхним временным пределом, при котором ack должен принимать значение "правда". Эта ситуация известна, как живучие свойства. Живучие свойства характеризуются тем фактом, что они не захватывают конечный контр-пример, и следовательно они не могут быть остановлены моделированием. Однако, живучие свойства, в принципе, могут быть остановлены или разрешены программой статической проверки модели. Свойства, которые захватывают конечные контр-примеры, известны, как безопасные свойства.
Живучие свойства были написаны в PSL, используя сильные операторы, все из которых содержат восклицательный знак в своем имени. Существуют сильные формы некоторых временных операторов: next!, until! и before!. Например:
assert always req -> next (ack until! grant);
Это означает,что когда бы req не принимало значение "правда", ack принимает "правда" в следующем цикле, ack держит "правда" до тех пор, пока не придет первый последовательный цикл, в котором grant принимает значение правда и grant должен принять "правда" в конечном счете.
Не отрицательные сильные операторы всегда создают живучие свойства, но вы должны понимать, что:
not eventually! (not P)
это эквивалентно:
always P
Последовательности
Последовательность, которая синтаксически эквивалентна временной диаграмме, часто обеспечивают наиболее удобный путь написания свойств в PSL, с временным продвижением, таким же как,если бы мы двигались по тексту слева направо. Последовательные расширенные регулярные выражения или SERE представляют компактную аббревиатуру для многих основных временных взаимоотношениях.
Рассмотрим следующее выражение:
assert always {a;b} |-> {c;d};
Как объяснялось выше, оператор "точка с запятой" выполняется только в одном цикле, в то время как оператор окончания импликации |-> означает, что первая последовательность всегда должна сопровождаться второй с перекрытием в одном цикле. (Существует альтернативный оператор окончания импликации |=>, который предполагает, что две последовательности не перекрываются.)
SERE использует длинные последовательности и семейства связанных последовательностей, написанных в компактном обозначении. Например:
-
{a[*2]}означает{a;a} -
{a[+]}означает{a;a;...;a}с повторением один или более раз -
{a[*]}означает{a;a;...;a}с повторение один или более раз, или не повторясь вообще -
{[*]}соответствует любой последовательности -
{a[=2]}означает{[*];a;[*];a;[*]}, т.е. непоследовательные повторения -
{a[*1 to 3]}означает{a}или{a;a}или{a;a;a}
Вот еще некоторые операторы,которые работают с полными последовательностями:
-
{seq1} | {seq2}означает, что одна из двух последовательностей должна удерживаться -
{seq1} & {seq2}означает, что обе последовательности должны удерживаться -
{seq1} && {seq2}означает, что обе должны удерживаться и быть одной длины
Семантика
Семантика PSL более декларативная, чем императивная, это значит, что PSL позволяет вам описывать и размышлять об абстрактных успехах состояний, в таком виде, как если бы это было применимо для проверки моделирования генерации, для формальных доказательств и документации. В отличии от свойств других языков, определение PSL не связано с идеей проверки реализации, как конечного состояния машины, выполняющегося в монотонно возрастающем времени. Действительно, есть возможность написания свойств PSL, которые не могут быть выполнены так эффективно, как проверки моделирования. Те свойства, которые могут быть выполнены также эффективно, как конечные состояния машинного автомата, говорят, что они принадлежат к простому подмножеству PSL. Большинство практических свойств попадают в категорию простого подмножества.
Семантика временного уровня определенна, учитывая все возможные пути через все возможные состояния проекта. Свойство PSL удерживается в конкретном цикле, если это соответствует ( зависит от значения временного оператора в запросе) пути, начинающемуся с текущего цикла и продолжающемуся конечное или бесконечное число циклов в будущем. Другими словами, если вы видите, что конкретное свойство удерживается, вы должны выбрать конкретный цикл, чтобы начать в нем и заглянуть вперед в дальнейший процесс, сравнивая актуальное свойство проекта с обязательствами, наложенными временным оператором. Для типичного свойства PSL (например always), это правило принимается одинаково и независимо для каждого цикла.
Семантика SERE определена отчасти по-разному, учитывая набор всех возможных последовательностей, которые могут быть сгенерированы из конкретного SERE. Например, SERE {a[+]} генерирует последовательности {a}, {a;a}, {a;a;a},... SERE плотно удерживается на конечном пути, если последовательность состояний, которые составляют этот путь, принадлежит набору последовательностей сгенерированых SERE. Другими словами, SERE, которая соответствует конкретной конечной последовательности состояний, плотно удерживается в этом пути, в то время как свойство удерживается в конкретном цикле, если это соответствует конечной или бесконечной последовательности состояний, ожидая времени, чтобы начать с этого цикла.
Еще PSL?
Изучайте больше PSL и используйте его для улучшения своего процесса верификации. Подумайте о вступлении в Assertion-Based Verification with PSL. Или,если вы хотите изучать VHDL или Verilog на более продвинутом уровне, загляните сюда Expert VHDL или Expert Verilog здесь присутствует и PSL.
