Tuesday, 2019-07-02

*** tpb has joined #yosys00:00
*** emeb has quit IRC00:07
*** emeb_mac has joined #yosys00:11
*** gsi__ has joined #yosys00:41
*** gsi_ has quit IRC00:44
*** Stary has quit IRC00:58
*** Stary has joined #yosys01:32
*** Kamilion has quit IRC02:12
*** citypw has joined #yosys02:17
*** Kamilion has joined #yosys02:20
*** _whitelogger has quit IRC02:26
*** _whitelogger has joined #yosys02:29
*** PyroPeter has quit IRC02:41
*** vonnieda has joined #yosys02:44
*** PyroPeter has joined #yosys02:53
*** tlwoerner has quit IRC03:06
*** tlwoerner has joined #yosys03:07
*** dys has quit IRC03:48
*** citypw has quit IRC05:08
*** m4ssi has joined #yosys05:11
*** rohitksingh_work has joined #yosys05:12
*** proteusguy has joined #yosys05:14
*** rohitksingh_work has quit IRC05:27
*** vonnieda_ has joined #yosys05:40
*** vonnieda has quit IRC05:42
*** s_frit has quit IRC05:59
*** s_frit has joined #yosys06:00
*** citypw has joined #yosys06:48
*** emeb_mac has quit IRC07:12
*** jakobwenzel has quit IRC07:19
*** jakobwenzel has joined #yosys07:19
*** Wolf481pl is now known as Wolf480pl09:18
*** citypw has quit IRC10:37
*** AlexDaniel has quit IRC12:01
*** AlexDaniel has joined #yosys12:14
*** rrika has quit IRC12:34
*** rrika has joined #yosys12:37
somlodaveshah: 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
daveshahI think I've found the problem now12:40
daveshahI'll know in a minute12:40
somlooh, cool, thank goodness  :)12:40
somloif/when there's anything I could test, happy to do so12:41
daveshahI 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 bug12:41
tpbTitle: Comparing master...dave/fix_multi_mux · YosysHQ/yosys · GitHub (at github.com)12:41
daveshahJust routing with that fix applied now12:42
daveshahsomlo: Yup, that looks to have fixed it12:45
somloawesome! I just downloaded the patch, building yosys with it now...12:46
ZirconiumXI must not understand SAT very well, because according to Yosys just proved that a design is not equivalent to itself and caused a logic bomb12:48
ZirconiumXs/just/I just/12:48
daveshahProbably related to register initial values12:49
*** vonnieda_ has quit IRC13:35
*** emeb_mac has joined #yosys13:44
*** rohitksingh has joined #yosys13:56
*** voxadam has quit IRC13:58
*** voxadam has joined #yosys13:59
*** vonnieda has joined #yosys14:03
*** emeb_mac has quit IRC14:06
*** adjtm has quit IRC14:33
*** promach has joined #yosys14:33
promachMay I know why https://gist.github.com/promach/ae6d49ebca9b9f209f918622c3b5abe7#file-dff-sby-L10 could only covered 2 steps in gtkwave output ?14:34
tpbTitle: D flip-flop with asynchronous reset · GitHub (at gist.github.com)14:34
daveshahpromach: because you don't constrain the initial DFF state, starting at 1 and then asserting reset in the next cycle is enough to cover it14:36
daveshahnever mind, I misread, you don't even have q in the cover14:37
daveshahso all you are covering is 3 unconstrained inputs and the clock14:37
*** alexhw has quit IRC14:39
*** alexhw has joined #yosys14:41
*** adjtm has joined #yosys14:42
promachdaveshah : huh ?14:43
promachI was asking for 30 steps14:44
promachnot just 2 steps14:44
promachwait, I think I got it14:45
ZipCPUpromach: That's not how cover works14:45
promachtry to cover within 30 steps14:45
promachI need to append14:45
ZipCPUThe 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 true14:45
ZipCPUappend 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
ZipCPUA 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
promachcan we combine cover() and assume() ?14:47
ZipCPUYou can.  There are better ways of doing things though.14:48
promachwhat better ways ?14:48
ZipCPUFor 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
ZipCPUThat 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() statement14:49
*** rohitksingh has quit IRC14:49
*** rohitksingh has joined #yosys14:50
promachbut sequence is only supported in the verific version14:50
tpbTitle: Using Sequence Properties to Verify a Serial Port Transmitter (at zipcpu.com)14:50
somlodaveshah: fix confirmed, on yoloRISC and LiteX+Rocket, with and without "-nowidelut -abc9" -- thanks again!14:52
daveshahsomlo: sorry about this, thanks for reporting!14:52
promachZipCPU: the problem is I do not have verific14:54
somlono reason to feel sorry, this is awesome progress -- I can *almost* fit that MMU on the LiteX SoC now :)14:54
ZipCPUpromach: Not at all.  The problem is that you didn't read the article.14:55
promachI am reading14:56
promachI saw  =>14:56
promachwhich is for verific14:56
promachnow, I see   Poor Man’s Sequences14:57
*** proteusguy has quit IRC14:59
*** alexhw has quit IRC15:43
*** alexhw has joined #yosys15:48
*** m4ssi has quit IRC16:01
promachZipCPU: but using poor man method for these few assume() https://gist.github.com/promach/ae6d49ebca9b9f209f918622c3b5abe7#file-dff-v-L31-L49 seems a bit difficult16:13
tpbTitle: D flip-flop with asynchronous reset · GitHub (at gist.github.com)16:13
ZipCPUWhich of those lines is the assumption that's a bit difficult?16:15
promachto put those assume() as a sequence for a single cover()16:16
ZipCPUThen don't16:19
promachZipCPU: I want to emulate https://www.edaplayground.com/x/5dzJ using cover()16:24
tpbTitle: D flip-flop with asynchronous reset(1) - EDA Playground (at www.edaplayground.com)16:25
*** kraiskil has joined #yosys16:30
*** edwinbalani has quit IRC16:47
*** edwinbalani has joined #yosys16:48
*** proteusguy has joined #yosys16:51
*** edwinbalani has quit IRC16:53
*** edwinbalani has joined #yosys16:54
*** fsasm has joined #yosys17:08
*** kraiskil has quit IRC17:33
*** rohitksingh has quit IRC17:40
*** rohitksingh has joined #yosys17:59
*** rohitksingh has quit IRC18:06
*** rohitksingh has joined #yosys18:16
*** promach has quit IRC18:19
*** rohitksingh has quit IRC18:34
*** dys has joined #yosys19:16
*** proteusguy is now known as proteusdude19:41
*** cr1901_modern has quit IRC20:07
*** cr1901_modern has joined #yosys20:17
*** fsasm has quit IRC20:58
*** vonnieda has quit IRC23:03
*** alexhw has quit IRC23:32

Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!