| *** tpb has joined #yosys | 00:00 | |
| *** aaaa has quit IRC | 00:12 | |
| *** Degi has quit IRC | 03:05 | |
| *** Degi has joined #yosys | 03:07 | |
| *** citypw has joined #yosys | 04:23 | |
| *** awordnot has quit IRC | 04:43 | |
| *** awordnot has joined #yosys | 04:44 | |
| *** emeb_mac has quit IRC | 06:31 | |
| *** jakobwenzel has joined #yosys | 07:12 | |
| *** az0re has quit IRC | 07:51 | |
| *** az0re has joined #yosys | 08:03 | |
| *** forrestv has quit IRC | 08:57 | |
| *** forrestv has joined #yosys | 09:01 | |
| *** N2TOH has quit IRC | 10:22 | |
| *** flaviusb has joined #yosys | 10:35 | |
| *** citypw has quit IRC | 10:35 | |
| *** citypw has joined #yosys | 10:36 | |
| *** nengel has quit IRC | 11:09 | |
| *** attie has joined #yosys | 11:11 | |
| *** citypw has quit IRC | 13:04 | |
| *** az0re has quit IRC | 13:04 | |
| *** citypw has joined #yosys | 13:16 | |
| *** kristianpaul has joined #yosys | 13:54 | |
| z0ttel | I am somewhat puzzled by what I read about the verific frontend. Does it really allow SymbiYosys to prove sequence expressions? Are these expanded by the frontend and reduced to what the expressions understood by the open-source front-end are capable of, or are there more powerful temporal logic expression understood internally than the regular front-end supports? | 13:56 |
|---|---|---|
| daveshah | The expansion code is all open source | 14:00 |
| daveshah | https://github.com/YosysHQ/yosys/blob/master/frontends/verific/verificsva.cc | 14:01 |
| tpb | Title: yosys/verificsva.cc at master · YosysHQ/yosys · GitHub (at github.com) | 14:01 |
| daveshah | aiui, it basically compiles them down to a FSM of sorts | 14:01 |
| daveshah | All Verific is doing is parsing and elaboration, it doesn't do any of the real 'magic' in compiling these | 14:01 |
| z0ttel | Ah, interesting. Thank you :) | 14:03 |
| *** klotz has joined #yosys | 14:28 | |
| *** az0re has joined #yosys | 14:31 | |
| *** Asu has joined #yosys | 14:36 | |
| *** emeb has joined #yosys | 15:47 | |
| *** somlo has quit IRC | 16:04 | |
| *** somlo has joined #yosys | 16:05 | |
| *** LJ_cache has joined #yosys | 16:38 | |
| *** citypw has quit IRC | 17:14 | |
| ZipCPU | z0ttel: You can find a fascinating discussion of sequence properties using the Verific front end here: https://zipcpu.com/formal/2019/02/21/txuart.html | 18:38 |
| tpb | Title: Using Sequence Properties to Verify a Serial Port Transmitter (at zipcpu.com) | 18:39 |
| z0ttel | @ZipCPU: Already had a look at that today :) | 18:43 |
| ZipCPU | Cool. That should help you understand the power of the sequence properties | 18:43 |
| z0ttel | Well, I haven't touched verific itself yet. | 18:44 |
| z0ttel | Used to do LTL/CTL* at university tho, so I have some familiarity with temporal logic. | 18:44 |
| z0ttel | My first attempt at verifying a FIFO: https://gist.github.com/Zottel/6b5075602dfae367be0c8305423e474c | 18:52 |
| tpb | Title: generic_fifo_proof.sv · GitHub (at gist.github.com) | 18:52 |
| z0ttel | I'm pretty confident that I can trust a FIFO that succeeds in cover and bmc checks with that scaffolding, but somehow, a more integrated version that will help when the FIFO is embedded in a whole system would be nice too. | 18:53 |
| ZipCPU | z0ttel: The typical proof of a FIFO is that you can write an arbitrary two values into it, and then some time later read them back out and in the same order | 19:27 |
| ZipCPU | To see how you might handle that, feel free to check out the FIFO lesson of my tutorial: https://zipcpu.com/tutorial | 19:28 |
| tpb | Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com) | 19:28 |
| *** kristianpaul has quit IRC | 19:35 | |
| z0ttel | Ah, I must've skipped the presentation. cool, thx. | 19:41 |
| z0ttel | @ZipCPU: There's something I thought about when reading your skynet/exchanging asserts/assumes article: Wouldn't a general assert(all assumptions imply property) style solve that issue? | 19:44 |
| ZipCPU | I'm not sure how it would or could | 19:45 |
| *** kristianpaul has joined #yosys | 19:52 | |
| *** klotz has quit IRC | 20:08 | |
| *** emeb_mac has joined #yosys | 20:38 | |
| ZipCPU | z0ttel: The problem with skynet was roughly: assume(A); B = A; assert(B); If you switch it to B=A; if (A) assert(A) ... you still have the same problem. | 21:16 |
| z0ttel | I meant switch "assume(A) ... assert(B)" to "assert (A -> B)". | 21:24 |
| z0ttel | but will have another look at the issue tomorrow, EU sleepy time now. | 21:25 |
| ZipCPU | o/ | 21:29 |
| ZipCPU | But ... A = B; assert(A |-> B) is next to tautologous. So also is: A = B; assert(B |-> A); It doesn't make a difference | 21:30 |
| z0ttel | but having assume(A); B=A; assume(B) is just as tautologous^^ | 21:36 |
| z0ttel | (the latter assume being an assert) | 21:37 |
| ZipCPU | Yes | 21:48 |
| *** Asu has quit IRC | 21:53 | |
| *** Asuu has joined #yosys | 21:53 | |
| *** Asuu has quit IRC | 23:03 | |
| *** pacak has quit IRC | 23:17 | |
| *** pacak has joined #yosys | 23:18 | |
| *** lf_ has joined #yosys | 23:25 | |
| *** lf has quit IRC | 23:25 | |
| *** FFY00 has quit IRC | 23:42 | |
| *** FFY00 has joined #yosys | 23:43 | |
| *** FFY00 has quit IRC | 23:47 | |
| *** FFY00 has joined #yosys | 23:48 | |
| *** FFY00 has quit IRC | 23:49 | |
| *** FFY00 has joined #yosys | 23:50 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!