Верифікація моделей цифрових пристроїв, які подано мовами опису апаратури

Для побудови внутрішньої моделі вихідний опис перетворюється у графову модель, що є композицією двох графів. Перший - інформаційний, який описує потоки даних і їх перетворення (подібно до операційного автомату в класичній композиційній моделі з мікропрограмним керуванням) без урахування умовних гілок. Другий граф відповідає ланцюгу умов. Інформаційний I-граф містить два типи вершин: операнди і функції із синтезованої підмножини VHDL. Дуги з'єднують вершини у такий спосіб: вершина-джерело з'єднується з функціональною вершиною, потім дуга виходить з функціональної вершини і входить у вершину-приймач (операндову вершину).

Дуги можуть бути умовні і безумовні. Умовні дуги відповідають операторам, що знаходяться усередині умовних конструкцій VHDL. Умовні дуги мають мітки. Керуючий С-граф містить умовні конструкції з вихідного опису. Кожен предикат умови - підграф з визначеною міткою.

На рис. 1 наведено приклад опису синхронного D-тригера з прямим скиданням.

ФЕ моделі - це багаторозрядні функції, тобто оператори VHDL. Моделювання всіх можливих значень на всіх даних виконати за прийнятний час неможливо.

Запропоновано модель сигналу з поданням значень у вигляді діапазону. Таке подання зменшує кількість інформації, яка зберігається, тому що кількість діапазонів значно менша за кількість значень. Кожна змінна задається множиною областей можливих значень (ОМЗ):, де k - кількість елементів множини.

Кожна ОМЗ для цілочислових змінних задається парою (min, max), де min і max - цілочислові значення від 0 до 2³²-1. Перший елемент пари містить мінімальне значення i-тої ОМЗ, а другий елемент - максимальне:

.

Над діапазонами розроблені операції перетинання й об'єднання, алгоритми перетворення частково визначених і цілком невизначених векторів у діапазони, а також перетворення діапазонів у вектори. Наприклад, вектор A=xx1xx0xx перетворюється у таку множину діапазонів

_.

Запропоновані процедури прямої і зворотної імплікації через ФЕ для операцій обробки даних (логічні, арифметичні й операції порівняння).

Арифметичні операції розрядозалежні. Це не дає можливості використовувати табличні методи імплікації. Для прямої імплікації додавання C=A+B враховується, що результат матиме не більшу розрядність, ніж розрядність вихідної змінної: . Для зворотної імплікації базовий вираз A=C-B (для B=C-A аналогічно) . Процедури імплікації розроблені для ФЕ додавання і віднімання. Наприклад, зворотна імплікація для A, B, C через С=А+В дає такий результат: діапазон з індексом 1 виявився порожнім A. Тобто результат: A.

Запропоновано формули зворотної імплікації для всіх операцій порівняння. Для процедури зворотної імплікації для А<В: і .

Запропоновано формули імплікації для логічних операцій. Для прямої імплікації С= А and B було отримано . Зворотна імплікація змінної А (для В аналогічно): . Наприклад, зворотна імплікація для A, B, C через С = A and B дає такий результат: незаданий вхід B - він обробляється першим. Одержимо B, на вході B - “1”, і A, що дорівнює “”. Символ “” показує, що, маючи “0” на одному з входів, неможливо одержати “1” на виході. Тобто “0” на вході A, отриманий чи примусово встановлений на більш ранніх кроках, не правомочний. Якщо тепер виконати процедуру прямої імплікації, то одержимо “” на виході, тобто наявне протиріччя.

Відповідні формули імплікації отримані для С = A or B і для C=not A. Формули, отримані для двооперандних логічних операцій AND и OR, були розширені для довільної кількості входів.

Було запропоновано припущення, що оператор мови опису апаратури (будь-якої), а відповідно і функціональний елемент, не містить помилок і працює справно. Було розглянуто помилку коду на VHDL типу “заміна оператора”, яку викликано неадекватним вживанням різних операторів призначення (а не несправністю їх роботи). Визначити перелік помилок було необхідно для розробки стратегії верифікації опису пристрою.

У розділі 3 описано стратегію верифікації, засновану на графовій моделі пристрою, функціональних помилках проектування і розрізнюючих послідовностях.

У роботі було сформульовано систему доказів, яка дозволила використовувати методи структурного тестування, що ґрунтуються на активізації шляхів у моделі пристрою, з метою функціональної верифікації.

Було надано визначення розрізнюючих послідовностей (РПС), ідентифікації функціональних елементів, умови активізації функціонального елементу, активізованого шляху в графовій структурі.

Було сформульовано і доведено леми про існування умов активізації в коді, про умови перевірки механізму обробки даних у моделі на мові опису апаратури і про можливість ідентифікації всіх функціональних елементів на активізованому шляху.

Було показано, що інформацію про помилки проектування в коді можна одержати ще до діагностичного експерименту, на етапі активізації шляхів. Сформульовано і доведено теорему про те, що для ідентифікації всіх функціональних елементів в I-графі, необхідно і достатньо активізувати всі шляхи в графі, що покривають його, починаючи від функціонального елементу 1-го рангу до зовнішніх виходів чи контрольних точок (КТ).

Було зроблено висновок про те, що ідентифікація (активізація) усіх функціональних елементів перевіряє механізм обробки даних моделі. Сукупність перевірених механізмів обробки даних збігається з перевіркою моделі на відповідність специфікації.

Оператори мов опису апаратури не містять в собі помилок, тому подача на функціональні елементи тестів, які перевіряють закон їх функціонування, є недоцільною. Зміст тестування функціонального елементу було визначено у перевірці його типу: на функціональний елемент необхідно подати такі тести (РПС), щоб після аналізу реакцій на них можна було ідентифікувати його тип (функцію) і відрізнити від інших. Розрізнюючі послідовності дозволяють знайти помилки заміни оператора в коді.

На рис. 2 наведені розрізнюючі послідовності для операторів {and, or, xor, nand, nor, xnor} для довільного m та n>2, де m - кількість розрядів та n - кількість входів.

У цьому випадку формування послідовності відбувається при трьох наборах. Ліворуч надано вхідні набори, праворуч - реакції на них і розпізнані логічні оператори.

Запропоновано алгоритм побудови розрізнюючих послідовностей для логічних функціональних елементів на основі аналізу тестів перевірки справності відповідних логічних елементів.

Запропоновано алгоритм побудови розрізнюючих послідовностей для арифметичних операцій за типом “усі від усіх” із заданої підмножини арифметичних операцій {add (+), sub (-), mul (*), div (/)}.

Послідовність подач векторів із розрізнюючих послідовностей для функціонального елементу не впливає на результат розпізнавання типу функціонального елементу.

На рис. 3 наведено алгоритм побудови РПС для арифметичних операцій.

Доведення умов ідентифікації всіх функціональних елементів в інформаційному I-графі і побудова РПС для всіх функціональних елементів дозволили сформулювати такий алгоритм активізації шляхів.

1. Обирається i-й оператор (неактивізований функціональний елемент будь-якого рангу, починаючи з першого), на нього подається РПС.

2. Обчислюється реакція i-го функціонального елементу, що активізується, на РПС. Таким чином, функціональний елемент стає активізованим. Обчислення виконується за допомогою прямої імплікації із застосування подання даних діапазонами.

3. Якщо реакція i-го активізованого функціонального елементу збігається з РПС j-го функціонального елементу - наступника, то вона використовується замість РПС для активізації j-го функціонального елементу; в іншому випадку робиться пошук серед реакцій i-го функціонального елементу, що належать РПС j-го функціонального елементу - наступника, якщо такі мають місце. Відсутні вектори з РПС для наступника забезпечуються за допомогою зворотної імплікації.

4. Пп. 1-3 повторюються доти, доки буде досягнута контрольна точка чи зовнішній вихід. Якщо на i-тому кроці активізація наступного елемента неможлива, то необхідно вводити додаткові контрольні точки на кроці активізації (i-1) ФЕ. Якщо активізація можлива після контрольної точки, то значення в контрольній точці знімається, однак активізація продовжується.

Сформульоване визначення активізації шляху у свою чергу обумовлює забезпечення умов транспортування. Умови транспортування містять у собі вхідну послідовність, умови забезпечення і закон зміни виходу.

При забезпеченні можливі ситуації: вихідна послідовність цілком збігається з вхідною; закон зміни виходу щодо входу може легко обчислюватися; закон зміни виходу жорстко зв'язаний з типом функціонального елементу і значеннями на входах, що забезпечуються (вихід може бути визначений у ході прямої імплікації).

Виходячи зі сформованих визначень, доведених лем і теорем, у роботі була визначений загальна метод генерації тестів, який зумовив усю стратегія верифікації, засновану на активізації функціонального елементу, починаючи з 1-го рангу.

1. Мовний поведінковий опис моделі пристрою на мові опису апаратури перетворюється у графову модель.

2. На графовій моделі обчислюються типи та ранги функціональних елементів - операторів, які треба ідентифікувати.

3. Для кожного i-го функціонального елементу знайти множину розрізнюючи послідовностей, які розрізнюють функцію від усіх інших із заданої підмножини (ідентифікують її). Задати значення у діапазонах.

4. Активізується i-й функціональний елемент 1-го рангу. РПС подаються прямо із зовнішніх вершин графа (вхідні порти моделі на мові опису апаратури).

5. Будується активізований шлях від активізованого функціонального елементу до зовнішніх вершин графа (вихідних портів моделі на мові опису апаратури) або до контрольної точки.

6. Активізація шляху вважається завершеною, якщо досягнута задана операндова вершина або активізація шляху далі неможлива;

7. Активізацію необхідно повторити для всіх функціональних елементів 1-го рангу.

8. Після закінчення активізації функціонального елементу 1-го рангу наступним для активізації обирається k-й функціональний елемент p-го рангу (p>1,), який не належить жодному вже активізованому шляху;

9. Активізації йде доти, доки всі функціональні елементи не будуть активізовані.

10. Виконується забезпечення подання РПС шляхом моделювання назад від активізованого елементу до входів І-графу, суміщаючи моделювання у С-графі, яке забезпечує проходження значень по дугах з мітками (моделювання назад виконується з використанням процедур зворотної імплікації, які існують для кожного типу функціонального елемента). Усі процедури виконуються з діапазонами.

11. Отриманий результат забезпечення - тестовий вектор на входах графової моделі.

Було виділено три способи отримання еталонів: за специфікацією; з використанням зовнішньої моделюючої системи; за допомогою ітеративного інтерактивного підходу.

Було запропоновано послідовність дій при інтерактивному процесі уточнення специфікації, заснованому на взаємодії верифікатора і розробника.

Також було розроблено класифікацію типів мовних описів пристроїв:

- прості (описи логічних і арифметичних комбінаційних пристроїв; описи послідовнісних пристроїв; описи моделей цифрових автоматів тощо);

- складні (описи пристроїв з мікропрограмним керуванням; описи алгоритмічних пристроїв; апаратно-орієнтовані описи; описи інтерфейсів; описи композиційних пристроїв; нешаблонні описи, тощо).

Після аналізу запропонованої стратегії верифікації було зроблено висновок про те, що стратегія дозволяє цілком перевірити описи типу 1 (прості). Для типу 2 (складні описи) використання стратегії дозволяє перевірити “явні” і “неявні” режими функціонування.

Було сформульовано твердження про те, що якщо функція, реалізована поведінковою моделлю деякого пристрою, безперервна на ОМЗ вхідних сигналів, то в межах ОМЗ модель поводить себе однозначно й у відповідності до обчисленої області значень функції. Доведення засновано на теоремі Больцано-Коші та її узагальненні. У роботі було зроблено висновок про те, що кількість точок при перевірці опису безперервної функції не залежить від ОМЗ вхідних сигналів.

У розділі 4 було розроблено прототип системи автоматизованої тестової верифікації на основі поведінкової моделі цифрового пристрою на VHDL, наведено результати діагностичних експериментів над трьома видами описів, розроблено вимоги по створенню описів, придатних до верифікації.

У розділі було проаналізовано результати діагностичних експериментів над різнотипними пристроями, результати яких показали спроможність обраної стратегії для проведення верифікації.

Було розглянуто три моделі (описи) пристроїв: класичний представник мікропрограмних пристроїв - КР 1804ВР1, пристрій керування b06 з бібліотеки ITC, послідовнісний пристрій s27 з бібліотеки ISCAS. Для всіх моделей був наявний код-опис на VHDL.

Висновки за проведеними діагностичними експериментами:

- результати для КР 1804ВР1 показали, що для структурованого опису ЦП, у якому кожний фрагмент коду відповідає визначеному режиму, отримані тести дозволяють знаходити помилки в коді, ідентифікувати їх з визначеним режимом (частково локалізувати несправність) і розширяти специфікацію в інтерактивній взаємодії з розробником;

- результати для b06 показали, що для опису ЦП з використанням автоматного шаблону, у якому кожен блок коду відповідає логічно закінченій апаратній реалізації, отримані тести дозволяють знаходити помилки в коді, пов'язані з несправністю функцій переходів і виходів;

- результати для s27 показали, що отримані тести дозволяють знайти помилки в неструктурованому коді, у якому досить складно виділити окремі режими роботи пристрою. Було зроблено висновок про можливість паралельної активізації функціональних елементів з метою оптимізації верифікації і зменшення кількості тестових векторів без втрати діагностичних властивостей тесту.

Аналіз запропонованої методики здійснювався за кількістю векторів, необхідних для тестування коду.

Було запропоновано гістограми для трьох типів описів. На рис. 4 надано залежності довжини тесту від типу тестування.

При цьому: 1 - тест з повним переліком усіх можливих значень (2ⁿ2^m, де n - кількість вхідних розрядів, m - кількість елементів пам`яті); 2 - тест для програмного коду (2ⁿ); 3 - тест перевірки режимів із специфікації (2ⁿМ, де n - кількість вхідних розрядів, М - кількість режимів); 4 - тест з використовуванням розробленого методу генерації тестів.

В роботі не було наведені чисельні показники усіх проаналізованих моделей (усього їх кількість понад 100 з бібліотек ISCAS та ITC), тому що усі розглянуті моделі поводили себе приблизно однаково, згідно зі своїм типом.

Як видно з гістограм не у всіх випадках стратегія приносить значне зниження довжини тесту, але незначне зростання об'єму тестів на основі активізації шляхів дає 100% покриття несправностей (помилок проектування “заміна оператора”).

На рис. 5 надано діаграми залежності покриття несправностей (помилок проектування “заміна оператора”) від типу тестування.

У всіх описах тест на основі активізації шляхів дає 100% покриття несправностей, що не завжди досягається класичними методами.

На рис. 6 надано залежності довжини тесту від типу функціонального елемента (логічного та арифметичного типу) та числа розрядів. При цьому ТПС- це тест перевірки справності, повний перелік - це перелік усіх можливих значень на входах елементу.

Довжина тесту під час застосування повного переліку обчислюється як Y=(2ⁿ)*X, де n - число входів функціонального елементу, а Х - число розрядів входів. Оскільки розглядалися тільки 2-хвходові функціональні елементи, то формула набула вигляд Y=4*X. Довжина тесту під час моделювання функціонального елементу на тестах перевірки справності прирівнюється до Y=(n+1)*X=3*X.

Як видно з графіків, зростання довжини тесту (а саме, РПС) під час використання стратегії верифікації на основі активізації шляхів зі збільшенням кількості розрядів операндів залишається незмінним. Розрахунок проводився для двовходового логічного функціонального елементу із змінною розрядністю входів.

У розділі 4 наведено приклад інтерактивного розширення специфікації за методикою, яку описано в розділі 3, і етапи виконання верифікації. Показано, що можливе виникнення ситуації, коли набір векторів, що не належить специфікації, відповідає деякому режиму. Якщо на цьому режимі у розробника (чи будь-якої ідеальної зовнішньої моделі) існує можливість надати еталонні реакції, то специфікація динамічно розширюється і доповнюється.

Було розглянуто фрагмент специфікації мікропроцесора, у якому частина режимів описана, а частина - ні. Розробник має надати верифікаторові додаткову інформацію про те, що буде в регістрі під час подачі на керуючий сигнал значень, відмінних від перерахованих у специфікації. Таким способом відбувається уточнення і розширення специфікації.

Було запропоновано кількісну оцінку якості тесту з урахуванням можливостей розширення специфікації

,

де f_спец - режими зі специфікації; f_доп - внесені в специфікацію додаткові режими; f^пров_спец - перевірені режими в коді.

Було розроблено рекомендації (шаблони) щодо формування описів, які збільшують критерій придатності до верифікації на етапі введення проекту в САПР РЕА до його моделювання та верифікації.

У роботі було запропоновано прототип системи FunVerifier. Система дозволяє проводити функціональну верифікації і реалізує розроблені алгоритми. Прототип являє собою окремий програмний продукт із можливістю інтеграції в існуючі більш потужні САПР РЕА.

Висновки

У результаті виконаних досліджень за темою дисертації було досягнуто мети - розроблено методи зменшення кількості тестової інформації при верифікації моделей цифрових пристроїв, які подано мовами опису апаратури, що дозволяє зменшити час на проектування цифрових пристроїв.

Були вирішені такі практично-орієнтовані задачі, які виносяться на захист і складають наукову новизну.

1. Удосконалення стратегії верифікації мовних моделей цифрових пристроїв шляхом узгодження її етапів із сапр реа дає можливість проводити верифікацію в рамках автоматизованого проектування цифрових пристроїв, не вносячи у вирішення задачі людський фактор [4, 8-9, 13].

2. Удосконалення методу функціональної верифікації на основі синтезу тестів при активізації шляхів в структурі, що описує цифровий пристрій, дозволило формалізувати верифікацію моа-моделей та автоматизувати процес побудови тестів [1, 15-16, 19].

3. Модифікація алгоритмів побудови розрізнюючих послідовностей для ідентифікації функціональних елементів в моделі цифрового пристрою дозволило перевірити основні режими його функціонування та знайти розбіжності між моа-моделлю та специфікацією на основі аналізу областей можливих значень операндів [5, 13].

4. Модель сигналу з поданням цілочислових та логічних значень у вигляді діапазонів, а також операції прямої та зворотної імплікації на ній дозволили застосовувати детерміновані методи генерації тестів для усіх типів операндів [2-3, 6, 12].

5. Модель цифрового пристрою у вигляді композиції двох графів на основі поведінкової моделі на мові опису апаратури дозволила виконувати процедури прямої і зворотної імплікації, необхідні для генерації тестів верифікації [10, 14, 17].

6. Процедура проведення діагностичного експерименту за розробленою стратегією дозволила визначити хід верифікації на етапі опису проекту в САПР РЕА [7, 11, 18].

7. Результати експериментів на мовних моделях реальних проектів цифрових пристроїв та тестових схем з каталогів провідних фірм в області проектування цифрових пристроїв на моа показують спроможність застосування методів зменшення обсягу тестів. Проведений аналіз показав краще покриття несправностей у порівнянні з класичними тестами [5, 9].

8. Програмна реалізація компонентів системи автоматизованої верифікації на основі графової моделі та впровадження теоретичних та практичних результатів у навчальний та технологічний процеси виробництва з метою автоматизації верифікації дозволили формалізувати процес верифікації та підвищити її вірогідність, що в підсумку приведе до зменшення часу на проектування апаратури [16, акти впровадження].