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