| *** tpb has joined #yosys | 00:00 | |
| *** develonepi3 has quit IRC | 00:04 | |
| *** azzizi has quit IRC | 00:16 | |
| *** azzizi has joined #yosys | 00:17 | |
| *** emeb has quit IRC | 01:06 | |
| *** emeb_mac has joined #yosys | 01:24 | |
| *** promach_ has quit IRC | 01:45 | |
| *** maartenBE has quit IRC | 02:25 | |
| *** maartenBE has joined #yosys | 02:25 | |
| *** leviathan has joined #yosys | 04:46 | |
| *** cr1901_modern has quit IRC | 05:25 | |
| *** cr1901_modern has joined #yosys | 06:07 | |
| *** ZipCPU has joined #yosys | 06:22 | |
| *** cr1901_modern has quit IRC | 06:36 | |
| *** cr1901_modern has joined #yosys | 07:00 | |
| *** emeb_mac has quit IRC | 07:05 | |
| *** AlexDaniel has quit IRC | 07:16 | |
| *** pie_ has joined #yosys | 07:28 | |
| *** pie_ has quit IRC | 07:42 | |
| *** ZipCPU has quit IRC | 07:51 | |
| *** pie_ has joined #yosys | 08:02 | |
| *** GuzTech has joined #yosys | 08:09 | |
| *** zetta has quit IRC | 08:22 | |
| *** zetta has joined #yosys | 08:22 | |
| *** Guest72074 is now known as jayaura | 09:08 | |
| *** xerpi has joined #yosys | 10:12 | |
| *** AlexDaniel has joined #yosys | 10:28 | |
| *** proteus-guy has joined #yosys | 10:36 | |
| *** AlexDaniel has quit IRC | 10:45 | |
| *** AlexDaniel has joined #yosys | 10:45 | |
| promach | For https://i.imgur.com/dsuXWHl.png , what do you guys understand by the difference between safety and liveness verification ? | 11:09 |
|---|---|---|
| *** xerpi has quit IRC | 11:41 | |
| *** pie_ has quit IRC | 11:47 | |
| *** ZipCPU has joined #yosys | 12:02 | |
| *** develonepi3 has joined #yosys | 12:22 | |
| *** promach_ has joined #yosys | 13:11 | |
| *** AlexDaniel has quit IRC | 13:26 | |
| *** pie_ has joined #yosys | 13:38 | |
| *** ralu has quit IRC | 13:46 | |
| promach_ | ZipCPU awygle : what would you do if you are really stucked at induction ? | 14:03 |
| ZipCPU | I thought you just had it working the other day? | 14:04 |
| promach_ | it is only for induction depth of 26 | 14:07 |
| promach_ | ZipCPU: now, I am at depth of 10 | 14:07 |
| ZipCPU | Why is 10 better than 26? | 14:08 |
| promach_ | it prompts for more assert() | 14:08 |
| promach_ | which will uncover some of the deepest bug | 14:08 |
| 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 | 14:08 |
| promach_ | design bug | 14:08 |
| ZipCPU | cr1901_modern: +1 | 14:08 |
| promach_ | cr1901_modern: but what if my CLOCKS_PER_BIT is 8 | 14:08 |
| ZipCPU | ... and .... ? | 14:08 |
| promach_ | ZipCPU: no, 26 is not enough | 14:09 |
| ZipCPU | Why not? Somethings require longer induction depths to be successful. | 14:09 |
| cr1901_modern | decreasing the induction length may make it _completely impossible_ for the design to pass temporal induction | 14:09 |
| promach_ | shorter the induction depth, the better it is | 14:09 |
| cr1901_modern | (without adding a bunch of assumes that make your asserts meaningless) | 14:09 |
| ZipCPU | promach_: Not true. That's an application dependent thing | 14:09 |
| promach_ | ZipCPU: what is your induction depth for your UART ? | 14:10 |
| ZipCPU | 120 | 14:10 |
| promach_ | huh ? | 14:10 |
| ZipCPU | Yes. | 14:10 |
| promach_ | what about your CLOCKS_PER_BIT ? | 14:11 |
| ZipCPU | 16 | 14:11 |
| cr1901_modern | I wish I had time to create a graphviz example showing this, but basically... | 14:11 |
| promach_ | ZipCPU: try decrease induction depth for your UART | 14:11 |
| cr1901_modern | promach: if your induction step fails, that doesn't mean that your design can actually _reach_ that state | 14:12 |
| promach_ | cr1901_modern: maybe | 14:12 |
| 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. | 14:13 |
| promach_ | I already the same reset for both Tx and Rx | 14:13 |
| promach_ | I already had the same reset for both Tx and Rx | 14:14 |
| 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_ | 14:14 |
| promach_ | ZipCPU knew this fact regarding the reset quite well | 14:14 |
| cr1901_modern | promach_: I don't care that you had the same reset for both Tx and Rx. It's irrelevant here. | 14:15 |
| promach_ | cr1901_modern: you mean the induction counter-example is not reachable in reality ? | 14:15 |
| 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 | 14:16 |
| promach_ | hmm... I am not really convinced with my own source code yet | 14:17 |
| cr1901_modern | promach_: You proved that BMC passes for =26, right? | 14:17 |
| promach_ | yes, actually it had passed BMC=11 , inducton=11 | 14:17 |
| cr1901_modern | Alright, that's good too (BMC=11, induction=11 gives you the same information as BMC=26, induction=26) | 14:18 |
| promach_ | sorry, BMC should be more | 14:18 |
| cr1901_modern | well, it needs to be greater-than-or-equal-to | 14:19 |
| promach_ | actually I ran my BMC for 200 steps before I stop it | 14:19 |
| promach_ | I am more worried regarding induction than BMC | 14:20 |
| cr1901_modern | promach_: Let's pretend you _only_ ran your design for induction=10 | 14:20 |
| cr1901_modern | No BMC | 14:20 |
| cr1901_modern | So you don't know _any_ info about BMC | 14:20 |
| cr1901_modern | can you pretend that for a second? | 14:20 |
| promach_ | ok, I will let you continue | 14:20 |
| 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. | 14:21 |
| cr1901_modern | If you keep increasing the induction length, and you eventually find an induction length that passes, that tells you >> | 14:22 |
| cr1901_modern | That the failing state for induction length=10 isn't actually reachable if BMC passes for the greater induction length | 14:23 |
| cr1901_modern | I.e. suppose you find induction length=11 passes | 14:23 |
| cr1901_modern | if you do BMC=11, and that _also_ passes, that guarantees that the induction failure for step=10 isn't reachable | 14:23 |
| cr1901_modern | _This_ is why it isn't all that important to keep decreasing induction length after you find that your design passes | 14:24 |
| promach_ | no, you don't just do BMC=11 , that amount of BMC does not make sense | 14:24 |
| cr1901_modern | Why don't you think it makes sense? | 14:24 |
| *** seldridge has joined #yosys | 14:24 | |
| promach_ | BMC=11 is so little info | 14:24 |
| cr1901_modern | Doesn't matter as long as it's greater than or equal to induction length! :) | 14:25 |
| promach_ | BMC=11 gives so little info about the system | 14:25 |
| cr1901_modern | You can mathematically _show_ it doesn't matter | 14:25 |
| 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) | 14:26 |
| promach_ | you mean maths relationship between induction length and BMC length ? | 14:26 |
| cr1901_modern | yes | 14:26 |
| promach_ | how do you come up with such maths relationship ? | 14:26 |
| 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. | 14:27 |
| promach_ | huh ? | 14:27 |
| cr1901_modern | promach_: If I had time to draw an example, I would. But unfortunately I don't | 14:27 |
| cr1901_modern | promach_: Basically, to convince myself of the maths relationship, I drew lots of pictures. | 14:29 |
| promach_ | do you still keep one of those pictures of yours ? | 14:31 |
| promach_ | ;) | 14:31 |
| promach_ | I suppose all those paper went to dustbin ;) | 14:31 |
| 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 | 14:31 |
| 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 | 14:32 |
| 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. | 14:33 |
| promach_ | ZipCPU: what do you think about my UART coding ? is it bug-free enough in your perspective ? | 14:33 |
| cr1901_modern | ZipCPU: We're you there the whole time watching me wing it :P? | 14:34 |
| promach_ | cr1901_modern : your blog post will supplement clifford proof engine ;) take your own sweet time to create one such blog post ;) | 14:35 |
| ZipCPU | cr1901_modern: No, I wasn't ... I'm back reading now before powering off. | 14:36 |
| 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 | 14:37 |
| ZipCPU | promach_: If you want to convince yourself of what cr1901_modern was sharing, google "k-induction" | 14:37 |
| promach_ | ok | 14:37 |
| *** seldridge has quit IRC | 14:37 | |
| promach_ | I just listened to a webinar by someone modifying ic3 | 14:38 |
| promach_ | cr1901_modern ZipCPU awygle https://www.testandverification.com/conferences/verification-futures/ | 14:46 |
| *** seldridge has joined #yosys | 14:57 | |
| *** ZipCPU has quit IRC | 15:02 | |
| *** ralu has joined #yosys | 15:11 | |
| *** xerpi has joined #yosys | 15:36 | |
| *** m_w has joined #yosys | 15:37 | |
| *** seldridge has quit IRC | 15:44 | |
| *** AlexDaniel has joined #yosys | 16:04 | |
| *** ZipCPU has joined #yosys | 16:09 | |
| *** seldridge has joined #yosys | 16:10 | |
| *** leviathan has quit IRC | 16:17 | |
| *** seldridge has quit IRC | 16:23 | |
| *** seldridge has joined #yosys | 16:40 | |
| *** dys has joined #yosys | 16:52 | |
| *** GuzTech has quit IRC | 16:52 | |
| *** pie_ has quit IRC | 16:57 | |
| *** promach_ has quit IRC | 17:03 | |
| *** xerpi has quit IRC | 17:07 | |
| *** sklv1 has quit IRC | 17:33 | |
| *** sklv has joined #yosys | 17:34 | |
| *** azzizi has quit IRC | 17:56 | |
| *** azzizi has joined #yosys | 17:57 | |
| azzizi | Hello! has anybody written any pass in any other language than c++? | 17:57 |
| *** develonepi3 has quit IRC | 19:20 | |
| *** sklv1 has joined #yosys | 19:44 | |
| *** sklv has quit IRC | 19:46 | |
| daveshah | azzizi: c++ is I think the only real option right now, although in a few months there might be some Python bindings | 20:13 |
| 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 | 20:15 |
| 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 | 20:19 |
| daveshah | But good luck debugging that... | 20:19 |
| *** emeb_mac has joined #yosys | 20:57 | |
| ZipCPU | LUT statistics for a fully pipelined 15-stage CORDIC on an ice40: 2416 | 21:00 |
| ZipCPU | LUT statistics for a non-pipelined version: 500 | 21:01 |
| ZipCPU | Hmm ... if your design doesn't need high speed, you probably want the non-pipelined version. | 21:01 |
| sorear | What precision? Does it use rams? | 21:02 |
| ZipCPU | The second one uses a block RAM, yes. | 21:02 |
| ZipCPU | The output precision is about 12 bits. | 21:02 |
| 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 | 21:04 |
| ZipCPU | Oh, and both cases above used 19-bits of phase information. That's not something you could easily look up in a table. | 21:05 |
| ZipCPU | Why 19-bits? It was the example I had lying around that so that I could do a comparison with it. | 21:05 |
| *** ZipCPU has quit IRC | 21:21 | |
| 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 ? | 21:22 |
| daveshah | azzizi: yes, of course, but I personally wouldn't want to try and parse and generate RTLIL in Matlab | 21:24 |
| daveshah | Probably be faster to learn C++ | 21:25 |
| daveshah | The relevant command is read_ilang though | 21:27 |
| daveshah | The Json format is also worth looking into as a way of processing designs in another language | 21:28 |
| *** dys has quit IRC | 22:23 | |
| *** pie_ has joined #yosys | 22:30 | |
| *** danieljabailey has quit IRC | 23:14 | |
| *** danieljabailey has joined #yosys | 23:19 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!
