You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
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
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
https://github.com/cr1901/spi_tb I did this when learning how to do formal in 2017. I could probably introduce a deliberate bug that satisfies #2 (I feel #1 and #3 are already satisfied). Uses yosys-smtbmc instead of symbiyosys though...
https://github.com/cr1901/spi_tb/commit/190dfacb405b0e3e8991d9e6284b493d2ba9e111 … Here's an example of an easy-to-make mistake that formal will catch easily (#2 satisfied, if I just "revert" this change :D).
#FollowerPower maybe @zipcpu can help here. He's done a series of tutorials on formal verification.
As a novice I'm interested in learning back UT this, and am struggling ,within my projects, thinking of what the hell to assert... 
@adumont,I know what you mean about struggling to figure out what to assert. I found it helpful to think of assertions from the “test” side: http://bitsbytesgates.blogspot.com/2018/12/fwrisc-turbo-charged-unit-tests-with.html?m=1 …
Would this work? http://zipcpu.com/formal/2018/12/28/axilite.html … Not sure if you'd call an AXI-lite slave "simple", but the requirement of one acknowledgement per transaction request is simple enough to understand. That Xilinx's demo code can't meet this requirement is a fun bonus.
How about a 4-bit synchronous BCD counter with preset? The "bug" is that you can preset a non-decimal number and the counter will do weird things. It's "hard to find" because maybe you never thought of the non-decimal case.
Maybe an arbiter (check that it is fair)?
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
