| *** tpb has joined #yosys | 00:00 | |
| *** richbridger has joined #yosys | 00:13 | |
| *** aquijoule_ has quit IRC | 00:15 | |
| *** lf has quit IRC | 00:28 | |
| *** lf has joined #yosys | 00:29 | |
| *** Degi has quit IRC | 01:09 | |
| *** flaviusb has quit IRC | 01:35 | |
| *** X-Scale has quit IRC | 02:13 | |
| *** X-Scale has joined #yosys | 02:23 | |
| *** citypw has joined #yosys | 02:30 | |
| *** jfcaron has quit IRC | 04:18 | |
| *** davidlattimore has quit IRC | 04:21 | |
| *** davidlattimore has joined #yosys | 04:21 | |
| *** sorear has quit IRC | 04:22 | |
| *** sorear has joined #yosys | 04:23 | |
| *** davidlattimore has quit IRC | 04:37 | |
| *** bluesceada has quit IRC | 04:37 | |
| *** davidlattimore has joined #yosys | 04:42 | |
| *** bluesceada has joined #yosys | 04:42 | |
| *** fevv8[m] has quit IRC | 04:45 | |
| *** wiizzard has quit IRC | 04:46 | |
| *** notafile has quit IRC | 04:47 | |
| *** jryans has quit IRC | 04:47 | |
| *** promach3 has quit IRC | 04:49 | |
| *** wiizzard has joined #yosys | 05:09 | |
| *** fevv8[m] has joined #yosys | 05:12 | |
| *** FFY00 has quit IRC | 05:13 | |
| *** notafile has joined #yosys | 05:21 | |
| *** jryans has joined #yosys | 05:22 | |
| *** promach3 has joined #yosys | 05:25 | |
| *** bwidawsk has quit IRC | 05:31 | |
| *** bwidawsk has joined #yosys | 05:32 | |
| *** emeb_mac has quit IRC | 07:01 | |
| *** danvet has joined #yosys | 07:08 | |
| *** mndza has joined #yosys | 07:13 | |
| *** vidbina has joined #yosys | 08:27 | |
| *** jakobwenzel1 has joined #yosys | 08:29 | |
| *** jakobwenzel has quit IRC | 08:31 | |
| *** jakobwenzel1 is now known as jakobwenzel | 08:31 | |
| *** jakobwenzel has quit IRC | 09:20 | |
| *** miek has quit IRC | 09:37 | |
| *** jakobwenzel has joined #yosys | 09:39 | |
| *** jakobwenzel has quit IRC | 09:48 | |
| *** jakobwenzel has joined #yosys | 10:13 | |
| *** jakobwenzel has quit IRC | 11:05 | |
| *** citypw has quit IRC | 11:14 | |
| *** citypw has joined #yosys | 11:18 | |
| *** jakobwenzel has joined #yosys | 11:18 | |
| *** vidbina has quit IRC | 11:35 | |
| *** vidbina has joined #yosys | 12:36 | |
| *** FFY00 has joined #yosys | 14:00 | |
| *** dxld has joined #yosys | 14:14 | |
| *** jakobwenzel has quit IRC | 14:15 | |
| *** jakobwenzel has joined #yosys | 14:17 | |
| *** miek has joined #yosys | 14:21 | |
| *** vidbina has quit IRC | 15:18 | |
| *** emeb has joined #yosys | 15:47 | |
| *** vidbina has joined #yosys | 15:57 | |
| *** vidbina has quit IRC | 16:09 | |
| *** kraiskil has joined #yosys | 16:16 | |
| *** Degi has joined #yosys | 16:19 | |
| *** citypw has quit IRC | 16:27 | |
| *** gmc has quit IRC | 16:28 | |
| *** GenTooMan has quit IRC | 16:32 | |
| *** GenTooMan has joined #yosys | 16:32 | |
| *** jakobwenzel1 has joined #yosys | 16:48 | |
| *** _whitelogger has quit IRC | 16:48 | |
| *** jakobwenzel has quit IRC | 16:48 | |
| *** jakobwenzel1 is now known as jakobwenzel | 16:48 | |
| *** _whitelogger has joined #yosys | 16:51 | |
| *** DrWhax has joined #yosys | 16:55 | |
| *** emeb has quit IRC | 17:01 | |
| *** kraiskil has quit IRC | 17:16 | |
| *** kraiskil has joined #yosys | 17:56 | |
| *** nengel has joined #yosys | 18:01 | |
| *** jakobwenzel has quit IRC | 18:07 | |
| *** emeb_mac has joined #yosys | 18:26 | |
| *** kraiskil has quit IRC | 18:34 | |
| *** vidbina has joined #yosys | 18:35 | |
| *** kraiskil has joined #yosys | 18:47 | |
| *** wifasoi has quit IRC | 18:53 | |
| *** nengel has quit IRC | 19:04 | |
| *** nengel has joined #yosys | 19:13 | |
| *** danvet has quit IRC | 19:26 | |
| *** nengel has quit IRC | 19:55 | |
| *** nengel has joined #yosys | 19:57 | |
| *** jakobwenzel has joined #yosys | 20:06 | |
| *** jakobwenzel has quit IRC | 20:07 | |
| *** vidbina has quit IRC | 20:11 | |
| *** vidbina has joined #yosys | 20:13 | |
| roamingryan | Is this channel an appropriate venue for asking some basic questions about formal verification with SymbiYosys? | 20:39 |
|---|---|---|
| *** nengel has quit IRC | 20:51 | |
| roamingryan | My question is this: I have a module with input and output valid/ready interfaces. The module does some processing on the data. For each word loaded into the module, a output word should be eventually produced. I am trying to implement an assertion that ensures that <# of input words> is equal to <# of output words>. I have implemented some counters that increment in response to (input_valid && | 20:52 |
| roamingryan | input_ready) and (out_valid && out_ready). The problem is, under induction those can start at any value. Similarly, the internal state of the module isn't necessarily empty under induction. How should I be constraining them to stay matched? | 20:52 |
| *** kraiskil has quit IRC | 20:55 | |
| *** vidbina has quit IRC | 21:03 | |
| awygle | roamingryan: this is a tricky problem, with a few approaches, but let me suggest the biggest hammer first - have you tried switching from `smtbmc` to `abc pdr` as your proof engine? sometimes that Just Works, as it uses a different algorithm that doesn't have the same issues with induction | 21:06 |
| roamingryan | awygle: so far, I've only been using smtbmc but I do love "Just Works" solutions. Thanks for the tip. | 21:22 |
| awygle | roamingryan: the "gotchas" are mostly that abc pdr doesn't handle memories intelligently, so if you have a large BRAM or something it will expand it to that many bits, which in practice means it will never finish | 21:25 |
| awygle | to solve your induction problem you need to set up your asserts in such a way that the induction can't start from invalid states. increasing the depth of the induction may help with this, depending | 21:25 |
| roamingryan | Cool, `abc pdr` seems to have worked on one of my modules. No changes necessary to the asserts. | 21:26 |
| awygle | awesome :). it's still good to learn how to prove things with k-induction, but i find it kinda frustrating that k-induction is often the only strategy discussed in much of the documentation and examples | 21:27 |
| roamingryan | I will have to read up more on that proof engine as I'm curious how it works. I can wrap my head around the k-induction method, but as you said that's much better documented. | 21:28 |
| awygle | the paper is at https://www.cs.utexas.edu/~ragerdl/fmcad11/papers/7.pdf | 21:32 |
| ZipCPU | There's an easier way than switching from an smtbmc based approach. | 22:42 |
| ZipCPU | roamingryan: Add assertions to your design. You should have an input counter, and an output counter, and then an assertion relating the two counters together, together with whatever's in your pipeline. | 22:43 |
| ZipCPU | I did something similar in this example: https://zipcpu.com/blog/2020/08/31/run-length-encoding.html | 22:44 |
| tpb | Title: Run length encoding an AXI stream (at zipcpu.com) | 22:44 |
| ZipCPU | Indeed, I have a whole section dedicated to counting the two streams--the one going in and the other going out. | 22:45 |
| roamingryan | Cool, I'll check that out. Indeed, I have another module where `abc pdr` isn't completing in a reasonable amount of time (presumably because it has more internal memory elements). | 22:46 |
| ZipCPU | Also, by "easier" I suppose I should say more reliable--for the exact same reason you just noticed. | 22:46 |
| ZipCPU | "abc pdr" doesn't always finish for me. At least when smtbmc doesn't pass induction it tells me where to look. | 22:46 |
| roamingryan | So my assert will basically need to compare the counters *and* add a correction/delta to account for the internal state of the module? | 22:47 |
| ZipCPU | I often handle the corrections in a combinatorial signal, separate from the assert, but then make an assertion about the counter. | 22:47 |
| roamingryan | Yeah, I can see how that would be more readable to future me. | 22:48 |
| ZipCPU | The thing you have to be aware of is that the induction engine might pick a counter value that will over flow just to spite you, so making sure you can deal with overflow is important. | 22:48 |
| ZipCPU | In most cases involving this type of counter, "dealing with overflow" simply means truncating to the right number of bits. Provided that number is sufficient .. ;) | 22:48 |
| *** mndza has quit IRC | 22:51 | |
| *** jfcaron has joined #yosys | 22:59 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!