Hallo, mich würde interessieren, ob jemand Erfahrungen hat, wie man als Privatmann etwas mit fomaler Verifikation (SVA etc.) spielen kann. Auf Arbeit hat unser Verifikationsteam ein Design von mir neulich formal verifiziert und ich muss sagen, dass das schon cool war. Leider habe ich auf Arbeit gerade keine Zeit mich da einzuarbeiten bzw damit herumzuspielen. Gibt es für den Privatmann im FPGA Umfeld eine Möglichkeit damit etwas herumzuspielen? Vermutlich wird der Wunsch VHDL Design + SystemVerilog Assertions utopisch sein, da kaum ein opensource Tool beide Sprachen gleichzeitig versteht. Aber vielleicht gibt es ja was für "nur" Verilog? Ansonsten muss ich damit wohl warten, bis ich auf der Arbeit wieder etwas Zeit dafür habe und die Lizenzen frei sind :)
:
Bearbeitet durch User
https://en.wikipedia.org/wiki/Formal_verification Leider ist unter den 21 Sprachen kein deutscher Artikel. Wir müssen also dumm bleiben. Oder uns mit den drei Zeilen in simplifiziertem Englisch begnügen. Oder die KI befragen (kleiner Scherz).
Warum tut man hier so als bedeute "Privatmann" "kein Geld ausgeben wollen" ?! * https://osvvm.org/ * http://ghdl.free.fr/ > Leider ist unter den 21 Sprachen kein deutscher Artikel. Wir müssen also > dumm bleiben. Oder auf die gedruckten Artikel zu den Thema zurückgreifen wie bspw.: * https://www.amazon.de/Handbuch-Electronic-Design-Automation-Jansen/dp/3446212884 * https://www.all-electronics.de/wp-content/uploads/migrated/article-pdf/70698/f8672272ab1.pdf
:
Bearbeitet durch User
Klingt brandaktuell, 2001 und 2004. Und da klickt man einfach auf "solve" und schon hat man ein fertiges verifiziertes Programm (oder FPGA)?
Bradward B. schrieb: > Warum tut man hier so als bedeute "Privatmann" "kein Geld ausgeben > wollen" ?! Leider bedeutet Geld ausgeben in der EDA Welt gleich sehr sehr viel Geld ausgeben. Mehr als mancher von uns im Jahr überhaupt verdient. Ich bastel zu Hause gern mal was auf dem FPGA. Aber wenn ich das mit dem Tooling bei der Arbeit vergleiche ist das leider eine andere Hausnummer. GHDL, NVC und verilator sind zwar cool, aber verglichen mit Xcelium schon ziemliche Krücken. Bradward B. schrieb: > * https://osvvm.org/ > * http://ghdl.free.fr/ Sind leider "klassische" Simulatoren / UVM Methodiken. Ich interessiere mich für was formales. So wie es bspw mit Cadence Jasper oder Siemens Onespin möglich ist. Gibt es irgendwas, was zugänglich ist, wo man mit Systemverilog properties etc bisschen formal herumspelen kann?
Leider bedeutet Geld ausgeben in der EDA Welt gleich sehr sehr viel Geld ausgeben. Mehr als mancher von uns im Jahr überhaupt verdient. Wiedermal ein Vorurteil das auch noch sehr schwammig formuliert ist, warum schreibt man da nicht, das man höchstens xyz €/a für ne Lizenz ausgeben will? Und vielleicht mal einen Blick auf die "Educational Lizenzen(Studenten)" (wie es sie für simulink ab und zu gibt) wirft? Und oft gibt es Evallizenzen für ein paar Wochen/Durchläufe - hatte da mal von Siemens was für PCN-Layout-Check Wichtig wäre auch zu wissen, welche Wunder man nun mal konkret von der "formalen Verifikation" per Softwareautomat erwartet. Da wird einem oft viel versprochen, insbesonders hinsichtlich Vollständigkeit, was sich dann im nachhinein doch als unerreichbar herausstellt oder nebenher verfrühstückt wurde. Und trotz formaler Verifikation muss man in einer späteren Entwicklungsphase durch die Tests in der Klima-kammer. Also muss man doch Testcases und stimuli dafür erstellen, was man sich eigentlich dank der Möglichkeit der formalenb verifikation spären wollte. Beispiel, was mir in Erinnerung blieb, ist die FSM - Analyse, Weil das ein Graph ist, kann man da mit mathematischen methoden formal verifizieren, ob es bspw. nicht erreichbare States gibt oder states ohne Abgänge. Aber das hat man ohnehin im Blick und was nutz einem der Haken vpn Verifikationstool, wenn die Toolchain "weiter hinten" wieder "Murks" baut. Bspw. die Staemachine durch (platzspärendes) binary encoding zu einer Schaltung mit "Sackgassen" Zuständen überführt. Und in der Risikoanalyse steht, das man auch zufällig kippende FF (SEU) zu betrachten hat, aber nur für DAL-A relevante Blöcke... die dann redunt auszulegen ist. (aber kein Verifikationstool sagt dir wo DAL-A oder DAL-E gilt, das muss schon das Projekt-managment, system-Architekt vorgeben. Aber vielleicht hat sich ja in den letzten Jahren was für die Praxis relevantes ergeben, was man vielleicht mal evaluieren sollte? Was hat nun den TO so begeistert, welche Designfehler hat die formale Verifikation für ihn gefunden?
Ich habe mal Property Specification Language (PSL) ausprobiert. Das ging alles mit Open-Source-Programmen. Ich weiß nicht mehr genau wie, aber das lässt sich rausfinden. Zum Beispiel als Einstieg: https://pepijndevos.nl/2019/08/15/open-source-formal-verification-in-vhdl.html
Bradward B. schrieb: > Wiedermal ein Vorurteil das auch noch sehr schwammig formuliert ist, > warum schreibt man da nicht, das man höchstens xyz €/a für ne Lizenz > ausgeben will? Grundsätzlich möchte ich als Privatperson zum spielen da erstmal gar kein Geld für ausgeben. Ich hatte mal bei einem Hersteller angefragt, ob es eine Möglichkeit gibt sein Tool als Privatmann weiterzuverwenden nach der Uni. Mir wurde daraufhin ein Schnäppchen angeboten: Single User Lizenz ohne Updates für einmalig 165.000€. Das war mir dann doch ein wenig zu teuer für meinen Hobbykeller. Bradward B. schrieb: > Wichtig wäre auch zu wissen, welche Wunder man nun mal konkret von der > "formalen Verifikation" per Softwareautomat erwartet. Ich erwarte gar keine Wunder. Muss ich zu Hause zum Glück ja auch nicht. Ich würde einfach mal gerne mit Systemverilog Assertions herumspielen und brauche somit ein Tool, was die zumindest rudimentär supported. Bradward B. schrieb: > Da wird einem oft viel versprochen, insbesonders hinsichtlich > Vollständigkeit, was sich dann im nachhinein doch als unerreichbar > herausstellt oder nebenher verfrühstückt wurde. > Und trotz formaler Verifikation muss man in einer späteren > Entwicklungsphase durch die Tests in der Klima-kammer. Das sind zumindest bei uns auf Arbeit sowieso mehrere Paar Stiefel. Wir nutzen beruflich wie gesagt Siemens Onespin für formale Modulverifikation, die eben nur das Ziel hat das RTL auf Fehlerfreiheit zu prüfen. Dass das RTL dann so auch real geht ist ne andere Baustelle. Erst recht, wenn man Silizium selbst baut. https://eda.sw.siemens.com/en-US/ic/questa-one/formal-verification/ Als Designer setzen wir selbst die von dir beschriebenen FSM checks etc. auf. Das sind aber für uns nur "Sanity Checks", die schnell laufen und verhindern, dass man was komplett Vermurkstes an die Verifikation weiterleitet. Da macht onespin so grundlegende Sachen, wie stick-Checks, ob alles toggeln kann, oder jeder FSM state irgendwie erreichbar ist und irgendwelche Counter nicht überlaufen. Konkret finde ich aber tatsächliche formale Methoden, die auf tatsächliche Spezifikation prüfen total cool. Klar hat man das Problem, dass sich der Solver auch mal komplett verirren kann, wenn man 20 32-bit Zähler im Design hat oder so. Wenn das aber gut formuliert ist und er dann am ende "Property Holds" sagt, kann man sich sicher sein, dass das Design eben bezogen auf die Property, die man definiert hat unter allen Umständen funktioniert. So simple Sachen wie das hier:
1 | property my_prop; |
2 | @(posedge clk) disable iff (!rst_n) |
3 | my_input |-> ##[1:5] my_output; |
4 | endproperty |
5 | |
6 | assert property (my_prop); |
finde ich schon ganz cool, dass man einfach definieren kann, dass bspw wenn my_input true is0t, innerhalb von einem bis fünf Zyklen der Output gesetzt sein muss (nur ein dummes Beispiel). wenn der Solver sagt, dass das passt, ist eben formal sichergestellt, dass das auch so genau ist und es keinen komischen edge case gibt in dem das dann eben nicht so ist. Weitere Beispile für assertions, die von der Form her so sind: https://www.systemverilog.io/verification/sva-basics/#assertion-examples Wir haben bspw. einen RISC-V Kern inklusive FPU vollständig formal verifiziert. Es gibt parallel dazu noch eine UVM testbench. Die hat aber nie alle edge cases gefunden, trotz zehntausender Seeds. Habe gesehen, dass wohl Yosys support für SVA hat: https://yosyshq.readthedocs.io/projects/sby/en/latest/ Damit werde ich mich mal beschäftigen. Wie gesagt, ich verfolge damit primär erstmal das Ziel mich persönlcih mit diesen Assertions vertraut zu machen und mit der Sprache etwas herumzuspielen, um ein Gefühl dafür zu bekommen.
:
Bearbeitet durch User
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.