| *** tpb has joined #yosys | 00:00 | |
| *** pie_ has joined #yosys | 00:10 | |
| *** pie_ has quit IRC | 02:07 | |
| *** lutsabound has quit IRC | 05:34 | |
| *** dh73 has joined #yosys | 05:37 | |
| *** dh73 has quit IRC | 06:08 | |
| *** _whitelogger has quit IRC | 06:31 | |
| *** _whitelogger has joined #yosys | 06:33 | |
| *** _whitelogger has quit IRC | 06:55 | |
| *** _whitelogger has joined #yosys | 06:57 | |
| *** emeb_mac has quit IRC | 07:00 | |
| *** Twix has quit IRC | 07:05 | |
| *** Jybz has joined #yosys | 08:02 | |
| *** kraiskil has quit IRC | 09:52 | |
| *** _whitelogger has quit IRC | 10:25 | |
| *** _whitelogger has joined #yosys | 10:27 | |
| *** _whitelogger has quit IRC | 10:37 | |
| *** _whitelogger has joined #yosys | 10:39 | |
| *** kraiskil has joined #yosys | 12:12 | |
| *** kraiskil has quit IRC | 12:51 | |
| *** kraiskil has joined #yosys | 13:11 | |
| *** _whitelogger has quit IRC | 13:58 | |
| *** _whitelogger has joined #yosys | 14:00 | |
| *** kraiskil has quit IRC | 14:03 | |
| *** rombik_su has joined #yosys | 15:50 | |
| *** kraiskil has joined #yosys | 15:56 | |
| *** rombik_su has quit IRC | 16:16 | |
| *** vidbina has joined #yosys | 16:54 | |
| *** maikmerten has joined #yosys | 17:06 | |
| maikmerten | it's that season of the year where the blessings of formal verification look particularly bright - finally trying to prove some properties of my designs. | 17:11 |
|---|---|---|
| maikmerten | starting with an ALU | 17:11 |
| maikmerten | I find that some checks on combinatorial logic is easier than I thought | 17:12 |
| maikmerten | struggling a bit with clocked stuff | 17:12 |
| maikmerten | https://paste.debian.net/1123053/ | 17:12 |
| tpb | Title: debian Pastezone (at paste.debian.net) | 17:12 |
| maikmerten | ('result' is a reg[31:0] that receives values on posedge) | 17:14 |
| maikmerten | s/is easier/are easier | 17:16 |
| ZipCPU | maikmerten: I'm not sure that second block checked what you wanted | 18:01 |
| ZipCPU | The key issue is the idea of $past() --- you want to assert if I_en was true on one clock cycle and I_aluop == `ALUOP_ADD on that same cycle, then result == I_dataS1+I_dataS2 on the next cycle | 18:02 |
| ZipCPU | Or ... am I missing something? 'Cause that's not what you've written | 18:02 |
| *** kraiskil has quit IRC | 18:05 | |
| maikmerten | ZipCPU, yeah, basically if on the preceding posedge I_en was asserted with an ADD-aluop and with values dataS1 and dataS2, then on the current posedge the result should be the sum of the previous input values | 18:06 |
| maikmerten | I assume that https://paste.debian.net/1123060/ is a bit closer | 18:06 |
| tpb | Title: debian Pastezone (at paste.debian.net) | 18:06 |
| maikmerten | (btw, hi!) | 18:07 |
| ZipCPU | Yeah ... that's pretty decent. How'd that work out for you? | 18:07 |
| ZipCPU | (Hi) | 18:07 |
| maikmerten | fails :) | 18:07 |
| ZipCPU | Ok, there's a common bug with addition and widths | 18:07 |
| ZipCPU | Could it be that I_dataS1 + I_dataS2 requires an extra bit that result doesn't have? | 18:07 |
| ZipCPU | A bit that would typically be dropped? | 18:07 |
| maikmerten | very possible | 18:08 |
| ZipCPU | That is, if you force it to the right number of bits, does it then pass? | 18:08 |
| *** emeb has joined #yosys | 18:13 | |
| maikmerten | okay, truncating doesn't help, but the counterexample was an addition with zero as second operand anyways | 18:17 |
| maikmerten | https://pasteboard.co/INwPDYP.png | 18:17 |
| tpb | Title: Pasteboard - Uploaded Image (at pasteboard.co) | 18:17 |
| maikmerten | waveform looks as expected, so I guess the asserts are meh | 18:18 |
| ZipCPU | So ... what's going on? | 18:18 |
| ZipCPU | Can you post your sby file at all? | 18:18 |
| ZipCPU | I'm betting that's where the problem is | 18:19 |
| ZipCPU | Are you running with either "clk2fflogic" or "multiclock on" in your sby file? | 18:19 |
| maikmerten | https://paste.debian.net/1123061/ | 18:19 |
| tpb | Title: debian Pastezone (at paste.debian.net) | 18:19 |
| maikmerten | and yes, multiclock, for no particular reason... | 18:19 |
| maikmerten | so much copy paste, so little insight ;) | 18:20 |
| ZipCPU | Ok, let's take that back out, so remove "multiclock on" and remove any assumptions about your clock within your design. This works if 1) you only have one clock, and 2) you only transition on it's positive edge | 18:20 |
| ZipCPU | If you do otherwise, then we'll need to work a little harder | 18:20 |
| ZipCPU | Are you using $global_clock in your design at all? | 18:22 |
| ZipCPU | If so ... I'd have you remove that as well. (Again, assuming only one continuous clock, and all transitions on its positive edge) | 18:23 |
| maikmerten | no $global_clock | 18:24 |
| ZipCPU | How about clocks and clock edges? Are you using only the one edge of one clock? | 18:24 |
| maikmerten | in that design, I only use posedge I_clk to do stuff | 18:25 |
| ZipCPU | Ok, good ... let's keep going with removing "multiclock on" then | 18:25 |
| maikmerten | https://github.com/maikmerten/spu32/blob/master/cpu/alu.v <-- currently messing around with that | 18:26 |
| tpb | Title: spu32/alu.v at master · maikmerten/spu32 · GitHub (at github.com) | 18:26 |
| maikmerten | removing multiclock provides the same counterexample | 18:26 |
| ZipCPU | Really? Can you post it again? | 18:26 |
| ZipCPU | Also ... does any of your logic use I_clk for anything other than a posedge? | 18:27 |
| maikmerten | https://pasteboard.co/INwUyEf.png <-- fresh trace | 18:29 |
| tpb | Title: Pasteboard - Uploaded Image (at pasteboard.co) | 18:29 |
| ZipCPU | Check I_aluop | 18:30 |
| maikmerten | it's constant zero, which is ALUOP_ADD | 18:30 |
| ZipCPU | Also be aware, when using a test in a clocked logic block, the error will be one step prior to the final step of the trace. In this case, your error is that the MSB is set. | 18:30 |
| ZipCPU | How about I_reset? | 18:30 |
| maikmerten | constant zero | 18:31 |
| ZipCPU | Hmm ... | 18:33 |
| ZipCPU | How old is your Yosys distro? | 18:33 |
| maikmerten | git master from ~2 days ago | 18:33 |
| maikmerten | but quite frankly, I'll assume I messed up before assuming this really is a yosys thing | 18:34 |
| ZipCPU | And your yices distro? | 18:34 |
| ZipCPU | ... a not unlikely assumption ... | 18:34 |
| maikmerten | Yices 2.6.1 | 18:34 |
| maikmerten | Copyright SRI International. | 18:34 |
| maikmerten | Linked with GMP 6.1.2 | 18:34 |
| maikmerten | Copyright Free Software Foundation, Inc. | 18:34 |
| maikmerten | Build date: 2019-05-17 | 18:34 |
| ZipCPU | Ok, your yices is more recent than mine, so I'll assume that's not a problem then | 18:35 |
| maikmerten | fresh bugs, fresh bugs ;-) | 18:35 |
| maikmerten | (nah) | 18:35 |
| ZipCPU | Lol | 18:35 |
| ZipCPU | How about a verilator -Wall check, to see if you are missing anything? | 18:35 |
| * ZipCPU steps away for lunch --will look back again later | 18:36 | |
| ZipCPU | Also ... adding `default_nettype none should find a couple bugs too | 18:37 |
| *** fsasm has joined #yosys | 18:37 | |
| maikmerten | enjoy your lunch :) | 18:38 |
| maikmerten | (it's not verilator, but iverilog -Wall is perfectly happy) | 18:39 |
| maikmerten | ZipCPU, it *was* the reset | 18:48 |
| maikmerten | https://paste.debian.net/1123066/ <-- this is PASS | 18:50 |
| tpb | Title: debian Pastezone (at paste.debian.net) | 18:50 |
| maikmerten | SBY 19:47:20 [alu_prf] summary: successful proof by k-induction. | 18:50 |
| maikmerten | ^^ that sounds nice | 18:50 |
| maikmerten | (pretty amazing that such an automated proof finishes in around 2 seconds) | 18:59 |
| maikmerten | (also passes without truncating the addition) | 19:03 |
| ZipCPU | I thought you had told me reset was low in the trace? | 19:07 |
| maikmerten | yes, and my current theory is that I done goofed badly by confusing GTKWave instances... :( | 19:09 |
| maikmerten | getting a hinch of "let's start over" I cleaned up my window mess, rm -rf'ed some dirs and started fresh | 19:10 |
| maikmerten | and then I could indeed observe a counterexample of I_reset being non-zero at the first clock edge, so that was that... | 19:11 |
| maikmerten | I'm seriously sorry for wasting your time :( | 19:11 |
| *** vidbina has quit IRC | 19:55 | |
| *** fsasm has quit IRC | 20:10 | |
| *** kraiskil has joined #yosys | 20:36 | |
| *** maikmerten has quit IRC | 20:49 | |
| *** emeb_mac has joined #yosys | 20:57 | |
| *** X-Scale has quit IRC | 21:00 | |
| ZipCPU | Oh, ah, okay then. I'm glad you were able to discover the problem! | 21:16 |
| *** vidbina has joined #yosys | 21:18 | |
| *** m_w has joined #yosys | 21:28 | |
| *** m_w has quit IRC | 21:28 | |
| *** m_w has joined #yosys | 21:30 | |
| *** m_w has quit IRC | 21:30 | |
| *** m_w has joined #yosys | 21:32 | |
| *** X-Scale has joined #yosys | 21:38 | |
| *** vidbina has quit IRC | 21:47 | |
| whitequark | daveshah: what(): no enum named 'SLICED.REG0.LSRMODE' | 22:06 |
| whitequark | any idea what can cause this error in ecppack? | 22:07 |
| daveshah | Out o d | 22:07 |
| daveshah | *out of date trellis | 22:07 |
| daveshah | ? | 22:07 |
| whitequark | I just rebuilt prjtrellis and nextpnr-ecp5 twice | 22:07 |
| daveshah | hmm | 22:07 |
| whitequark | let's try third time? | 22:07 |
| daveshah | bet you it's a git issue with the database submodule then | 22:07 |
| whitequark | uh ugh | 22:08 |
| whitequark | i'll try to update that | 22:08 |
| daveshah | or a cmake issue and you have two trellises installed | 22:08 |
| whitequark | btw, do you happen to know what are the conditions for LDR to work? | 22:08 |
| daveshah | I've never actually tried it | 22:08 |
| whitequark | i got it to work, actually | 22:08 |
| whitequark | i had to add TDRV_SLICE_* parameters | 22:08 |
| whitequark | which is... strange | 22:09 |
| daveshah | I guess it's because it still ultimately uses the output H-bridge | 22:09 |
| whitequark | ohh right, so even the BSCAN cell would use the SERDES output? | 22:10 |
| daveshah | Yeah, it still uses the same final output stage | 22:11 |
| whitequark | oh yes I see it now, thanks | 22:11 |
| daveshah | Because they recommend it for things like doing low speed standard and HD SDI on the same pins | 22:11 |
| daveshah | so it would be odd if the signalling level changed | 22:11 |
| whitequark | I'm not sure I understand how the TDRV slices actually work in that case | 22:12 |
| whitequark | but then again it's the sort of thing I can directly observe now | 22:12 |
| whitequark | daveshah: yep, it was the database submodule, thanks! | 22:14 |
| whitequark | daveshah: do you know if there's a way to get EXTREFB.REFCLKO to fabric? | 22:19 |
| daveshah | I don't think there is a direct route, no | 22:22 |
| whitequark | hm, so there's actually no way to get the onboard clock from lfe5um5g-85f-evm to some sort of connector | 22:30 |
| whitequark | i continue to be impressed how useless lattice devboards are | 22:30 |
| whitequark | right now i'm grabbing PCLK and routing it through LDR to one of the SMAs | 22:30 |
| whitequark | but there's something pretty weird about it | 22:30 |
| daveshah | You could just use one of the IO pins and route PCLK to an ODDRX1F? | 22:35 |
| daveshah | if you think LDR is the issue | 22:35 |
| *** lutsabound has joined #yosys | 22:37 | |
| whitequark | I actually think PCLK might be the issue | 22:40 |
| whitequark | or rather, there's something about PCLK I don't understand | 22:40 |
| whitequark | oh I figured it out | 22:46 |
| whitequark | the PCLK duty cycle is very strange | 22:48 |
| whitequark | can be as large as 55% | 22:48 |
| whitequark | daveshah: is this an ecppack bug or is it more likely some issue with prjtrellis versioning again? https://github.com/SymbiFlow/prjtrellis/issues/112 | 23:00 |
| daveshah | No it is a genuine issue of some kind | 23:04 |
| daveshah | I see it here too | 23:04 |
| daveshah | whitequark: I think the problem is nextpnr used a connection that doesn't exist any more | 23:08 |
| whitequark | hmm | 23:09 |
| daveshah | Can you try `touch ecp5/trellis_import.py` and rebuild nextpnr now the db issue is solved (sorry in advance for the CPU time) | 23:09 |
| whitequark | building | 23:09 |
| whitequark | i think that fixed it | 23:27 |
| *** emeb has quit IRC | 23:39 | |
| *** kraiskil has quit IRC | 23:40 | |
| *** m_w has quit IRC | 23:46 | |
| *** Jybz has quit IRC | 23:47 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!
