| *** tpb has joined #yosys | 00:00 | |
| *** emeb has quit IRC | 00:07 | |
| *** emeb_mac has joined #yosys | 00:11 | |
| *** gsi__ has joined #yosys | 00:41 | |
| *** gsi_ has quit IRC | 00:44 | |
| *** Stary has quit IRC | 00:58 | |
| *** Stary has joined #yosys | 01:32 | |
| *** Kamilion has quit IRC | 02:12 | |
| *** citypw has joined #yosys | 02:17 | |
| *** Kamilion has joined #yosys | 02:20 | |
| *** _whitelogger has quit IRC | 02:26 | |
| *** _whitelogger has joined #yosys | 02:29 | |
| *** PyroPeter has quit IRC | 02:41 | |
| *** vonnieda has joined #yosys | 02:44 | |
| *** PyroPeter has joined #yosys | 02:53 | |
| *** tlwoerner has quit IRC | 03:06 | |
| *** tlwoerner has joined #yosys | 03:07 | |
| *** dys has quit IRC | 03:48 | |
| *** citypw has quit IRC | 05:08 | |
| *** m4ssi has joined #yosys | 05:11 | |
| *** rohitksingh_work has joined #yosys | 05:12 | |
| *** proteusguy has joined #yosys | 05:14 | |
| *** rohitksingh_work has quit IRC | 05:27 | |
| *** vonnieda_ has joined #yosys | 05:40 | |
| *** vonnieda has quit IRC | 05:42 | |
| *** s_frit has quit IRC | 05:59 | |
| *** s_frit has joined #yosys | 06:00 | |
| *** citypw has joined #yosys | 06:48 | |
| *** emeb_mac has quit IRC | 07:12 | |
| *** jakobwenzel has quit IRC | 07:19 | |
| *** jakobwenzel has joined #yosys | 07:19 | |
| *** Wolf481pl is now known as Wolf480pl | 09:18 | |
| *** citypw has quit IRC | 10:37 | |
| *** AlexDaniel has quit IRC | 12:01 | |
| *** AlexDaniel has joined #yosys | 12:14 | |
| *** rrika has quit IRC | 12:34 | |
| *** rrika has joined #yosys | 12:37 | |
| somlo | daveshah: I'm going to start bisecting yosys with good=c907899, bad=dd8d264; If you think there's a less labor-intensive way to go about this, please feel free to interrupt me :) | 12:40 |
|---|---|---|
| daveshah | I think I've found the problem now | 12:40 |
| daveshah | I'll know in a minute | 12:40 |
| somlo | oh, cool, thank goodness :) | 12:40 |
| somlo | if/when there's anything I could test, happy to do so | 12:41 |
| daveshah | I didn't finish bisecting, but I got it down to a few commits and I think https://github.com/YosysHQ/yosys/compare/dave/fix_multi_mux should fix at least one bug | 12:41 |
| tpb | Title: Comparing master...dave/fix_multi_mux · YosysHQ/yosys · GitHub (at github.com) | 12:41 |
| daveshah | Just routing with that fix applied now | 12:42 |
| daveshah | somlo: Yup, that looks to have fixed it | 12:45 |
| somlo | awesome! I just downloaded the patch, building yosys with it now... | 12:46 |
| ZirconiumX | I must not understand SAT very well, because according to Yosys just proved that a design is not equivalent to itself and caused a logic bomb | 12:48 |
| ZirconiumX | s/just/I just/ | 12:48 |
| daveshah | Probably related to register initial values | 12:49 |
| *** vonnieda_ has quit IRC | 13:35 | |
| *** emeb_mac has joined #yosys | 13:44 | |
| *** rohitksingh has joined #yosys | 13:56 | |
| *** voxadam has quit IRC | 13:58 | |
| *** voxadam has joined #yosys | 13:59 | |
| *** vonnieda has joined #yosys | 14:03 | |
| *** emeb_mac has quit IRC | 14:06 | |
| *** adjtm has quit IRC | 14:33 | |
| *** promach has joined #yosys | 14:33 | |
| promach | May I know why https://gist.github.com/promach/ae6d49ebca9b9f209f918622c3b5abe7#file-dff-sby-L10 could only covered 2 steps in gtkwave output ? | 14:34 |
| tpb | Title: D flip-flop with asynchronous reset · GitHub (at gist.github.com) | 14:34 |
| daveshah | promach: because you don't constrain the initial DFF state, starting at 1 and then asserting reset in the next cycle is enough to cover it | 14:36 |
| daveshah | never mind, I misread, you don't even have q in the cover | 14:37 |
| daveshah | so all you are covering is 3 unconstrained inputs and the clock | 14:37 |
| *** alexhw has quit IRC | 14:39 | |
| *** alexhw has joined #yosys | 14:41 | |
| *** adjtm has joined #yosys | 14:42 | |
| promach | daveshah : huh ? | 14:43 |
| promach | I was asking for 30 steps | 14:44 |
| promach | not just 2 steps | 14:44 |
| promach | wait, I think I got it | 14:45 |
| ZipCPU | promach: That's not how cover works | 14:45 |
| promach | append | 14:45 |
| promach | try to cover within 30 steps | 14:45 |
| promach | I need to append | 14:45 |
| ZipCPU | The depth specified for "cover" in the sby file is how many steps the formal tool will search to find a way to make the cover() statement true | 14:45 |
| promach | yes | 14:46 |
| ZipCPU | append has a couple problems associated with its usage. I know one user covered a condition (X), and then appended 30 steps. He say condition (Y) take place in those 30 steps, yet his cover(Y) statement failed--because it wasn't in the initial depth. | 14:46 |
| ZipCPU | A second problem with "append" is that it tends to set all of the rest of the interaction to something fairly benign and typically useless. | 14:47 |
| promach | can we combine cover() and assume() ? | 14:47 |
| ZipCPU | You can. There are better ways of doing things though. | 14:48 |
| promach | what better ways ? | 14:48 |
| ZipCPU | For example, create a sequence and then cover the 9the step in that sequence: cover(sequence[8]). If any of what you would assume is ever not the case, reset the sequence. | 14:48 |
| ZipCPU | That way, you don't need to make assumptions about internal state, and your assumptions won't necessarily impact the rest of your design--just the cover() statement | 14:49 |
| *** rohitksingh has quit IRC | 14:49 | |
| *** rohitksingh has joined #yosys | 14:50 | |
| promach | but sequence is only supported in the verific version | 14:50 |
| ZipCPU | http://zipcpu.com/formal/2019/02/21/txuart.html | 14:50 |
| tpb | Title: Using Sequence Properties to Verify a Serial Port Transmitter (at zipcpu.com) | 14:50 |
| somlo | daveshah: fix confirmed, on yoloRISC and LiteX+Rocket, with and without "-nowidelut -abc9" -- thanks again! | 14:52 |
| daveshah | somlo: sorry about this, thanks for reporting! | 14:52 |
| promach | ZipCPU: the problem is I do not have verific | 14:54 |
| somlo | no reason to feel sorry, this is awesome progress -- I can *almost* fit that MMU on the LiteX SoC now :) | 14:54 |
| ZipCPU | promach: Not at all. The problem is that you didn't read the article. | 14:55 |
| promach | I am reading | 14:56 |
| promach | I saw => | 14:56 |
| promach | which is for verific | 14:56 |
| promach | now, I see Poor Man’s Sequences | 14:57 |
| *** proteusguy has quit IRC | 14:59 | |
| *** alexhw has quit IRC | 15:43 | |
| *** alexhw has joined #yosys | 15:48 | |
| *** m4ssi has quit IRC | 16:01 | |
| promach | ZipCPU: but using poor man method for these few assume() https://gist.github.com/promach/ae6d49ebca9b9f209f918622c3b5abe7#file-dff-v-L31-L49 seems a bit difficult | 16:13 |
| tpb | Title: D flip-flop with asynchronous reset · GitHub (at gist.github.com) | 16:13 |
| ZipCPU | ?? | 16:14 |
| ZipCPU | Which of those lines is the assumption that's a bit difficult? | 16:15 |
| promach | to put those assume() as a sequence for a single cover() | 16:16 |
| ZipCPU | Then don't | 16:19 |
| promach | ZipCPU: I want to emulate https://www.edaplayground.com/x/5dzJ using cover() | 16:24 |
| tpb | Title: D flip-flop with asynchronous reset(1) - EDA Playground (at www.edaplayground.com) | 16:25 |
| *** kraiskil has joined #yosys | 16:30 | |
| *** edwinbalani has quit IRC | 16:47 | |
| *** edwinbalani has joined #yosys | 16:48 | |
| *** proteusguy has joined #yosys | 16:51 | |
| *** edwinbalani has quit IRC | 16:53 | |
| *** edwinbalani has joined #yosys | 16:54 | |
| *** fsasm has joined #yosys | 17:08 | |
| *** kraiskil has quit IRC | 17:33 | |
| *** rohitksingh has quit IRC | 17:40 | |
| *** rohitksingh has joined #yosys | 17:59 | |
| *** rohitksingh has quit IRC | 18:06 | |
| *** rohitksingh has joined #yosys | 18:16 | |
| *** promach has quit IRC | 18:19 | |
| *** rohitksingh has quit IRC | 18:34 | |
| *** dys has joined #yosys | 19:16 | |
| *** proteusguy is now known as proteusdude | 19:41 | |
| *** cr1901_modern has quit IRC | 20:07 | |
| *** cr1901_modern has joined #yosys | 20:17 | |
| *** fsasm has quit IRC | 20:58 | |
| *** vonnieda has quit IRC | 23:03 | |
| *** alexhw has quit IRC | 23:32 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!