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
> Ich habe mal Property Specification Language (PSL) ausprobiert. ... > Zum Beispiel als Einstieg: > https://pepijndevos.nl/2019/08/15/open-source-formal-verification-in-vhdl.html Interessanter Hinweis, ich hab gestern das Beispiel kurz angeschaut werd aber mal noch etwas länger brauchen. Auf den ersten Blick scheint das Ganze Probleme zu finden, deren Auftritt man auch durch Befolgung eines code style vermeiden kann. Konkret nichtkonforme sensitive list (zuviele oder zuwenig signale darin) und Nichtbeachtung des Verhaltens unmittelbar nach reset (insbesonders weil an dieser Stelle sich Synthese ergebnis und Simulation abhängig von der Verwendeten FPGA/ASIC-Technologie unterscheiden.
1 | process(opcode, a, b, ci) |
2 | begin
|
3 | case opcode is |
4 | when "000" => -- add |
5 | y <= a xor b xor ci; -- output |
6 | co <= (a and b) or (a and ci) or (b and ci); -- carry |
7 | cr <= '0'; -- carry reset value |
8 | -- [...]
|
9 | end case; |
10 | end process; |
11 | |
12 | process(clk, rst_n) |
13 | begin
|
14 | if(rising_edge(clk)) then |
15 | if(rst_n = '0') then |
16 | ci <= cr; -- reset the carry |
17 | else
|
18 | ci <= co; -- copy carry out to carry in |
19 | end if; |
20 | end if; |
21 | end process; |
Beispiel aus dem link bzgl. PSL . Das sehe ich ale eine Hauptschwierigkeit bei der Ausbildung von FPGA-Designern, denen beizubringen, das man nicht alle (syntaktischen) Freiheiten im Code nutzt, sondern stur erwiesenermassen "sichere templates" benutzt. Und zuweilen hat sich ein blindes Vertrauen an "Tests" entwickelt, so dass man immer wieder daran erinnern muss, das nur die Anwesenheit von "Fehlern" durch Tests ermitteln kann aber nicht die generelle Abwesenheit der "Fehler". (Dijkstra: "Program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence." https://de.wikiquote.org/wiki/Edsger_Wybe_Dijkstra ) Und das man Sicherheit nicht in ein System "hinein testen" kann.
:
Bearbeitet durch User
Bradward B. schrieb: > Auf den ersten Blick scheint das Ganze Probleme zu finden, deren > Auftritt man auch durch Befolgung eines code style vermeiden kann. Auch. Aber noch mehr. Der Link war gedacht für den Einstieg und das Installieren der benötigten Programme. Unter https://zipcpu.com/ gibt es einige praktische Beispiele. Bradward B. schrieb: > Und zuweilen hat sich ein blindes Vertrauen an "Tests" entwickelt, so > dass man immer wieder daran erinnern muss, das nur die Anwesenheit von > "Fehlern" durch Tests ermitteln kann aber nicht die generelle > Abwesenheit der "Fehler". Formale Verifikation ist ja nicht direkt ein Test. Und theoretisch kann man damit die Abwesenheit von Fehlern nachweisen, wenn die Annahmen richtig gesetzt sind. Zum Beispiel kann vorgegeben werden, dass ein Wert niemals einen Grenzwert überschreiten darf. Mit der formalen Verifikation kann (theoretisch) mit Sicherheit nachgewiesen werden, dass das mit dem Code niemals passieren kann. Das setzt natürlich wieder richtige Annahmen (assume und assert) voraus, die auch wieder Fehler haben können. Es ist also natürlich nicht hundertprozentig sicher. Aber man schreibt den eigentlichen Code möglichst fehlerfrei und unabhängig vom Code die Annahmen für die Verifikation. Da sind die Chancen höher, dass ein logischer Fehler nicht in beidem Auftritt und somit gefunden wird.
> Bradward B. schrieb: >> Und zuweilen hat sich ein blindes Vertrauen an "Tests" entwickelt, so >> dass man immer wieder daran erinnern muss, das nur die Anwesenheit von >> "Fehlern" durch Tests ermitteln kann aber nicht die generelle >> Abwesenheit der "Fehler". > Formale Verifikation ist ja nicht direkt ein Test. Und theoretisch kann > man damit die Abwesenheit von Fehlern nachweisen, wenn die Annahmen > richtig gesetzt sind. Naja Theorie und Praxis und nein im Gegenteil es ist bspw. durch den Mathematiker Kurt Gödel vor fast 100 Jahren bewiesen wurden, das es Bereiche in der Theorie gibt, in der man eben nicht beweisen kann, ob jede Aussage widerspruchsfrei richtig oder falsch ist. https://de.wikipedia.org/wiki/G%C3%B6delscher_Unvollst%C3%A4ndigkeitssatz > Zum Beispiel kann vorgegeben werden, dass ein Wert niemals einen > Grenzwert überschreiten darf. Mit der formalen Verifikation kann > (theoretisch) mit Sicherheit nachgewiesen werden, dass das mit dem Code > niemals passieren kann. Naja im binären kann man ohnehin nie den oberen ('1') oder unteren ('0') Grenzwert überschreiten... SCNR Bei Integer bietet VHDL die Möäglichkeit des range und der simulator meldet auch wenn dieser Bereich verlassen wird. Das Problem mit der angeblichen vollständigen Beweis in der Logik ist, das Anzahl der Zustände und deren Übergange zu hoch sind als das man sie alle abprüfen kann.
M. N. schrieb: > Ich bastel zu Hause gern mal was auf dem FPGA. Was bastelst Du denn so sauschnelles, würde mich mal interessieren. Mir ist bisher nicht wirklich was eingefallen für den Hobbybereich, was einen FPGA auch ausnutzen könnte.
Peter D. schrieb: > M. N. schrieb: >> Ich bastel zu Hause gern mal was auf dem FPGA. > > Was bastelst Du denn so sauschnelles, würde mich mal interessieren. > Mir ist bisher nicht wirklich was eingefallen für den Hobbybereich, was > einen FPGA auch ausnutzen könnte. Tatsächlich ist das häufig ein Problem. Zum einen mache ich tatsächlich einfach mal Sachen des Spieltriebs wegen. Sprich ich schaue mir mal opensource Risc V Kerne an, oder so. Konkrete Projekte mit FPGA: - Galvanisch getrennter Analogübertrager: ADC -> Lattice FPGA -> Ethernet PHy -> Ethernat Kabel -> Phy -> FPGA -> DAC Hab mal was gebraucht, was aus einem total elektrisch verseuchten Schaltschrank ein Analogsignal 0-10 V irgendwie rausführt. Habe also einen kleinen lattice XO2 mit so nem Ethernet Phy Board von adafruit verbastelt und übertrage roh ADC Werte über diesen Ethernet Link (Kein echtes Ethernet. Nur die Präambel + FCS sind richtig). War tatsächlich eine der billigsten Lösungen das galvanisch getrennt und robust rauszubekommen. Gesamtaufwand für's Design: 2 Tage mal zwischen den Jahren - Ein bekannter wollte aus einer Anlagensteurung ein Signal herausbekommen, um in seiner Werkstatt eine Warnlampe leuchten zu lassen, wenn ein Fehler auftritt. Problem war, man kam programatisch da nirgends ran, weil das alles ein geschlossenes kommerzielles System war. Einziger Weg ist der Grafische VGA Ausgang der Bedienobefläche, wo irgendwo eine Anzeige von grün auf rot springt. Lösung: XO2 mit VGA input, der in dem Videosignal schaut, ob in einem Bereich was von grün auf rot geht. Ziemlich dumm, funktioniert aber :) Der analoge VGA Input wurde mit den LVDS input Buffern des FPGAs gelöst, die als simpler 1 bit AD Wandler irgendwie auf die Mitte des Bereichs geschaut haben. Für die erkennung, ob das eher rot oder eher grün ist hat's gereicht :) Ich hatte mal mit Kommilitonen zu Uni Zeiten einen 8x8x8 RGB LED-Würfel gebaut. Habe mir dann irgendwann selber nochmal einen gebaut und da ist auch ein FPGA mit Picorv32 drin. Auch unnötig. Aber es hatte irgendwie was, diese ganze LED Matrix Ansteuerung in Hardware zu gießen und einen eigenen "Displaycontroller" mit double buffering zu basteln. Wäre auch mit einem normalen uC gegangen. - Auch auf Basis von einem kleinen XO2: Ein Multichannel WS2812 Controller. Mir ging am uC die Performance / Peripherie aus, um viele WS2812 zu bespaßen, weil das mit dem timing ja bisschen ungeschickt ist. Und wenn man nicht genug SPIs hat, um die zu misbrauchen, wird's irgendwann eng. Habe dann einfach einem XO2 Ein 20 MHz Quad SPI -> 8 channel WS2812 gebaut. Auch so ein kalte Tage Winterprojekt an nem Nachmittag. Ein ehemaliger Kommilitone von mir hat mal vor einigen Jahren so ein kleines Devboard mit nem XO2 deignt: https://www.pcbway.com/project/shareproject/Tiny_XO2_FPGA_Development_Board_for_Lattice_MachXO2.html davon fahren bei mir einige rum. da kann man dann schon häufige mal kleinere Glue-logic Aufgaben auslagern, wegen des praktischen Formfaktors.
:
Bearbeitet durch User
Bradward B. schrieb: > Bei Integer bietet VHDL die Möäglichkeit des range und der simulator > meldet auch wenn dieser Bereich verlassen wird. Das ist genau das Problem: Mann muss erstens VHDL schreiben (das machen die ASIC Leute leider ungern :)) und zweitens muss man den Fall in der Simulation auch treffen. Bradward B. schrieb: > Das Problem mit der angeblichen vollständigen Beweis in der Logik ist, > das Anzahl der Zustände und deren Übergange zu hoch sind als das man sie > alle abprüfen kann. Ja. Ist schwierig. Ne volle CPU kann man da nicht als Blackbox gegenwerfen. Aber wenn man die zerschlägt und die Schnittstellen gut definiert, können die einzeln gut verifiziert werden. Wir machen jetzt selbst auch selten ne CPU, aber ich habe Kollegen, die bei IBM, Intel und AMD waren und die sagen auch, dass da eigentlich fast alles formal gemacht wurde. IBM hat glaube ich sogar eigene formale Solver. Der krasse Vorteil ist häufig nicht der Beweis, dass dass alles gut ist, das kann durchaus mal Monate lang rechnen... Das krasse ist, dass der solver ja versucht ein Gegenbeispiel zu finden. Konkret hatten wir diesen Fall: Dem Solver ist die Schnittstelle zwischen CPU und FPU formal beschrieben worden, was da legal ist. und wie sich das zu verhalten hat. Jetzt hat der Solver tatsächlich den edge case gefunden: Eine Float-Multiplikation zweier register wird ausgeführt. Im zweiten Zyklus kommt ein Interrupt und gleichzeitig hängt in der Memory-Stufe der Pipeline ein write auf dem AXI fest, weil der bus nicht ready ist. Gab dann noch zwei andere Randbedingungen, die aber für das grobe Bild unwichtig sind. Sind diese Bedingungen gegeben, geht eine weitere Floating point operation in dem darauffolgenden Kontext schief und bekommt als zweiten Operand den gleichen operanden, den die Multiplikation n Befehle davor hatte, weil da ein pipeline register nicht korrekt gehandelt wurde. Und das ist schon beeindruckend. Das hat der Solver innerhalb von ner viertel Stunde oder so gefunden. Unsere constraint random UVM TB hat trotz hoher coverage genau diesen edge case halt nie getroffen. Im FPGA hat das auch nie jemand getroffen, weil nie alle Randbedingungen gegeben waren. Und genau deswegen finde ich das Konzept so interessant. Florian schrieb: > Aber man schreibt den eigentlichen Code > möglichst fehlerfrei und unabhängig vom Code die Annahmen für die > Verifikation. Da sind die Chancen höher, dass ein logischer Fehler nicht > in beidem Auftritt und somit gefunden wird. Ist bei uns sowieso Standard. Vier Augen Prinzip. Ich darf meinen eigenes RTL nicht selbst verifizieren und der Verifikant darf nur die Spezifikation nehmen als Guideline. Sämtliche Unklarheiten müssen dann über Interation der Spezifikation geklärt werden. Markus W. schrieb: > Bitte sehr. > > https://github.com/YosysHQ/oss-cad-suite-build Danke. Über Yosys's SVA Support bin ich dann auch noch gestolpert. Das scheint das einzige Zugängliche zu sein. Damit werde ich mal herumspielen.
:
Bearbeitet durch User
Bradward B. schrieb: > [...]im Gegenteil es ist bspw. durch den > Mathematiker Kurt Gödel vor fast 100 Jahren bewiesen wurden, das es > Bereiche in der Theorie gibt, in der man eben nicht beweisen kann, ob > jede Aussage widerspruchsfrei richtig oder falsch ist. Die Aussage ist in etwa 'Auf FPGAs kann man nicht rechnen, weil es Bereiche der Mathematik gibt, die nicht lösbar sind.' In den Verifikationssystemen, die ich kenne, werden SAT-Solver benutzt. SAT ist ein lösbares Problem (wenn auch NP-vollständig). Dafür ist es egal, ob es irgendwo noch unlösbare Probleme gibt. Bradward B. schrieb: > Bei Integer bietet VHDL die Möäglichkeit des range und der simulator > meldet auch wenn dieser Bereich verlassen wird. Ja, der Simulator. Und dann passiert es auf dem Chip trotzdem. Diese Fälle findet die formale Verifikation. Bradward B. schrieb: > Das Problem mit der angeblichen vollständigen Beweis in der Logik ist, > das Anzahl der Zustände und deren Übergange zu hoch sind als das man sie > alle abprüfen kann. Deshalb werden sie ja auch nicht abgeprüft. Die Nachkommastellen von Pi sind auch zu hoch, als dass man sie alle berechnen könnte, trotzdem ist bekannt, dass es unendlich viele gibt.
Angehängte Dateien:
-
Backcover.jpg
230 KB -
Inhalt.jpg
220 KB
> 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). Anbei Rückcover und Inhalt des IMHO besten Buch zum Thema aus meiner Handbibliothek. Nicht in deutsch, zu dem Thema gibt es IMHO es die brauchbare Literatur nur in englisch. In deutschen Fachzeitschriften wie "Elektronik Praxis" u.ä. gibt es selten mal einen Artikel zum Thema ASIC/FPGA Verifikation, die aber für meinen Geschmack zu oberflächlich sind.
> Dem Solver ist die Schnittstelle zwischen CPU und FPU formal beschrieben > worden, was da legal ist. und wie sich das zu verhalten hat. Jetzt hat > der Solver tatsächlich den edge case gefunden: Eine Float-Multiplikation > zweier register wird ausgeführt. Im zweiten Zyklus kommt ein Interrupt > und gleichzeitig hängt in der Memory-Stufe der Pipeline ein write auf > dem AXI fest, weil der bus nicht ready ist. Gab dann noch zwei andere > Randbedingungen, die aber für das grobe Bild unwichtig sind. Sind diese > Bedingungen gegeben, geht eine weitere Floating point operation in dem > darauffolgenden Kontext schief und bekommt als zweiten Operand den > gleichen operanden, den die Multiplikation n Befehle davor hatte, weil > da ein pipeline register nicht korrekt gehandelt wurde. Sehr spannendes Beispiel und typisch für "Fehler" die leicht "durch die Maschen rutschen": es sind mehrere parallele Bedingungen gleichzeitig erfüllt und zeitliches pipilining (FF-stufen in Logik) ist involviert. Persönliches Beispiel: Laden des programm counters: *Ein Sprungbefehl liegt zur Ausführung vor *gleichzeitig Interrupt *gleichzeitig Exception *Instruction-Cache Besonderheit (miss, dirty) *der processor kommt grad aus dem "Power Save" Das kann man gern nach Prioritäten auflösen, die aber nicht unbedingt spezifiziert sind. Manchmal ist das Ergebnis auch kein Bug also "Verrechner" sondern nur eine geringe Performance-einbuße. So leert wohl mancher Processor seine Pipeline wegen supoptimalen Branch-Prediction(Sprung vorhersage) häufiger als nötig. Kostet höchstens einzelne µs, merkt der Anwender nicht. Es wäre jetzt interessant zu wissen, was das tool jetzt bei der formalen verification konkret anstellt, nach Anhang scheint es im Wesentlichen ein Logik(boolsche)-Equivalenz check zu sein. Also, es scheint, ob im obigen Beispiel das tool quasi "nachrechnet", ob unter den genannten Vorbedingngen das gleiche herauskommt wie für den Fall, das eine der Vorbedingungen nicht zutrifft. "Equivalenz-check kenne ich eher zur Überprüfung der Synthese oder router, als ob nach der Umwandlung der RTL-Beschreibung in eine Gatterliste funktional noch alles "beim Alten ist" als als Anwendung bei der "formalen Verifikation". Der Scan der angehangenen vier Seiten hat ein paar Macken (die automatische Erkennung des Formats und der Ausrichtung der Vorlage hat versagt), nglw. kann das ein moderner pdf-reader ausgleichen. Besonders interessant die Passage zu "the myth of complete verification with FV". Stichworte für die Suche nach konkreten tools ist wohl das bereits oben genannte PSL oder "Property specification language". Der Anhang stammt aus dem in Beitrag "Re: Formale Verifikation als Privatmann" genannten Werk.
:
Bearbeitet durch User
Bradward B. schrieb: > Es wäre jetzt interessant zu wissen, was das tool jetzt bei der formalen > verification konkret anstellt Es gibt zwei Varianten. In der einen, die tatsächlich nicht alle Fälle abdecken kann, werden vom Anfangszustand alle möglichen Signalkombinationen durchgegangen. Zustände, die durch assume ausgeschlossen sind, werden dabei übergangen. Erreicht ein Zustand einen durch assert ausgeschlossenen Zustand, wird der Zustand als Fehler gemeldet und der Weg dahin in einem Minimalbeispiel gezeigt. Aber das Verfahren ist natürlich sehr ressourcenintensiv. Das kann Fehler finden, wenn nur wenige Takte bis zu diesem Fehlerzustand gebraucht werden. Aus meiner (sehr geringen) Erfahrung würde ich sagen, dass es so bis etwa 100 Takte anwendbar ist. In der anderen Variante wird die Bescheibung in eine boolsche Formel umgewandelt und durch Induktion und einen (SAT-)Solver mathematisch-logisch nachgewiesen, dass ein durch assert ausgeschlossener Zustand nie erreicht werden kann. Einfaches Beispiel: y = A'last and (A and B'last or C or (A and not C)) and not A'last and (not B'last or not C) assert y != 1 A and not A schließen sich gegenseitig aus, damit ist für alle Eingangskombinationen für alle Zeiten ausgeschlossen, dass y=1 wird. Ohne alle Zustände durchgehen zu müssen und ohne einen einzigen Zustand ausprobiert zu haben. Allerdings muss ich zugeben, dass ich das Verfahren nicht ganz verstanden habe. Es gibt noch eine genauere Beschreibung zur formale Verifikation unter https://zipcpu.com/blog/2017/10/19/formal-intro.html
Was soll denn das Ziel der ÜBung sein? Für eine formale Verfikation benötigt man nicht zwingend eine VHDL-Beschreibung oder einen diesbezüglichen Simulator. Es geht ja darum, das Konzept, also die Methode, Formel und Schaltung zu verifizieren, ob sie den Anforderungen genügt. Eine Regelschleife könnte man z.B. mit MATLAB prüfen unter Nutzung physikalischer Modelle und einer Beschreibung der Totzeit der Regelung und deren Anpassung, also der Messung von Solldaten und Istdaten, um die Parameter anzugleichen. Das braucht erst mal nur die Formelstruktur und die Grenzen der Physik in denen sich das abspielen soll. Daraus kann man dann ableiten, ob die Formelstruktur und Regelschleife sowie die mögliche Umsetzung das Gewünschte überhaupt können kann. Den FPGA wird man da nur als Verzögerer simulieren. Man wird aber ADC und DAC-Effekte simulieren und ausleiten, welche Kriterien die erfüllen müssen, respektive die zur Verfügung stehende Technik in die FV einwerfen. Will sagen: Was man da tun muss, hängt stark von den Zielen ab. Da braucht es auch erst mal funktionelle Anforderungen. Eine FV wird man auch nur dann durchführen, wenn gefordert oder wenn man nicht offensichtlich eine Lösung darlegen kann. Oft genug ist eine Lösung evident, d.h. man kann z.B. angeben, eine Lösung mit einem FPGA bauen zukönnen, die alle 100ms einen Wert ausgibt, wenn man abschätzt, dass alle Datenstrecken von ADC und DAC sowie Rechungen schnell genug sind, ohne das im Detail vorher noch formell nachzuweisen. Was man da zuhause üben soll, sehe ich nicht. Die Herangehensweise ist schon strukturell bei jedem Projekt eine andere.
Fuer FV kann man auf jeden Fall mal zuhause den Einstieg mit der Symbiosys-Toolchain ausprobieren und dem Wort zum Sonntag von Gisselquist was anfangen. Ging mir persoenlich allerdings nicht weit genug, und produktiv arbeiten sieht dann doch etwas anders aus. Mit Verlaub, mit mindestens drei verschiedenen Sprachen draufhauen zu muessen, um einen CPU-Kern verifiziert zu kriegen, ist nicht so ganz auf dem Pfad moderner Mixware-Entwicklung. Coverage und Failsafe-Analysen kann man schon mal nach Norm abfruehstuecken, die Frage ist nach dem Dogma ob das per statische Analyse oder effektiver Ausfuehrung von Code und Tracing geschehen soll. Statische Analyse von VHDL ist halt einfach so unfassbar aufwendig 'from scratch', was die Toolkosten erklaert. Interessant wird es dann bei Pipeline-Verifikation oder Glitchfestigkeit, wie auch gewisse automatische Verifikation, z.b. ob das Neudesign dasselbe tut wie das alte. Da machen die Python-Ansaetze eine richtig gute Nummer. Der Gag ist dabei, dass z.B. einzelne Pipeline-Stufen per Iteration (yield) an entweder HDL-Transpiler oder Simulator uebergeben werden. Dazwischen macht man quasi out-of-band im ausgefuehrten Bereich seine Verifikation, schleift Solver ein, oder kontrolliert einfach, ob die HW exakt das gleiche rechnet wie der Python-Prototyp. Das Resultat ist dann allerdings eine sehr lange, ausgerollte HDL-Testbench, oder eleganter eine Co-Simulation. Mit bestehender V*HDL hat man leider diese Moeglichkeiten nur auf Blackbox-Ebene, d.h. die HDL-Quelle muss bereits in einfache, induktiv verifizierbare Primitiven aufgespaltet sein, sonst ist man entweder bei der nicht ganz automatisierbaren Uebersetzung in die Python HDL oder doch wieder bei statischer Analyse.
Martin S. schrieb: > mit mindestens drei verschiedenen Sprachen Welche meinst du? PSL, die Beschreibungssprache, und welche noch? Oder man macht alles mit SystemVerilog, dann ist es nur eine Sprache. PS: Noch eine Seite zum Einstieg: https://vhdlwhiz.com/formal-verification-in-vhdl-using-psl/
:
Bearbeitet durch User
Also typischerweise kommt hier mal so eben noch dazu: - TCL/Makefile um die Tools zu scripten (continuous integration) - C/C++ : GCC-Regresstests oder PLI/VPI-Anbindung fuer spezifische Co-Simulation (Realdaten von 'aussen') - XML-Geraffel fuer allfaellige Konfigurationen oder SoC-Memory-Maps Mal ganz zu schweigen von komplett anderen Scala-basierenden HDL, auf denen einige RISC-V-Designs beruhen. Und von VHDL kommt man aufgrund gewisser Legacy die einfach funktioniert auch nicht immer weg. SystemVerilog hat zwar nette Features, aber es ist halt immer noch Verilog (mit seinen arithmetischen Stolperfallen).
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.