Харківський національний університет радіоелектроніки

УДК 681.518.54: 004.415.5

Сиревич Євгенія Юхимівна

ВЕРИФІКАЦІЯ МОДЕЛЕЙ ЦИФРОВИХ ПРИСТРОЇВ, ЯКІ ПОДАНО МОВАМИ ОПИСУ АПАРАТУРИ

Спеціальність 05.13.12 – системи автоматизації проектувальних робіт

Автореферат дисертації на здобуття наукового ступеня кандидата технічних наук

Харків 2007

Дисертацією є рукопис.

Робота виконана в Харківському національному університеті радіоелектроніки, Міністерство освіти і науки України.

Науковий керівник – доктор технічних наук, професор Кривуля Геннадій Федорович, Харківський національний університет радіоелектроніки, завідувач кафедри автоматизації проектування обчислювальної техніки.

Офіційні опоненти: доктор технічних наук, професор Дербунович Леонід Вікторович, Національний технічний університет “Харківський політехнічний інститут”, професор кафедри автоматики та управління в технічних системах;

доктор технічних наук, професор Скобцов Юрій Олександрович, Донецький національний технічний університет, завідувач кафедри автоматизованих систем управління.

Провідна установа? – Національний технічний університет України “КПІ”, кафедра спеціалізованих комп’ютерних систем, Міністерство освіти і науки України, м. Київ.

Захист відбудеться “20” листопада 2007 р. у 14:00 на засіданні спеціалізованої вченої ради Д .052.02 у Харківському національному університеті радіоелектроніки за адресою: 61166, м. Харків, пр. Леніна, 14.

З дисертацією можна ознайомитися в бібліотеці Харківського національного університету радіоелектроніки за адресою: 61166, м. Харків, пр. Леніна, 14.

Автореферат розіслано “15” жовтня 2007 р.

Вчений секретар

спеціалізованої вченої ради В.В. Безкоровайний

загальна ХАРАКТЕРИСТИКА Роботи

Актуальність теми. У сучасних системах автоматизованого проектування радіоелектронної апаратури (САПР РЕА) основним способом опису пристроїв є мови опису апаратури (МОА), наприклад, VHDL або Verilog. В основі структурно-функціональних підходів до проектування та верифікації РЕА лежить дуалізм МОА-коду.

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

З іншого боку, МОА-модель – це опис цифрового пристрою (ЦП) для САПР РЕА. Стандартизовані фрагменти коду перетворюються у схемні реалізації, які використовують бібліотечні елементи системи синтезу. Синтезовані моделі перетворюються у схемні реалізації пристрою (логіки, що програмується користувачем, замовних НВІС (надвеликих інтегральних схемах), мікропроцесорних структур).

Таким чином, МОА-модель – це фактично схема, і до неї можуть бути застосовані методи схемного аналізу, синтезу тестів, побудови алгоритмів пошуку дефектів, які достатньо добре розроблені для цифрових схем.

На теперішній час існує попит на засоби верифікації моделей ЦП, тому що системи верифікації, які використовуються у світовій практиці (HDL Score, Verix™, Hammer 100, SpyGlass, Questa AFV), не працюють у режимі функціональної верифікації на високому рівні абстракції (під час опису моделі у САПР РЕА).

Актуальність дисертації зумовлена відсутністю ефективних методів і засобів верифікації моделей ЦП на стадії їхнього опису на поведінковому рівні.

Значний внесок у вирішенні проблем верифікації і діагностики моделей ЦП, у тому числі й описаних за допомогою МОА, внесли вчені: F.G.B.J.S. Devadas, П.П. Пархоменко, R.С.Г. Шаршунов, M.A.F.H.

Зв'язок роботи з науковими програмами, планами, темами. Робота виконувалася в Харківському національному університеті радіоелектроніки за планами виконання НДР і договорів: 127-5 – “Розробка основ нових інформаційних технологій в автоматизованому проектуванні, діагностиці засобів обчислювальної техніки” (№ ДР 0101U001948), 179-2 – “Система тестування цифрових засобів, що проектуються” (№ ДР 0104U004074), госпдоговір № 05-19 с ЗАТ “Северодонецкое НПО Импульс” за темою “Розробка технології проектування відмовостійких програмно-технічних комплексів”.

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

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

Для досягнення поставленої мети необхідно вирішити такі задачі:

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

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

- розробити стратегію функціональної верифікації моделей ЦП на етапі опису та моделювання проекту в САПР РЕА, яка дозволяє формалізувати верифікацію;

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

- розробити інформаційне та методичне забезпечення системи верифікації в стандарті VHDL, яке дозволяє інтегрування у сучасні САПР РЕА.

Об’єкт дослідження – процеси автоматизованого проектування цифрових пристроїв, поданих мовами опису апаратури високого рівня.

Предмет дослідження – методи аналізу і функціональної верифікації високорівневих моделей цифрових пристроїв в системах проектування РЕА.

Методи дослідження використовують: теорію множин, теорію автоматів і графів – для побудови та аналізу моделі ЦП; технічну діагностику і логічне моделювання – для формування стратегії верифікації на основі активізації шляхів та побудови тестів; методи програмної інженерії, мови програмування та проектування – для розробки та програмної реалізації алгоритмів верифікації.

Наукова новизна отриманих результатів. В результаті проведеної роботи було отримано такі наукові результати:

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

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

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

- уперше запропоновано модель ЦП у вигляді композиції двох графів на основі поведінкової моделі на МОА, що дозволяє виконувати процедури прямої і зворотної імплікації під час генерації тестів методом активізації шляхів;

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

Практичне значення одержаних результатів визначається:

- розробкою процедури проведення діагностичного експерименту і прототипу програмного забезпечення для верифікації VHDL-кодів на основі графової моделі.

- використанням процедур активізації шляхів у графовій моделі для генерації тестів верифікації;

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

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

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

Результати дисертації у вигляді алгоритмів і програмних модулів використовуються на підприємствах: ЗАТ "Імпульс", Сєверодонецьк (довідка про впровадження від 10 жовтня 2006 р.); у навчальному процесі ХНУРЕ (акт про впровадження від 16 жовтня 2006 р.).

Особистий внесок здобувача. Всі основні результати отримані здобувачем особисто. У роботах, опублікованих спільно, автору належать: у [2] розроблено інтервальний метод подання багаторозрядних операндів для виконання імплікації під час синтезу тестів верифікації, наведено формули та приклади перетворення векторних та цілочислових значень у діапазони (інтервали); у [3] розроблено процедури імплікації на арифметичних операціях; у [4] запропоновано алгоритм побудови розрізнюючих послідовностей для функціональних елементів у графовій моделі; у [5] запропоновано оцінку якості тестів на основі перевірених режимів пристрою; у [6] виявлено недоліки в існуючих методах верифікації; у [7] запропоновано теоретичні основи стратегії верифікації моделей на МОА у вигляді лем та теорем, які доводять можливість використання методів тестової діагностики для верифікації; у [8] наведено приклади імплікації вперед та назад з різними початковими умовами; у [9] розроблено алгоритм активізації шляхів та приклади застосування стратегії верифікації до мікропрограмних пристроїв; у [11] розроблено алгоритми моделювання I-графу; у [12] розроблено структуру програмного забезпечення верифікації VHDL-кодів на основі графової моделі; у [13] розроблено алгоритми генерації тестів, які будуються на основі розрізнюючих тестів для ідентифікації функціональних елементів; у [14] запропоновано приклади розрізнюючих послідовностей для арифметичних операцій; у [15] запропоновано формули імплікації для операцій порівняння; у [16] запропоновано метод отримання еталонів за різними специфікаціями; у [17] запропоновано підхід до проектування та верифікації моделей ЦП, що проектуються за допомогою МОА, який поєднує стандарти, прийняті у проектуванні, та новітні технології; у [18] розроблено подання моделі ЦП на МОА у вигляді композиції двох графів; у [19] розглянуто засоби подання тестів під час верифікації мовних моделей.

Апробація результатів дисертації здійснювалася на конференціях міжнародного рівня, що мають безпосередній зв’язок з темою дисертаційної роботи, а саме: 6-й і 7-й міжнародних науково-технічних конференціях “TCSET” (Львів, 2004 р. та 2006 р.); 8-й міжнародній науково-технічній конференції “CADSM” (Поляна, 2005 р.); міжнародних науково-технічних конференціях “EWDTW” (Ялта, 2004 р., Одеса, 2005 р.; Сочі, 2006 р.); 8-му, 9-му, 10-му міжнародних молодіжних форумах (Харків, 2004-2006 рр.).

Публікації. Результати наукових досліджень викладено у 19 друкованих працях. За темою дисертації 7 статей опубліковано в наукових виданнях, включених до переліків, затверджених ВАК України, та 12 тез доповідей – у збірниках матеріалів конференцій.

Структура й обсяг дисертації. Дисертаційна робота містить 178 сторінки, 37 рисунків на 14 сторінках, 8 таблиць на 3 сторінках. Її структура включає: вступ, 4 розділи, перелік джерел із 108 найменувань на 11 сторінках, 4 додатки на 27 сторінках.

ЗМІСТ РОБОТИ

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

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

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

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

Розділ 2 присвячений розробці опису МОА-моделі ЦП у вигляді графової структури, методів її моделювання, розробці подання сигналів у вигляді діапазонів, процедур прямої і зворотної імплікації на логічних й арифметичних функціональних елементах (ФЕ) цієї структури, визначенню списку моделей помилок проектування.

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

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

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

а) (б) (в)

Рис. 1. Приклад опису синхронного D-тригера: (а) – вихідний опис, (б) – інформаційний граф, (в) – керуючий граф

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

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

Кожна ОМЗ для цілочислових змінних задається парою (min, max), де min і max – цілочислові значення від 0 до 232-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 – кількість входів.

Рис. 2. Розрізнюючі послідовності для логічних операторів

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

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

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

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

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

Рис. 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 – тест з повним переліком усіх можливих значень (2n2m, де n – кількість вхідних розрядів, m – кількість елементів пам`яті); 2 – тест для програмного коду (2n); 3 – тест перевірки режимів із специфікації (2nМ, де n – кількість вхідних розрядів, М – кількість режимів); 4 – тест з використовуванням розробленого методу генерації тестів.

(a) (б) (в)

Рис. 4. Залежність довжини тесту від типу тестування для S27(a), КР1804ВС1(б), В06(в)

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

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

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

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

(а) (б) (в)

Рис. 5. Залежності покриття несправностей від типу тестування: S27(a), КР1804ВС1(б), В06 (в)

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

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

(a) (б)

Рис. 6. Залежність довжини тесту від типу функціонального елемента ((а) – логічного типу, (б) – арифметичного типу) та числа розрядів

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

У розділі 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, акти впровадження].

Практичні та теоретичні результати можуть бути використані у проектних та навчальних закладах, що займаються розробкою цифрових пристроїв з використанням МОА та розробкою САПР РЕА, зокрема систем верифікації.

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Сыревич Е.Е. Верификация высокоуровневых моделей цифровых устройств // Радиоэлектроника. Информатика. Управление. – 2006. – Вып. 2. – С. 74 – 77.

2. Рустинов В.А., Сыревич Е.Е., Сыревич А.В. Интервальный метод представления многоразрядных операндов для выполнения импликации при синтезе тестов верификации // Автоматизированные системы управления и приборы автоматики. – 2003. – Вып. 122. – С. 96 –103.

3. Рустинов В.А., Сыревич Е.Е., Сыревич А.В., Чегликов Д.И. Процедуры импликации на арифметических операциях при синтезе тестов верификации // Автоматизированные системы управления и приборы автоматики. – 2005. – Вып. 130. – С. 5 – 11.

4. Кривуля Г.Ф., Сыревич Е.Е., Карасев А.Л. Верификация моделей цифровых устройств, представленных на языке описания аппаратуры // Радиоэлектроника. Информатика. Управление. – 2005. – Вып.2. – С. 63 – 68.

5. Syrevitch Yev., Karasyov A., Mehana S.S. Functional verification quality metrics at HDL-models verification // Радиоэлектронные компьютерные системы. – 2006. – Вып. 6. – С. 153 – 157.

6. Сиревич Є.Ю., Липчанський О.І. Верифікація при автоматизованому проектуванні цифрових пристроїв // Інформаційно-керуючі системи на залізничному транспорті. – 2004. – Вип. 4-5. – С. 102.

7. Шкиль А.С., Сыревич Е.Е., Карасев А.Л., Чегликов Д.И. Тестовая верификация поведенческих языковых моделей цифровых устройств // Автоматизированные системы управления и приборы автоматики. – 2006. – Вып. 134.– С. 4 – 12

8. Syrevitch Yev., Rustinov V. Implication of arithmetic operations with multibit operands for verification test generation // TCSET’04: Proc. of the International conf. (February 24-28, 2004). – Lviv - Slavsko, Ukraine: Lviv Polytechnic National University, 2004. – С. 259 – 262.

9. Krivulya G., Shkil A., Syrevitch Yev., Antipenko O., Verification Tests Generation Features for Microprocessor - based Structures // EWDTW’04: Proc. of the International conf. (September 23-28, 2004). – Alushta, Ukraine: KhNURE, 2004. – Р. 57 – 63.

10. Сыревич Е.Е. Верификация моделей цифровых систем: проблемы, задачи, перспективы развития // Материалы 8-го Междунар. молодеж. форума “Радиоэлектроника и молодежь в XXI веке” (13-15 апреля 2004). – Харьков: ХНУРЭ, 2004. – С. 273.

11. Kryvulya G., Syrevitch Yev., Karasyov A. Cheglikov D. Internal Model Algorithms For Digital Design Verification of VHDL Descriptions // CADSM'2005: Proc. of the International conf. (February 23-26, 2005). – Lviv – Polyana, Ukraine: Lviv Polytechnic National University, 2005. – Р. 369 – 372.

12. Kryvulya G., Syrevitch Yev., Karasyov A. Cheglikov D. Test Generation for VHDL Descriptions Verification // EWDTW'05: Proc. of the International conf. (September 15-19, 2005). – Odessa, Ukraine: KhNURE, 2005. – Р. 191 – 194.

13. Сыревич Е.Е., Карасев А.Л. Функциональная верификации VHDL описаний // Материалы 9-го Междунар. молодеж. форума “Радиоэлектроника и молодежь в XXI веке” 19-21 апреля, 2005. – Харьков: ХНУРЭ, 2005. – С. 538.

14. Kryvulya G., Syrevitch Yev., Karasyov A. HDL-models verification // TCSET’06: Proc. of the International conf. (February 28 – March 4, 2006). – Lviv - Slavsko, Ukraine: Lviv Polytechnic National University, 2006. – Р. 570 – 573.

15. Syrevitch Yev., Cheglikov D. Graph model of a digital device at HDL-models verification // Материалы 10-го Междунар. молодеж. форума “Радиоэлектроника и молодежь в XXI веке” (10-12 апреля 2006 г.). – Харьков: ХНУРЭ, 2006. – С. 578.

16. Shkil A., Syrevitch Yev., Karasyov A., Cheglikov D. Path sensitization at functional verification of HDL-models // EWDTW'06: Proc. of the International conf. (September 15-19, 2006). – Sochi, Russia: KhNURE, 2006. – Р. 126 – 132.

17. Сыревич Е.Е., Чегликов Д.И. Сопоставление традиционной и современной методик проектирования // Материалы 8-го Междунар. молодеж. форума “Радиоэлектроника и молодежь в XXI веке” (13-15 апреля 2004 г.). – Харьков: ХНУРЭ, 2004. – С. 274.

18. Rustinov V., Syrevitch Yev. A Model of Data Path for Verification Test Generation for Microprogramming SOC // CADSM'2005: Proc. of the International conf. (February 23-26, 2005). – Lviv – Polyana, Ukraine: Lviv Polytechnic National University, 2005. – Р. 365 – 368.

19. Сыревич Е.Е., Чегликов Д.И. Аппаратная реализация функциональной верификации // Материалы 9-го Междунар. молодеж. форума “Радиоэлектроника и молодежь в XXI веке” (19-21 апреля 2005 г.). – Харьков: ХНУРЭ, 2005. – С. 537.

АНОТАЦІЯ

Сиревич Є.Ю. Верифікація моделей цифрових пристроїв, які подано мовами опису апаратури. – Рукопис. – Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.12 – системи автоматизації проектувальних робіт. – Харківський національний університет радіоелектроніки, Харків, 2007.

Робота присвячена функціональній верифікації високорівневих моделей цифрових пристроїв (ЦП), які подано мовами опису апаратури (МОА). Мета роботи – розробка методів зменшення кількості тестової інформації при верифікації моделей цифрових пристроїв, які подано мовами опису апаратури.

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

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

АННОТАЦИЯ

Сыревич Е.Е. Верификация моделей цифровых устройств, представленных на языках описания аппаратуры. – Рукопись. – Диссертация на научной степени кандидата технических наук по специальности 05.13.12 – системы автоматизации проектных работ. – Харьковский национальный университет радиоэлектроники, Харьков, 2007.

Работа посвящена верификации высокоуровневых моделей цифровых устройств (ЦУ) на языках описания аппаратуры (ЯОА). Целью исследования являлась разработка методов сокращения объема тестовой информации при верификации моделей ЦУ, представленных на ЯОА.

В основе разрабатываемых структурно-функциональных подходов к проектированию и верификации ЯОА - моделей лежит дуализм HDL-кода. С одной стороны ЯОА - модель – это описание на алгоритмическом языке с формализацией языковых конструкций и наличием специализированной среды разработки. С другой