Checking of circuit implementation of incompletely specified Boolean functions .pdf Полупроводниковая промышленность за последнее десятилетие сделала возможным проектирование сверхбольших интегральных схем (СБИС), состоящих из сотен миллионов транзисторов. В то же время все возрастающая важность быстрой поставки продукции на рынок требует производить схемы за короткое время. В таких условиях появление ошибки в функциональности проектируемых устройств обходится очень дорого. По мере усложнения СБИС все более ответственным этапом проектирования становится верификация. Целью верификации является доказательство того, что реализованное и требуемое поведение проектируемого устройства совпадают. В настоящее время верификация используется на всех этапах проектирования: от концептуального проектирования до проектирования комбинационных схем, и занимает до 70% общего времени проектирования.Задача верификации в традиционной постановке состоит в проверке функциональной эквивалентности пары комбинационных схем, представляющих разные структурные реализации одного и того же устройства. Решению этой задачи посвящены многочисленные научные публикации, ссылки на некоторые из них можно найти в [1 - 5]. При проверке эквивалентности комбинационных схем обе верифицируемые схемы обычно преобразуются в одну схему, называемую схемой сравнения. Схема сравнения - это комбинационная схема с теми же самыми входами, что и исходная схема и одним выходом. Она получается путем объединения пар одноименных входов схем и подачи пар одноименных выходов схем на двух-входовые элементы исключающее ИЛИ, выходы которых подаются на элемент ИЛИ. Константа 0 на выходе элемента ИЛИ появляется тогда и только тогда, когда исходные схемы эквивалентны, т.е. порождают одинаковые значения на выходах при любых возможных комбинациях сигналов на входах.В данной статье задача верификации рассматривается для случая, когда заданная функциональность проектируемого устройства не полностью определена. Такая ситуация обычно возникает на начальных этапах проектирования, когда существуют такие комбинации значений входных переменных проектируемого устройства, которые никогда не появятся при нормальном режиме его работы. В процессе проектирования устройства его выходные реакции на такие входные воздействия доопределяются произвольным образом. В этом случае при решении задачи верификации достаточно рассмотреть только возможные сценарии поведения верифицируемого устройства и проверить, имеют ли выходные реакции реализованного устройством поведения специфицированные значения.В настоящее время наиболее широко используемым в промышленности подходом для проверки функциональности цифровых интегральных схем является логическое моделирование по причине простоты его реализации и предсказуемости времени выполнения. Этот подход основан на тестировании устройства путем подачи на его входы двоичных сигналов, продвижения их по схеме и соответствующей активации выходов, на которых сигналы должны иметь ожидаемые значения. Для рассматриваемого случая верификации можно применить особый тип моделирования, а именно направленное моделирование, когда тестирующие входные воздействия задаются спецификацией на проектирование устройства. Данная идея развивается в настоящей работе для случая, когда исходная спецификация проектируемого устройства задана на наборах значений входных переменных или интервалах (совокупностях наборов) небольшого размера. В том случае, когда исходное задание определено на интервалах большого размера, моделирование практически не применимо, поскольку необходимое расщепление интервалов на отдельные наборы в этом случае приводит к экспоненциальному взрыву. Для такого случая в настоящей работе предлагается метод, основанный на сведении задачи верификации к задаче проверки выполнимости КНФ.Таким образом, в данной статье рассматривается задача верификации для случая, когда:спецификация на проектирование задана в виде системы частично определенных булевых функций; функции системы заданы на интервалах значений входных переменных; система реализована комбинационной схемой в базисе многовходовых логических элементов типа И, ИЛИ, И-НЕ, исключающее ИЛИ и т.д. и инверторов. Предлагается комбинированный подход к проверке, реализуется ли система частично определенных булевых функций заданной комбинационной схемой. Метод основан на моделировании комбинационной схемы на наборах значений входных переменных части области задания системы функций и сведении проверки реализации остальной части к задаче выполнимости КНФ.2. Основные определения2.1. Булевы функции и их представленияСистема F = ■ ■ ■, fm(X) } (или f (x) в векторной форме, где x и f век-торы значений входных и выходных переменных) полностью определенных булевых функций (ПБФ) есть отображение между n-мерным и m-мерным булевыми пространствами E = {0, 1}:f (x): En - Em. Частично определенная булева функция (ЧБФ) задается отображением f (x): En - {0,1,-}m, где символ - обозначает неопределенное значение. ЧБФ не полностью определена на всем булевом про-странстве En. ПБФ f (x) реализует ЧБФ g(x), если f (x) можно получить из g(x) доопределением (до 0 или 1) значений g(x) на тех элементах пространства En, на которых ее значения не определены.Множество равенств типа xt = ст,- (где ст,- е {0, 1}, i = {1, 2,„., n}) назовем присваиванием значений компонентам вектора x = (x1, x2, ■ xn). Присваивание а значений компонентам вектора x может быть полным, если задаются все x,, или частичным в противном случае. Полное присваивание представляет собой элемент (набор), а частичное присваивание - интервал булевого пространства En. Интервал ранга k фиксирует значения k переменных и покрывает 2n-k элементов булева пространства. Его можно представить также в виде конъюнкции k литералов (под литералом понимается булева переменная или ее отрицание). В общем случае элементарная конъюнкция kj и соответствующий ей интервал покрывает (или поглощает) элементарную конъюнкцию k (и соответствующий ей интервал), если множество литералов из kj являются подмножеством литералов из k;.ЧБФ f (x) задается множествами Uf0, Uf и Uf* интервалов (или элементов) булева пространства En, на которых она принимает соответственно нулевое, единичное и неопределенное значения, при этом Uf u U0 u UfS = En . Будем задавать систему ЧБФ f(x) множеством многовыходных интервалов. Многовыходной интервал (и, t ) представляется парой троичных векторов длины n и m, которые называются соответственно его входной и выходной частями. Входная часть и представляет собой интервал из En или конъюнкцию литералов некоторых x; е X. Выходная часть t является троичным вектором значений функций на интервале и или конъюнкцией литералов некоторых f е F. Для каждой функции f е F справедливо: если j-я компонента tj вектора t есть 1 (tj = 1) или 0 (tj = 0), то все элементы интервала и принадлежат множеству Ufj1 единичных значений функции fj или соответственно множеству Uf0 ее нулевых значений; если же значение tj не определено (tJ = -), то функция fj либо может принимать разные значения на разных наборах из интервала и, либо ее значение может быть не определено на всем интервале.Конъюнктивная нормальная форма представляет булеву функцию в виде конъюнкции одного или более дизъюнктов. Каждый дизъюнкт, в свою очередь, является дизъюнкцией одного или более литералов (соответствующих разным переменным).КНФ задает некоторую полностью определенную булеву функцию f(x), и каждый из ее дизъюнктов соответствует имплиценте этой функции. Задача проверки выполнимости КНФ заключается в нахождении такого присваивания (может быть частичного) значений переменным из X, которое обращает КНФ в 1. Если такое присваивание удается найти, то говорят, что КНФ выполнима и полученное присваивание называют выполняющим эту КНФ. Иначе КРФ не выполнима, невыполнимая КНФ представляет функцию, тождественно равную 0.Матричные модели представления булевых функций и КНФ. Матричное представление КНФ, имеющей k дизъюнктов и n переменных, задается троичной матрицей C, строки которой задают дизъюнкты, столбцы соответствуют переменным. Элемент cj на пересечении i-й строки и j-го столбца матрицы C принимает значение 1, 0 или -, в зависимости от формы (x,- или xj) переменной xj или ее отсутствия в i-ом дизъюнкте КНФ. Аналогичным образом ЧБФ f (x) в матричном виде представляется парой троичных матриц tf1 и Uf0, в которых каждая строка соответствует некоторому интервалу из Uf и Uf0 соответственно.Система ЧБФ f (x), заданная множеством S многовыходньгх интервалов (и;, t; ), может быть представлена парой троичных матриц U и T с одинаковым числом строк (рис. 1). Строки матрицы U задают входные части многовыходных интервалов из S; аналогично строки матрицы T задают их выходные части.Xi Х2 Х3 Х4 XS f f- -111 1 - 111--- 10 2U =- 0 0 0 - T = 0 1 30 1 - 1 0 0 0 4-010- - 0 5-0-10 - 1 6Рис. 1. Пример матричного задания системы частично определенных булевых функцийПредставление функций в форме многовыходных интервалов имеет следующие отличительные особенности. Интервалы и;, и,- е U могут пересекаться (в отличие от задания функции на наборах значений аргументов). Неопределенное значение элемента tj матрицы T может трактоваться двояко: или значение функции fj не определено на всем интервале и;, или функция f принимает разные значения на отдельных наборах этого интервала.2.2. Комбинационная схемаРассматриваемая комбинационная схема представляет собой сеть из инверторов и многовыходных логических элементов, которые реализуют простые логические функции типа И, ИЛИ, И-НЕ, ИЛИ-НЕ, исключающее ИЛИ и т.д. На рис. 2 приведен пример комбинационной схемы с пятью входами, двумя выходами и семью логическими элементами. Структура комбинационной схемы может быть представлена направленным ациклическим графом, в котором вершины соответствуют логическим элементам, внешним входам и выходам схемы, а ребра - соединениям элементов и внешних полюсов.Xi Х2 Хз Х4 Х5 Zi Z2 Z3 ух у21--- -0- --- 1-1---0 200-- -1- --- 3--- 1 --0--- 4 1-0--- 5•·- - 00 - 1- - - 6 •-0- --1 0-- 7 •- 1- - - - 1-- 8 •- - - - - 01-- 9 •- - - -11 - 0- 10 •- - - - 0 - - 1- 11 •- - - - -0 - 1- 12 •0- - - - - - -0 13 •- - - - - - 1 - 0 14 •1 - - - - - 0 - 1 15Рис. 2. Комбинационная схема и ее КНФ разрешенияБудем обозначать выходные полюсы элементов и сами элементы одним и тем же именем. Локальная функция элемента (полюса схемы) определяет зависимость сигнала на выходе элемента от сигналов на его входах (т. е. задается в терминах локальных входных переменных). Глобальная функция элемента (полюса) определяет зависимость сигнала на выходе элемента от сигналов на входах схемы (т. е. задается в терминах входных переменных схемы).3. Верификация, основанная на моделировании комбинационной схемыПри проверке реализуемости системы частично определенных булевых функций поведение комбинационной схемы моделируется на области задания этой системы. Система F булевых функций, заданная множеством S многовыходных интервалов, реализуется схемой, если для каждого набора bk значений переменных, покрываемого входной частью и, е U каждого из многовыходных интервалов (и,, tj ) е S, выполняется условие поглощаемости булева вектора y (bk) значений функций, реализуемых на выходах схемы, троичным вектором ti е T.Будем использовать идею параллельного моделирования [6, 7], проводя моделирование многовыходной логической схемы сразу на всех двоичных наборах, покрываемых входными частями и, е U многовыходных интервалов (и,, t, ) е S. При переходе к представлению системы F на наборах многовыходной интервал (щ, ti ) е S порождает 2n-k многовыходных наборов (b,,-, tt ), где k - ранг интервала иь bji - набор значений переменных, покрываемый интервалом и,. После раскрытия многовыходных интервалов и группирования полученных многовыходных наборов, имеющих равные входные части, каждое из множеств многовыходных наборов (b, tt ) (с одной и той же входной частью b) заменяется одним многовыходным набором (b, t ), где t поглощается каждой из выходных частей ti этих наборов.Таким образом, троичная матрица U преобразуется в булеву матрицу B, задающую наборы значений входных переменных системы F, а матрица T преобразуется в матрицу T ', задающую значения частично определенных булевых функций на этих наборах.При параллельном моделировании схемы на / наборах состояние каждого полюса (включая входные и выходные) схемы представляется булевым вектором размерности /. Таким образом, каждый вектор представляет состояния одного полюса для всех / состояний на входе схемы, а совокупность одноименных компонент всех векторов соответствует состоянию всех полюсов схемы для одного и того же входного набора.В начале моделирования имеется упорядоченное множество n булевых векторов размерности /, представляющих состояния n входных полюсов для всех / наборов. Затем последовательно просматриваются элементы (в порядке возрастания их номеров) предварительно ранжированной схемы, и для каждого i-го элемента вычисляется локальная функция

Скачать электронную версию публикации