Kamilion has quit [Quit: I am kamilion. But you knew that, didn't you.]
citypw has joined #yosys
Kamilion has joined #yosys
_whitelogger has joined #yosys
PyroPeter has quit [Ping timeout: 264 seconds]
vonnieda has joined #yosys
PyroPeter has joined #yosys
tlwoerner has quit [Ping timeout: 245 seconds]
tlwoerner has joined #yosys
dys has quit [Ping timeout: 244 seconds]
citypw has quit [Ping timeout: 258 seconds]
m4ssi has joined #yosys
rohitksingh_work has joined #yosys
proteusguy has joined #yosys
rohitksingh_work has quit [Ping timeout: 272 seconds]
vonnieda_ has joined #yosys
vonnieda has quit [Ping timeout: 276 seconds]
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
citypw has joined #yosys
emeb_mac has quit [Ping timeout: 245 seconds]
jakobwenzel has quit [Remote host closed the connection]
jakobwenzel has joined #yosys
Wolf481pl is now known as Wolf480pl
citypw has quit [Ping timeout: 244 seconds]
AlexDaniel has quit [Ping timeout: 246 seconds]
AlexDaniel has joined #yosys
rrika has quit [Ping timeout: 245 seconds]
rrika has joined #yosys
<somlo>
daveshah: I'm going to start bisecting yosys with good=c907899, bad=dd8d264; If you think there's a less labor-intensive way to go about this, please feel free to interrupt me :)
<daveshah>
I think I've found the problem now
<daveshah>
I'll know in a minute
<somlo>
oh, cool, thank goodness :)
<somlo>
if/when there's anything I could test, happy to do so
<daveshah>
somlo: Yup, that looks to have fixed it
<somlo>
awesome! I just downloaded the patch, building yosys with it now...
<ZirconiumX>
I must not understand SAT very well, because according to Yosys just proved that a design is not equivalent to itself and caused a logic bomb
<ZirconiumX>
s/just/I just/
<daveshah>
Probably related to register initial values
vonnieda_ has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
emeb_mac has joined #yosys
rohitksingh has joined #yosys
voxadam has quit [Read error: Connection reset by peer]
<tpb>
Title: D flip-flop with asynchronous reset · GitHub (at gist.github.com)
<daveshah>
promach: because you don't constrain the initial DFF state, starting at 1 and then asserting reset in the next cycle is enough to cover it
<daveshah>
never mind, I misread, you don't even have q in the cover
<daveshah>
so all you are covering is 3 unconstrained inputs and the clock
alexhw has quit [Ping timeout: 268 seconds]
alexhw has joined #yosys
adjtm has joined #yosys
<promach>
daveshah : huh ?
<promach>
I was asking for 30 steps
<promach>
not just 2 steps
<promach>
wait, I think I got it
<ZipCPU>
promach: That's not how cover works
<promach>
append
<promach>
try to cover within 30 steps
<promach>
I need to append
<ZipCPU>
The depth specified for "cover" in the sby file is how many steps the formal tool will search to find a way to make the cover() statement true
<promach>
yes
<ZipCPU>
append has a couple problems associated with its usage. I know one user covered a condition (X), and then appended 30 steps. He say condition (Y) take place in those 30 steps, yet his cover(Y) statement failed--because it wasn't in the initial depth.
<ZipCPU>
A second problem with "append" is that it tends to set all of the rest of the interaction to something fairly benign and typically useless.
<promach>
can we combine cover() and assume() ?
<ZipCPU>
You can. There are better ways of doing things though.
<promach>
what better ways ?
<ZipCPU>
For example, create a sequence and then cover the 9the step in that sequence: cover(sequence[8]). If any of what you would assume is ever not the case, reset the sequence.
<ZipCPU>
That way, you don't need to make assumptions about internal state, and your assumptions won't necessarily impact the rest of your design--just the cover() statement
rohitksingh has quit [Ping timeout: 248 seconds]
rohitksingh has joined #yosys
<promach>
but sequence is only supported in the verific version