So far all I got are ideas that satisfy max two of those three requirements. Maybe someone here has a great idea? Or has done a formal verification "beginners project" that would fit all three requirements? #FollowerPower
Show this thread
Needed: Ideas for hardware formal verification demo. I'm looking for: - A simple design with easy to understand requirements - With a bug that's easy to understand once pointed out, but otherwise hard to find - And simple formal safety properties that expose the bug
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
8 bit RISC CPU. Perfect example of what a real formaly verified project might look like, while also being small enough that anyone could understand it
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Designing an exercise that is hard enough to grow on but not so hard to exceed the learner's level of frustration is an art! On the way there the teacher has to struggle with his own level of frustration. May the Force be with you!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
UART with off-by-one sample point meaning a lower tolerance to clock drift than calculated
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@oe1cxw Multi cycle paths form a good case for a formal demo and also highlights it's advantages over simulationThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Crypto wallet secure enclave chip ?
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Would this be too complex: 1) Take a simple 1-stage processor. 2) Pipeline into fetch-decode without adding any interlock. 3) Don't let anyone use the name "branch delay slot" for the resulting bug.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Data path or control? Once you start to get into the details of some more complex operations there is lots of room for "should have seen it and there is only small n in 2-to-the word size test vectors that would find it".
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
PWM peripheral module with all the fixings? (Deadtime, shadow update registers, fast fault trip)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.