<Stas[m]1>
<vup> "i can also recommend formal..." <- Formal is interesting, but I have found scarce info on how to do it. There are posts from Zipcpu, and a dude on Youtube doing formal for a 6800 cpu he was implementing
<whitequark[cis]>
yeah unfortunately the tools aren't that good either; this is a part of why there's not much formal support in Amaranth
<whitequark[cis]>
doing BMC is easy but limited, anything beyond that I'm not convinced is even worth it time wise
<vup>
whitequark: what do you mean its not worth it time wise? The runtime of the formal tool would be too long?
<vup>
*mean with
<Stas[m]1>
I understood it is more about ergonomics. The formal verification stuff is also toolchain specific. Like yosys does it one way, and proprietary tools do it different
<Stas[m]1>
I looked only into BMC, as it is discussed more on the internets
<whitequark[cis]>
yes, ergonomics and productivity is what I mean
<vup>
I see. Well for me it has been super useful and productive, but it of course depends on what kind of things you are wrinting. Maybe I am also missing something, I dont really see, how going from BMC to full proofs makes things less ergonomic or productive?
<whitequark[cis]>
induction is a huge pain to get working and you have to expose the implementation details of your gateware, which you previously didn't need to at all
<whitequark[cis]>
like, i don't want to have a register exposed for the sole benefit of some proof
<whitequark[cis]>
i've never had a situation where an inductive proof was useful to me
<whitequark[cis]>
also the way yosys does it is particularly messy, although i don't remember the details of it anymore (i last tried using k-induction back when symbioticeda was still a company doing eda)
<whitequark[cis]>
(also, although it wasn't a concern back then, today i'm broadly disinclined to do anything with a technique whose loudest advocate and the person who wrote the most documentation on it is an outspoken transphobe who i will ban on sight anywhere i have the power to do so)
<vup>
well yeah, i found (k)-induction super annoying to work with aswell, but sby also supports formal tools that do full proofs and don't use (k)-induction, rather IC3, which I found very pleasant to work with. (rIC3 seems to be the fastest supported one at the moment, but even the `abc pdr` mode works super well for most stuff I do. IC3 also doesn't force you to expose any of your implementation details.
<whitequark[cis]>
oh.
<whitequark[cis]>
okay, that explains why our experiences were so different
<whitequark[cis]>
I don't think there were other options back then, or perhaps they were too immature to use
<vup>
thats very possible, I only started using them about a year ago