kristianpaul has quit [Read error: Connection reset by peer]
citypw has quit [Remote host closed the connection]
kristianpaul has joined #yosys
citypw has joined #yosys
Degi has quit [Ping timeout: 240 seconds]
Degi has joined #yosys
<awygle>
hm. how would i go about asserting "this state machine can't get stuck in any state but IDLE forever"?
<awygle>
i can think of a few ways but they feel hacky to me
<awygle>
(this is a question about formal verification in case that wasn't clear)
<awygle>
seems like i'd have to put a bound on it, instead of "forever", which is fine, i can do that math
<awygle>
but then i have to do like "assert state == idle or past state == idle or past past state == idle or......"
<awygle>
actually that's not too bad is it. just have a counter that gets reset when state is idle and assert it never gets above bound.
<awygle>
thanks rubber duck irc channel :)
az0re has quit [Remote host closed the connection]
emeb has joined #yosys
Forty-Bot has quit [Ping timeout: 240 seconds]
Forty-Bot has joined #yosys
<awygle>
hm either yosys is just doing whatever with this design or i've done something terribly wrong
<awygle>
probably the latter
az0re has joined #yosys
emeb_mac has quit [Quit: Leaving.]
emeb has quit [Quit: Leaving.]
mmicko has quit [Quit: leaving]
mmicko has joined #yosys
Asu has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
cr1901_modern has joined #yosys
cr1901_modern has quit [Ping timeout: 256 seconds]
cr1901_modern has joined #yosys
cr1901_modern has quit [Client Quit]
cr1901_modern has joined #yosys
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #yosys
cr1901_modern has quit [Client Quit]
cr1901_modern has joined #yosys
cr1901_modern has quit [Ping timeout: 256 seconds]
cr1901_modern has joined #yosys
cr1901_modern has quit [Client Quit]
cr1901_modern has joined #yosys
cr1901_modern has quit [Client Quit]
cr1901_modern has joined #yosys
cr1901_modern has quit [Client Quit]
cr1901_modern has joined #yosys
cr1901_modern has quit [Ping timeout: 246 seconds]
cr1901_modern has joined #yosys
<thardin>
awygle: use the induction, luke
cr1901_modern has quit [Ping timeout: 256 seconds]
<lambda>
awygle: proving liveness is kinda difficult in my experience, at least tooling-wise
<whitequark>
yosys does have some built-in support for proving liveness but i second what lambda says
<ZipCPU>
awygle: I'd use a counter. Clear the counter when you are in the idle state, otherwise add 1 per clock. Assert it stays below some value.
<ZipCPU>
The challenge is that either 1) your induction length now needs to be at least as long as the counters limit, or 2) you need to tie counter bounds to various FSM states
<daveshah>
Yeah I think only the more esoteric aiger solvers support liveness with symbiyosys
cr1901_modern has joined #yosys
fcserr has quit [Read error: Connection reset by peer]
cr1901_modern has quit [Ping timeout: 265 seconds]
cr1901_modern has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
cr1901_modern has joined #yosys
cr1901_modern has quit [Ping timeout: 244 seconds]
Asu has quit [Ping timeout: 244 seconds]
Asuu has joined #yosys
thoughtpolice_ has joined #yosys
y2kbugger_ has joined #yosys
ktemkin_ has joined #yosys
bubble_buster_ has joined #yosys
flammit_ has joined #yosys
benreynwar_ has joined #yosys
ric96_ has joined #yosys
gruetze_ has joined #yosys
lukego has quit [Ping timeout: 272 seconds]
ktemkin has quit [Ping timeout: 272 seconds]
ric96 has quit [Ping timeout: 272 seconds]
bubble_buster has quit [Ping timeout: 272 seconds]
flammit has quit [Ping timeout: 272 seconds]
benreynwar has quit [Ping timeout: 272 seconds]
unkraut has quit [Ping timeout: 272 seconds]
thoughtpolice has quit [Ping timeout: 272 seconds]
lambda has quit [Ping timeout: 272 seconds]
y2kbugger has quit [Ping timeout: 272 seconds]
Sarayan has quit [Ping timeout: 272 seconds]
cyrozap has quit [Ping timeout: 272 seconds]
gruetzkopf has quit [Ping timeout: 272 seconds]
whitequark has quit [Ping timeout: 272 seconds]
z0ttel has quit [Ping timeout: 272 seconds]
emilazy has quit [Ping timeout: 272 seconds]
ktemkin_ is now known as ktemkin
bubble_buster_ is now known as bubble_buster
benreynwar_ is now known as benreynwar
emilazy_ has joined #yosys
flammit_ is now known as flammit
y2kbugger_ is now known as y2kbugger
thoughtpolice_ is now known as thoughtpolice
ric96_ is now known as ric96
emilazy_ is now known as emilazy
maartenBE has quit [Ping timeout: 246 seconds]
cyrozap has joined #yosys
filt3r has quit [Ping timeout: 272 seconds]
filt3r has joined #yosys
lukego has joined #yosys
maartenBE has joined #yosys
lambda has joined #yosys
cr1901_modern has joined #yosys
gruetze_ is now known as gruetzkopf
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
ross_s has joined #yosys
AdamHorden has quit [Ping timeout: 256 seconds]
<ross_s>
Does yosys have any support for converting reals to bits? Looking at frontends/ast/simplify.cc I don't spot anything. Are there other methods if one wanted to generate a look up table of floating point values at synthesis time?
<awygle>
thanks for the suggestions everybody
<awygle>
i'm going with the counter approach (because the counter length is pretty easy to bound) but now my bounded model check seems to be taking impossible FSM transitions, so i gotta figure that out this morning
<awygle>
yosys formal won't recode my FSM states will it? i'm only doing `read_ilang` and `prep`
AdamHorden has joined #yosys
<awygle>
hm i updated yosys and now i get "unsupported cell type sdffe" errors. mwk is this related to https://github.com/YosysHQ/yosys/pull/1818/commits? gonna try checking out the version right before that
<awygle>
oh, helps to update sby, my bad
<mwk>
pretty much yes
<awygle>
works now (or, uh, fails to work in the same way as before the update). sorry to bother you :)
<mwk>
... and yeah, the formal won't do FSM recoding
<mwk>
(not that FSM recoding actually works all that often)
citypw has quit [Ping timeout: 240 seconds]
emeb has joined #yosys
kristianpaul has quit [Remote host closed the connection]
kristianpaul has joined #yosys
emeb_mac has joined #yosys
kristianpaul has quit [Ping timeout: 256 seconds]
kristianpaul has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]