hallo! ich wuerde mir gerne ein wenig verfahrensweisen zur formellen verifikation von software/hardware und von VHDL im speziellen anschauen, hat da zu zufaellig jemand einen guten buchtipp? in unserer unibib hab ich leider nix gefunden, mir fehlen aber auch echt die suchbegriffe. waere euch sehr dankbar, zachso
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
> gibt es da einen weg oder muss ich mir einfach einen schaltplan malen > und dann schauen dass mein vhdl auch wirklich meinen schaltplan darstellt? Ob dein Design das macht, was du von ihm verlangst, das wird mit einer Testbench geprüft. Ob deine Testbench alle Fälle abdeckt obliegt deiner Sorgfalt. Deshalb sollte idealerweise nur die Schnittstelle definiert werden und das Design von der Person A, die Testbench aber von der Person B geschrieben werden. Aber ganz klar, es bleibt die Frage: wer kontrolliert den Kontrolleur?
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.
> Er hat von formaler Verifikation gefragt. Das schon. Ich bin mir aber gar nicht sicher, ob das auch gewollt ist. Oder nur das Stichwort "formell" irgendwo im Kleinhirn verankert ist... > Er hat von formaler Verifikation gefragt. von geredet oder nach gefragt ;-)
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/
wow! den CADP hatte ich noch nicht gefunden, vielen dank. ich werde mir das zeug mal "reinziehn" und hoffe mal ich werde das ein wenig verstehn. und danke fuer den tipp mit citeseer, aber ich hab auch nen offiziellen zugang zum springerlink :) ich wollt noch fragen wo du arbeitest, ich bewerb mich gerade fuer nen paar praktikas im FPGA development? wenn du lust hast kannste mir ja ne pm schicken, wuerde dir/euch gerne mal ne bewerbung zukommen lassen. dank fuer die viele hilfe nochmal.
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 ;)
Thread beobachten
Seitenaufteilung abschaltenBitte melde dich an um einen Beitrag zu schreiben. Anmeldung ist kostenlos und dauert nur eine Minute.
Bestehender Account
Schon ein Account bei Google/GoogleMail? Keine Anmeldung erforderlich!
Mit Google-Account einloggen
Mit Google-Account einloggen
Noch kein Account? Hier anmelden.