The Hidden Power of Formal Methods in Hardware Design: Crash Course

Рет қаралды 2,369

Күн бұрын

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...

Пікірлер: 21

@stewartmackenzieindaba 10 ай бұрын

Fantastic to see this material. Thanks for the crash course and the pointer to the full talk!

@PsychogenicTechnologies 10 ай бұрын

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 :)

@bleeptrack 10 ай бұрын

Never heard about cover before. Super interesting! Thanks!

@PsychogenicTechnologies 10 ай бұрын

It's only recently that I started getting how crazy useful cover could be! I hope it's as helpful to you :)

@deadbugengineering3330 10 ай бұрын

The test-first approach for designing hardware without micromanaging signals is really cool! Thanks for sharing!

@PsychogenicTechnologies 10 ай бұрын

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 :)

@Oguz286 7 ай бұрын

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 :)

@PsychogenicTechnologies 7 ай бұрын

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?

@Oguz286 7 ай бұрын

@@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 :)

@akira410 10 ай бұрын

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!

@PsychogenicTechnologies 10 ай бұрын

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.

@zdenkostanec1622 10 ай бұрын

Just came to say hello, nice job as always! 😁

@PsychogenicTechnologies 10 ай бұрын

Hallo to you, and many thanks! :D

@fluffyvillain968 10 ай бұрын

Really really superb content

@PsychogenicTechnologies 10 ай бұрын

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.

@fluffyvillain968 Ай бұрын

@@PsychogenicTechnologies would actually appreciate a more in depth tutorial for setting this up and usage, etc :)

@gryzman 10 ай бұрын

for an amateur designers out there, what is "cover" ?

@PsychogenicTechnologies 10 ай бұрын

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.

@_-martin-_ 10 ай бұрын

Goat, cabbage, sailor... huh?? :D

@PsychogenicTechnologies 10 ай бұрын

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