Верифікація мікропроцесорів

Робоча програма навчальної дисципліни (відповідно до вимог МОН України).
Документ містить мету, результати навчання, структуру змісту, систему оцінювання та літературу.

Код курсу: КА-121-03

Кафедра: Кафедра мовного забезпечення

Кількість кредитів ECTS: 6 (180 годин)

Рівень: Бакалавр / Магістр

Базис: BTRON BX Series — Scalable Vector Machines 8→64 (bx.btron.pro), VEX Vector Extension, Bluespec SystemVerilog, RISC-V Vector (RVV 1.0 / Zve*) mapping, OpenGL ES 1.x transform pipelines

Мета та завдання

Формування глибоких знань і практичних навичок у галузі формальної та напівформальної верифікації мікропроцесорів на прикладі сімейства BTRON BX Series — когерентної лінійки чистих FPGA RTL-машин зі масштабованим векторним розширенням VEX від 8-біт до 64-біт. Курс інтегрує класичні методи верифікації апаратури (модельна перевірка, еквівалентність, property-based verification) із сучасними підходами Bluespec SystemVerilog (Guarded Atomic Actions), відповідністю RISC-V Vector Extension та довжино-агностичними ядрами для OpenGL ES-подібних transform/lighting пайплайнів. Особливий акцент — на 1:1 трасованості архітектурного наміру (technical notes) до синтезованого RTL, масштабованості векторної моделі (SEW, VLEN, VL) та збереженні програмної сумісності між BX-16 / BX-32 / BX-64.

Результати навчання

• Розуміти архітектуру сімейства BX Series (BX-8, BX-16, BX-32, BX-64) як єдиної дизайн-культури зі спільним Bluespec-інфраструктурою та прогресивним векторним розширенням.
• Пояснювати модель VEX (Vector Extension): SEW 8/16/32/64, VLEN, VL-агностичні цикли, відображення на RVV / Zve32f / Zve64f / Zve64d та custom-0/1 простір.
• Аналізувати OpenGL ES 1.x transform path (matrix×vertex, dot/lighting, cross product, load/store) у термінах VEX
• Застосовувати теоретичні результати до розв’язання задач.
• Формалізувати ключові твердження в системах доведення теорем (за можливості).
• Демонструвати навички самостійного дослідження та академічної доброчесності.

Структура курсу (модулі)

1. Теоретичні основи
2. Алгоритми та реалізації
3. Інструменти верифікації
4. Практичні кейси
5. Формальні методи

Система оцінювання (100 балів)

• Поточний контроль (практичні, домашні, лабораторні, формалізація): 40 балів
• Модульні контрольні роботи (2): 20 балів
• Підсумковий іспит / захист проєкту: 40 балів

Шкала: 90–100 — відмінно; 75–89 — добре; 60–74 — задовільно; <60 — незадовільно.

Рекомендована література

• Основні монографії та підручники з теми (рекомендовані кафедрою).
• Статті та матеріали з формальної математики (HoTT, теорія категорій).
• Внутрішні конспекти та формалізації Інституту Формальної Математики / Groupoid Infinity.

← Назад до каталогу курсів