4.1 RTL parametrisiert, eine Takt-Domaene, synchrone Resets
PruefaufgabeRTL parametrisiert, eine Takt-Domaene, synchrone Resets
Beweis-Artefaktrtl/<block>.v
Eine Domaene, synchrone Resets, Parameter statt Magic Numbers - jede Abweichung braucht einen dokumentierten Grund, sonst ist sie ein zukuenftiger Geist.
4.2 Nonblocking-Disziplin (Register <=, Kombinatorik =)
PruefaufgabeNonblocking-Disziplin (Register <=, Kombinatorik =)
Beweis-ArtefaktReview-Vermerk
Nur Nonblocking macht den Tick-Vergleich reproduzierbar. a=b; b=a; ist KEIN Tausch, sondern undefinierte Reihenfolge.
4.3 Latchfrei (jede if/case-Kette vollstaendig)
PruefaufgabeLatchfrei (jede if/case-Kette vollstaendig)
Beweis-Artefaktyosys CHECK: 0 Latches
Ein inferiertes Latch simuliert freundlich und geistert auf dem Brett. Jede Kette vollstaendig, default immer - yosys CHECK ist der Zeuge.
4.4 Async-Eingaenge ueber 2-FF-Synchronizer (+ Entpreller)
PruefaufgabeAsync-Eingaenge ueber 2-FF-Synchronizer (+ Entpreller)
Beweis-ArtefaktSynchronizer-Modul im RTL
Metastabilitaet ist in der Simulation UNSICHTBAR. Taster und fremde Domaenen nur ueber 2-FF + Entpreller - ein Tastendruck ist nie flankensynchron.
4.5 Kompiliert sauber
PruefaufgabeKompiliert sauber
Beweis-Artefaktiverilog -g2012 Exit 0
Das kleinste Tor - und die wichtigste Demut: RTL_WRITTEN ≠ TB_PASS. Geschriebener Code hat noch nichts bewiesen.