Формальна перевірка еквівалентності

Формальна перевірка еквівалентності є частиною проектування електронних систем (англ. Electronic design automation,EDA), що широко використовується при розробці цифрових інтегральних схем, щоб формально довести, що два представлення схеми пристрою демонструють однакову поведінку.

Перевірка еквівалентності та рівні абстракції

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

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

Розробники мікропроцесорів використовують перевірку еквівалентності для порівняння функцій, зазначених для архітектури набору команд з реалізацією рівня регістрових передач (англ. Register-transfer level,RTL), забезпечуючи, що будь-яка програма, що виконується на обох моделях, призведе до однакового оновлення вмісту основної пам'яті. Це більш загальна проблема.

Для проектування на системному рівні абстракції потрібно провести порівняння між моделлю рівня транзакції (англ. transaction level model,TLM), наприклад, написаною в SystemC та відповідній специфікації RTL. Така перевірка стає дедалі більш привабливою для розробки системи на кристалі (англ. System on a Chip, SoC).

Перевірка на еквівалентність на етапах проектування

Рівень регістрових передач цифрового чипу зазвичай описується мовою опису апаратури, таким як Verilog або VHDL. Цей опис являє собою модель золотого еталону, яка детально описує, які операції будуть виконуватись протягом якого циклу синхросигналу і якими модулями системи. Після того, як розробники, шляхом моделювання та інших методів перевірки, перевірили опис рівня регістрових передач, проект зазвичай перетворюється в список нетліста[en] за допомогою інструмента логічного синтезу. Еквівалентність не слід плутати з функціональною правильністю, яка повинна визначатися функціональною перевіркою.

Первинний нетліст[en], як правило, проходить ряд перетворень, таких як оптимізація, додавання структур Design For Test[en] (DFT) тощо, перш ніж використовувати його як основу для розміщення логічних елементів на фізичному носії. Сучасне програмне забезпечення для фізичного проектування іноді також може зробить суттєві зміни (наприклад, заміна логічних елементів на еквівалентні аналогічні елементи, що мають більший або менший опір джерела і та / або більшу чи меншу площину) до нетліста[en]. Протягом кожного кроку дуже складної багатоетапної процедури початкова функціональність та поведінка, описана в початковому коді має бути збережена. Після цієї процедури, нетліст[en] може зазнати деяких змін як за допомогою EDA-програм, так і ручного втручання.

Теоретично інструмент логічного синтезу гарантує, що перший нетліст[en] логічно еквівалентний початковому коду RTL. Всі програми, що пізніше вносять зміни в нетліст[en], теоретично гарантують, що ці зміни логічно еквівалентні попередній версії.

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

Історично, один із способів перевірки еквівалентності полягав у повторній симуляції, використовуючи остаточний нетліст[en] та тестове покриття, розроблене для перевірки правильності RTL. Цей процес називається логічним моделюванням рівня логічних примітивів. Проте проблема полягає в тому, що якість перевірки залежить від якості тестового покриття. Крім того, симуляція рівня логічних примітивів дуже повільна, що є основною проблемою, оскільки розмір цифрових проектів продовжує зростати експоненціально.

Альтернативний спосіб вирішення цієї проблеми - формально довести, що RTL-код та синтезований з нього нетліст[en] мають однакову поведінку у всіх (відповідних) тестах. Цей процес називається формальною перевіркою еквівалентності, і це проблема, яка вивчається в більш широкій області формальної перевірки.

Формальну перевірку еквівалентності можна виконувати між будь-якими двома представленнями проекту: RTL <> netlist, netlist <> netlist або RTL <> RTL, хоча останнє зустрічається доволі рідко порівняно з першими двома. Як правило, інструмент перевірки формальної еквівалентності також з великою точністю вказує, у чому полягає різниця між двома представленнями.

Методи

Існує дві основні технології, що використовуються для логічного обґрунтування у програмах перевірки еквівалентності:

  • Бінарні діаграми рішень або БДР: спеціалізована структура даних, призначена для підтримки аргументації булевих функцій. БДР стали надзвичайно популярними через їх ефективність та універсальність.

Комерційні програми для еквівалентної перевірки

  • FormalPro від Mentor Graphics
  • Questa SLEC від Mentor Graphics
  • Conformal від Cadence
  • JasperGold від Cadence
  • Formality від Synopsys
  • 360 EC від OneSpin Solutions

Висновки

  • Перевірка еквівалентності відновлених схем: іноді корисно переміщати логіку з однієї сторони реєстру до іншого, що ускладнює перевірку.
  • Перевірка послідовної еквівалентності: Іноді два автомата на комбінаційному рівні абсолютно різні, однак вони повинні давати однакові результати, якщо вони мають однакові данні на вході. Класичним прикладом є дві ідентичних скінечних автомати з різними кодуваннями для станів. Оскільки це не можна звести до комбінаційної проблеми, потрібні більш загальні методи.
  • Еквівалентність програмного забезпечення, тобто перевірка того, чи дві чітко визначені програми, які приймають N вхідних даних та віддають M, є еквівалентними: концептуально ви можете перетворити програмне забезпечення на скінечний автомат (це те, що робить компілятор, оскільки комп'ютер і його пам'ять утворюють дуже велику скінечний автомат). Тоді, теоретично, різні форми перевірки властивостей можуть забезпечити той самий результат. Ця проблема ще складніше, ніж перевірка послідовної еквівалентності, оскільки результати двох програм можуть з'являтися в різний час; але це можливо, і дослідники працюють над цим.

Посилання