VHDL code beweisen

Thomas Kropf: Introduction to Formal Hardware Verification; Springer 
1998
ISBN: 3-540-65445-3

Beschreibt die formalen Grundlagen und Algorithmen für die formale 
Hardware Verifikation

Danke sehr, werde ich mir mal besorgen. ich habe aber gehoert es wurde 
bei VHDL2004 noch einiges in der richtung zur verifikation ergaenzt, ist 
das so richtig? und braucht man dann evtl. noch ein neueres werk?

Ich glaube du hast eine falsche Vorstellung von formaler Verifikation.
Formale Verifikation sind mathematische Beweise ob zwei Schaltungen 
äquivalent sind (equivalence checking) bzw. ob eine Schaltung bestimmte 
Eigenschaften besitzt (model checking). Und beides ist vollkommen 
unabhängig von der Representation der Schaltung. D.h. prinzipiell ist es 
egal ob Du in einen Equivalence-Checker VHDL, Verilog, Spice-Netzliste 
ne Cadence Datenbank oder sonst was rein wirfst.
In VHDL gibt es keine Konstrukte die für die formale Verifikation 
bestimmt sind. Deshalb wirst Du auch kein Buch finden das beschreibt wie 
Du "formale Verifikation mit VHDL" durchführst. Dafür ist VHDL auch 
nicht gedacht.

Okay, dann mal andersherum: ich moechte gerne beweisen dass mein code 
"richtig" arbeitet. wir haben sowas schonmal in java in der uni gemacht, 
und ich dachte(!) sowas gibts auch fuer vhdl? ich weiss leider wirklich 
nicht mehr viel davon, damals habe ich das nich wirklich gemocht aber 
jetzt find ichs doch recht spannend und wuerde das gerne mit meinem 
VHDL-zeuch machen. gibt es da einen weg oder muss ich mir einfach einen 
schaltplan malen und dann schauen dass mein vhdl auch wirklich meinen 
schaltplan darstellt?

ciao
zachso

Per Hand wird das wohl nix werden. Zunächst musst Du unterscheiden ob Du 
einen Equivalence Check oder einen Model Check machen willst.
Für einen EC brauchst Du ein Referenz Modell Deines VHDL-Codes. Diese 
werden dann auf Isomorphie getestet. Für ein "echtes" VHDL-Modul wirst 
Du das nie per Hand hinbekommen. Da brauchst Du Tools für. Die gibt es 
auf dem Markt ab etwa 100000$ zu kaufen.
Fürs Model Checking musst Du ein temporales Modell spezifizieren und das 
wird dann mit Deinem VHDL-Modul "verglichen". Auch das ist kaum per Hand 
möglich. Aber auch dafür gibt es fertige Tools zu kaufen bzw. auch 
kostenfrei im Netz. Allerdings nehmen die kein VHDL als Eingabe.
Eigentlich bleibt da nur das selber implementieren, wenn man nicht das 
Geld in die Hand nehmen kann/will.

Ihr habt Java in der Uni selber verifiziert? Oder habt ihr ein Tool 
dafür benutzt?

Lothar Miller schrieb:
> Ob dein Design das macht, was du von ihm verlangst, das wird mit einer
> Testbench geprüft.

Er hat von formaler *Verifikation* gefragt. Und da ist nix mit 
Testbench.

in der uni haben wir in java selber verifiziert, obwohl ich mir auch 
nicht mehr sicher bin ob das wirklich verifikation war, ich muss da mit 
den fachbegriffen nochmal nachschlagen glaube ich. auf jeden fall haben 
wir java code geschrieben und dann geguckt ob er terminiert und welcher 
aufwand (zuerst) und dann spaeter auch wirklich bewiesen dass er macht 
was er machen soll. leider habe ich da so wirklich 0 aufgepasst (wie 
studenten halt so sind... ;)) und mit dementsprechend auch nicht viel 
gemerkt.
die sache mit der testbench abe ich schonmal gehoert, die benutze ich 
immer (wie soll man sonst auch fehler finden?) und das klappt auch ganz 
gut, nur schrieb ich die immer selber, da ich einfach nur allein 
arbeite, ist halt alles nur hobby.
dass solche beweise sehr schwer zu erbringen sind und dafuer tool noetig 
werden war mir schon klar, nur ich wuerde es (in gaaanz kleinem 
massstab) gerne erstmal per hand koennen um ueberhaupt erstmal zu wissen 
wie es geht. eine wirkliche anwendung dafuer gibts bei mir (noch) nicht 
und das wird sich wohl so bald auch nicht aendern, mich ahben einfach 
die moeglichkeiten interssiert, mehr als nen multiplexer wuerde ich wohl 
nicht verifiziern wollen.
gibts denn zu Model checking und equivalence check literatur ausser das 
bisschen auf der wikipedia? zum model check habe ich den CV gefunden und 
auf springerlink gleich nen buch dazu, das sieht schonmal 
vielversprechend aus, dank der uni habe ich ja zugang zum springerlink.
bei dem equivakence check allerdings scheints nur teure software zu 
geben (btw: stehen die 100.000$ fuer eine FormalPro-Lizenz oder is das 
zeuch noch teurer?)
wie gesagt: ist halt alles just for fun, habe also keinen dicken 
gledbeutel und kann mir absolut keien software kaufen.

danke schonmal,
zachso

ps: mathi arbeitest du in dem gebiet bzw. machst du sowas beruflich oder 
warum kennste dich damit so gut aus?

@Zachso:
Ja, ich arbeite in dem Bereich. Ich versuche es anderen bei zubringen ;)
Was Du mit Java gemacht hast, hat nicht viel mit der formalen 
Verifikation zutun. Es hört sich eher so an <vermutung>, als ob ihr euch 
im Rahmen Komplexität damit beschäftigt habt </vermutung>.
Selbst ein sehr kleines Design per Hand wird es sehr schwer werden. Was 
genau hast Du vor per Hand zu verifizieren?

zachso schrieb:
> btw: stehen die 100.000$ fuer eine FormalPro-Lizenz oder is das
> zeuch noch teurer?


Das ist ne Hausnummer von einer der drei großen EDA-Herstellern. Aber 
nicht von Mentor. Das wird aber sicherlich auch in dem Bereich liegen ;)

wie ich oben schon schrieb, ich habe vor damit vllt. mal nen multiplexer 
zu verifiziern, nicht mehr. ich moechts mir just for fun angucken und 
werde mit evtl. uebungsbeispielen schon genug zu tun haben denke ich ;)
ja, komplexitaet haben wir auch gemacht, aber das war nicht so schwer 
als dass ich da abgeschalten haette, das wirkliche beweisen haben wir 
auf jeden fall auch gemacht, ich weiss nur nicht ob wirs verifikation 
genannt haben. komplexitaet haben wir bis zum erbrechen gemacht, das 
geht jetzt ganz gut.
was wir da bewiesen haben war aber auch nicht lang, das waren nur kurzes 
beispiel in einer VL und dann nochmal einen 6-zeiler in tutorium, da 
blieb halt nicht viel uebrig.

Ich werde mir mal aus der Bib "Modellbildung und Verifikation von 
komplexen digitalen Schaltungen in einem Designflow basierend auf VHDL 
und Synthese" besorgen und dann ein wenig lesen. ich danke dir schonmal 
fuer deine hilfe, nur eine frage bleibt da noch: sind dir noch andere 
tools bekannt ausser die kommerziellen? nur falls mich das thema doch 
packen sollte... :)

Zum Model-Checking gibt es sehr viele freie Softwarepakete (s. eng. 
wikipedia Artikel zu model checking), jedoch kaum mit Bezug zu 
Hardwarebeschreibungssprachen. Lediglich eins habe ich bisher gefunden, 
allerdings noch nicht selber getestet: http://www.cs.cmu.edu/~cmuvhdl/
Zu diesem Model-checker gibt es auch ein Paper aus dem Springer-Verlag: 
http://www.springerlink.com/content/15ra8t8863cwxrgf/
oder vom ieee:
http://ieeexplore.ieee.org/Xplore/login.jsp?reload=true&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel4%2F5815%2F15504%2F00715418.pdf%3Farnumber%3D715418&authDecision=-203
ersteres über citeseer zu finden.

Zum Equivalence Checking habe ich bisher kaum Tools gefunden. Eigentlich 
nur: http://www.inrialpes.fr/vasy/cadp/

Hi Arne,
mit dem Praktika wird das bei mir nix. Denn nach meiner Zeit in der 
Industrie bin ich wieder an der Uni gelandet. Deswegen darf ich auch 
formale Verifikationsmethoden unterrichten ;)

Ach schade, aber nen versuch wars wert ;-)