Thursday, 2018-06-14

*** tpb has joined #yosys00:00
*** develonepi3 has quit IRC00:04
*** azzizi has quit IRC00:16
*** azzizi has joined #yosys00:17
*** emeb has quit IRC01:06
*** emeb_mac has joined #yosys01:24
*** promach_ has quit IRC01:45
*** maartenBE has quit IRC02:25
*** maartenBE has joined #yosys02:25
*** leviathan has joined #yosys04:46
*** cr1901_modern has quit IRC05:25
*** cr1901_modern has joined #yosys06:07
*** ZipCPU has joined #yosys06:22
*** cr1901_modern has quit IRC06:36
*** cr1901_modern has joined #yosys07:00
*** emeb_mac has quit IRC07:05
*** AlexDaniel has quit IRC07:16
*** pie_ has joined #yosys07:28
*** pie_ has quit IRC07:42
*** ZipCPU has quit IRC07:51
*** pie_ has joined #yosys08:02
*** GuzTech has joined #yosys08:09
*** zetta has quit IRC08:22
*** zetta has joined #yosys08:22
*** Guest72074 is now known as jayaura09:08
*** xerpi has joined #yosys10:12
*** AlexDaniel has joined #yosys10:28
*** proteus-guy has joined #yosys10:36
*** AlexDaniel has quit IRC10:45
*** AlexDaniel has joined #yosys10:45
promachFor , what do you guys understand by the difference between safety and liveness verification ?11:09
*** xerpi has quit IRC11:41
*** pie_ has quit IRC11:47
*** ZipCPU has joined #yosys12:02
*** develonepi3 has joined #yosys12:22
*** promach_ has joined #yosys13:11
*** AlexDaniel has quit IRC13:26
*** pie_ has joined #yosys13:38
*** ralu has quit IRC13:46
promach_ZipCPU awygle : what would you do if you are really stucked at induction ?14:03
ZipCPUI thought you just had it working the other day?14:04
promach_it is only for induction depth of 2614:07
promach_ZipCPU: now, I am at depth of 1014:07
ZipCPUWhy is 10 better than 26?14:08
promach_it prompts for more assert()14:08
promach_which will uncover some of the deepest bug14:08
cr1901_modernpromach_: If you've proven induction for 26, _as well as_ bounded model check for 26, then you've proven that asserts hold for all time14:08
promach_design bug14:08
ZipCPUcr1901_modern: +114:08
promach_cr1901_modern: but what if my CLOCKS_PER_BIT is 814:08
ZipCPU... and .... ?14:08
promach_ZipCPU: no, 26 is not enough14:09
ZipCPUWhy not?  Somethings require longer induction depths to be successful.14:09
cr1901_moderndecreasing the induction length may make it _completely impossible_ for the design to pass temporal induction14:09
promach_shorter the induction depth, the better it is14:09
cr1901_modern(without adding a bunch of assumes that make your asserts meaningless)14:09
ZipCPUpromach_: Not true.  That's an application dependent thing14:09
promach_ZipCPU: what is your induction depth for your UART ?14:10
promach_huh ?14:10
promach_what about your CLOCKS_PER_BIT ?14:11
cr1901_modernI wish I had time to create a graphviz example showing this, but basically...14:11
promach_ZipCPU: try decrease induction depth for your UART14:11
cr1901_modernpromach: if your induction step fails, that doesn't mean that your design can actually _reach_ that state14:12
promach_cr1901_modern: maybe14:12
cr1901_modernIf 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 Rx14:13
promach_I already had the same reset for both Tx and Rx14:14
cr1901_modernpromach: 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 well14:14
cr1901_modernpromach_: 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_modernpromach_: 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=2614:16
promach_hmm... I am not really convinced with my own source code yet14:17
cr1901_modernpromach_: You proved that BMC passes for =26, right?14:17
promach_yes, actually it had passed BMC=11 , inducton=1114:17
cr1901_modernAlright, 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 more14:18
cr1901_modernwell, it needs to be greater-than-or-equal-to14:19
promach_actually I ran my BMC for 200 steps before I stop it14:19
promach_I am more worried regarding induction than BMC14:20
cr1901_modernpromach_: Let's pretend you _only_ ran your design for induction=1014:20
cr1901_modernNo BMC14:20
cr1901_modernSo you don't know _any_ info about BMC14:20
cr1901_moderncan you pretend that for a second?14:20
promach_ok, I will let you continue14:20
cr1901_moderninduction 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_modernIf you keep increasing the induction length, and you eventually find an induction length that passes, that tells you >>14:22
cr1901_modernThat the failing state for induction length=10 isn't actually reachable if BMC passes for the greater induction length14:23
cr1901_modernI.e. suppose you find induction length=11 passes14:23
cr1901_modernif you do BMC=11, and that _also_ passes, that guarantees that the induction failure for step=10 isn't reachable14:23
cr1901_modern_This_ is why it isn't all that important to keep decreasing induction length after you find that your design passes14:24
promach_no, you don't just do BMC=11 , that amount of BMC does not make sense14:24
cr1901_modernWhy don't you think it makes sense?14:24
*** seldridge has joined #yosys14:24
promach_BMC=11 is so little info14:24
cr1901_modernDoesn'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 system14:25
cr1901_modernYou can mathematically _show_ it doesn't matter14:25
cr1901_modernBMC 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
promach_how do you come up with such maths relationship ?14:26
cr1901_modernpromach_: 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_modernpromach_: If I had time to draw an example, I would. But unfortunately I don't14:27
cr1901_modernpromach_: 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_I suppose all those paper went to dustbin ;)14:31
cr1901_modernpromach_: 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 it14:31
cr1901_modernUntil 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 time14:32
ZipCPUpromach_: 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_modernZipCPU: 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
ZipCPUcr1901_modern: No, I wasn't ... I'm back reading now before powering off.14:36
awyglepromach_: 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 thinking14:37
ZipCPUpromach_: If you want to convince yourself of what cr1901_modern was sharing, google "k-induction"14:37
*** seldridge has quit IRC14:37
promach_I just listened to a webinar by someone modifying ic314:38
promach_cr1901_modern ZipCPU awygle
*** seldridge has joined #yosys14:57
*** ZipCPU has quit IRC15:02
*** ralu has joined #yosys15:11
*** xerpi has joined #yosys15:36
*** m_w has joined #yosys15:37
*** seldridge has quit IRC15:44
*** AlexDaniel has joined #yosys16:04
*** ZipCPU has joined #yosys16:09
*** seldridge has joined #yosys16:10
*** leviathan has quit IRC16:17
*** seldridge has quit IRC16:23
*** seldridge has joined #yosys16:40
*** dys has joined #yosys16:52
*** GuzTech has quit IRC16:52
*** pie_ has quit IRC16:57
*** promach_ has quit IRC17:03
*** xerpi has quit IRC17:07
*** sklv1 has quit IRC17:33
*** sklv has joined #yosys17:34
*** azzizi has quit IRC17:56
*** azzizi has joined #yosys17:57
azziziHello! has anybody written any pass in any other language than c++?17:57
*** develonepi3 has quit IRC19:20
*** sklv1 has joined #yosys19:44
*** sklv has quit IRC19:46
daveshahazzizi: c++ is I think the only real option right now, although in a few months there might be some Python bindings20:13
awygleyou 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 squint20:15
daveshahI 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 system20:19
daveshahBut good luck debugging that...20:19
*** emeb_mac has joined #yosys20:57
ZipCPULUT statistics for a fully pipelined 15-stage CORDIC on an ice40: 241621:00
ZipCPULUT statistics for a non-pipelined version: 50021:01
ZipCPUHmm ... if your design doesn't need high speed, you probably want the non-pipelined version.21:01
sorearWhat precision? Does it use rams?21:02
ZipCPUThe second one uses a block RAM, yes.21:02
ZipCPUThe output precision is about 12 bits.21:02
ZipCPUThe 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 needs21:04
ZipCPUOh, and both cases above used 19-bits of phase information.  That's not something you could easily look up in a table.21:05
ZipCPUWhy 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 IRC21:21
azziziI 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
daveshahazzizi: yes, of course, but I personally wouldn't want to try and parse and generate RTLIL in Matlab21:24
daveshahProbably be faster to learn C++21:25
daveshahThe relevant command is read_ilang though21:27
daveshahThe Json format is also worth looking into as a way of processing designs in another language21:28
*** dys has quit IRC22:23
*** pie_ has joined #yosys22:30
*** danieljabailey has quit IRC23:14
*** danieljabailey has joined #yosys23:19

Generated by 2.13.1 by Marius Gedminas - find it at!