mikrocontroller.net

Forum: FPGA, VHDL & Co. VHDL code beweisen


Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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?

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

Autor: Lothar Miller (lkmiller) (Moderator) Benutzerseite
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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?

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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?

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Lothar Miller (lkmiller) (Moderator) Benutzerseite
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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 ;-)

Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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?

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
@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?

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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 ;)

Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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... :)

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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...
ersteres über citeseer zu finden.

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

Autor: Arne Z. (zachso)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Mathi (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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 ;)

Autor: zachso (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
Ach schade, aber nen versuch wars wert ;-)

Antwort schreiben

Die Angabe einer E-Mail-Adresse ist freiwillig. Wenn Sie automatisch per E-Mail über Antworten auf Ihren Beitrag informiert werden möchten, melden Sie sich bitte an.

Wichtige Regeln - erst lesen, dann posten!

  • Groß- und Kleinschreibung verwenden
  • Längeren Sourcecode nicht im Text einfügen, sondern als Dateianhang

Formatierung (mehr Informationen...)

  • [c]C-Code[/c]
  • [avrasm]AVR-Assembler-Code[/avrasm]
  • [vhdl]VHDL-Code[/vhdl]
  • [code]Code in anderen Sprachen, ASCII-Zeichnungen[/code]
  • [math]Formel in LaTeX-Syntax[/math]
  • [[Titel]] - Link zu Artikel
  • Verweis auf anderen Beitrag einfügen: Rechtsklick auf Beitragstitel,
    "Adresse kopieren", und in den Text einfügen




Bild automatisch verkleinern, falls nötig
Bitte das JPG-Format nur für Fotos und Scans verwenden!
Zeichnungen und Screenshots im PNG- oder
GIF-Format hochladen. Siehe Bildformate.
Hinweis: der ursprüngliche Beitrag ist mehr als 6 Monate alt.
Bitte hier nur auf die ursprüngliche Frage antworten,
für neue Fragen einen neuen Beitrag erstellen.

Mit dem Abschicken bestätigst du, die Nutzungsbedingungen anzuerkennen.