promach_ has quit [Remote host closed the connection]
knielsen has quit [Ping timeout: 260 seconds]
ZipCPU|Laptop has quit [Ping timeout: 252 seconds]
knielsen has joined #yosys
dys has quit [Ping timeout: 268 seconds]
mbuf has joined #yosys
stoopkid has joined #yosys
awygle has quit [Remote host closed the connection]
awygle has joined #yosys
digshadow has quit [Ping timeout: 250 seconds]
pie_ has joined #yosys
awygle_ has joined #yosys
awygle has quit [Read error: Connection reset by peer]
awygle has joined #yosys
awygle_ has quit [Read error: Connection reset by peer]
digshadow has joined #yosys
proteus-guy has quit [Remote host closed the connection]
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 250 seconds]
stoopkid has quit [Quit: Connection closed for inactivity]
mbuf has quit [Ping timeout: 268 seconds]
mbuf has joined #yosys
<promach>
ZipCPU: I start to lose confidence in my code when it passes all BMC and temporal induction verification
<promach>
usuaally, when I code, it ended up with a lot of bugd
<promach>
bugs
pie_ has joined #yosys
digshadow has quit [Ping timeout: 240 seconds]
<cr1901_modern>
promach: And being skeptical is healthy! And I have the same issue re: bugs, and it took me a while before I was confident my proofs passed for the right reason (TM)
pie_ has quit [Ping timeout: 258 seconds]
pie_ has joined #yosys
sklv has joined #yosys
quigonjinn has quit [Ping timeout: 260 seconds]
pie_ has quit [Ping timeout: 268 seconds]
<ZipCPU>
The sad part of formal methods is that you may find yourself convinced to write your code twice--once to do it, once to prove it.
<ZipCPU>
If you find yourself doing that, promach, then you may find that you've just copied an error from one part of your code to another.
* ZipCPU
is feeling like the glass is half empty this morning. Full sarcasm is still waiting on more caffeine.
pie_ has joined #yosys
mbuf has quit [Quit: Leaving]
proteus-guy has joined #yosys
eduardo__ has quit [Remote host closed the connection]
stoopkid has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<promach>
is there any yosys-smtbmc parameter that could set the range of timestep for which vcd waveform is generated ?
quigonjinn has joined #yosys
<awygle>
promach: there must be because you can do it with symbiyosys, but I haven't been able to find it
pie_ has quit [Ping timeout: 268 seconds]
m_w has joined #yosys
sklv1 has joined #yosys
sklv has quit [Ping timeout: 248 seconds]
mbuf has joined #yosys
pie_ has joined #yosys
<ZipCPU>
Yaahhhh .... I'm just writing up the final report and I realized that an assume'ption was made when an assert was called for. Now nothing works. Argghh ...
mbuf has quit [Quit: Leaving]
pmezydlo has joined #yosys
m_t has joined #yosys
leviathanch has joined #yosys
<ZipCPU>
Recovered, whew!
<ZipCPU>
Finally posted: An examination of the wishbone bus, and how to formally prove that a wishbone bus master matches the specification!
nrossi has quit [Quit: Connection closed for inactivity]
digshadow has joined #yosys
sklv1 has quit [Remote host closed the connection]
sklv1 has joined #yosys
dys has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
dys has quit [Ping timeout: 250 seconds]
pie_ has quit [Ping timeout: 240 seconds]
sklv1 has quit [Ping timeout: 248 seconds]
sklv has joined #yosys
pmezydlo has quit [Quit: Leaving.]
m_t has quit [Quit: Leaving]
leviathanch has quit [Remote host closed the connection]