ТЕСТУВАННЯ І ВЕРИФІКАЦІЯ HDL-МОДЕЛЕЙ КОМПОНЕНТІВ SOC
1. Аналіз тестопригодності графа управління
Враховуючи, що автоматна модель програмного продукту представлена ​​взаємодією операційного та керуючого автомат, рис. 1, то поряд з моделюванням транзакційного графа, необхідно мати можливість аналізувати тестопригодності граф-схеми алгоритму керування (ДСА).
В
Рис. 1. Автоматна модель HDL-програми
Пропонується ДСА представити у вигляді змістовного графа управління (СГУ), який є подібним транзакційних графу. Тут вершини є операції програмного коду, а дуги представляють умови переходу з однієї вершини в іншу для виконання команди, позначеної вершиною-стоком.
Отже, для СГУ можна використовувати процедури, раніше розроблені для підрахунку критеріїв тестопригодності транзакційного графа в частині спостереження та управлiння. Прикладом змістовного графа може служити рис. 2, що має 6 вершин і 9 дуг. br/>В
Рис. 2. Змістовний граф HDL-програми
Підрахунок керованість графа, представленого на рис. 2, має наступний вигляд:
В В
В
Підрахунок наблюдаемо графа, представленого на рис. 2, містить такі вирази:
В В
В
В
Рис. 3. Графіки тестопригодності для графа управління
Для використання тестопригодності виконується побудова спостереження та управлiння всіх компонентів HDL-моделі (рис. 3). Потім обчислюється узагальнена характеристика - тестопригодності кожного компонента як твір спостереження та управлiння:
. (1)
Далі інтерес становить створення таблиці тестопригодності, спостереження та управлiння, а також відповідний їм графік для візуального контролю В«поганихВ» компонентів. Фіксація певної планки тестопригодності, нижче якої значення будуть вважатися неприйнятними, дозволить розробнику створювати ассерція та інші додаткові засоби підвищення тестопригодності для проблемних функціональних блоків. Крім того, засоби підвищення тестопригодності повинні забезпечувати глибину діагностування до функціонального компонента і прив'язаних до нього операцій у цілях швидкого відновлення працездатності програмної HDL-моделі. У цілях побудови алгоритмів пошуку помилок в програмному коді можна використовувати таблицю несправностей, за аналогією з технологією тестування hardware. Цікаве рішення в процесі перевірки функціональних блоків пов'язано з сигнатурним аналізом, де узагальнена сигнатура ототожнюється з справним поведінкою всього коду, а також з кожним компонентом. Будь-яке розбіжність еталонної сигнатури з фактичною призводить до виконання процедури діагностування і відновлення працездатності HDL-моделі шляхом виправлення семантики коду.
Запропонована модель верифікації HDL-проекту використовує testbench, функціональне покриття, механізм ассерція, описану вище метрику оцінки тестопригодності, таблицю несправностей і вектор експериментальної перевірки (ЗЕП), що формується за заданими контрольним точкам шляхом порівняння сигнатур. Функціональне обмеження testbench пов'язано з нерозрізненість компонентів програмного коду, в яких можуть бути помилки. Його основне призначення - перевірка справності HDL-моделі. Тому в якості доповнення до процедурі перевірки надається механізм ассерція, основна мета якого з заданою глибиною - до програмного компонента - визначити місце і вид помилки на стадії виконання діагностування, після того, як testbench зафіксував неправильне функціонування програмного проекту. Дві стадії верифікації: тестування і діагностування - представлені нижче у вигляді наступних двох векторно-матричних операцій:
Для першої стадії використовується двійковий вектор експериментальної перевірки, формується на основі процедури тестування. На другій стадії використовується вже матриця експериментальної перевірки, яка з наперед заданою глибиною визначає діагноз проекту на основі порівняння технічних станів HDL-моделі та механізму ассерція:
В
У процесі виконання процедури верифікації виконується порівняння фактичного і еталонного (специфікованого) технічного стану компонента шляхом застосування операції Xor:
Практично, якщо виконані умови тестопригодності і правильно розставлені ассерція у критичних точках програмного коду для діагностування всіх компонентів, то ЗЕП може однозначно ідентифікувати адресу (місце) і тип помилки на основі побудованої раніше таблиці несправностей - механізму ассерція.
2. Верифікація DCT IP-core, Xilinx
Представлені моделі верифікації програмного HDL-коду перевірені на реальному проекті Xilinx IP-core в цілях визначення наявності в ньому помилок. При цьому вдалося отримати позитивний результат щодо невірної семантики роботи програми для подальшого виправлення коду. Частковий модуля дискретного косинусного перетворення представлений лісти...
