Рис. 1. Складові елементи секвента
Відповідні терми можуть мати у цьому випадку наступний вигляд:
sequent = sequent_element*
sequent_element = formula ( formula_elements );
sequence_sign
Беручи до уваги прийняті визначення формули, а також застосовуючи рекуренцію, терми, що описують складові формули, можна представити у наступному вигляді:
formula_elements = formula_element*
formula_element = variable ( variableName );
negated_variable ( variableName );
conjunction ( conjunction_sign );
clause ( formula_elements );
negated_clause ( formula_elements )
variableName = symbol
conjunction_sign = symbol
При такому визначені термів запис секвентів, поданих на рис. 1, буде:
[ formula ( [ negated_variable ( "s1" ),
conjunction ( "*" ),
variable ( "s0" ) ] ),
sequence_sign,
formula ( [ clause ( [ variable ( "a1" ),
conjunction ( "->" ),
variable ( "y1" ) ] ),
conjunction ( "*" ),
clause ( [ variable ( "a0" ),
conjunction ( "->" ),
variable ( "y0" ) ] ) ] )]
Спосіб автоматизації процесу синтезу подано на прикладі правила вилучення знака заперечення у першому члені виразу:
αa,/ΦF,ΓG |- ΘQ
———————————
αa,ΓG |- ΘQ, ΦF
Це правило повинно бути використане, якщо першою неелементарною формулою у секвента є формула, яка має тільки змінну зі знаком заперечення, або вираз зі знаком заперечення.
Нижче подано словесний опис способу застосування розглянутого правила, який використовується при мануальній реалізації.
1. Необхідно виділити в перетворюваному секвенті три наступні частини:
I - послідовність елементарних формул, існуючих перед розгляданою формулою, що має оператор заперечення (αa),
II - формулу, що має елемент заперечення (/ΦF),
III - решта частини секвента, що має знак логічного включення (ΓG |- ΘQ).
2. Частину I необхідно поєднати з частиною III.
3. У кінці послідовності, створеної в пункті 2, необхідно дописати формулу з частини II, позбавлену, проте, знака заперечення.
Клаузули, які відповідають поданому вище словесному опису, мають наступний вид:
- для змінної:
rule ( PartI,
[ formula ( [ negated_variable ( Name ) ] )
| PartIII ],
NegationSign_in_predecesor, [ NewSequent ] )
:-
append ( PartI, PartIII, NewBeginning ),
append ( NewBeginning, [ formula ( [ variable ( Name ) ] ) ],
NewSequent ).
- для виразу:
rule ( PartI,
[ formula ( [ negated_clause ( Content ) ] )
| PartIII ],
NegationSign_in_predecesor,
[ NewSequent ] )
:-
append ( PartI, PartIII, NewBeginning ),
append ( NewBeginning, [ formula ( [ clause ( Content ) ] ) ],
NewSequent ),
де предикат
rule ( sequent, sequent, sequentSide, sequents ),
має наступні параметри:
- частина I перетворюваного секвента,
- частина II і III,
- бік секвента, з якого знаходиться знак заперечення,
- результат використання правила.
Перший параметр, тобто послідовність елементарних формул на початку секвента, виділяється при використані допоміжної клаузули предикату
rule ( PartI, [ formula ( [ variable ( N ) ] ) | Rest ],
SequentSide, Result )
:-
append ( PartI, [ formula ( [ variable ( N ) ] ) ], NewPartI ),
rule ( NewPartI, Rest, SequentSide, Result ).
Як видно, запис правила докладно відповідає словесному опису, а єдиним додатковим предикатом, що застосовується в операційних частинах клаузул, є стандартний предикат append.
Аналогічно виконується решта правил синтезу, що по суті є автоматизацію усього описаного процесу.
Розділ 5. Перетворення опису цифрових систем
Цей розділ має допоміжний характер. Він присвячений проблемі перетворення (трансляції) описів цифрових систем.
В процесі проектування трансляція часто має велике практичне значення, тому що дозволяє використовувати різні, не зв’язані безпосередньо поміж собою, засоби комп’ютерного забезпечення.
В розділі показано, що застосування логічного програмування дозволяє провести звичайну заміну однієї форми опису пристрою - іншою, навіть тоді, коли обидві форми дуже складні і різноманітні.
Представлений метод стосується, зокрема, створення експериментальних версій програм - версій, що призначені до перевірки слушності загальної концепції використовуваних методів, а також верифікації частин опису розв'язаної проблеми.
Характерною рисою методу є натуральність і простота використання, а також те, що окремі предикати і клаузули є простим відбиттям відповідних словесних описів, або формальних специфікацій, наприклад, синтактичних діаграм. Завдяки цьому, слушність імплементації є очевидною, а можливість помилитися - дуже мала. Крім того, транслятор також може просто модифікуватися і розбудовуватися через зміну або доповнення одиничних клаузул, наприклад, в випадку розширення початкового опису.
В розділі використано приклад перетворення опису, поданого за допомогою списку поєднань у форматі Intergraph, до опису на мові VHDL.
Метод був використаний для конструювання описово-моделюючих правил мови моделювання Pro Waves, представлених в шостому розділі.
Розділ 6. Розпізнавання часових діаграм
Однією з основних проблем, існуючих при проектуванні і моделюванні інтегральних систем високого рівня інтеграції VLSI, є проблема дотримування часових вимог між діаграмами окремих вхідних і вихідних сигналів. Ці вимоги можуть бути дуже складними з урахуванням того, що одиничний елемент VLSI може виконувати багато різних функцій, а також беручи до уваги складність окремих еталонних діаграм. Через те моделі роботи більшості елементів VLSI або протоколів комунікації, що написані традиційним способом, наприклад, за допомогою мови VHDL, можуть мати багато тисяч ліній, а їх підготування може бути надто трудомістким.
В цьому розділі представлено новий, оригінальний метод моделювання роботи (behavioral simulation) цифрових пристроїв високого рівня інтеграції VLSI, а також процесів, що відбуваються в цих цифрових системах, які характеризуються складними часовими залежностями. Приклад таких залежностей подано на рис. 2.
Запропонований метод дозволяє значно скоротити час приготування моделей і, тим самим, скоротити процес проектування пристрою.
В цьому методі розпізнавання часових діаграм виконано методом порівняння з еталоном і застосуванням метапрограмування.
Завдяки цьому задача зводиться до типово декларативного виду. Це дозволяє принципово зменшити рівень труднощів і час, необхідний для створення моделі, а завдання проектувальника обмежується виключно формальним записом еталонів часових діаграм, без необхідності використання будь-якого алгоритму.
Метод використовується до побудування мови опису і моделювання діаграм Pro Waves (Prolog based system for Waves recognition), що працює спільно з мовою VHDL. Мова має велике практичне значення і була використана, між іншими, для побудови моделі динамічної пам’яті VRAM, інтерфейсної системи декодера зображення (MPEG Video Decoder), моделювання протоколів комунікації з трансп’ютерними системами, а також для проектування спеціалізованих інтегральних пристроїв, які використовуються в цифровому телебаченні. Згідно з інформацією, відомою з літератури, а також власних праць автора, процес створення таких моделей традиційним способом, за допомогою мови VHDL, триває часто майже місяць. В випадку використання розгляданого методу час створення можна скоротити до кількох днів.
Рис. 2. Приклад складних часових залежностей в інтегральному пристрої VLSI: одна з кількох часових діаграм динамічної пам’яті DRAM - page early write cycle.
В розгляданому методі опис часових залежностей, існуючих у еталоні циклу, поділений на групи і зв’язаний з головними подіями циклу, які називаються подіями віднесення. Для кожної такої події, в залежності від необхідності, може бути подана група значень часів, зв’язаних з нею лівобічним (leftSideGroup), правобічним (rightSideGroup), а також двобічним способом (bothSideGroup).
Загальний, формальний запис кожної з груп є наступний:
leftSideGroup( ReferenceEvent ) ->>
t ( TimeName, BoundaryEvent )
{ , t ( TimeName, BoundaryEvent ) };
rightSideGroup( ReferenceEvent ) ->>
t ( TimeName, BoundaryEvent )
{ , t ( TimeName, BoundaryEvent ) };
bothSideGroup( ReferenceEvent ) ->>
t ( TimeName,
LeftBoundaryEvent,
RightBoundaryEvent )
{ , t ( TimeName,
LeftBoundaryEvent,
RightBoundaryEvent ) };
де:
- подія гранична - є другою з подій, яка обмежує даний час відповідно з лівого або з правого боку відносно до події віднесення,
- ліва подія гранична і права подія гранична є подіями, які обмежують даний час; цей час належить до двобічної групи, відповідно з лівого і правого боку відносно до події віднесення,
- дужки (“{}”) означають можливість появи в даному фрагменті нуля, один або багато разів.
Події записуються згідно з наступною схемою:
event( SignalName,
PriorToChange_SignalValue,
AfterChange_SignalValue )
Граничні події можуть мати також невизначений характер, наприклад, event(Add,_,_). Це можливе в наступних випадках:
- Істотним є сам факт зміни сигналу, а не його виду.
- Істотним є те, що зміна сигналу не відбувається у визначений інтервал часу, поза яким цей сигнал може змінюватися, або бути незмінним. В цьому випадку визначення "подія гранична” має характер умовний, і має значення межі інтервалу. Подія, як така, що приймається як зміна сигналу, може в цілому не відбутися. Така ситуація має місце, наприклад, при адресних сигналах.
На рис. 3 поданий приклад еталона циклу, а також відповідний формальний запис.
а)
б)
Рис. 3. Фрагмент еталона циклу, а також відповідний формальний запис: (а) часова діаграма; (б) формальний запис циклу
В процесі розпізнавання діаграм можна виділити два основні етапи. Перший з них, як характеристичний елемент цього методу, має підготовчий характер. Використовуючи метапрограмування, ідентифікаційна програма самомодифікується, тобто на основі формального запису еталонів циклів автоматично створює відповідну групу прологових описово-моделюючих правил.
Задачею створення правил є розпізнавання виду циклу шляхом порівняння змін вхідних сигналів з еталонами різних циклів, а також ініціювання передачі даних, зв’язаних з роботою пристрою, що моделюється.
Метапрограмування – це механізм, який дозволяє програмі конструювати іншу програму і виконувати її, або може в процесі своєї роботи виконувати самомодифікацію, тобто змінювати фрагменти свого власного коду. Цей процес описано у вступі до розгляданого розділу.
На другому етапі відбувається необхідна ідентифікація, яка виконується за допомогою правил, що були створені на першому етапі. У випадку зміни будь-якого з вхідних сигналів відбувається модифікація поточного часу моделювання, відновлення бази даних, яка містить атрибути сигналів, а також відновлення клаузул, що описують ліво-, право-, і двобічні групи часів. Далі проводиться перевірка на вміст в базі даних описів, які відповідають лівобічнім часам. Усі відтинки часу, необхідні для ідентифікації якогось циклу, перевіряються одночасно на вміст в базі даних подій, пов’язаних, з виконанням право - і двобічних часів, а також перевіряється інформація про невиконання на якомусь з відтинків часу події, пов’язаної з цим циклом.
Нижче подано приклад правила-клаузули, створеної для лівобічної групи фронту, еталону циклу, поданого на рис. 3.
Формальний запис лівобічної групи, що містить два часи (tCRP і tASR):
leftSideGroup ( event ( RAS,1,0 )) ->> t ( tCRP, event (CAS,0,1)),
t ( tASR, event (Add,_,_));
Генероване описово-моделююче правило:
Розгляданий метод ідентифікації був використаний до побудови мови опису і моделювання діаграм Pro Waves (Prolog based system for Waves recognition). Ця система призначена для сумісної роботи на мові VHDL і служить для моделювання роботи (behavioral simulation) цифрових систем зі складними часовими діаграмами.
Модельований елемент описується в цій системі за допомогою групи еталонних циклів (CYCLE), аналогічно тому, як то має місце в випадку технічної документації пристрою, наприклад, опис елементу DRAM містить, між іншим, наступні цикли: read, early write, late write, read-write, page early write, та інші.
Опис кожного з еталонних циклів починається від подання необхідних кінцевих умов початку циклу, тобто визначення першої події віднесення, існуючої у цьому циклі, а також стану інших сигналів у момент надходження цієї події. Наприклад:
start_conditions ( event ( RAS,1,0 ), WE=0, CAS=1 )
Опис еталона даного циклу може бути поділений на частини (PART). Вони відповідають тим фрагментам еталона, які виявляються секвентно. Черговість запису частин в еталоні циклу вимагає необхідну черговість виникнення фрагментів поточного циклу.
Поділ на частини дозволяє дуже просто описувати фрагменти циклу, що повторюються. Одиничні частини супроводжуються декларацією part_type(single). Частини, що повторюються – декларацією part_type(repetitive).
Найважливішими фрагментами опису даного еталона є тіла описів окремих частин. Це тіло створено із записів відповідних груп ліво-, право- і двобічних часів, у відповідності з інструкцією під назвою action. Задачею інструкції є ініціювання передачі даних. Сама передача виконується модулем опису системи, написаному мовою VHDL (рис. 5). Модуль, написаний мовою Pro Waves, ініціює цю передачу після розпізнавання фрагмента відповідного циклу. Інструкція action має наступний загальний вигляд:
action ( ActionName, ConnectedWithAction_ReferenceEvent )
Ініціювання передачі даних відбувається тоді, коли виконані усі лівобічні часи, що зв’язані з подією віднесення названою раніше в інструкції action, а також усі лівобічні часи, що зв’язані з подіями віднесення, що виникали раніше в опису еталона даного циклу. Зважаючи на це, істотним є необхідність того, щоб черговість запису лівобічних груп відповідала черговості появи їх подій віднесення в еталоні циклу.
Нижче подано приклад формального запису еталона циклу в системі Pro Waves. Це є опис поданого на рис. 4 спрощеного еталона циклу Two-Byte Register Read системи декодера зображення MPEG2 STi3500.
Рис. 4. Спрощений еталон циклу Two-Byte Register Read системи декодера зображення MPEG2 STi3500 фірми SGS-Thomson
WAVE_DESCRIPTION MPEG_DekoderVideo_modulProWaves;
signal ( DATA, ADD, nWAIT, nCS, RnW, nCDSTR );
action( Read_HigherByte_Address,
Read_LowerByte_Address,
SendToBus_HigherByte,
SendToBus_LowerByte,
Generate_nWAIT_1_0_1__Read2_Signal,
Generate_nWAIT_Z__Read2_Signal );
CYCLE Two_Byte_Register_Read;
start_conditions ( event ( nCS,1,0 ), nCDSTR=1, RnW=1, nWAIT=Z,
DATA=Z );
BEGIN
PART OnePartCycle;
part_type ( single );
begin
leftSideGroup (event (nCS,1,0)) ->> t (tAVSL,event(ADD,_,_)),
t (tRVSL,event(RnW,0,1));
leftSideGroup (event (nWAIT,0,1)) ->> t (tSLWH,event(nCS,0,1)),
t (tDVWH,event(ADD,_,_));
leftSideGroup (event(nCS,0,1)) ->> t (tAVSH,event(ADD,_,_)),
t (tDVSH,event(DATA,_,_));
rightSideGroup(event(nCS,1,0)) ->> t (tSLWL,event(nWAIT,1,0)),
t (tSLWD,event(nWAIT,Z,1));
rightSideGroup(event(nWAIT,0,1)) ->> t (tWHAX,event(ADD,_,_)),
t (tWHDV,event(DATA,_,_));
rightSideGroup(event(nCS,0,1)) ->> t (tSHAX,event(ADD,_,_)),
t (tSHRX,event(RnW,1,0)),
t (tSHSL,event(nCS,1,0)),
t (tSHWZ,event(nWAIT,1,Z)),
t (tSHDI,event(DATA,_,_)),
t (tSHDZ,event(DATA,_,Z));
action ( Generate_nWAIT_1_0_1__Read2_Signal, event (nCS,1,0 ));
action ( Read_HigherByte_Address, event (nCS ,1,0));
action ( SendToBus_HigherByte, event (nCS ,1,0));
action ( Read_LowerByte_Address, event (nWAIT,0,1));
action ( SendToBus_LowerByte, event (nWAIT,0,1));
action ( Generate_nWAIT_Z__Read2_Signal, event (nCS ,0,1));
end;
END; --of_CYCLE;
END. --of_DESCRIPTION.
Як вже зазначалося, рівень складності часових залежностей, що можуть виникати між сигналами елементів високого рівня інтеграції, спричиняє те, що створення відповідної моделі на мові VHDL є процесом дуже кропітким і довготривалим. Створення такої моделі на мові Pro Waves відносно просте. В зв’язку з цим дуже ефективним, з точки зору часу, необхідного для підготовки моделі, є поєднання модуля розпізнавання діаграм, описаного мовою Pro Waves з операційним модулем, написаним мовою VHDL. Спосіб виконання такого поєднання подано на рис. 5, який відноситься до розглянутого вище прикладу декодера зображення.
Модуль, виконаний мовою Pro Waves, а точніше, генеровані на її основі описово-моделюючі правила, виконує дві основні функції. Перша з них - розпізнавання діаграм через порівняння їх з еталонами циклів, а також ініціювання виконання операцій системи, що моделюється, шляхом створення відповідних значень сигналу мовою VHDL action.
| 
