The Hidden Power of Formal Methods in Hardware Design: Crash Course
Вставка
- Опубліковано 27 чер 2024
- Great for verification, formal methods can also supercharge hardware development. In this quick tutorial overview, I'll provide key highlights from my recent talk at the Free Silicon Conference (FSiC2023) focusing on the tools and techniques I use while creating FPGA and ASIC designs: namely cover and BMC.
Cover statements are useful to see the system in action, to do simulations without micromanaging every single signal, and even to find solutions to problems.
Bounded model checks are great for hunting bugs but I also show a neat way to use BMC to do sneak path analysis.
The full "Black-tie Python: Formal verification with Amaranth" talk is available at:
peertube.f-si.org/videos/watc...
Details about the conference may be found at:
wiki.f-si.org/index.php?title...
All the other talks are also online at:
peertube.f-si.org/video-chann...
and they are well worth it.
Though the techniques covered here are all pretty independent of the language/toolkits you're using to implement your hardware FPGA/ASIC designs, here I'm using
Amaranth (Python):
amaranth-lang.org/docs/amaran...
Yosys/symbiyosys:
yosyshq.readthedocs.io/projec...
symbiyosys.readthedocs.io/en/...
And you can have a look at the amaranth_testbench library, which I introduced and used in much of the talk, that includes all the examples I covered and more:
github.com/psychogenic/amaran... - Наука та технологія
Fantastic to see this material. Thanks for the crash course and the pointer to the full talk!
Cool! Yeah, the talk is a little rough around the edges, but I think it has a few gems worth the time. Thanks for the feedback :)
The test-first approach for designing hardware without micromanaging signals is really cool! Thanks for sharing!
I agree! Using these testing tools in this manner has changed how I'm making stuff, it's pretty awesome. Thank you for the feedback :)
Never heard about cover before. Super interesting! Thanks!
It's only recently that I started getting how crazy useful cover could be! I hope it's as helpful to you :)
I saw this thumbnail in my feed and I thought "Hey, that guy looks like..."
Good to see you on here! Great video! Cover seems like a super useful tool. Looks like I have a bit of content to go through. I hope you've been well!
hah, Rob!! Wow... ok, I read this and... well neither your username nor thumb were all that helpful, lol! How ya been? Actually, I'll ping you via sidechannel... but yes, cover is super useful and, though I didn't emphasize as much, BMC manages to find some really weird/unexpected stuff, sometimes and is really good a preventing problems you didn't know you were going to have.
I used the open source formal methods tools a lot with FPGA design and recently I also used it with my first commercial ASIC that we made to prove critical parts of it. Suffice to say, those critical parts all work perfectly!
I would definitely recommend formal methods for anyone doing digital design :)
Yes, these are awesomely powerful tools. I'm still getting the hang of prove/induction mode (not to the point that I'm confident that I've actually proven the thing works for eternity), but BMC locates a lot of problems before they happen and I'm loving cover for inspection. Do you have any recommendations as starting points for defining formal specs used for reliable k-induction use?
@@PsychogenicTechnologies I don't have a simple resource that can used as a starting point, but I can give some pointers:
* With induction, every formal step *except the last* will *assume* that your *assertions* are true. Let's say you have two instances of a 5-bit up counter and you reset it back to zero whenever the counter is 9. If you assert that both counters have the same value, then it will pass BMC, but not induction because the initial value of one counter could have been different than that of the other counter. You will need to add extra assertions (that act as assume statements up until the last formal step) so that the "incorrect" initial values are flushed out.
* When proving asynchronous logic or logic with asynchronous resets for example, then the $prev statement refers to the previous clock transition, *not* the last clock cycle. This can be very confusing at first, because with synchronous logic, $past refers to the previous clock cycle (so the previous rising edge or previous falling edge, instead of the previous edge).
Most of it comes down to trying to prove a bunch of different types of hardware to gain more experience. You can also ask Matt Venn, who I believe taught a formal verification course before. Hope this helps, even if it's a little bit :)
Just came to say hello, nice job as always! 😁
Hallo to you, and many thanks! :D
Really really superb content
Many thanks! Sometimes I worry that content like this addresses itches that no one else share: comments such as yours let me know it's worth the effort :) Thanks again, cheers.
@@PsychogenicTechnologies would actually appreciate a more in depth tutorial for setting this up and usage, etc :)
for an amateur designers out there, what is "cover" ?
Hello gryzman,
Here "cover" is in the sense of "encompass" or "reach"--so you are asking the system: "reach this state ABC, and show me how you did that".
So that's what it does, if it can: it finds a way to meet all your demands and spits out a VCD file that you can look at.
Goat, cabbage, sailor... huh?? :D
hahaha, yes! I'd seen this problem handled this way before, and thought it was a really neat demo of the power of the solvers. Couldn't find the original source again (ok, didn't try too hard, I admit), anyway I wanted to try and do it myself 'cause I think it's kind of funny. You can see all the code at
github.com/psychogenic/amaranth_testbench/blob/main/amaranth_testbench/examples/ferryman.py