<_whitenotifier-4>
[amaranth-lang/amaranth-lang.github.io] github-merge-queue[bot] 771953d - Deploying to main from @ amaranth-lang/amaranth@a570317c365acacd67c52521e0eeab2605714235 🚀
frgo has quit [Ping timeout: 260 seconds]
mindw0rk has quit [Ping timeout: 248 seconds]
mindw0rk has joined #amaranth-lang
frgo has joined #amaranth-lang
Degi has quit [Ping timeout: 265 seconds]
Degi has joined #amaranth-lang
frgo has quit [Ping timeout: 244 seconds]
frgo has joined #amaranth-lang
frgo has quit [Ping timeout: 260 seconds]
frgo has joined #amaranth-lang
frgo has quit [Remote host closed the connection]
whitequark[cis]1 has quit [Quit: Bridge terminating on SIGTERM]
_catircservices has quit [Quit: Bridge terminating on SIGTERM]
eigenform[m] has quit [Quit: Bridge terminating on SIGTERM]
<_whitenotifier-4>
[YoWASP/yowasp.github.io] whitequark 3856ace - Fix the NPM badge for Yosys.
_whitelogger has joined #amaranth-lang
frgo has quit [Remote host closed the connection]
frgo has joined #amaranth-lang
frgo has quit [Remote host closed the connection]
<vup>
so regarding https://github.com/amaranth-lang/amaranth/issues/1555, what would the overall goal be for the formal verification story with amaranth? Should there eventually be support for things like formal cutpoints? Furthermore, should different backends be supported? Right now its tied quite closely to yosys / sby, although with a small helper module implementing the `$any{const,seq}` modules, it also works with jasper for example. I guess the main
<vup>
question there would be if the yosys verilog backend should / will ever be able to emit these cells in form of `assume`.
<vup>
Finally it would be nice if the `assume`,`cover`,`assert` cells could be given a label that is propagated to a statement label in the generated verilog, but this is again mostly a yosys `write_verilog` issue I assume.
whitequark[cis] has joined #amaranth-lang
<whitequark[cis]>
I thought the label does propagate, or maybe I misremember?
<whitequark[cis]>
ah I think we may've moved that around during the NIR migration
<cr1901>
And some ppl here are... not fans of sby, putting it mildly
<whitequark[cis]>
I used to think formal was annoying until I realized using yosys-smtbmc directly made it much easier!
<whitequark[cis]>
well, it's still annoying but in more interesting ways that don't involve subdirectories and subprocesses
<whitequark[cis]>
basically, the big issue with formal support right now is that there is no coherent use model
<whitequark[cis]>
I've added it long ago as a something between proof of concept and an item to tick, and it has never graduated from that
<whitequark[cis]>
we would need someone, ideally an FV expert, to come up with the answers to the questions: for whom is it built? what problems does it solve? and how does it solve these problems?
<whitequark[cis]>
in particular I think that the idea of "just delegate to sby" goes against our principles of delivering an easy-to-use, hard-to-misuse toolchain because it is quite easy to misuse an sby script, and also the whole thing is really annoyingly non-integrated with things like remote builds or build overrides, etc
<whitequark[cis]>
I think that if I went with launching yosys-smtbmc directly at the time I first implemented this we would've had a much nicer system today even if everything else went unchanged, by the virtue of me being forced to come up with some coherent use model
<whitequark[cis]>
but I guess it's exactly because I didn't have that that we ended up with delegating to sby
Guest39 has joined #amaranth-lang
Guest39 has quit [Client Quit]
Mimil has joined #amaranth-lang
Mimil has quit [Quit: Client closed]
FFY00_ has quit [Read error: Connection reset by peer]
FFY00_ has joined #amaranth-lang
<vup>
whitequark[cis]: not sure how it would, I don't even see code that would emit labels in the `write_verilog` backend, (Im not talking about the assertion message just to be clear)
<vup>
also I never get yosys-smtbmc to prove anything for me, `abc pdr` has been much more successful, but maybe I am just holding it wrong?
catlosgay[m] has joined #amaranth-lang
<catlosgay[m]>
this is roughly expected, the algorithms in yosys-smtbmc are much less powerful (even abc pdr isn't exactly state of the art, but most of the more modern open source model checkers are riddled with bugs in my experience)
<catlosgay[m]>
yosys-smtbmc is relatively stable and bug free though (most bugs affecting yosys formal verification tend to be in yosys in my experience)
<cr1901>
vup: Try my linked repo for a known-working example of k-induction. Unfortunately, that's the most powerful algorithm I know, and I've not had the bandwidth to really try and understand anything more difficult
<cr1901>
working example of k-induction using yosys-smtbmc*
<cr1901>
OTOH, I've never really used abc directly, and kinda don't want to after hearing horror stories lmao
<vup>
cr1901: do you have an example with a async reset? I think my problem with smtbmc always goes back to that. For example this https://paste.niemo.de/raw/dabisanozu.sv fails with it, but succeeds with `abc pdr`
<cr1901>
No, no examples with async reset. Would have to play around with them to comment further
<vup>
okay, thank you anyways :)
<catlosgay[m]>
to use an async reset you want to use async2sync in your yosys script (if you only have one clock domain). if you have multiple clock domains/clock gating you need to use clk2fflogic at the moment instead. these correspond to multiclock off/on in sby
<catlosgay[m]>
having said that that example snippet wont behave well anyway, the whole formal timestep bit is entirely unnecessary
<cr1901>
Doesn't help that I don't know SV; I've never seen (* gclk *) as opposed to $global_clock, and I don't know what always_ff does compared to an always block
<catlosgay[m]>
gclk is a yosys extension iirc, entirely unnecessary for this
<catlosgay[m]>
yosys does seem to choke on this particular design due to how it does check cell lowering, gimme a sec and i can try to work out why
<vup>
catlosgay[m]: yeah I put `multiclock on` in my sby file. And removing the (* gclk *) part does not change anything about induction failing.
<catlosgay[m]>
yeah but the gclk part does nothing to help at all
<catlosgay[m]>
induction fails because smtbmc doesnt implement a complete k-induction algorithm, if the design can stall and indefinitely make no progress k-induction will never pass with smtbmc
<cr1901>
Is gclk supposed to be different from $global_clock?
<cr1901>
> if the design can stall and indefinitely make no progress
<cr1901>
This is where I got stuck learning more
<cr1901>
it feels like that's an inherent limitation to k-induction
<cr1901>
if the design can get stuck in a loop, it doesn't matter if that actual state is unreachable from reset; k-induct will fail
<cr1901>
but how do you avoid getting stuck in a loop?
<catlosgay[m]>
you add constraints to prevent it being stuck in a loop
<catlosgay[m]>
fwiw that particular example you posted does seem to be hitting a bit of a bug, async2sync should be able to handle that
<catlosgay[m]>
i can write it up as an issue in a little bit
<vup>
can you give me an example of what assertion I would add to make this work? (I guess something around rst not being hold indefinitely and the clk actually toggeling?)
<catlosgay[m]>
the right assertion to add is one that blocks states that the solver shows in the inductive counterexample that aren't actually reachable
<catlosgay[m]>
unfortunately multiclock on adds these states in a way you cant do much about, its a known limitation that smtbmc will never get proofs with multiclock on
<catlosgay[m]>
really for that example you should be using multiclock off, theres just a bug in yosys it seems at the moment
<cr1901>
Section 2.2 looks like a definition of temporal induction
<vup>
yeah I hit that bug and thats why I made it multiclock on
<vup>
okay, so adding `always assert (counter <= 10)` makes its actually able to proof it. But for a complex design having to add all these helping asserts seems quite unfortunate.
<vup>
Is there any advantage to using smtbmc instead of `abc pdr`, which seems to be able to handle this without any help?
<catlosgay[m]>
cr1901: its the unique states part that smtbmc doesn't implement which is needed for complete k-induction
<catlosgay[m]>
not really, i think smtbmc is more stable and its word level so it can handle arrays better but otherwise pdr is more powerful
<cr1901>
Ahhh. Yea, I'm gonna have to chew on this for a while then
<catlosgay[m]>
the helper assert sitution is definitely unfortunate, the state of formal with yosys from a practical standpoint is generally painful
<catlosgay[m]>
fwiw with the work i do I output btor2 from yosys and then run academic model checkers like avr, pono and rIC3
<catlosgay[m]>
but this tends to require quite a lot of manual work configuring the yosys script correctly, its definitely not an intuitive flow
<cr1901>
It's ironic because smtbmc has genuinely helped me find bugs. I don't want to have to annotate the output SMTv2s by hand, which is what yosys-smtbmc does (--dumpsmt2)
<catlosgay[m]>
cr1901: im not quite sure i follow. the alternative to smtbmc isnt annotating smt2 by hand, its using other output formats like btor with btor solvers
<cr1901>
I don't understand the btor format, and not sure I am in a position to sit down and really study it :P
<catlosgay[m]>
its just another word level netlist format like rtlil or others but specifically for hardware formal verification
<vup>
yeah I used rIC3 with sby recently and it was incredibly more quick than `abc pdr`. Although that did used aiger. btor is wordlevel compared to aiger, right? Does that help with rIC3, I thought that just does btor2aiger as the first step?
<catlosgay[m]>
its basically the bitvector and array logics from smt2 extended with state elements and properties
<catlosgay[m]>
yeah rIC3 eagerly encodes to aiger, so it also cant handle things like arrays, but as a bit level solver its probably the best going atm
<catlosgay[m]>
(although its license terms are weird and potentially not enforceable)
<cr1901>
catlosgay[m]: A lot of this is "I'm used to the smtbmc flow, even if it's flawed, and I think I'll get overwhelmed trying to learn if I deviate too far from it". 1/2
<catlosgay[m]>
there are people with plans to improve these types of things but i dont think they will materialise for a while
<cr1901>
Maybe it might not be a good use of my time, but looking at the uniqueness constraints that smtbmc doesn't have and trying to figure out how to _add_ that to the smt files is a good first step where I won't get overwhelmed
<cr1901>
Maybe it might not be a good use of my time <-- in that it's useful to others, I seem to be one of the few ppl who has a high opinion of smtbmc
<cr1901>
Anyways, thanks for the paper... it'll be very useful now that you pointed out the differences :P
<catlosgay[m]>
this is the nature of being at the intersection of a fairly technical/theory heavy field which not too many people are familiar with and working on open source tooling where the few people that are interested in this stuff either go to industry to be paid more or are in academia where the incentives aren't well aligned with high quality open source development
<catlosgay[m]>
i believe the view when it came up before was that you don't actually have a clear view of what the state elements are in the smt2 output so doing the simple path constraints is a bit of a pain, but maybe you can work it out
<catlosgay[m]>
an alternative could be to extend sby's `btormc` support to also support `btormc --kind --simplepath`. `btormc` is a (faster) implementation of the same algorithms as smtbmc but using the btor output and is already supported in `bmc` mode, just not in `prove` mode
<cr1901>
(To be explicit for future-me: that PR is doing detection only and will warn you that "yosys-smtbmc can't handle this")
<cr1901>
I thought state was implemented as a bunch of declare-funs with constraints- i.e. "let the solver decide how to represent state". It's been a while since I took a look however.
<catlosgay[m]>
yeah, maybe the issue was actually in checking equality of arrays or something. it has similarly been a while since i looked inside smtbmc so i dont remember
<cr1901>
That makes two of us :P; I don't know if I'd succeed in adding the uniqueness constraints to smtbmc. I just need to be careful not to overwhelm myself.
mindw0rk has quit [Ping timeout: 252 seconds]
<catlosgay[m]>
if you do, make sure you check section 4.2 of that paper cos eagerly adding the constraints doesn't work well for performance, you have to do it incrementally :>
<cr1901>
Never can be simple, huh :P?
<catlosgay[m]>
i mean you can try it non-incrementally, but my experience is that it greatly overwhelms the solver
<vup>
(ah I remember why I added the gclk rst thing. Its necessary to make `$past` work. `$past` seems to be impossible to be used under async reset, so I have to move to a sync reset process and manually check the reset, which of course breaks if its allowed to deassert rst asynchronously)
<cr1901>
catlosgay[m]: I privmsg'd some exposition to avoid reducing SNR of the room if interested
<catlosgay[m]>
im running through the 1b2 discord bridge so i dont think imma see that unfortunately, wheres it going to?
<cr1901>
Ahhh I was doing an IRC privmsg. You appear to be a Matrix user from my perspective "catlosgay[m]". IRC to Matrix privmsg _does_ work
<catlosgay[m]>
ahh yeah im through two layers of bridges unfortunately
<catlosgay[m]>
vup: have submitted the multiclock bug here https://github.com/YosysHQ/yosys/issues/4875 (wasn't sure what github username to tag you with). not sure if anyone will have a chance to look at it anytime soon but at least its there for now
<cr1901>
Well, the TL;DR version is "learning about SMT solvers from YT videos, and looking at the intermediate outputs from yosys-smtbmc (--dumpsmt2) and yosys (write_smt2) was what got k-induction to click for me. 1/2
<cr1901>
And I've struggled to extend my knowledge beyond that: e.g. AIGER for liveness/s_eventually, even safety and liveness aren't intuitive to me lol"
<cr1901>
Safety: "Bad things can't happen". Yes, that's _technically_ correct. In a temporal induction proof, you're solving to make sure a counterexample (a bad thing) can't occur. But in your Verilog code, you're doing "assert this always occurs" :D.
<catlosgay[m]>
ahh yes, i think me also. despite all its flaws it was playing about with sby that got me into formal and my jobs have been doing various formal things for the last few years as a result
<catlosgay[m]>
good thing always happens and bad thing never happens are just duals right
* cr1901
has to philosophically think about that... there are days that are neither good or bad :)
<catlosgay[m]>
liveness is instead saying good thing eventually happens or equivalently we never stay in bad states forever
<cr1901>
One of my early attempts to understand liveness was in the spi_tb repo I linked... it requires a depth of 180 to pass in it's current form. A lot of that is "waiting for the clock divider to eventually get to 0"
<cr1901>
I wish it was possible for: 1. An SMT solver to realize "oh wait, nothing's going to happen until the clock divider count reaches 0" and skip all those states with just waiting
<catlosgay[m]>
in the finite state setting `a -> eventually b` is equivalent to saying "there is no trace where after a occurs we can stay in a loop where b doesnt occur". because if there was that loop can be extended as much as you like so you can create an arbitrarily long trace that never reaches b
<cr1901>
Hmmmm
<catlosgay[m]>
fwiw commercial tools struggle a lot with liveness too, in the open source world hardly anything supports it and if it does it tends to be buggy or not performant in my experience
<cr1901>
and 2. An SMT solver to be able to realize "for any finite clock divider value, we will eventually make forward progress, so we can prove this core works for all clock dividers > some int"
<cr1901>
Like both of these are "well, duh" things for humans (for want of a nicer term), so why can't the tools see it?
<catlosgay[m]>
yeah thats definitely a hard problem
<cr1901>
> fwiw commercial tools struggle a lot with liveness too <-- well that makes me feel better
<cr1901>
your definition of "a -> eventually b", coupled with the uniqueness constrait that yosys-smtbmc doesn't satisfy gives me some hints to go forward tho (at my own pace :P)
<cr1901>
Maybe I can even apply some of it back to the spi_tb... If I prove that the clock divider always goes to 0 for some large int, then can't I shorten the clock divider int and do k-induct without loss of generality?
<cr1901>
(Btw, I doubt wq minds the OT, but there's an ##smt IRC channel... dunno if avail on the bridge tho)
<catlosgay[m]>
https://fmv.jku.at/papers/BiereArthoSchuppan-FMICS02.pdf you may find this classic paper interesting. it explains how to convert liveness to safety by looking for these "lasso" shapes where you have some finite prefix and then a loop that can be extended arbitrarily without witnessing b. looking for these loops is very similar to the loops in k-induction uniqueness and they serve a similar purpose - a loop is something that
<catlosgay[m]>
doesn't make progress
<catlosgay[m]>
i have to head off in a minute anyway unfortunately
* cr1901
nods
<cr1901>
Will take a look, thanks
frgo has joined #amaranth-lang
frgo has quit [Ping timeout: 248 seconds]
mindw0rk has joined #amaranth-lang
frgo has joined #amaranth-lang
frgo has quit [Ping timeout: 276 seconds]
FFY00_ has joined #amaranth-lang
FFY00 has quit [Ping timeout: 252 seconds]
<vup>
catlosgay[m]: thanks for filing it. Also thanks for the hints re making smtbmc pass.