PSL/A Practical Introduction to PSL/Some Philosophy/ru

Немного философии

Мы рассмотрели немного основ PSL и получили ощущение того, как используется. Перед тем как продолжить, мы обсудим некоторые концепции в корне PSL.

3.1 Утверждения против свойств

Как мы уже видели, утверждения PSL состоят из ключевого слова assert плюс свойства PSL для утверждения, разделенных точкой с запятой. Например, в утверждении assert always (a -> next b);, свойство - always (a -> next b). Свойство выполняется или не выполняется в данном тракте. Утверждение, с другой стороны, указывает программе верификации, что свойство было утверждено, и требуется выполнение. Далее в книге мы будем внимательно рассматривать отличия между свойствами, которые просто описывают поведения, и утверждения,которые устанавливают требования. Например, мы можем сказать, что утверждение assert always (a -> next b); требует, чтобы когда бы сигнал a не утверждался, сигнал b должен будет утвердиться в следующем цикле. Однако, мы никогда не скажем такого о свойстве always (a -> next b), по двум причинам. Первая - потому что если свойство используется в предположении (assume always (a -> next b);), то нету никаких требований. Вторая - потому что свойство может использоваться, как под-свойство более сложного свойства, и если так, то не может исходить требований от него самого.

3.2 Понятие времени

Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении - утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется. Для более сложных утверждений PSL, которые, во-первых, находяться отдельно от кода (таким образом понятие “исполнение” чужое для них), и во-вторых охватывает множество шагов во времени, понятию времени необходими уелить больше внимания.

PSL предполагает, что время дискретно, таким образом, время состоит из последовательности оцененных циклов. Значение свойства PSL определенно по отношению к такой последовательности циклов. В этой книге, мы будем называть такую последовательность циклов трактом.

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

Тем не менее, существует путь гарантировать, что значение свойства PSL не влияет на степень детализации времени, с точки зрения программ верификации. Свойства PSL могут быть модифицированы, используя временное выражение для того, чтобы показать, что время должно быть получено во временных циклах временного выражения. В случаи временного свойства, результат программы базирующейся на циклах должен быть такой же, как и для программы базирующейся на изменениях. PSL допускает спецификацию времени по-умолчанию, таким образом, что время не должно быть упомянуто отдельно для каждого свойства. Далее в этой книге мы предполагаем однократный тактовый проект под модель, базирующуюся на циклах, таким образом в большинстве примеров опущены явные упоминания о времени.

3.3 Проекты и тракты

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

Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11.

3.4 Текущий цикл, субтракты, модульность

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

Предполагая, что циклы тракта нумеруются, начиная с 0, текущий цикл утверждения - 0. Текущий цикл под-свойства, какого-нибудь вшитого свойства, зависит от своего использования во вшитом свойстве. Операнды Булевого оператора получают такой же текущий цикл, как и родительское свойство. Операнды временных операторов получают текущий цикл, который связан с текущим циклом родительского свойства, в случаи, если это указано временным оператором. Например, оператор next увеличивает текущий цикл на один, оператор always создает “несколько экземпляров” под-свойства, каждый из которых получает текущий цикл, который соответствует текущему циклу или некоторому будущему циклу.

Примечание: Очень важно понять, что термин “несколько экземпляров” предназначен для смысла, который используется для понимания оператора always. Не предназначем показать, что каждый экземпляр существует; причем это не значит, что программе реализации PSL надо создать много экземпляров проверки утверждения, порождение нескольких экземпляров процесса или в любом другом случаи слова “несколько экземпляров” означают актуальные экземпляры чего-либо. Наоборот, существуют множество эффективных реализаций PSL, в которых оператор always не создает нескольких экземпляров. Термин “несколько экземпляров” - это хороший способ усилить понятие того, как работает оператор always, наивная и неэффективная реализация могжет также реализовывать несколько экземпляров проверки или процесса.

Возвращаясь к нашему основному пункту рассмотрения, рассмотрим утверждение assert always (a -> next b);. Текущий цикл always (a -> next b) - 0. Выполнение always (a -> next b) в цикле 0, зависит от выполнения под-свойства (a -> next b) в каждом цикле с нулевого. Текущий цикл для частной оценки под-свойства (a -> next b) будет некий цикл N. В итоге, для того, чтобы определить действительно ли под-свойство (a -> next b) выполняется в цикле N, мы должны оценить под-свойство a и следующий b с текущим циклом N, что значит, что нам надо оценить под-свойство b с текущим циклом N + 1.

Для того чтобы сделать обсуждения конкретней, давайте рассмотрим наше утверждение, утверждение 3.1а на тракте 3.1(i). Сигнал а выполняется в циклах 4 и 8. Сигнал b выполняется в цикле 5, next b выполняется в цикле 4. Это показано в тракте 3.1(ii), аннотированная версия тракта 3.1(i). В то время, как а выполняется в циклах 4 и 8, и next b выполняется в цикле 4, мы получаем, что (a -> next b) выполняется во всех циклах, а цикл 8,как показано на тракте 3.1(ii). (Запомните, что в других частях по умолчанию справедливо, что (a -> next b) выполняется во всех циклах, где a не выполняется, и в дополнение во всех циклах где a выполняется и next b тоже.) Все свойство always (a -> next b) выполняется в циклах 9, 10, 11, 12, 13 (потому что в этих циклах (a -> next b) выполняется “сейчас” и во всех следующих циклах). Таким образом, утверждение 3.1a не выполняется на тракте 3.1(i) (потому что оно не выполняется в цикле 0 - первом цикле тракта).

assert always (a -> next b); (3.1a)
Рис. 3.1: Конкретный пример

Приведенное выше описание кажется простым. Однако, идея модульности скрывает некоторые тонкие моменты, например, что значение свойства a зависит только от текущего цикла. Таким образом, утверждение 3.2а выполняется нна тракте 3.2(i), потому что сигнал a выполняется в цикле 0. Если вы хотите выразить тот факт, что a должен выполняться в каждом цикле, вы должны использовать оператор always, как в утверждении 3.2b. Утверждение 3.2b не выполняется на тракте 3.2(i).

Другой тонкий момент, что свойство может выполняться в суффиксе тракта,а не на самом тракте. Таким образом, свойство always a выполняется на субтракте тракта 3.2(i), начиная с циклов 12, 13, 14. Это будет важно, если мы используем свойство always a, как под-свойство какого-либо друо свойства. Например, утверждение 3.2c выполняется на тракте 3.2(i), потому что свойство always a выполняется на 12^ти следующих циклах.

Последнее, циклы вовлеченные в в подсчет левой стороны логической импликации могут прекрываться с циклами вовлеченными в подсчет правой стороны логической импликации. Например, рассмотрим утверждение 3.3a на тракте 3.3(i). Утверждение 3.3a выполняется на тракте 3.3(i), потому что под-свойство (a && next[6] (b)) -> (c && next[2] (d)) выполняется на всех циклах. Оно выполняется в цикле 2, потому что левая сторона (a && next[6] (b)) выполняется и в дополнение правая сторона (c && next[2] (d)), тоже выполняется. Оно выполняется во всех других циклах, потому что, если часть “if” логического исполнения не выполняется, то по-умолчанию часть “else” принимает значение правда

(i) Утверждение 3.2a и 3.2c выполняются, но 3.2b нет
assert a; (3.2a) assert always a; (3.2b) assert next[12] (always a); (3.2c)
Рис. 3.2: Важность оператора always

(i) Иллюстрация перекрытие левой и правой стороны утверждение 3.3a. Утверждение 3.3a выполняется.
assert always ((a && next[6](b)) -> (c && next[2](d))); (3.3a)
Рис. 3.3: Текущий цикл

Предварительно, например в рассматриваемых утверждениях 2.2а и 2.3b, мы видели случаи, где были перекрытия между циклами вовлеченными в удовлетворение двух разных случаев левой стороны логической импликации. Эти перекрытия вызваны присутствием оператора always в свойстве. Если мы удалим этот оператор, вопрос перекрытия исчезнет из утверждений 2.2a и 2.3b. Перекрытие утверждения 3.3а отличается от перекрытия утверждений 2.2a и 2.3b, и это очень важно: утверждение 3.3a написано таким образом, что циклы вовлеченные в подсчет левой стороны логической импликации перекрываются с циклами правой логической импликации: подсчитывая часть “if” логической вовлекают рассматриваемый текущий цикл, а также “предстоящие” шесть циклов, в то время как подсчет части “then” логической импликации вовлекает рассматриваемый текущий цикл и также “предстоящие” два цикла. Таким образом,перекрытие появляется от самой логической импликации. Такой стиль PSL свойств, обычно, труден для новых пользователей PSL, и вообще это не интуитивный способ использования языка. Поэтому, такие свойства не рекомендуется использовать, и простое подмножество ограничений языка PSL не позволяет использование таких свойств. Мы обсудим простое подмножество в деталях поздней. На данный момент, запомните, что если вы написали свойство, в котором циклы вовлечены в подсчет левой стороны одного оператора перекрываются в течение более одного цикла с циклами вовлеченными для подсчета правой стороны того же оператора, то вы написали свойство не относящиеся к простому подмножеству.

3.5 Сообщение об ошибке

Рассмотрим утверждение 3.4а на тракте, показаном на рисунке 3.4. Очевидно, утверждение 3.4a не выполняется на нем. Сейчас рассмотрим четыре разных вида инструментов верификации, каждый из которых, выдает сообщение об ошибке утверждения 3.4a, индикаций сигнала, называемого “failure” в трактах 3.4(i), 3.4(ii), 3.4(iii) и 3.4(iv). Инструмент 1 выдал сообщение об ошибке на цикле 4, наиболее ранний выриант,на котором это можно выявить. Инструмент 2 выдал сообщение на цикле 4, а также на цикле 7, когда b утверждается второй раз. Инструмент 3 выдал сообщение в конце тракта, и инструмент 4 выдал сообщение на цикле 11,когда утверждается a.

Какой инструмент сработал правильно? Правильный ответ - все они. PSL определяет выполняется ли свойство в тракте - вот и все. ничего не сказано о том, когда инструмент, динамический или статический, должен выдать сообщение по результатам анализов. Таким образом, нету смысла в вопросе - какой инструмент правильный? Все они показали, что свойство не выполняется на тракте, поэтому все они верны. Индикация ошибки показанная на все тракте может пониматься, как помощь для дебага, помогая пользователям понять,где находиться ошибка на тракте. Пока PSL показывает эти ошибки на трактах, он делает свою работу.

assert always (a -> never b); (3.4a)
Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте