Azərbaycanca
Беларускі
Dansk
Deutsch
Española
Français
Indonesia
Italiana
日本語
Қазақ
Lietuvos
Nederlands
Português
Русский
සිංහල
แบบไทย
Türkçe
Українська
中國人
United State
Afrikaans
Формальна перевірка еквівалентності є частиною проектування електронних систем (англ. Electronic design automation,EDA), що широко використовується при розробці цифрових інтегральних схем, щоб формально довести, що два представлення схеми пристрою демонструють однакову поведінку.
Перевірка еквівалентності та рівні абстракції
Взагалі, існує широкий спектр можливих визначень функціональної еквівалентності, що охоплює порівняння між різними рівнями абстракції та різною деталізацією розподілення у часі.
Найпоширеніший підхід полягає в тому, щоб розглянути проблему еквівалентності автоматів, яка визначає дві синхронні характеристики проекту, функціонально еквівалентні, якщо за кожним тактовим імпульсом вони виробляють точно таку ж послідовність вихідних сигналів для будь-якої дійсної послідовності вхідних сигналів.
Розробники мікропроцесорів використовують перевірку еквівалентності для порівняння функцій, зазначених для архітектури набору команд з реалізацією рівня регістрових передач (англ. Register-transfer level,RTL), забезпечуючи, що будь-яка програма, що виконується на обох моделях, призведе до однакового оновлення вмісту основної пам'яті. Це більш загальна проблема.
Для проектування на системному рівні абстракції потрібно провести порівняння між моделлю рівня транзакції (англ. transaction level model,TLM), наприклад, написаною в SystemC та відповідній специфікації RTL. Така перевірка стає дедалі більш привабливою для розробки системи на кристалі (англ. System on a Chip, SoC).
Перевірка на еквівалентність на етапах проектування
Рівень регістрових передач цифрового чипу зазвичай описується мовою опису апаратури, таким як Verilog або VHDL. Цей опис являє собою модель золотого еталону, яка детально описує, які операції будуть виконуватись протягом якого циклу синхросигналу і якими модулями системи. Після того, як розробники, шляхом моделювання та інших методів перевірки, перевірили опис рівня регістрових передач, проект зазвичай перетворюється в список [en] за допомогою інструмента логічного синтезу. Еквівалентність не слід плутати з функціональною правильністю, яка повинна визначатися функціональною перевіркою.
Первинний [en], як правило, проходить ряд перетворень, таких як оптимізація, додавання структур [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, є еквівалентними: концептуально ви можете перетворити програмне забезпечення на скінечний автомат (це те, що робить компілятор, оскільки комп'ютер і його пам'ять утворюють дуже велику скінечний автомат). Тоді, теоретично, різні форми перевірки властивостей можуть забезпечити той самий результат. Ця проблема ще складніше, ніж перевірка послідовної еквівалентності, оскільки результати двох програм можуть з'являтися в різний час; але це можливо, і дослідники працюють над цим.
Посилання
| Ця стаття не містить . (грудень 2017) |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Formalna perevirka ekvivalentnosti ye chastinoyu proektuvannya elektronnih sistem angl Electronic design automation EDA sho shiroko vikoristovuyetsya pri rozrobci cifrovih integralnih shem shob formalno dovesti sho dva predstavlennya shemi pristroyu demonstruyut odnakovu povedinku Perevirka ekvivalentnosti ta rivni abstrakciyiVzagali isnuye shirokij spektr mozhlivih viznachen funkcionalnoyi ekvivalentnosti sho ohoplyuye porivnyannya mizh riznimi rivnyami abstrakciyi ta riznoyu detalizaciyeyu rozpodilennya u chasi Najposhirenishij pidhid polyagaye v tomu shob rozglyanuti problemu ekvivalentnosti avtomativ yaka viznachaye dvi sinhronni harakteristiki proektu funkcionalno ekvivalentni yaksho za kozhnim taktovim impulsom voni viroblyayut tochno taku zh poslidovnist vihidnih signaliv dlya bud yakoyi dijsnoyi poslidovnosti vhidnih signaliv Rozrobniki mikroprocesoriv vikoristovuyut perevirku ekvivalentnosti dlya porivnyannya funkcij zaznachenih dlya arhitekturi naboru komand z realizaciyeyu rivnya registrovih peredach angl Register transfer level RTL zabezpechuyuchi sho bud yaka programa sho vikonuyetsya na oboh modelyah prizvede do odnakovogo onovlennya vmistu osnovnoyi pam yati Ce bilsh zagalna problema Dlya proektuvannya na sistemnomu rivni abstrakciyi potribno provesti porivnyannya mizh modellyu rivnya tranzakciyi angl transaction level model TLM napriklad napisanoyu v SystemC ta vidpovidnij specifikaciyi RTL Taka perevirka staye dedali bilsh privablivoyu dlya rozrobki sistemi na kristali angl System on a Chip SoC Perevirka na ekvivalentnist na etapah proektuvannyaRiven registrovih peredach cifrovogo chipu zazvichaj opisuyetsya movoyu opisu aparaturi takim yak Verilog abo VHDL Cej opis yavlyaye soboyu model zolotogo etalonu yaka detalno opisuye yaki operaciyi budut vikonuvatis protyagom yakogo ciklu sinhrosignalu i yakimi modulyami sistemi Pislya togo yak rozrobniki shlyahom modelyuvannya ta inshih metodiv perevirki perevirili opis rivnya registrovih peredach proekt zazvichaj peretvoryuyetsya v spisok en za dopomogoyu instrumenta logichnogo sintezu Ekvivalentnist ne slid plutati z funkcionalnoyu pravilnistyu yaka povinna viznachatisya funkcionalnoyu perevirkoyu Pervinnij en yak pravilo prohodit ryad peretvoren takih yak optimizaciya dodavannya struktur en DFT tosho persh nizh vikoristovuvati jogo yak osnovu dlya rozmishennya logichnih elementiv na fizichnomu nosiyi Suchasne programne zabezpechennya dlya fizichnogo proektuvannya inodi takozh mozhe zrobit suttyevi zmini napriklad zamina logichnih elementiv na ekvivalentni analogichni elementi sho mayut bilshij abo menshij opir dzherela i ta abo bilshu chi menshu ploshinu do en Protyagom kozhnogo kroku duzhe skladnoyi bagatoetapnoyi proceduri pochatkova funkcionalnist ta povedinka opisana v pochatkovomu kodi maye buti zberezhena Pislya ciyeyi proceduri en mozhe zaznati deyakih zmin yak za dopomogoyu EDA program tak i ruchnogo vtruchannya Teoretichno instrument logichnogo sintezu garantuye sho pershij en logichno ekvivalentnij pochatkovomu kodu RTL Vsi programi sho piznishe vnosyat zmini v en teoretichno garantuyut sho ci zmini logichno ekvivalentni poperednij versiyi Na praktici programi mistyat bagi i vvazhati sho vsi kroki vid RTL do kincevogo en vikonani bez pomilok Takozh u realnomu zhitti rozrobnikam chasto dovoditsya robiti ruchni zmini do en takim chinom vprovadzhuyuchi velikij dodatkovij koeficiyent pomilok Tomu zamist togo shob slipo vvazhati sho pomilok ne bulo zrobleno neobhidna stadiya verifikaciyi dlya perevirki logichnoyi ekvivalentnosti ostatochnoyi versiyi en do originalnogo opisu dizajnu model zolotogo etalonu Istorichno odin iz sposobiv perevirki ekvivalentnosti polyagav u povtornij simulyaciyi vikoristovuyuchi ostatochnij en ta testove pokrittya rozroblene dlya perevirki pravilnosti RTL Cej proces nazivayetsya logichnim modelyuvannyam rivnya logichnih primitiviv Prote problema polyagaye v tomu sho yakist perevirki zalezhit vid yakosti testovogo pokrittya Krim togo simulyaciya rivnya logichnih primitiviv duzhe povilna sho ye osnovnoyu problemoyu oskilki rozmir cifrovih proektiv prodovzhuye zrostati eksponencialno Alternativnij sposib virishennya ciyeyi problemi formalno dovesti sho RTL kod ta sintezovanij z nogo en mayut odnakovu povedinku u vsih vidpovidnih testah Cej proces nazivayetsya formalnoyu perevirkoyu ekvivalentnosti i ce problema yaka vivchayetsya v bilsh shirokij oblasti formalnoyi perevirki Formalnu perevirku ekvivalentnosti mozhna vikonuvati mizh bud yakimi dvoma predstavlennyami proektu RTL lt gt netlist netlist lt gt netlist abo RTL lt gt RTL hocha ostannye zustrichayetsya dovoli ridko porivnyano z pershimi dvoma Yak pravilo instrument perevirki formalnoyi ekvivalentnosti takozh z velikoyu tochnistyu vkazuye u chomu polyagaye riznicya mizh dvoma predstavlennyami MetodiIsnuye dvi osnovni tehnologiyi sho vikoristovuyutsya dlya logichnogo obgruntuvannya u programah perevirki ekvivalentnosti Binarni diagrami rishen abo BDR specializovana struktura danih priznachena dlya pidtrimki argumentaciyi bulevih funkcij BDR stali nadzvichajno populyarnimi cherez yih efektivnist ta universalnist Zdijsnennist kon yunktivnoyi normalnoyi formi Cya zadacha vidpovidaye na pitannya chi mozhna priznachiti usim zminnim sho zustrichayutsya u formuli znachennya hibnist i istina tak shob formula stala istinnoyu Komercijni programi dlya ekvivalentnoyi perevirkiFormalPro vid Mentor Graphics Questa SLEC vid Mentor Graphics Conformal vid Cadence JasperGold vid Cadence Formality vid Synopsys 360 EC vid OneSpin SolutionsVisnovkiPerevirka ekvivalentnosti vidnovlenih shem inodi korisno peremishati logiku z odniyeyi storoni reyestru do inshogo sho uskladnyuye perevirku Perevirka poslidovnoyi ekvivalentnosti Inodi dva avtomata na kombinacijnomu rivni absolyutno rizni odnak voni povinni davati odnakovi rezultati yaksho voni mayut odnakovi danni na vhodi Klasichnim prikladom ye dvi identichnih skinechnih avtomati z riznimi koduvannyami dlya staniv Oskilki ce ne mozhna zvesti do kombinacijnoyi problemi potribni bilsh zagalni metodi Ekvivalentnist programnogo zabezpechennya tobto perevirka togo chi dvi chitko viznacheni programi yaki prijmayut N vhidnih danih ta viddayut M ye ekvivalentnimi konceptualno vi mozhete peretvoriti programne zabezpechennya na skinechnij avtomat ce te sho robit kompilyator oskilki komp yuter i jogo pam yat utvoryuyut duzhe veliku skinechnij avtomat Todi teoretichno rizni formi perevirki vlastivostej mozhut zabezpechiti toj samij rezultat Cya problema she skladnishe nizh perevirka poslidovnoyi ekvivalentnosti oskilki rezultati dvoh program mozhut z yavlyatisya v riznij chas ale ce mozhlivo i doslidniki pracyuyut nad cim PosilannyaCya stattya ne mistit posilan na dzherela Vi mozhete dopomogti polipshiti cyu stattyu dodavshi posilannya na nadijni avtoritetni dzherela Material bez dzherel mozhe buti piddano sumnivu ta vilucheno gruden 2017