<cr1901>
whitequark[cis]: Been distracted and haven't made the PRs to boolector yet
<cr1901>
Other than that, it should be ready for xfer
<whitequark[cis]>
ah ok! I'll do it shortly then
<cr1901>
Ack. And I'll take your ping as a signal to file those PRs rn
<cr1901>
I doubt they'll respond in a day
<cr1901>
the next step after this is to add support to yosys-smtbmc directly (*-smtbmc already works with a shell script wrapper called "boolector" which calls yowasp-boolector, but I'd rather have direct support)
<cr1901>
Between half and native. I don't remember the exact number/exact subset of tests I ran. Other than "it's definitely usable for RV Formal"
<whitequark[cis]>
btw, the reason setuptools_scm complains about the missing section is that you direct it to read that section by using Configuration
<cr1901>
Indeed, and setuptools_scm requires the Configuration parameter in the relevant version (I did pdm add, should it be the same exact version of setuptools_scm you're using?)
<whitequark[cis]>
yep, i used the exact version so that it's all in sync
<cr1901>
There's no good reason I need the setuptools version I used. I just did "pdm add" and didn't think of it much :P.
<whitequark[cis]>
hm, publishing doesn't work because the versions of the dependencies are .dirty (since they're patched)
<cr1901>
I'm fine w/ having ppl installing a git dep until upstream gets back to me
<cr1901>
err, that came out more forceful than intended
<whitequark[cis]>
you can't publish a +dirty package to pypi
<whitequark[cis]>
it's not a legal version
<cr1901>
I understand. So hold off on publishing until boolector upstream gets back, so the patches can be removed
<cr1901>
(also, wtf? Why does it treat non-python code as dirty?)
<whitequark[cis]>
huh?
<whitequark[cis]>
you wrote the code that generates a +dirty version, in setup.py
<cr1901>
Aaaaargh, if submodules are dirty, all the code is dirty
<cr1901>
I forgot about that
<whitequark[cis]>
that too but you also explicitly check for one of the submodules
<cr1901>
Perhaps "if upstream_git.dirty or package_git.dirty" should be "if package_git.dirty:", and I did a bad copypaste job from nextpnr
<cr1901>
oh right, that still won't work b/c of the submodules
<whitequark[cis]>
that doesn't work since submodules being dirty counts as the root being dirty
<cr1901>
I... think I'm stuck between a rock and a hard place here until upstream gets back?
<cr1901>
It's no worse than my idea (depend on my fork of boolector/btor2tools)
<whitequark[cis]>
can you check that that package works for you?
<whitequark[cis]>
why do you import importlib_resources? it's never used
<cr1901>
Every single question you have can be answered by "because I copied the scaffolding from nextpnr and yosys to get something working, and once I got it working, my brain shut off"
<whitequark[cis]>
right
<cr1901>
I am testing now, but I want to bench against native boolector
<whitequark[cis]>
oh, there's platformdirs 4.0
<whitequark[cis]>
the hell they incremented a major for
<whitequark[cis]>
> UNIX: revert site_cache_dir to use /var/cache instead of /var/tmp
<cr1901>
Isn't there a Standard about Filesystem Hierarchies that should be followed?
<tpw_rules>
looks like they had the linus problem
<cr1901>
whitequark[cis]: Right now I'm running the reg_ch0 test, which is the test that takes longest, with boolector native. This will take about 15 minutes.
<cr1901>
Once that's done, I'll have yowasp-boolector masquerade as the native one (via a shell script) and time that too
<cr1901>
(or it took 4 minutes native. Guess I misremember)
<cr1901>
Native: real 4m4.204s user 4m2.801s sys 0m1.340s
<whitequark[cis]>
looks like sby uses btorsim after all
<whitequark[cis]>
oh wait, btor is not boolector
<cr1901>
That's not for the smtbmc engine though
<cr1901>
btor is a file format IIRC
<whitequark[cis]>
ah
<whitequark[cis]>
where does boolector even get called
<cr1901>
We're up to 22 mins for yowasp-boolector. I promise that when I tested it before tonight, I made sure that rv formal tests completed in reasonable time.
<cr1901>
in yosys/backend/smtio.py
<cr1901>
(not sby)
<whitequark[cis]>
oh right
<whitequark[cis]>
cr1901: might be because of picosat vs minisat
<cr1901>
It's definitely possible. I know I didn't use picosat for the Linux build.
<cr1901>
But to reiterate, I _did_ test before tonight w/ PicoSAT, before even announcing the repo. Unfortunately, I don't remember which tests I ran other than I was satisfied w/ the perf
<cr1901>
Oh My God... I think I know what happened
<cr1901>
I think picosat's shell script didn't match "[s]ccache gcc" to gcc, and didn't enable optimizations
<whitequark[cis]>
it's totally irrelevant which license Yosys is covered by, you're packaging boolector
<whitequark[cis]>
please, do not turn your brain off the moment you get anything workng.
<whitequark[cis]>
you actually didn't put any license in the repo, too
<cr1901>
I ran an alternate set of tests... boolector w/ unoptimized (?) picosat took real 13m35.966s, user 13m43.592s, sys 0m0.918s
<whitequark[cis]>
I think I'm going to ask you to go through every change I've made to the boolector repo, and then pair with sporniket on his yices2 repo to ensure I don't have to redo all this boilerplate again
<whitequark[cis]>
and I still need a license from you
<whitequark[cis]>
you should submit a PR to yowasp/boolector adding LICENSE.txt covering your changes, to make it unambiguously clear that consent was given
<cr1901>
Yea wrong link: https://boolector.github.io/. yosys is ISC, nextpnr is ISC, boolector is MIT. ofl is Apache. MIT should be fine.
<cr1901>
>sporniket on his yices2 repo <-- while I'd be happy to do that, I thought yowasp-yices stalled b/c of copious sjlj
<whitequark[cis]>
see the logs for today or yesterday
<whitequark[cis]>
that can be replaced with import paramiko
<cr1901>
All b/c I like all my imports at the top of the file
<whitequark[cis]>
the import statement in python can appear anywhere
<whitequark[cis]>
you only need importlib.import_module() if you don't know the name of what you're importing upfront
<cr1901>
Okay, so it's a "useless use of importlib"
<whitequark[cis]>
yea
<whitequark[cis]>
the effect is, I think, the same
<whitequark[cis]>
so now that i'm looking at this closely, yosys-smtbmc implements the actual logic and sby is pretty much just an overgrown makefile
<cr1901>
sby is a glorified select() loop
<whitequark[cis]>
awful
<cr1901>
I rewrote it to use async in 2019 before I fell ill, and well... the PR bitrotted/is still open
<cr1901>
Actually you suggested I rewrite it lmao
<whitequark[cis]>
yeah I don't think I properly understood how it worked back then
<cr1901>
yosys-smtbmc takes smt2 output from yosys (which is not useful by itself for running an SMT query), annotates it with the asserts/assumes/extra scaffolding to make it a useful problem for an SMT solver to solve, and then feeds the resulting string via stdin to each SMT solver it supports, taking care of CLI arg diffs
<whitequark[cis]>
alright, i'm now super glad i ripped out assertFormal out of Amaranth
<whitequark[cis]>
because i don't think Amaranth should be using sby at all, anymore
<whitequark[cis]>
i think it should be calling yosys-smtbmc directly and that's it
<cr1901>
yosys-smtbmc is not that bad IMO.
<whitequark[cis]>
it's more that sby is
<whitequark[cis]>
it's complex and opinionated and not especially well written
<cr1901>
If you call both my highlight commands in parallel, you got 90% of sby functionality (minus the "solver running X mins" and "time elapsed" stuff)
<whitequark[cis]>
yes
<whitequark[cis]>
why is sby_engine_aiger even a separate thing from sby_engine_smtbmc
<whitequark[cis]>
match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
<whitequark[cis]>
if match: proc2_status = "FAIL"
<cr1901>
b/c AIGER, AFAIR, is the only engine that supports s_eventually and friends in any form
<whitequark[cis]>
wtf is sby_autotune
<cr1901>
I don't know, I have a guess reading the docs why you'd want it
* whitequark[cis]
hisses at sby
<cr1901>
sby supports you running the same query w/ multiple solvers at the same time. There's a valid reason to do this; yices took 12 hours for me on a query that took 15 mins on boolector
<cr1901>
looks like autotune is "figure out ahead of time which engine is actually gonna be good for the current problem"
<cr1901>
I have, in practice, never used multiple solvers at once. z3 is rarely better than yices, yices is good in general, performs badly on rv-formal
<whitequark[cis]>
so it looks like for yowasp (js), it is enough to somehow be able to run yosys-smtbmc and the engine
<cr1901>
yowasp-boolector perf is all over the place. For some rvformal test I got "pretty close to native speed" (72 secs vs 54 secs), I got ~40% earlier, and the test I originally ran seems pathologically bad (1 hour in and still running; took 4 mins w/ native)
<cr1901>
(pathologically bad test is "rvformal test that I remember taking the longest out of all of them")
<cr1901>
I could've _sworn it took ~15 mins native, but nope. Tonight it took 4.
<cr1901>
It's 1:30AM. The stream VOD I was watching while making PRs and benchmarking has ended. I'm gonna let it keep running and get some sleep. I'll rebuild native boolector w/ picosat when I get the chance and see what happens.
notgull has quit [Ping timeout: 256 seconds]
_whitenotifier has quit [Ping timeout: 268 seconds]
cr1901 has quit [Ping timeout: 256 seconds]
cr1901 has joined #amaranth-lang
<tpw_rules>
to support register arrays, could the action construction be deferred instead of introducing additional types?
<tpw_rules>
maybe at csr.reg.RegiserMap.freeze(). that might require/recommend additional internal types though
<whitequark[cis]>
we do need to consider both API ergonomics and how predictably it operates, here
<tpw_rules>
or maybe some sort of .clone function which reaches back down the tree and re-constructs the actions and returns new maps/arrays/registers
<whitequark[cis]>
absolutely not.
<whitequark[cis]>
that is not something that will ever be a part of a public interface of any part of Amaranth
<tpw_rules>
the ergonomics are what i'm getting at, the prospect of splitting up maps and arrays and stuff into even more types is a lot
<tpw_rules>
which is?
<whitequark[cis]>
deep cloning
<whitequark[cis]>
I am also not sure why are you discussing actions and not registersm
<whitequark[cis]>
s/registersm/registers?/
<whitequark[cis]>
register arrays involve instantiating several registers; what those registers do afterwards exists on a level below
<whitequark[cis]>
we do need a data structure, at least internally, that captures the fact that indexed access to the registers is possible
<tpw_rules>
my thought is the only reason you can't add the same register to a map twice is that it would end up with the same actions
<tpw_rules>
i guess it does have the component behavior too
<whitequark[cis]>
why would you want to add the same register to the same map twice? you are describing several different registers
<whitequark[cis]>
(which have the same interface, sure)
<whitequark[cis]>
we do need a RegisterArray and it will have to check that the registers do actually have the same interface, probably by grabbing their metadata and ensuring that exactly matches (otherwise you'd have a hard time generating a BSP with array access in it)
<tpw_rules>
that's true, you would be accessing each one independently in your logic
<tpw_rules>
actually i'm not sure with the implementation as it stands, can you construct the same csr.Register subclass twice and get different field action instances?
<tpw_rules>
looks like yes
<whitequark[cis]>
also, register arrays are relatively uncommon. we need to not pessimize ergonomics of the more common cases, but this particular one doesn't have to be as light as possible
<whitequark[cis]>
tpw_rules: you can subclass a register with arbitrary code
<tpw_rules>
ok, that pessimization is what i was worried about
<whitequark[cis]>
there are ways to accidentally end up with a varying interface too, which we should catch
catlosgay[m] has joined #amaranth-lang
<catlosgay[m]>
sby is not just a wrapper over smtbmc, it also wraps over other backends, like alternate btor solvers (btor is a word level model checking format) like pono and alternate aig solvers (aig being the bit level model checking format, and thus unsuitable in particular for anything with arrays in) like abc. sby is a bit of a pain to work with, but im not sure smtbmc is a particularly amazing solution. smtbmc is generally slower than
<catlosgay[m]>
all the other model checkers, and it doesnt even implement a complete proof procedure (there are some problems that smtbmc's k-induction engine can never prove, and making it complete while easy trivial is a bit of a pain given smtbmc is a glorified templating engine over the smtlib statements)
<catlosgay[m]>
smtbmc only implements bmc/k-induction, whereas the more modern (13 years old now) IC3/PDR technique is often much faster at getting proofs, e.g. i have some problems that smtbmc cant solve in any reasonable timeout but abc's pdr engine solves quickly
<tpw_rules>
what i'm saying is can i do self.my_regs = [Reg() for _ in range(4)] and have that work as expected, i.e. have them be four independent things. for sure Reg's constructor could do something to break this but it can't in a default/rfc sanctioned case
<tpw_rules>
and it looks like it's safe
<catlosgay[m]>
actually when i say smtbmc is generally slower than the others, that isn't always true, it will do better on things that benefit from it using word level SMT solvers than the bit level aiger solvers, and is reasonable as a bounded model checking engine (all the word level bounded model checking engines are basically the same)
<catlosgay[m]>
* the same modulo the smt solver they use)
<cr1901>
What irony that boolector converts it back to a SAT problem, and yet it's the fastest for rvformal
<whitequark[cis]>
catlos.gay: i avoid actually using formal because it's full of poorly made tools, performance cliffs, opaque behavior, and in general i've never felt that it's worth the time invested in it
<catlosgay[m]>
i mean it does more than that, boolector does this whole lemmas on demand thing where it lazily instantiates array and EUF stuff. all SMT solvers use SAT at their core, and basically every modern SMT solver eagerly encodes bitvectors to SAT (with some rewrite rule etc based preprocessing)
<catlosgay[m]>
catherine: yeah i totally get that, open source formal tools are frustrating to use, and most of the academic tools are impossible to even get to build. commercial formal tools, while they have their issues, are generally much more usable
<whitequark[cis]>
so the fact that smtbmc is a bit more usable is important, because it doesn't make the flow hugely less powerful (to me) while making it nontrivially less frustrating (to me)
<catlosgay[m]>
yeah thats very fair
<cr1901>
>IC3 >Incremental Construction of Inductive
<cr1901>
Clauses for Indubitable Correctness
<cr1901>
They need to hire a repairman for that acronym
<cr1901>
It does the same thing as k-induction, but more efficiently?
<catlosgay[m]>
it actually got renamed to PDR (property directed reachability) when implemented in abc for reasons, and now everyone calls it one of those two. the same in that it produces unbounded proofs yes, the actual manner in which it does it is slightly different. the rough idea is that it builds up an inductive invariant (boolean formula) implying the property that holds in the initial state, and if it holds in any given state, it also
<catlosgay[m]>
holds in the next
<catlosgay[m]>
(this is perhaps not the channel for an in depth description of these things haha)
<cr1901>
I don't think there's an ##smtsolvers channel
<cr1901>
but I didn't check
<cr1901>
Seeing as I don't know how to list channels in hexchat lmao
<whitequark[cis]>
eh it's a weekend, it's not like we're busy with anything else
<catlosgay[m]>
im on the 1b2 discord link rather than irc, but im not aware of any public forums for the discussion of model checking/smt at all haha, all my discussions have been at work/with academics/random interested parties
<cr1901>
catlosgay[m]: /join ##smt, apparently
<cr1901>
ahhh
<whitequark[cis]>
i'd really like better FV tooling to be available
<cr1901>
I don't think the current tooling is worthless (it has found several bugs for me, not just in rvformal context)
<catlosgay[m]>
i have a lot of thoughts/plans on how to do this, but unfortunately not the time/money to work on it atm. im expecting to start a phd working on security model checking stuff towards the end of the year and the thought of having to implement my ideas on top of basically any of the existing open tools makes me sad
<cr1901>
catlosgay[m]: It says you're on Matrix (the "[m]" after your name)?
<catlosgay[m]>
i guess an artefact of however the bridges are connected together? no clue
Hoernchen has left #amaranth-lang [Leaving]
<catlosgay[m]>
https://gist.github.com/georgerennie/0aed5dd3e42add972471f692ed746d60 if you wanna read more about model checking stuff i have a file full of notes about what i would like to see in a formal environment and papers about techniques (unfortunately not really catalogued, its just a load of links)
<cr1901>
whitequark[cis]: Currently trying native boolector w/ picosat as a comparison point. yowasp-boolector completed correctly, but the time was... bad, to say the least.
<catlosgay[m]>
picosat is 23 years old now so i would imagine not particularly performant, if you can use minisat instead it is probably better
<catlosgay[m]>
wait thats the satellite of the same name lmao
<catlosgay[m]>
either way its early 2000s
<catlosgay[m]>
iirc
<cr1901>
The native boolector is build w/ lingeling I think. But I don't remember why I couldn't get it to build in WASM (picosat was my _third_ choice)
<whitequark[cis]>
cr1901: if tooling finds bugs for me but also turns interacting with the project into an acutely miserable experience it can be worse than worthless
<whitequark[cis]>
i'm not necessarily saying sby is definitely that, but also there's a reason i basically never use it
<whitequark[cis]>
and i've actively avoided touching anything where it seemed like the way towards correctness would be to use FV tooling, instead considering all the other ways in which i could demonstrate correctness
<whitequark[cis]>
boneless isn't updated for years lol
<whitequark[cis]>
because the next step would be to make it pipelined and I was planning to use sby to prove equivalence and every time I contemplate that I think of all the other painful things I could do instead which would be more tolerable
<whitequark[cis]>
I think it's probably easier if you use FV tooling with a "frontend" like rv-formal where you don't actually write proofs, you just apply existing proofs to your DUT, because that has quite fewer ways in which it can go painfully wrong
<whitequark[cis]>
> But I don't remember why I couldn't get it to build in WASM
<whitequark[cis]>
I am very fond of writing things down :p
<cr1901>
I have a notebook. I should use it more often
<whitequark[cis]>
> i guess an artefact of however the bridges are connected together? no clue
<whitequark[cis]>
yes, the bridges go like irc <> matrix <> discord. so discord users appear to irc users as if they are on matrix (well, they are, but not natively)
<cr1901>
catlosgay[m]: Yea, this is a good list. I think an sby-like driver would be best done w/ async (I don't think the language matters), so that way all the select() stuff is abstracted out
<whitequark[cis]>
I think the important bit about sby isn't whether it's using select or async or whatever
<whitequark[cis]>
(tbf it would probably work just fine with a thread per engine, and could be simpler in some ways too)
<whitequark[cis]>
I think it's that it does too much in a way that's coupled too closely
<whitequark[cis]>
there is no well defined interface of an "engine" and also except for smtbmc, you can't really use an engine outside of using sby
<whitequark[cis]>
what i mean is: sby_engine_aiger should have been something like yosys-aiger, and both it and yosys-smtbmc should've been talking to sby via a well defined protocol (in the loose sense of the word. a CLI is a protocol) so they're not coupled together
<cr1901>
I've only ever used the smtbmc part, but if what you're saying is correct, yea, that's bad IMO
<cr1901>
used/studied*
<whitequark[cis]>
I mean you can look at the source and see for yourself
<catlosgay[m]>
yeah i think theres a tight coupling between the sby format and the engines, but then at the other end, the information lost by going from yosys to smtlib is too loose a coupling. because smtbmc doesnt really reason about things as a netlist, but as a load of smtlib statements, which prevents it doing various useful things to improve performance
<catlosgay[m]>
with some previous work i was doing, i wanted to enumerate all the values for a given set of variables that lead to counterexamples, without having to reset the engines each time (as there is a lot of incremental information shared). i ended up having to write my own little model checker because smtbmc etc cant do that very easily
<whitequark[cis]>
catlos.gay: yeah, yosys-smtbmc isn't that good of a way to slice things either! i'm not saying it's well designed, i'm just saying that it's *more usable*, mostly by virtue of being smaller
<catlosgay[m]>
oh yeah i mean from the perspective of just getting verification done, smtbmc is fine and more usable. its just if you start wanting to check weirder things, or do stuff the fancy model checkers do like putting properties proofs on different threads but sharing information between them etc, the smtbmc architecture will never really scale well to that
<whitequark[cis]>
my view of what the root cause is is that there's no political will nor resources to put thought upfront into FV tool architecture, instead they are just an amalgamation of things that were cool at one point or a customer wanted at another
<whitequark[cis]>
this has been a general problem with yosys (the verilog frontend is probably the apex of it). it has been slowly changing in the last few years, and some things were engineered decently well, though often at the cost of someone burning out and leaving
<whitequark[cis]>
which isn't really the way to go either
<whitequark[cis]>
the new "yosys witness trace" (yw) format is definitely a step in the right direction
<catlosgay[m]>
yeah, outside of smtbmc theres also a lot of the academic effect of things only get developed if you can get a publication out of it and abandoned after phd. AVR is (supposedly) the best performing open source model checker atm but i advise everyone against using it cos its difficult to get to build/setup and the codebase is entirely unreadable
<whitequark[cis]>
for sure
<whitequark[cis]>
that's how the original verilog parser was written, according to claire (iirc), and then it just kept being extended well past the point when it was whatsoever maintainable
<catlosgay[m]>
yeah thats the other thing, academic tools have had the btor format for problems/witnesses for a while, but theres never been an easy way to get a btor witness back into like a vcd that people can use for actual verification. again its just a political will thing, and a mismatch between what different communities want/need
<cr1901>
Pretty sure yosys-witness can convert to btor (and back?)
<whitequark[cis]>
incidentally, i realized recently that i can fairly easily add javascript support to yowasp's yosys-witness and yosys-smtbmc, using this: https://github.com/bytecodealliance/componentize-py
<cr1901>
I'm sorry, can only convert _from_ btor
<whitequark[cis]>
which turns a python file into a wasm file by concatenating it with a python interpreter built for wasi :D
<catlosgay[m]>
cr1901: yeah it can, but adding more layers of converters between things doesnt make a great experience for users
<cr1901>
The only thing I'd add to your list is that "users should be able to inspect all the intermediate files if they wish". This is the big reason I was able to learn yosys-smtbmc successfully. I don't want only an opaque blob.
<catlosgay[m]>
cr1901: yes inspecting intermediate steps is fair. i have some academic stuff (that i cut off the bottom of that list sorry) i have been working on about viewing the whole model checking process as a series of abstractions and invariant strengthening. this naturally admits model checking as producing a series of related circuits, each refined until the last one can be proven correct easily. my interest in this is for using it to
<catlosgay[m]>
generate witness circuits so proofs can be checked for correctness, but the bookkeeping needed to do this would also allow you to extract those intermediate steps and see how things relate
<catlosgay[m]>
i believe boolector will just pick one sat solver
<cr1901>
ack
<cr1901>
FWIW, I've only used witness files to make my unit tests better. I don't understand how they're used for proofs other than "a witness file is generated as a side effect that your proof failed"
<cr1901>
which you can then examine to auto-generate a test-case without having to run all the damn proof machinery again.
<cr1901>
yosys-smtbmc's intermediate files include the --dump-smt2 option, which will write to file "the smt2 string it sends to the stdin of the solver". I studied those files for a while, and honestly, understand the smtbmc source code was much easier after that.
<cr1901>
whitequark[cis]: Yea, it's picosat that's the problem. I'll look into adding more SAT solvers. When I add more, will it hurt anything to keep picosat in (boolector will default to e.g. cadical if it exists), or is it a waste of bits?
<whitequark[cis]>
I don't know how to answer that
<whitequark[cis]>
do you expect anybody using the package to opt into using picosat? if not, it's a waste of bandwidth
<cr1901>
Looks like you answered it just fine. Realistically, no, I don't expect people to care if it's gone.
<whitequark[cis]>
then feel free to rip it out
<whitequark[cis]>
it can always be restored from git history if there ever exists a reason to care
* cr1901
nods
<catlosgay[m]>
cr1901: in this case im talking about witness circuits/proof witnesses. When the solver finds a trace, it produces a trace witness like you have seen, but if the solver tells you there are no counterexamples, how do you verify that it actually gave the right result (model checkers can be complex beasts)? the idea is that it produces a proof witness which is a way for the model checker to communicate to a proof checker the
<catlosgay[m]>
relevant facts it learnt to prove the property correct. the proof checker can then verify that those facts actually imply that the proof is true (the proof checker is also generally much simpler than the original model checker). This is really of particular interest to tool developers for improving correctness rather than end users, but could be useful if you think you are getting incorrect results from the model checker. a
<catlosgay[m]>
similar idea is very common in the SAT world, and the SAT competition has required solvers to produce proofs for quite a few years now.
<catlosgay[m]>
emily yu's from jku's phd thesis over the last few years develops quite a bit of theory around this stuff for the case of k-induction and preprocessing, but ive been trying to generalise it to arbitrary abstraction/preprocessing techniques
<cr1901>
I think this is a bit beyond me. My current understanding of this stuff is "If you asked me to explain the input to the SMT solver that yosys-smtbmc emits, I could do so in a blog post for both bmc and k-induction"
<cr1901>
(In fact, that's a blog post I want to do)
<catlosgay[m]>
thats fair enough, the high level idea is answering questions like "yosys-smtbmc says the circuit is k-inductive for k=10, how do we check that that is true (whilst relying on trusting as little software as possible), and what extra information could yosys-smtbmc give us to help us check"
<cr1901>
Is there a (gentle) intro paper you could send me to read?
<cr1901>
.oO(Should a symbiyosys alternative be called "meiyosys")?
<cr1901>
(like "meiosis", which is like mitosis, Except Not)
<whitequark[cis]>
heh
<cr1901>
Okay with picosat, boolector native took 147m... vs 180m for yowasp-boolector. This is a much more reasonable comparison- wasm is ~80% of native speed
<whitequark[cis]>
with minisat?
<cr1901>
I need to still build that and get back to you. Previous msg was meant to supercede all other benchmarks thus far as "not a fair comparison"
<whitequark[cis]>
no, I mean, picosat is what is currently in yowasp/boolector, and what was in the repo you gave me originally
<whitequark[cis]>
so I don't understand what's different
<cr1901>
ooooh, I recompiled native with picosat only (the default solver on my native copy was to use cadical
<whitequark[cis]>
oh, I see
<cr1901>
nothing is different in yowasp, I just wanted to know for certain whether the problem was picosat (yes). I get reasonable performance on some rvformal tests w/ picosat, but this particular test (reg_ch0) is Just Plain Bad w/ picosat. Guess it's fortunate I found the problem sooner rather than later.
FFY00 has quit [Remote host closed the connection]