Aceasta este dovada comenzii care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
dovada - Dovada formala intre doua descrieri comportamentale
REZUMAT
dovadă [-a] [-d] file1 file2
DESCRIERE
Realizat pentru a rula pe o descriere a fluxului de date, dovadă acceptă același subset de VHDL ca și asimut
și boom și boog (pentru informații suplimentare despre acest subset, vă rugăm să sunați la VHDL
manual). dovadă utilizează o reprezentare Reduced Ordered Binary Decision Diagrams care permite
proiectantul să demonstreze cu ușurință echivalența funcțională dintre două comportamentale
descrieri. dovadă este utilizat în general pentru a compara o specificație comportamentală
cu un comportament extras obţinut de yagle.
În modul implicit, se face o fază de colaps pe descriere prin eliminarea tuturor
semnalele auxiliare (BDD-ul ieșirilor, registrelor și magistralelor sunt descrise din
intrările sau registrele). Cele două descrieri trebuie să conțină aceleași resurse
(semnale se înregistrează cu același nume). Este posibil să utilizați .inf fișier în yagle (A se vedea
remarcă suplimentară despre YAGLE în acest document) să redenumească registrele din extras
descriere comportamentală (vezi om yagle). Datele și comenzile (pazat
expresii) trebuie să se potrivească separat. Autobuzele corespunzătoare logice complet specificate
funcțiile sunt reprezentate de un multiplexor logic în ambele descrieri. Cei doi
descrierile trebuie să aibă aceeași interfață (entitate VHDL), dacă nu, cea formală dovadă
este oprit.
dovadă folosește doar două variabile de mediu de sistem legate de directorul de lucru.
MEDIUL VARIABILE
MBK_WORK_LIB dă calea descrierilor comportamentale. Valoarea implicită este
directorul curent.
MBK_CATA_LIB oferă câteva căi auxiliare pentru descrierile comportamentale. Implicit
valoare este directorul curent.
OPŢIUNI
Opțiunile pot fi date în orice ordine înaintea numelor fișierelor.
-a Această opțiune întreabă dovadă pentru a păstra semnalele auxiliare comune. dovadă păstrează tot
semnale intermediare care au același nume în ambele descrieri (Un semnal comun
este considerată o intrare și o ieșire a fiecărei descrieri). Această opțiune poate fi
util pentru descrieri care conțin ecuații mari. Poate fi folosit când dovadă are
a eșuat sau dacă doriți să depanați în modul pas cu pas cele două descrieri diferite.
-d Programul afișează erori atunci când descrierile comportamentale sunt diferite. Ecuații
sunt afișate atunci când este posibil.
EXEMPLU
dovada -a -d sumator1 sumator2
YAGLE
YAGLE (abstracția funcțională) este acum distribuit comercial de Avertec
(http://www.avertec.com/). Mai multe informații pot fi obținute pe site-ul lor web. Binare
Acest instrument poate fi descărcat și pentru cercetarea universitară necomercială.
Folosiți dovezi online folosind serviciile onworks.net
