<promach>
the 2^32 possible states will be whittled down to roughly 860k after 5k clock ticks, not 1-2. ==> I do not get this at all :(
<cr1901_modern>
I'm not sure I get it either... the solver is gonna figure out a large portion of those 2^32 states the counter can possible take aren't reachable, even for temporal induction.
pmezydlo has left #yosys [#yosys]
<ZipCPU>
cr1901_modern: The problem is ... all of those states are possible.
<ZipCPU>
Have you seen his code?
<cr1901_modern>
I can't prove it, but my gut feeling is that during even temporal induction (save for the first step), there's gonna be boolean identities the solver can use
<cr1901_modern>
to whittle down how many states that need to be manually checked.
<promach>
ZipCPU: give me some time to learn about BMC and temporal induction. have not finished all clifford presentation slides as well as video
<cr1901_modern>
ZipCPU: Actually I don't know at this point whether 2^32 states are checked. An interesting experiment for me would be to simplify the example down to a managable state >>
<cr1901_modern>
space to do induction by hand (using BV/UF and Array identities) and see what happens.
aw- has joined #yosys
<awygle>
ZipCPU: Symbiyosys is a front-end to all the formal verification Yosys can do, which includes some stuff ABC can do. At least if I'm interpreting the documentation correctly.
_whitelogger has joined #yosys
<awygle>
promach: can you share exactly the way that you're running your BMC?
<awygle>
running just the baud_generator module and using the yosys-smtbmc command line you provided upthread took 20 seconds to do 20010 steps on yices, 30 on z3
stoopkid has quit [Quit: Connection closed for inactivity]
<awygle>
promach: interesting. that takes _much_ longer than the module by itself, even though that module is the only one with asserts. on my hardware, i calculated it would take 17 minutes to finish BMC with yices, and more than an hour with z3. also, when i removed the --dump-vcd and the -g, yices finished all 20010 steps in 143 seconds.
_whitelogger has joined #yosys
aw-2 has joined #yosys
aw-1 has quit [Read error: Connection reset by peer]
aw- has quit [Ping timeout: 240 seconds]
<promach>
awygle: 17 minutes for Tx and Rx together ?
proteusguy has joined #yosys
proteus-guy has quit [Ping timeout: 248 seconds]
<awygle>
promach: whatever you had set up in there (Which looks like just Tx)
<awygle>
or no, i guess that does include Rx
<awygle>
at any rate i literally just typed "make". are you running on something particularly potato? this laptop is decent but nothing too special. could be a linux/cygwin thing but that usually goes the other direction
pie_ has quit [Read error: Connection reset by peer]
pie_ has joined #yosys
pmezydlo has joined #yosys
pmezydlo has quit [Client Quit]
pmezydlo has joined #yosys
<awygle>
promach: that looks like an old version problem to me too. Tried building from source?
<promach>
old version --> for yosys ?
<promach>
I have installed yosys-git today
<promach>
awygle
<awygle>
For yices
<promach>
let me do it then
<promach>
awygle: already upgraded yices to 2.5.4
<promach>
still same problem
<awygle>
promach: i'm not sure then :/. i will say that yices and yices-smt are different binaries on my system, neither is symlinked to the other
<promach>
awygle: problem solved by building yices from source rather than using pre-compiled yices-binary
<promach>
thanks
<awygle>
np, hope it improves things!
<promach>
yices is so much faster
digshadow has quit [Ping timeout: 260 seconds]
<awygle>
Does the noncommercial license of yices apply to the cores proved with it? Seems like it shouldn't... Just if you were to sell software that included it, right?
<thoughtpolice>
Yices 2 is under GPL now
<thoughtpolice>
As of version 2.5.3
<thoughtpolice>
(Boolector will also go from non-commercial to MIT in a future release as well, from what I've heard on the grapevine of twitter.)
digshadow has joined #yosys
<awygle>
Oh! That's cool
<awygle>
I suppose the question still applies though. If I prove a core with yices does it need to be GPL?
<thoughtpolice>
No, I don't believe so, anymore than if you use 'xargs' in your 'Makefile', does your project have to be under the same license as coreutils (GPL). However, you can also link to yices as a library, and obviously that would fall under the GPL. In general if you just feed yices a problem and ask for 'sat' or 'unsat', you don't really constitute a "derivative work" -- it's a property that really applies more to the *usage and
<thoughtpolice>
distribution of the source code*.
<awygle>
Yeah that was my belief too. See for example gcc.
<thoughtpolice>
Like, if you modified yices, and used your modified yices to prove things about your core and shipped that to commercial customers, that would also require you to release your changes to Yices to them, if they used it (e.g. to run verification themselves). It's a property about Yices source, and its usage, more than the input or output it takes/gives.
<thoughtpolice>
For compilers it's more complicated because they often 'insert' code into the code you give them. This is the reason for things like the Runtime Exception for GCC
nrossi has quit [Quit: Connection closed for inactivity]
pie_ has quit [Ping timeout: 248 seconds]
befedo has joined #yosys
eduardo_ has quit [Ping timeout: 246 seconds]
eduardo_ has joined #yosys
ekiwi has joined #yosys
pie_ has joined #yosys
befedo has quit [Read error: Connection reset by peer]
befedo has joined #yosys
Marex_ has joined #yosys
ekiwi has quit [*.net *.split]
qu1j0t3 has quit [*.net *.split]
promach has quit [*.net *.split]
Marex has quit [*.net *.split]
nurelin has quit [*.net *.split]
indy has quit [Ping timeout: 240 seconds]
befedo has quit [Quit: befedo]
indy has joined #yosys
promach has joined #yosys
pmezydlo has quit [Quit: Leaving.]
ekiwi has joined #yosys
qu1j0t3 has joined #yosys
nurelin has joined #yosys
marbler has quit [Ping timeout: 240 seconds]
jayaura has quit [Ping timeout: 240 seconds]
aynah[m] has quit [Ping timeout: 246 seconds]
pointfree1 has quit [Ping timeout: 264 seconds]
lok[m] has quit [Ping timeout: 264 seconds]
MatrixTraveler[m has quit [Ping timeout: 264 seconds]