<tpw_rules>
i had considered doing option 1 before but wq seemed to desire something akin to 3
Lunaphied[m] has joined #amaranth-lang
<Lunaphied[m]>
Did multiclock formal support kind of lose steam?
<Wanda[cis]>
as in, in amaranth?
<Wanda[cis]>
there were serious doubts about formal support in general
<Wanda[cis]>
as in, the current model is completely tied to yosys and its formal methodology, which ... doesn't seem all that good in the grand scheme of things
<Wanda[cis]>
and so formal support is effectively frozen in place until someone competent in formal comes along and proposes something a) actually reasonable, b) implementable with the tools we have
<Wanda[cis]>
tbh amaranth is outgrowing yosys, in many ways. all the memory stuff I ranted about above is one area in which it is quite visible; formal is another
<Lunaphied[m]>
It seems like Yosys in general is being outgrown by itself and Amaranth is suffering for it
Degi_ has joined #amaranth-lang
Degi has quit [Ping timeout: 245 seconds]
Degi_ is now known as Degi
FireFly has quit [Ping timeout: 255 seconds]
indy_ is now known as indy
frgo has joined #amaranth-lang
<whitequark[cis]>
Yosys isn't growing much, for various cursed resasons I don't want to go into
<whitequark[cis]>
it's... expanding, but not growing
<whitequark[cis]>
as for formal, the only mode I see being supported is multiclock only smtbmc only without any sby being involved whatsoever (with Amaranth managing processes)
<whitequark[cis]>
Jannis knows my reasoning and broadly agrees with it, so it's not even a niche view
<Lunaphied[m]>
<whitequark[cis]> "as for formal, the only mode I..." <- Sorry I'm a bit long in memory on formal, the split between sby and smtbmc here is what again?
Maja has quit [Quit: No Ping reply in 180 seconds.]
<catlosgay[m]>
smtbmc is a particular formal verification engine, sby is a tool that wraps around it and other formal verification engines and provides a configuration format etc
<catlosgay[m]>
(smtbmc is distributed as part of yosys, it is a python script that wraps around the output of write_smt2 and calls into SMT solvers)
Maja has joined #amaranth-lang
d_olex has joined #amaranth-lang
d_olex has quit [Quit: Leaving]
d_olex has joined #amaranth-lang
d_olex has quit [Remote host closed the connection]