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

Єгоров Олександр Андрійович

УДК 004.415.5:519.718

МОДЕЛІ І МЕТОДИ СПІЛЬНОЇ ВЕРИФІКАЦІЇ ПРОЕКТОВАНИХ ЦИФРОВИХ СИСТЕМ НА КРИСТАЛАХ

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

Автореферат

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

кандидата технічних наук

Харків – 2006

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

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

Науковий керівник – доктор технічних наук, професор Хаханов Володимир Іванович, Харківський національний університет радіоелектроніки, декан факультету комп’ютерної інженерії і управління.

Офіційні опоненти: доктор технічних наук, професор Харченко В’ячеслав Сергійович, Національний аерокосмічний університет ім. М.Є. Жуковського “Харківський авіаційний інститут”, завідувач кафедри комп’ютерних систем та мереж;

кандидат технічних наук, доцент Литвинова Євгенія Іванівна, Харківський національний університет радіоелектроніки, доцент кафедри технології і автоматизації виробництва.

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

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

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

Автореферат розісланий  “ 14 ” червня 2006 р.

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

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

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Новітні технології виробництва кристалів ПЛІС (програмувальні логічні інтегральні мікросхеми) дозволяють розміщувати процесори разом з десятками мільйонів програмованих логічних матриць, що дає можливість інтегрувати системи і мережі в одному виробі. Прикладом цього є останні ПЛІС фірми Xilinx – серії Virtex II Pro, Virtex 4. Це означає, що розробники ПЛІС мають потребу у все більш складних системах верифікації та тестування, які здатні працювати не тільки з описом логічних схем, а і з програмним забезпеченням, що входить до складу SoC та/або NoC. Проблема ефективності верифікації ускладнюється також наявністю різних середовищ для традиційного налагоджування програмного забезпечення і апаратних блоків, а також значними часовими витратами на обробку структурно і функціонально складних проектів, що включають мільйони еквівалентних вентилів і тисячі рядків програмного коду.

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

Найбільший внесок у наукові досягнення, що стосуються автоматизації проектування і тестування цифрових систем зробили такі вчені: D.Gajski, J.Roth, D.B.Armstrong, Y.Levendel, M.Breuer, M.Abramovici, Y.Zorian, P.Prinetto, J.Abraham, H.Fujiwara, I.Pomeranz, T.Nishida, F. Fummi, О.Г.Біргер, Д.В.Сперанський, П.П.Пархоменко, Ю.В.Малишенко, Р.Убар, В.П.Чіпуліс, Н.П.Байда, С.С.Бадулин, В.С.Харченко, Л.В.Дербунович, І.В.Кузьмин, В.Н.Ярмолик.

Зв’язок роботи з науковими програмами, планами, темами. Розробка основних положень дисертаційної роботи виконувалася відповідно до планів НДР, програм і договорів Харківського національного університету радіоелектроніки: 1) Договір про науково-технічне співробітництво з фірмою Аldec Inc. (USA), № 02 від 19.11.2001 “Розробка програмних і апаратних засобів верифікації систем на кристалах, що реалізуються на основі програмувальних логічних інтегральних схем”; 2) Договір про науково-технічне співробітництво з Таллінським технічним університетом № 01 від 07.04.2004; 3) Договір про науково-технічне співробітництво з фірмою “Лаборатория Касперского”, Москва, Росія, № 01 від 14.04.2005; 4) Дослідницький проект за грантом “SIGETEST – моделювання та синтез тестів для складних цифрових систем” за пропозицією компанії Intel, 2003; 5) Господарський договір № 05-19 з ЗАТ “Северодонецкое НПО Импульс” “Розробка технології автоматизованого проектування відмовостійких програмно-технічних комплексів (ПТК)”; 6) Держбюджетна НДР “Дослідження і розробка методів, структурних і архітектурних принципів апаратних і програмних засобів швидких цифрових перетворень зображень”, розділ “Система тестування цифрових засобів, що проектуються” (№ ДР 0104U004074); 7) Держбюджетна НДР “Розробка математичних методів, алгоритмів та інструментальних засобів надшвидких перетворень зображень”, розділ “Розробка основ нових інформаційних технологій в автоматизованому проектуванні, діагностиці засобів обчислювальної техніки” (№ ДР 0101U001948).

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

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

розробити модель спільної верифікації для обробки неоднорідних апаратно-програмних систем, що являють собою алгоритмічні, структурнофункціональні описання “С” подібними мовами та мовами опису апаратури VHDL, Verilog;–

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

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

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

Об’єкт дослідження: складна неоднорідна цифрова система, яка містить один або декілька процесорів, що проектується на кристалах з програмованою логікою і подається мовою опису апаратури VHDL, Verilog та “С” подібними мовами.

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

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

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

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

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

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

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

Результати дисертації впроваджено на підприємствах: Aldec Inc. (сертифікат про впровадження від 14 січня 2005); ЗАТ НДІРВ, Харків (довідка про впровадження від 17 листопада 2005); ЗАТ "Импульс", Сєвєродонецьк (довідка про впровадження від 22 грудня 2005); Міжнародний консорціум “Енергозбереження”, Харків (довідка про впровадження від 26 грудня 2005); а також у навчальному процесі Харківського національного університету радіоелектроніки (акт про впровадження від 26 грудня 2005).

Особистий внесок здобувача. Усі основні результати, що виносяться на захист, отримано здобувачем особисто. У роботах, написаних у співавторстві, здобувачеві належить: [1] – розробка методу проектування тестопридатних цифрових систем, модель механізму асерцій для формальної верифікації; [2] – дослідження моделей та методів автоматизованого проектування систем на кристалі; [3] – удосконалення моделі реалізації спільної верифікації систем на кристалі; [4] – розробка методу підвищення якості тесту при функціональній верифікації на основі методології граничного сканування; [5] – розробка методу підвищення продуктивності програмної реалізації процедур моделювання; [6] – дослідження стратегій тестування програмного забезпечення; [7] – удосконалення моделі автоматизованих систем моделювання несправностей, реалізація автоматизованої системи моделювання несправностей; [8] – розробка методу тестування SoC та аналізу дефектів надскладних схем; [9] – розробка моделі HW-SW спільної верифікації цифрових систем на кристалах; [10] – розробка методу моделювання і синтезу тестів для SoC; [11] – розробка універсальної моделі тестів для застосування на усіх рівнях верифікації цифрових систем на ПЛІС; [12] – розробка методу моделювання і синтезу тестів для складних цифрових систем; [13] – обґрунтування застосування універсальної моделі тестів для спільної верифікації апаратних і програмних частин систем на кристалах; [14] – розробка архітектури верифікації для застосування з сучасними САПР; [15] – розробка архітектури системи програмно-апаратної верифікації; [16] – розробка методу динамічної емуляції та моделювання блоків цифрових систем на ПЛІС; [17] – дослідження застосування надлишковості опису апаратних блоків при верифікації; [18] – розробка моделі та методу асерцій для формальної верифікації систем на кристалах.

Апробація результатів дисертаційної роботи. Матеріали дисертаційних досліджень доповідалися, обговорювалися і були схвалені на таких науково-технічних конференціях і семінарах: 1) Design Automation Conference (DAC) (Anaheim, USA, 2003); 2) Altera SOPC’03 (system on programmable chip) developer days (San Hose CA., USA, 2003); 3) 1-а, 2-а і 3-я Міжнародна наукова конференція “East-West Design and Test Conference” (Ялта, 2003; Алушта, 2003; Одеса, 2004); 4) 9-а і 10-а Міжнародна конференція "Теория и техника передачи, приема и обработки информации" (Харків – Туапсе, 2003; 2004); 5) 7-а Міжнародна конференція “The Experience of designing and Application of CAD Systems in Microelectronics” (Львів, 2003); 6) 16-а Міжнародна науково-технічна конференція “Перспективные информационно-управляющие системы на железнодорожном, промышленном и городском транспорте” (Алушта, 2003); 7) Міжнародна наукова конференція “Единое информационное пространство” (Дніпропетровськ, 2004); 8) Міжнародна наукова конференція EuroMicro Symposium (Rennes, France, 2004); 9) 8-а Міжнародна конференція “CADSM 2005” (Львів, 2005).

Публікації. Основні наукові положення дисертації відбиті в 18 друкованих працях. Серед них 5 статей, що опубліковані в наукових виданнях, включених до переліків ВАК України, а також 13 публікацій у працях конференцій.

Структура й обсяг дисертації. Дисертаційна робота складається із вступу, 4 розділів, висновків, переліку використаної літератури із 136 джерел на 12 с., 1 додатка на 5 с. Загальний обсяг становить 151 с., ілюстрацій – 72, таблиць – 3.

ОСНОВНИЙ ЗМІСТ РОБОТИ

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

У першому розділі розглянуто стан розвитку технологій виробництва програмованих логічних інтегральних схем на кристалах. Наведено аналіз робіт у галузі автоматизованого проектування і тестування цифрових систем на кристалах (Systems on Chip – SoC). Визначено основні технології та маршрути проектування, системи автоматизованого проектування (САПР); методи, алгоритми та засоби тестування, верифікації та діагностування складних цифрових систем. Запропоновано шляхи підвищення ефективності тестування і верифікації та зменшення часу (і вартості) процесів автоматизованого проектування.

З появою нового покоління ПЛІС з десятками мільйонів вентилів на одному кристалі (фірми Xilinx, Altera) стало можливим розміщувати на них складні спеціалізовані багатопроцесорні системи (Embedded Systems) і мережі (Networks on Chip – NoC). Однак для використання усіх можливостей, що надаються виробниками кристалів, і засобів проектування необхідні програмні засоби розробки і тестування (верифікації) функціонально складних систем з багаторазовим використанням ідентичних блоків і програмного забезпечення, що включаються в систему. Все більш актуальною стає проблема створення систем проектування і верифікації SoC, що використовують для прискорення моделювання апаратурні ресурси сучасних ПЛІС.

Стадія верифікації сучасних спеціалізованих цифрових систем є критичною за своєю актуальністю у зв’язку з тим, що складає до 70% загальних витрат на проектування. Зменшення часу верифікації та мінімізація терміну загального циклу розробки – одне із головних завдань у галузі Electronic Design Automation (EDA – автоматизація проектування в електроніці). Складність і неоднорідність об’єктів проектування потребує створення нових методів і інструментарію тестування апаратно-програмного інтерфейсу SoC. Тестування і верифікацію необхідно виконувати на ранніх стадіях проектування для виключення витрат на повторне проектування в разі виникнення катастрофічних невідповідностей у проекті.

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

Кількість транзисторів в одній мікросхемі щорічно зростає на 60%, однак їх використання в нових проектах збільшується тільки на 20%. Це пов’язано з недосконалістю сучасних засобів САПР і, перш за все, методів і засобів сумісної функціональної верифікації. Специфікою сучасних SoC є надвелика продуктивність (ніж в системах на платах), використання широкого спектра технологій на кристалах (жорстка і програмувальна логіка, програмне забезпечення, множина синхронізуючих доменів), використання модульності. Останнє дозволяє створювати великі проекти завдяки багаторазовому використанню IP-cores (апаратний блок, що спроектований). Однак ефективна верифікація таких проектів потребує реалізації black-box (реалізація тільки через інтерфейс з обмеженою інформацією щодо внутрішньої структури) технології тестування замість white-box (з використанням інтерфейсу і доступом до внутрішніх точок блока).

У другому розділі запропоновано, обґрунтовано і досліджено удосконалену модель проектування цифрових систем Гайського. Дослідження виявило, що, в середньому процесорні системи складаються більш ніж на 70% з раніше розроблених та повторно використаних модулів (IP core). Під час моделювання є можливість відразу використовувати точні моделі таких модулів (процесорів, шин, периферійних пристроїв), які вміщують точні обчислювальні і комунікаційні затримки та гарантують точність здобутих під час верифікації параметрів SoC.

Виявляється зайвим використання абстрактних моделей обчислювальних та комунікаційних модулів SoC: модель обчислювальних транзакцій (2 на рис. 1), модель комунікаційних транзакцій (3 на рис. 1), модель транзакцій на шині (4 на рис. 1). Розроблена універсальна модель верифікації апаратно-програмних систем орієнтована на спільне моделювання низькорівневих апаратних розроблених блоків та блоків, що проектуються (алгоритмічне надання, поведінкове та у формі регістрових передач) і програмних модулів (2’ на рис. 1).

Точка 1 – початок проектування. Модель системи на даному етапі не враховує комунікаційних та обчислюваних затримок. Точка №5 – кiнець проектування.

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

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

Рис. 1. Схема удосконаленої моделі та методу спільної верифікації цифрових систем

Наведено структуру часової моделі для аналізу перехідних процесів з метою виявлення змагань (рис. 2), надано два види затримок, що пов’язані з номінальними параметрами елементів і параметрами розкиду появи сигналів на зовнішніх входах пристрою.

Рис. 2. Універсальна часова модель цифрової системи на кристалі

Універсальна модель аналізу змагань заснована на варіаціях затримок :

; ; ; . (1)

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

Досліджено модель тестування , або точніше у компонентах:

, (2)

де – множина несправностей цифрової системи , що перевіряються тестом;

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

– модель системи на кристалі, що вміщує програмну (S) і апаратну (Н) частини;

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

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

Рис. 3. Схема рівнів проектування і рівнів тестів

Відповідно до цього може бути сформована система рівнянь, яка відображує стратегію тестування і верифікації цифрового виробу на стадіях проектування:

(3)

де – множина, що включає несправності усіх етапів проектування систем на ПЛІС .

Між типами тестів виконується відношення неточного включення .

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

Рис. 4. Схема процесу тестування SoC на стадіях проектування

Множину несправностей , що перевіряються, можна навести як:

, (4)

де – тестові дії відповідно до (2);

– модель системи на кристалі;

– програмна частина системи на кристалі, що
подана відповідно до конструкцій мов: UML, С++, Assembler, виконавчого коду;

– апаратна частина ЦС відповідно до (2);

– компоненти моніторингу, що включають механізм асерцій для програмних і апаратних модулів, налагоджувач програмних частин і регістр граничного сканування (Boundary Scan) для моніторингу і управлінням внутрішніми лініями апаратурної реалізації системи.

Модель процесу тестування, що розроблена, дозволяє розрізняти множину усіх компонентів SoC на: hardware і software частини, black-boxes і white-boxes, а також розділяти моделі цифрової системи за рівнем проектування. Це дає можливість генерувати простіші спеціальні тести для кожного типу моделі та збільшувати їх розмірність за необхідності.

Розроблено та обґрунтовано архітектуру системи спільної верифікації на основі універсальної моделі, що наведена вище. Замість швидких програмних моделей апаратних блоків запропоновано використання ПЛІС кристала спільно з програмою логічного моделювання (ПЛМ), (рис. 5). Це дозволяє прискорити моделювання та використовувати при верифікації складні низькорівневі, але точніші моделі блоків SoC та великі обсяги програмного коду.

Рис. 5. Схема архітектури системи спільної верифікації SoC

Отримані результати дозволяють для запропонованої архітектури ввести динамічний режим синхронізації. Коли через інтерфейс І між блоками в ПЛІС та в ПЛМ проходить обмін даними або командами, всі компоненти моделювання синхронізуються єдиним найбільшим синхросигналом CLKS, що генерується ПЛМ. Якщо інтерфейс І незмінний (І=const), тобто через І немає обміну командами або даними, то блоки в ПЛІС синхронізуються апаратно-згенерованим синхросигналом CLKH (CLKH>>CLKS), а блоки в ПЛМ синхронізуються CLKS. Коли інтерфейс І змінюється, синхронізація всіх блоків знову переходить на CLKS. Застосування CLKH дозволяє прискорити моделювання до 100 разів за рахунок швидкого виконання великої кількості транзакцій між процесором та блоками пам’яті, що розташовані в ПЛІС.

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

, (5)

де – відповідно робочі (функціональні) тестові дії;

– відповідно специфікована (основна) модель і додаткова модель для верифікації та валідації проектованого пристрою;

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

Тестова верифікація на підставі класичного тесту Тt (T={Tw, Tt}) потребує створення таких перевіркових послідовностей, що синтез повного відносно заданого класу дефектів тесту (NP повне завдання) стає одним з найбільш витратних етапів проектування. Функціональна верифікація із застосуванням надмірності Fv (5) більш економічна, хоч і передбачає додаткові разові витрати. Вона використовує функціональні робочі (псевдовипадкові) вхідні послідовності . Ці процеси мають суттєві різниці за часом їх підготовки та проведення, оскільки час генерації класичного testbench , що орієнтовано на 100% повноту виявлення дефектів, у сотні разів більший за час розроблення функціонального тесту . Таким чином, . Для компенсації низького рівня покриття несправностей за допомогою необхідно збільшувати кількість точок аналізу в моделі, що і виконує механізм асерцій. Він використовується як доповнення до специфікації проекту.

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

.

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

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

Розроблена модель макропроцесу верифікації проектованого пристрою (рис. 6) включає такі компоненти. 1. Testbench, що написаний С/C++ або HDL мовою. 2. Повна специфікована модель проекту. 3. Модель асерцій, що надана спеціалізованою мовою або мовою опису апаратури і занесена в середовище для аналізу асерцій. На рис. 6 наведена схема процесу верифікації.

Рис. 6. Схема процесу верифікації та діагностування на підставі асерцій

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

Загальні витрати на процес верифікації, відповідно до (5), складаються із витрат на стадії підготовки (розробка і синтез testbench)

,

за умов, що , та на виконання діагностичного експерименту (час роботи процесора):

.

Найбільш суттєвими компонентами є: , . Тому ефективність методу залежить, в першу чергу, від часу розробки або синтезу testbench:

. (6)

Використання наведеного маршруту тестування суттєво зменшує час повної верифікації пристрою завдяки імплементації програмної системи аналізу асерцій в засоби моделювання проектованої системи. Натурні дослідження показали скорочення загального часу проектування в 2-3 рази для систем високої складності та розміром до 1 млн. вентилів.

Використання верифікації на підставі асерцій має такі переваги: 1) скорочується обсяг коду для створення testbench; 2) повідомлення про порушення асерції безпосередньо вказує місце в ієрархії пристрою і момент виникнення відмови; 3) момент порушення асерції може бути використаний в середовищі верифікації як додаткова точка зупинки (breakpoint), а також для запуску спеціальних алгоритмів обробки для підвищення глибини діагностування, що переводить testbench на вищий рівень абстракції; 4) за умов адекватності асерцій статистика процесу може бути використана для аналізу якості покриття; 5) виникає можливість побудови моделі із самотестуванням.

Четвертий розділ присвячений експериментальному аналізу засобів і моделей сумісної верифікації. Розроблено систему сумісної апаратно-програмної верифікації СoVer, що призначена для проектування складних цифрових систем на ПЛІС (інтегрована в EDA tools Active-HDL v.6.3 фірми Aldec, USA). Система CoVer містить засоби логічного моделювання Active-HDL, апаратний прискорювач аналізу справної поведінки цифрових систем Aldec HES, GNU-компілятор і налагоджувач. Розроблена система верифікації та тестування інтегрована як частина САПР SoC у маршрути проектування цифрових систем на ПЛІС компаній Xilinx, Altera. Запропонований маршрут верифікації SoC дозволяє покрити більш ніж 90% усіх ідентифікованих невідповідностей і дефектів, що виникають в процесі проектування і імплементації.

Розроблено та побудовано графічні інтерфейси для автоматичного імпорту проектів із бібліотек Xilinx EDK, Altera SOPC, що підтримують САПР SoC на системному рівні. Розроблено модуль синхронізації Quick-Bridge для управління побудовою логічних елементів у ПЛІС і моделюванням блоків в Active-HDL. Програмний модуль синхронізації процесів моделювання і передачі даних під час тестування та налагоджування програмного забезпечення і апаратних блоків SoC містить налагоджувачі GNU, Active-HDL. Модуль запобігає конфліктам між налагоджувачами С++ та HDL і дозволяє одночасно проводити верифікацію кодів програмних і апаратних блоків SoС.

Оцінка коефіцієнта прискорення верифікації цифрового виробу під час використання апаратного прискорювача для моделювання програмно-апаратних блоків формується профайлером HDL коду. У цьому випадку – частка ресурсів ПЛМ, що використується для моделювання блоків, що імплементуються в ПЛІС апаратного прискорювача. Для сучасних проектованих SoC, що містять до 90% і більше апаратних блоків багаторазового використання, які одразу можна розміщувати в ПЛІС, коефіцієнт прискорення верифікації має фактичне значення

Для зв’язку програмного налагоджувача (GDB) з процесором SoC, виконаним на ПЛІС (рис. 7), реалізовано віртуальний COM-порт через PCI-шину апаратного прискорювача Aldec HES, що дає можливість використовувати програмний налагоджувач у процесі сумісного моделювання частин SoC. Багатовіконний графічний інтерфейс користувача (що додається у вигляді plig-in в Active-HDL) дозволяє здійснювати візуалізацію процесів моделювання та моніторингу апаратних і програмних блоків SoC.

Під час тестування SoC на базі Xilinx MicroBlaze процесора при використанні середовища CoVer (MicroBlaze процесор розташований у ПЛІС), час встановлення операційної системи ucLinux на розроблену SoC зменшився в 6 разів, а при використанні режиму емуляції на частоті 16 МГц – у 40 разів.

Використання усіх розроблених методів, прийомів і маршрутів сумісної апаратно-програмної верифікації SoC суттєво зменшує витрати на виявлення, діагностування і виправлення несправностей (у середньому кожна процедура відносно до традиційних прийомів: механізм асерцій – на 10%, апаратне прискорення – на 5%, емуляція – на 15%, універсалізація тестів – на 10%, сумісна апаратно-програмна верифікація – до 50%), що в загальній кількості дозволяє зменшити в 2-3 рази загальний час проектування цифрових систем на кристалах. Тестування розроблених засобів моделювання і верифікації виконувалося шляхом порівняння з існуючими світовими аналогами, перевіркою усіх функціональних режимів за допомогою тестових прикладів з відкритих бібліотек провідних фірм світу в галузі проектування і верифікації цифрових систем: Aldec, Synopsis, Xilinx, Altera

Рис. 7. Структура програмно-апаратних засобів у середовищі CoVer

Програмні засоби системи CoVer успішно використовуються в ряді компаній та організацій, що розробляють складні спеціальні цифрові системи на кристалах (Dillon Engineering USA; Altera, USA; MBT, China; НДІРВ, Україна), де підтвердилися переваги наведених засобів, моделей і методів сумісної верифікації SoC.

ВИСНОВКИ

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

2. Удосконалено архітектуру моделі спільної верифікації неоднорідних систем на основі використання ПЛІС кристалів та існуючих засобів САПР. Запропонована архітектура враховує особливість перепрограмування крис-талів ПЛІС, дозволяє прискорити моделювання складних систем з великим обсягом ПЗ (таких, як ОС реального часу). Дозволяє на ранніх стадіях проектування моделювання взагалі всієї SoC та виключення основних ризиків некоректностей специфікації, що призводять до значних витрат на повторне проектування.

3. Обґрунтовано ефективність використання програмної надлишковості у вигляді асерцій для верифікації та діагностування проектованих цифрових систем. Механізм асерцій дозволяє підвищити глибину діагностування несправностей та зменшити витрати на генерацію тестів та аналіз реакцій ЦС на предмет наявності несправностей.

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

5. Введено та досліджено структуризацію моделі ЦС для одночасного виконання верифікації за допомогою програмного моделювання та емуляції в ПЛІС, що дозволяє здійснювати верифікацію на високих частотах (декілька МГц). Вирішено проблему синхронізації сумісного моделювання та емуляції.

6. Шляхом експериментальних досліджень на однопроцесорних системах на ПЛІС кристалах продемонстровано високі показники виявлення несправностей (особливо несправностей апаратно-програмного інтерфейсу SoC), зменшення часу верифікації. Розроблена система верифікації та тестування інтегрована як частина САПР SoC у маршрути проектування цифрових систем на ПЛІС провідних фірм в галузі проектування і верифікації цифрових систем.

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

1. Хаханов В.И., Егоров А.А., Зайченко С.А., Обризан В.И., Каминская М.А. Механизм ассерций для функциональной верификации проектируемых цифровых систем // АСУ и приборы автоматики. – 2005. – №131.– C. 147–157.

2. Сысенко И.Ю., Побеженко И.А., Побеженко В.В., Егоров А.А. Средства верификации цифровых проектов на основе программируемой логики // АСУ и приборы автоматики. – 2003. – № 122. – С. 36–44.

3. Хаханов В.И., Егоров А.А., Хаханова И.В., Гузь О.А. Co-design технология проектирования SOC на основе Active-HDL 6.2 // Радиоэлектроника и информатика. – 2004. – №2. – C. 76–80.

4. Хаханов В.И., Каминская М.А., Егоров А.А., Побеженко И.А. Повышение качества теста на основе технологии Boundary Scan // Радиоэлектроника и информатика. – 2004. – №3. – C. 85–90.

5. Хаханов В.И., Зайченко С.А., Егоров А.А. Анализ быстродействия базовых операций в дедуктивном методе моделирования неисправностей // АСУ и приборы автоматики. – 2004. – № 127. – С. 138–148.

6. K. Mostovaya, O. Yegorov, Le Viet Huy Software Test Strategies // Proceedings of the 3rd East-West Design and Test Workshop.– Odessa, Ukraine, 2005. – P. 266–267.

7. Hahanov V., Egorov A., Melnikova O., Obrizan V., Kamenuka E., Krapchunova O., Guz O. Advanced software tools for fault simulation and test generation // Proc. East-West Design and Test Workshop. – Yalta, 2003. – C. 77–82.

8. Егоров А.А., Горбунов Д.М., Черкашин А.В. BDP-метод анализа дефектов сверхсложных цифровых систем // Материалы 7-го Международного молодежного форума "Радиоэлектроника и молодежь в 21 веке". – Харьков, 2003. – С.462.

9. Егоров А.А., Киященко А.В., Парфентий А.Н. HW-SW коверификация цифровых систем на кристаллах // Материалы 9-го международного молодежного форума "Радиоэлектроника и молодежь в 21 веке". – Харьков, 2005. – C. 542.

10. Горбунов Д.М., Мирошниченко Я.В., Егоров А.А. Технология моделирования и синтеза тестов для сложных цифровых систем // Материалы международной научной конференции "Теория и техника передачи, приема и обработки информации". – Харьков– Туапсе, 2003. – С. 20–21.

11. Olga Skvortsova, Oleksandr Yegorov, Dmitriy Gorbunov, Hayk Chamyan. TestBuilder – ATPG System for Digital Devices Based on FPGA // Proceedings of the 7-th International Conference "The Experience of designing and Application of CAD Systems in Microelectronics". – Lviv-Slavske, 2003. – P.412–416.

12. Горбунов Д.М., Мирошниченко Я.В., Егоров А.А., Крапчунова О.В. Технология моделирования и синтеза тестов для сложных цифровых систем // Материалы 16-й международной научно-технической конференции "Перспективные информационно-управляющие системы на железнодорожном, промышленном и городском транспорте". – Алушта, 2003. – C. 20–21.

13. Егоров А.А., Мирошниченко Я.В., Каменюка Е.А. Совместная верификация аппаратной и программной частей систем на кристалле (SOC), реализуемых на FPGA и CPLD // Тезисы докладов 10-й юбилейной международной научной конференции “Теория и техника передачи, приема и обработки информации”.– Туапсе, 2004. – С.141–142.

14. Егоров А.А., Хаханова И.В., Обризан В.И., Мельникова О.В. Верификация цифровых систем на основе современных средств проектирования // Сборник докладов международной конференции “Единое информационное пространство”.– Днепропетровск, 2004. – С. 173–176.

15. S. Hyduke, A.A. Yegorov, O.A. Guz, I.V. Hahanova. Co-design Technology of SOC Based on Active-HDL 6.2 // Proceedings of the 2nd East-West Design and Test Workshop 2004. – Alushta, Ukraine.– 2004. – P. 227–233.

16. O. Yegorov, V. Obrizan, M.K. Shahzad, O. Guz. FPGA SoC Hardware/Software Co-Simulation // Proceedings of the Work in Progress Session.– EuroMicro.– Rennes, France.– 2004.– Р.11.

17. Alexandr Yegorov, Irina Hahanova, Olga Melnikova, Vladimir Yeliseyev. Eda-Market and Soc Design Verification Technologies // Proceedings of the 8th International Conference CADSM 2005. – Lviv, Ukraine, 2005. – P. 352–355.

18. V. Hahanov, O. Yegorov, S. Zaychenko, A. Parfentiy, M. Kaminska, A. Kiyaschenko. Assertion-based Mechanism for the Functional Verification of the Digital Designs // Proceedings of the 3rd East-West Design and Test Workshop. – Odessa, Ukraine, 2005. – P. 261–265.

АНОТАЦІЯ

Єгоров О.А. Моделі і методи спільної верифікації проектованих цифрових систем на кристалах. – Рукопис.

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

Дисертація присвячена питанням функціональної верифікації складних проектованих цифрових систем на кристалах. У роботі розроблено структурну модель i метод спільної верифікації апаратних i програмних складових системи на кристалi. Встановлено, що більшу частину системи на кристалі, яка складається з неодноразово використаних апаратних i програмних блоків, можна розміщувати на програмованих логічних iнтeгральних схемах, починаючи з перших етапів проектування, для прискорення моделювання i зменшення часу процесів верифікації. Модернізованo архiтектуру системи моделювання цифрової системи (ЦС) для забезпечення можливості спільної верифікації програмних блоків, низькорівневих представлень апаратних блоків, моделей апаратних блоків, що розробляються. Обгрунтовано ефективність використання програмної надлишковості опису ЦС у вигляді асерцiй, що дозволяє автоматизувати функціональну верифікацію, зменшити витрати на тестування завдяки використанню псевдовипадкового тесту, а також збільшити глибину діагностування пристрою. Основні результати теоретико-експериментальних досліджень реалізовано у вигляді програмно-апаратного комплексу CoVer функціональної верифікації складних цифрових систем на кристалі, який знайшов промислове використання в проектуванні складних процесорних систем на ПЛІС.

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

АННОТАЦИЯ

Егоров А.А. Модели и методы совместной верификации проектируемых цифровых систем на кристаллах.– Рукопись.

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

Диссертация посвящена вопросам функциональной верификации сложных проектируемых цифровых систем на кристаллах. В работе разработана структурная модель и метод совместной верификации аппаратных и программных составляющих системы на кристалле. Установлено, что большую часть системы на кристалле, которую составляют неоднократно используемые аппаратные и программные блоки, можно размещать на программируемых логических интегральных схемах (ПЛИС), начиная с ранних этапов проектирования, для ускорения моделирования и сокращения времени процесса верификации. Усовершенствована архитектура системы моделирования цифровой системы (ЦС) для обеспечения
возможности совместной верификации программных блоков, неоднократно используемых низкоуровневых представлений аппаратных блоков, моделей разрабатываемых аппаратных блоков. Обоснована эффективность использования программной избыточности описания ЦС в виде ассерций, позволяющей автоматизировать функциональную верификацию, уменьшить затраты на тестирование благодаря использованию псевдослучайного теста, а также увеличить глубину диагностирования устройства. Основные результаты теоретико-экспериментальных исследований реализованы в виде программно-аппаратного комплекса CoVer функциональной верификации сложных цифровых систем на кристалле, который нашел промышленное применение при проектировании сложных процессорных систем на ПЛИС.

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

ABSTRACT

Yegorov O.A. Models and methods of co-verification of digital system on a chip.– Thesis.– dissertation to achieve academic degree of candidate of technical sciences by specialty 05.13.12 – design automation systems.– Kharkov national university of radio electronics, Kharkov, 2005.

Work is dedicated to the testing of the digital circuits on a chip. It is based on the development of models, methods and algorithms of hardware-software co-verification, which allows performing diagnosis of faults on the