Трансляция VHDL программы в BDD структуры
В статье представлена автоматизированная система, упрощающая процесс верификации. Рассмотрен процесс преобразования VHDL программы в BDD структуры.
Saved in:
| Date: | 2003 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2003
|
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/6394 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Трансляция VHDL программы в BDD структуры / Д.А. Закутайло // Комп’ютерні засоби, мережі та системи. — 2003. — № 2. — С. 144-150. — Бібліогр.: 3 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860013553296080896 |
|---|---|
| author | Закутайло, Д.А. |
| author_facet | Закутайло, Д.А. |
| citation_txt | Трансляция VHDL программы в BDD структуры / Д.А. Закутайло // Комп’ютерні засоби, мережі та системи. — 2003. — № 2. — С. 144-150. — Бібліогр.: 3 назв. — рос. |
| collection | DSpace DC |
| description | В статье представлена автоматизированная система, упрощающая процесс верификации. Рассмотрен процесс преобразования VHDL программы в BDD структуры.
|
| first_indexed | 2025-12-07T16:43:18Z |
| format | Article |
| fulltext |
Комп’ютерні засоби, мережі та системи. 2003, №2 144
В статье представлена автома-
тизированная система, упрощаю-
щая процесс верификации. Рас-
смотрен процесс преобразования
VHDL программы в BDD струк-
туры.
Д.А. Закутайло, 2003
ÓÄÊ 519.713.1
Ä.À. ÇÀÊÓÒÀÉËÎ
ÒÐÀÍÑËßÖÈß VHDL ÏÐÎÃÐÀÌÌÛ
 BDD ÑÒÐÓÊÒÓÐÛ
В настоящее время в Институте кибернетики
им. В.М.Глушкова НАН Украины разраба-
тывается автоматизированная система вери-
фикации цифровых систем, позволяющая
тестировать истинность временных утвер-
ждений. В качестве входной информации ис-
пользуется описание устройства на VHDL.
Особенности системы заключаются в сле-
дующем:
1) разрабатываемая система верификации
ориентирована на взаимодействие с сущест-
вующими САПР для проектирования цифро-
вых систем на ПЛИС;
2) предложен вариант временной логики,
упрощающий запись временных свойств для
разработчиков цифровых систем;
3) реализована возможность верификации
схем с задержками;
4) возможна генерация тестовых последо-
вательностей, удовлетворяющих пользова-
тельским критериям;
5) по желанию пользователя осуществля-
ется проверка достижимости состояния в си-
стеме.
Разработанная система для верификации
временных формул позволяет тестировать
истинность временных утверждений, исполь-
зуя в качестве входной информации описа-
ние устройства на VHDL. Этот язык описа-
ния был выбран благодаря широкому ис-
пользованию его среди языков описания в
САПР на ПЛИС. Выбор такого входного
языка обеспечивает широкое применение
разработанной системы. Входной информа-
цией системы может быть как поведенческое
описание, так и структурное описание
ТРАНСЛЯЦИЯ VHDL ПРОГРАММЫ В BDD СТРУКТУРЫ
Комп’ютерні засоби, мережі та системи. 2003, №2 145
на VHDL. В качестве языка задания временных свойств был выбран вариант
CTL логики, обеспечивающий компромисс между выразительными возможно-
стями и сложностью верификации. Отличия собственного варианта временной
логики от CTL заключаются в следующем:
- можно ссылаться на предыдущее значение сигнала;
- введен ряд операторов для манипуляции с сигналами.
Очевидно, разработчик должен хорошо разбираться в CTL логике, чтобы
задать требуемые свойства. Система, получив входные данные, проверяет ис-
тинность или ложность сформулированных утверждений на всех достижимых
состояниях схемы, описанной на VHDL. При невыполнимости требуемого свой-
ства генерируется контрпример. В случае выполнения свойства система (по же-
ланию пользователя) генерирует пример, подтверждающий истинность утвер-
ждения. Упрощенно алгоритм работы системы изображен на рис. 1.
Разработанная система позволяет устанавливать эквивалентность двух опи-
саний устройств на VHDL. Такая возможность может быть полезна в следую-
щих случаях:
1) даны два описания на VHDL, требуется установить их семантическую
идентичность;
2) с помощью САПР получено структурное описание устройства на VHDL,
пользователь вносит изменения и необходимо узнать, не повлияют ли они на
функционирование схемы;
3) поведенческое описание на VHDL преобразуется в структурное описа-
ние посредством синтезатора САПР. В этом процессе очень важно гарантиро-
вать эквивалентность двух описаний. Если обнаруживается несоответствие, то
это свидетельствует о серьезных ошибках в работе синтезатора САПР. Таким
образом, можно провести тестирование синтезатора САПР.
Свойство истинно?
Трансляция VHDL
описания
Генерация
контрпримера
Генерация тестового
примера
Да
Нет
Трансляция CTL
формул
Проверка
выполнимости
свойства
РИС. 1. Алгоритм работы системы
Д.А. ЗАКУТАЙЛО
Комп’ютерні засоби, мережі та системи. 2003, №2 146
Для автоматизированных систем верификации важным является внутренний
способ представления различных описаний в виде структур данных, а также ме-
тоды для манипулирования такими структурами. В разрабатываемой системе в
качестве внутренних структур данных, представляющих описание на VHDL, ис-
пользуются структуры данных типа BDD [1].
BDD расшифровывается как «binary decision diagram» (диаграмма двоичного
решения). BDD представляет собой структуру данных для описания булевых
функций. Современное представление BDD предложено Bryant [2], хотя общие
идеи появились гораздо раньше, в виде так называемых «ветвящихся программ»,
в отечественной литературе − так называемые релейные деревья.
BDD обладает рядом полезных свойств:
1) многие функции имеют компактное представление в виде BDD. На рис.2
изображена BDD для функции, сумма по модулю 2. Функции такого типа тре-
буют для своего представления 2n-1 узлов, где n – число переменных, тогда как
стандартное представление занимает экспоненциальное количество узлов [2];
2) BDD удобно манипулировать. Эффективные алгоритмы существуют как
для простейших булевских операций (AND, OR, NOT и т.д.), так и для более
сложных;
3) если зафиксировать порядок, в котором появляются переменные, то BDD
является каноническим представлением булевой функции, т.е. любая функция f:
Bn->B имеет в точности только одно представление в виде ROBDD. Таким обра-
зом, сравнение булевских функций сводится к простому сравнению указателей.
РИС. 2. ROBDD для функции x ⊕ y ⊕ z
ТРАНСЛЯЦИЯ VHDL ПРОГРАММЫ В BDD СТРУКТУРЫ
Комп’ютерні засоби, мережі та системи. 2003, №2 147
Рассмотрим преобразование VHDL описания в BDD структуры. На рис. 3
представлено описание трехбитного сбрасываемого счетчика. Если на входе
счетчика сигнал reset='0', то счетчик сбрасывается в ноль и устанавливает сиг-
нал ready='1'. После этого ожидается подтверждение от внешнего устройства по-
средством сигнала ack, который должен изменить свое состояние с 0 в 1. Если
ack='1', то сигнал готовности сбрасывается и ожидается сброс подтверждения от
внешнего устройства. Только после прихода заднего фронта этого сигнала
счетчик устанавливает сигналы b0 <= '1', b1 <= '0', b2 <= '0'. Дальнейший счет
будет осуществляется по переднему фронту сигнала clk. На рис. 4 представлена
граф-схема (ГС) счетчика.
entity cnt is
port ( start, reset, ack, clk: in BIT;
ready: out BIT;
b0, b1, b2 : inout BIT := '0');
end entity cnt;
architecture cnt_arch of cnt is
begin
process
begin
if (reset='0') then
b0 <= '0';
b1 <= '0';
b2 <= '0';
ready='1';
wait until ack='1'; --1
ready='0';
wait until ack='0'; --2
else
b0 <= not b0;
b1 <= b1 xor b0;
b2 <= b2 xor (b1 and b0);
wait until clk='1'; --3
end if;
end process;
end architecture cnt_arch;
РИС. 3. Трехбитный сбрасываемый счетчик
На первом этапе необходимо найти участки исходного текста, где выполне-
ние программы может приостановиться. Такими участками служат конструкции
типа wait on signal_list until cond. Если условие cond не выполняется или в спи-
ске сигналов signal_list не произошло ни одного события, то выполнение про-
граммы приостанавливается.
Д.А. ЗАКУТАЙЛО
Комп’ютерні засоби, мережі та системи. 2003, №2 148
b0 <= '0'; b1 <= '0'; b2 <= '0';
ready='1';
wait until ack='1'
b0 <= not b0;
b1 <= b1 xor b0;
b2 <= b2 xor (b1 and b0);
wait until clk='1';
reset='1'res
et=
'0'
if
ready='0';
wait until ack='0'
РИС. 4. ГС счетчика
В вышеприведенном примере существуют три wait конструкции. Каждой из
этих конструкций необходимо присвоить некоторое уникальное числовое значе-
ние. Пометим их числами 1, 2 и 3 (указаны в комментариях). Введем понятия
счетчика состояний исходной программы. Такой счетчик будет изменять свое
значение при переходе из одного wait выражения в другое. Обозначим состоя-
ние этого счетчика переменной state. Для учета начального состояния програм-
мы зарезервировано значение state равное 0. Из wait выражения можно выде-
лить условие, при котором программа возобновит свое выполнение. Например,
выполнение будет продолжено для первого wait выражения, если выполнится
ready='1' and ready’event = ‘1’. С учетом введения счетчика состояний условие,
при котором программа возобновит свое выполнение, запишется следующим
образом:
resumption = r0 or r1 or r2 or r3;
r0 = (state=0);
r1 = (state=1 and ack='1' and ack’event = ‘1’);
r2 = (state=2 and ack='0' and ack’event = ‘1’);
r3 = (state=3 and clk ='1' and clk’event = ‘1’).
В более общем виде запишем таким образом:
( ) ( ) ( )event'scondistate0state isigsi
n
2i ∈= ∨∨ ∧∧=∨=
Здесь индекс i служит для указания номера wait конструкции; n – количество
таких конструкций; condi – условие i wait конструкции; sigi – список сигналов из,
которых образовано i-е условие и список сигналов перечисленных явно в спи-
ске чувствительности.
ГС программы преобразуется следующим образом: перед каждым wait вы-
ражением ставится конструкция вида state = i, где i - уникальный номер; wait
ТРАНСЛЯЦИЯ VHDL ПРОГРАММЫ В BDD СТРУКТУРЫ
Комп’ютерні засоби, мережі та системи. 2003, №2 149
выражения удаляются; первым выражением программы становится условный
оператор выбора участка программы, с которого начнется выполнение; послед-
ним выражением становится оператор wait, учитывающий все условия, при ко-
торых программа возобновит работу. Преобразованная ГС программы изобра-
жена на рис. 5.
b0 <= '0'; b1 <= '0'; b2 <= '0';
ready='1';
state = 1;
b0 <= not b0;
b1 <= b1 xor b0;
b2 <= b2 xor (b1 and b0);
state = 3;
reset='1'rese
t='0'
if
ready='0';
state=2;
ifr0 or r2
r1
wait until ((state=1 and ack='1') or (state=2 and ack='0') or (state=3 and clk='1'));
РИС. 5. Преобразованная ГС счетчика
Дальнейшие преобразования ГС связаны с применением нижеследующих
трансформаций:
1) конструкция вида
конструкция вида
2) если на некотором участке осуществляется присвоение переменной, и эта
переменная используется в последующих выражениях, то заменить все вхожде-
ния переменной ее значением.
if cond1 then seq_statM
seq_stat1
else seq_statM
seq_statN
end if;
seq_statM
if cond1 then seq_stat1
else seq_statN
end if;
преобразуется в
if cond1 then seq_stat1
seq_statM
else seq_statN
seq_statM
end if;
if cond1 then seq_stat1
else seq_statN
end if;
seq_statM
преобразуется в
Д.А. ЗАКУТАЙЛО
Комп’ютерні засоби, мережі та системи. 2003, №2 150
Пример: конструкция вида
1) и 2) преобразования осуществляются для того, чтобы переместить опера-
торы if как можно ближе к вершине ГС и избавиться от тех переменных, значе-
ние которых можно легко вычислить. В примере со счетчиком эти преобразова-
ния применять нет необходимости, так как ГС уже находится в нужном состоя-
нии.
На втором этапе необходимо из ГС выделить ГС для всех переменных и
сигналов, оставшихся после преобразований. На рис. 6 изображены ГС для сиг-
нала b0 и переменной state. Каждая из этих структур представляет собой дерево,
узлами которого являются условные вершины, а листьями - выражения при-
своения. Такие деревья легко преобразуются в BDD структуры.
b0 <= '0'; b0 <= not b0;
reset='1'reset='0'
if
if
r0
o
r r
2
state = 1; state = 3;
reset='1're
se
t=
'0'
if
state=2;
if
r0 or r2
r1
РИС. 6. ГС для сигнала b0 и переменной state
Автоматизированная система для верификации цифровых устройств, ис-
пользующая BDD структуры, находится в завершающей стадии разработки. С
ее помощью будет верифицирована многокластерная интеллектуальная систе-
ма [3], разрабатываемая в Институте кибернетики им. В.М.Глушкова
НАН Украины.
1. Закутайло Д.А. Использование структур данных типа BDD для формальной верифика-
ции аппаратуры //Нові комп`ютерні засоби, обчислювальні машини та мережі. – К.: Ін-т
кібернетики ім. В.М. Глушкова НАН України, 2001. – Т. 1. – С.140–152.
2. Randal E.Bryant. Graph-based algorithms for Boolean function manipulation // IEEE Transac-
tions on Computers. – 1986. – 8(C-35). – P. 677-691.
3. Koval V., Bulavenko O., Rabinovich Z. Parallel Architectures and Their Development on the
Basis of Intelligent Solving Machines // Intern. Conf. On Parallel Computing in Electrical
Eng. – Warsaw, Poland, 22-25 September 2002. – P. 21-26.
Получено 15. 06. 2003
преобразуется в d<=k; s<=13; v:=12; d<=k; s<=v+1;
|
| id | nasplib_isofts_kiev_ua-123456789-6394 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1817-9908 |
| language | Russian |
| last_indexed | 2025-12-07T16:43:18Z |
| publishDate | 2003 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Закутайло, Д.А. 2010-03-02T10:16:28Z 2010-03-02T10:16:28Z 2003 Трансляция VHDL программы в BDD структуры / Д.А. Закутайло // Комп’ютерні засоби, мережі та системи. — 2003. — № 2. — С. 144-150. — Бібліогр.: 3 назв. — рос. 1817-9908 https://nasplib.isofts.kiev.ua/handle/123456789/6394 519.713.1 В статье представлена автоматизированная система, упрощающая процесс верификации. Рассмотрен процесс преобразования VHDL программы в BDD структуры. ru Інститут кібернетики ім. В.М. Глушкова НАН України Трансляция VHDL программы в BDD структуры Article published earlier |
| spellingShingle | Трансляция VHDL программы в BDD структуры Закутайло, Д.А. |
| title | Трансляция VHDL программы в BDD структуры |
| title_full | Трансляция VHDL программы в BDD структуры |
| title_fullStr | Трансляция VHDL программы в BDD структуры |
| title_full_unstemmed | Трансляция VHDL программы в BDD структуры |
| title_short | Трансляция VHDL программы в BDD структуры |
| title_sort | трансляция vhdl программы в bdd структуры |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/6394 |
| work_keys_str_mv | AT zakutailoda translâciâvhdlprogrammyvbddstruktury |