develonepi3 has quit [Remote host closed the connection]
azzizi has quit [Quit: Page closed]
azzizi has joined #yosys
emeb has quit [Quit: Leaving.]
emeb_mac has joined #yosys
promach_ has quit [Quit: WeeChat 2.1]
maartenBE has quit [Ping timeout: 240 seconds]
maartenBE has joined #yosys
leviathan has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
cr1901_modern has joined #yosys
ZipCPU has joined #yosys
cr1901_modern has quit [Ping timeout: 268 seconds]
cr1901_modern has joined #yosys
emeb_mac has quit [Quit: Leaving.]
AlexDaniel has quit [Ping timeout: 256 seconds]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
ZipCPU has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
GuzTech has joined #yosys
zetta has quit [Read error: Connection reset by peer]
zetta has joined #yosys
Guest72074 is now known as jayaura
xerpi has joined #yosys
AlexDaniel has joined #yosys
proteus-guy has joined #yosys
AlexDaniel has quit [Remote host closed the connection]
AlexDaniel has joined #yosys
<promach>
For https://i.imgur.com/dsuXWHl.png , what do you guys understand by the difference between safety and liveness verification ?
xerpi has quit [Quit: Leaving]
pie_ has quit [Ping timeout: 256 seconds]
ZipCPU has joined #yosys
develonepi3 has joined #yosys
promach_ has joined #yosys
AlexDaniel has quit [Ping timeout: 256 seconds]
pie_ has joined #yosys
ralu has quit [Ping timeout: 260 seconds]
<promach_>
ZipCPU awygle : what would you do if you are really stucked at induction ?
<ZipCPU>
I thought you just had it working the other day?
<promach_>
it is only for induction depth of 26
<promach_>
ZipCPU: now, I am at depth of 10
<ZipCPU>
Why is 10 better than 26?
<promach_>
it prompts for more assert()
<promach_>
which will uncover some of the deepest bug
<cr1901_modern>
promach_: If you've proven induction for 26, _as well as_ bounded model check for 26, then you've proven that asserts hold for all time
<promach_>
design bug
<ZipCPU>
cr1901_modern: +1
<promach_>
cr1901_modern: but what if my CLOCKS_PER_BIT is 8
<ZipCPU>
... and .... ?
<promach_>
ZipCPU: no, 26 is not enough
<ZipCPU>
Why not? Somethings require longer induction depths to be successful.
<cr1901_modern>
decreasing the induction length may make it _completely impossible_ for the design to pass temporal induction
<promach_>
shorter the induction depth, the better it is
<cr1901_modern>
(without adding a bunch of assumes that make your asserts meaningless)
<ZipCPU>
promach_: Not true. That's an application dependent thing
<promach_>
ZipCPU: what is your induction depth for your UART ?
<ZipCPU>
120
<promach_>
huh ?
<ZipCPU>
Yes.
<promach_>
what about your CLOCKS_PER_BIT ?
<ZipCPU>
16
<cr1901_modern>
I wish I had time to create a graphviz example showing this, but basically...
<promach_>
ZipCPU: try decrease induction depth for your UART
<cr1901_modern>
promach: if your induction step fails, that doesn't mean that your design can actually _reach_ that state
<promach_>
cr1901_modern: maybe
<cr1901_modern>
If you choose a larger induction step that _eventually_ passes, that's a hint that _possibly_ the induction step was failing at an unreachable state from reset.
<promach_>
I already the same reset for both Tx and Rx
<promach_>
I already had the same reset for both Tx and Rx
<cr1901_modern>
promach: i.e. if induction step of 10 fails, but induction step of 26 passes (in your example), that's a _hint_ that the induction step of 10 was failing in a way that your design _can't reach from reset_
<promach_>
ZipCPU knew this fact regarding the reset quite well
<cr1901_modern>
promach_: I don't care that you had the same reset for both Tx and Rx. It's irrelevant here.
<promach_>
cr1901_modern: you mean the induction counter-example is not reachable in reality ?
<cr1901_modern>
promach_: Correct. The induction counter-example (for induction step 10) is not reachable in reality b/c you've proven your design for BMC=26 and induction=26
<promach_>
hmm... I am not really convinced with my own source code yet
<cr1901_modern>
promach_: You proved that BMC passes for =26, right?
<promach_>
yes, actually it had passed BMC=11 , inducton=11
<cr1901_modern>
Alright, that's good too (BMC=11, induction=11 gives you the same information as BMC=26, induction=26)
<promach_>
sorry, BMC should be more
<cr1901_modern>
well, it needs to be greater-than-or-equal-to
<promach_>
actually I ran my BMC for 200 steps before I stop it
<promach_>
I am more worried regarding induction than BMC
<cr1901_modern>
promach_: Let's pretend you _only_ ran your design for induction=10
<cr1901_modern>
No BMC
<cr1901_modern>
So you don't know _any_ info about BMC
<cr1901_modern>
can you pretend that for a second?
<promach_>
ok, I will let you continue
<cr1901_modern>
induction failed for step=10. That doesn't tell you whether that failing state is actually reachable. It _may_ be, it _may not_ be.
<cr1901_modern>
If you keep increasing the induction length, and you eventually find an induction length that passes, that tells you >>
<cr1901_modern>
That the failing state for induction length=10 isn't actually reachable if BMC passes for the greater induction length
<cr1901_modern>
I.e. suppose you find induction length=11 passes
<cr1901_modern>
if you do BMC=11, and that _also_ passes, that guarantees that the induction failure for step=10 isn't reachable
<cr1901_modern>
_This_ is why it isn't all that important to keep decreasing induction length after you find that your design passes
<promach_>
no, you don't just do BMC=11 , that amount of BMC does not make sense
<cr1901_modern>
Why don't you think it makes sense?
seldridge has joined #yosys
<promach_>
BMC=11 is so little info
<cr1901_modern>
Doesn't matter as long as it's greater than or equal to induction length! :)
<promach_>
BMC=11 gives so little info about the system
<cr1901_modern>
You can mathematically _show_ it doesn't matter
<cr1901_modern>
BMC just needs to be greater-than-or-equal to your induction length to prove that your asserts hold for all time (when BMC and induction _both_ pass)
<promach_>
you mean maths relationship between induction length and BMC length ?
<cr1901_modern>
yes
<promach_>
how do you come up with such maths relationship ?
<cr1901_modern>
promach_: Well, by drawing graphs of contrived state transistions for _simple_ designs on paper, and graphically doing BMC/induction, and convincing myself it works.
<promach_>
huh ?
<cr1901_modern>
promach_: If I had time to draw an example, I would. But unfortunately I don't
<cr1901_modern>
promach_: Basically, to convince myself of the maths relationship, I drew lots of pictures.
<promach_>
do you still keep one of those pictures of yours ?
<promach_>
;)
<promach_>
I suppose all those paper went to dustbin ;)
<cr1901_modern>
promach_: No, and I want to create an example digitally and post it online as a blog post, but no time (and bad software) means I haven't had time to do it
<cr1901_modern>
Until I get to that blog post, just trust me that BMC needs to be greater-than-or-equal-to your induction length to prove that your asserts hold for all time
<ZipCPU>
promach_: Got to run ... but I cannot decrease the induction depth. The proof would fail if I did, and I have no way to fix it.
<promach_>
ZipCPU: what do you think about my UART coding ? is it bug-free enough in your perspective ?
<cr1901_modern>
ZipCPU: We're you there the whole time watching me wing it :P?
<promach_>
cr1901_modern : your blog post will supplement clifford proof engine ;) take your own sweet time to create one such blog post ;)
<ZipCPU>
cr1901_modern: No, I wasn't ... I'm back reading now before powering off.
<awygle>
promach_: not only am I uninterested in trying to push my induction depth towards zero, I've almost convinced myself that it's fine to run other proof engines which don't take so much fiddling to reach a QED. But I haven't worked on formal in months so I haven't been able to really follow up that line of thinking
<ZipCPU>
promach_: If you want to convince yourself of what cr1901_modern was sharing, google "k-induction"
<promach_>
ok
seldridge has quit [Ping timeout: 240 seconds]
<promach_>
I just listened to a webinar by someone modifying ic3
<azzizi>
Hello! has anybody written any pass in any other language than c++?
develonepi3 has quit [Remote host closed the connection]
sklv1 has joined #yosys
sklv has quit [Ping timeout: 250 seconds]
<daveshah>
azzizi: c++ is I think the only real option right now, although in a few months there might be some Python bindings
<awygle>
you are however free to write your own script which consumes and emits any of the yosys netlist formats, which is sort of like a pass, if you squint
<daveshah>
I suppose if you have a language that can link with C++ then you can write a Yosys pass with that and even load it as a shared library using the module system
<daveshah>
But good luck debugging that...
emeb_mac has joined #yosys
<ZipCPU>
LUT statistics for a fully pipelined 15-stage CORDIC on an ice40: 2416
<ZipCPU>
LUT statistics for a non-pipelined version: 500
<ZipCPU>
Hmm ... if your design doesn't need high speed, you probably want the non-pipelined version.
<sorear>
What precision? Does it use rams?
<ZipCPU>
The second one uses a block RAM, yes.
<ZipCPU>
The output precision is about 12 bits.
<ZipCPU>
The block RAM is used for the cordic angles, though, not for any initial RAM based approximation. That's still a viable method that might compete with a CORDIC depending upon your needs
<ZipCPU>
Oh, and both cases above used 19-bits of phase information. That's not something you could easily look up in a table.
<ZipCPU>
Why 19-bits? It was the example I had lying around that so that I could do a comparison with it.
ZipCPU has quit [Ping timeout: 240 seconds]
<azzizi>
I had a question .........can I create a script using matlab or any other language and create a modified RTLIL and can Yosys work with that ? I mean can I input the modified RTLIL ?
<daveshah>
azzizi: yes, of course, but I personally wouldn't want to try and parse and generate RTLIL in Matlab
<daveshah>
Probably be faster to learn C++
<daveshah>
The relevant command is read_ilang though
<daveshah>
The Json format is also worth looking into as a way of processing designs in another language
dys has quit [Ping timeout: 256 seconds]
pie_ has joined #yosys
danieljabailey has quit [Ping timeout: 265 seconds]