*** tpb has joined #yosys | 00:00 | |
*** Cerpin has quit IRC | 00:02 | |
*** Cerpin has joined #yosys | 00:09 | |
*** emeb has quit IRC | 00:12 | |
*** BinaryLust has joined #yosys | 01:31 | |
*** strobokopp has quit IRC | 01:52 | |
*** Degi has quit IRC | 03:38 | |
*** Degi has joined #yosys | 03:38 | |
*** Cerpin has quit IRC | 04:16 | |
*** Cerpin has joined #yosys | 04:17 | |
awygle | are there any good examples of throughput-based formal properties? | 04:21 |
---|---|---|
awygle | trying to phrase the requirement "assuming a sink which tries to read every cycle, this core's sink must be able to accept one transaction every clock cycle unless [list of exceptions]" | 04:22 |
awygle | and i can't really figure out how to do that... | 04:22 |
awygle | i guess i can do a cover trace fairly easily actually | 04:28 |
*** BinaryLust has quit IRC | 05:00 | |
az0re | Do you have a signal for "able to accept a transaction"? | 05:35 |
az0re | then it should be not(redor(exception_bitvector)) -> able_to_accept_transaction, no? | 05:36 |
az0re | so "or(not(redor(exception_bitvector)), able_to_accept_transaction)" | 05:39 |
*** BinaryLust has joined #yosys | 06:09 | |
*** Cerpin has quit IRC | 06:40 | |
*** emeb_mac has quit IRC | 06:42 | |
*** N2TOH has quit IRC | 07:01 | |
*** N2TOH has joined #yosys | 07:03 | |
*** jakobwenzel has joined #yosys | 07:06 | |
*** dys has quit IRC | 07:08 | |
*** N2TOH has quit IRC | 07:21 | |
*** dys has joined #yosys | 07:23 | |
*** N2TOH has joined #yosys | 07:24 | |
*** Cerpin has joined #yosys | 07:51 | |
*** Thorn has quit IRC | 08:05 | |
*** vidbina has joined #yosys | 08:07 | |
*** N2TOH has quit IRC | 08:10 | |
*** vidbina has quit IRC | 08:12 | |
*** N2TOH has joined #yosys | 08:15 | |
*** Thorn has joined #yosys | 08:23 | |
*** N2TOH has quit IRC | 08:24 | |
*** N2TOH has joined #yosys | 08:26 | |
*** N2TOH has quit IRC | 08:32 | |
*** N2TOH has joined #yosys | 08:44 | |
*** Asu has joined #yosys | 08:48 | |
*** futarisIRCcloud has quit IRC | 08:55 | |
*** N2TOH has quit IRC | 09:11 | |
*** captain_morgan has quit IRC | 09:12 | |
*** captain_morgan has joined #yosys | 09:13 | |
*** N2TOH has joined #yosys | 09:18 | |
*** N2TOH has quit IRC | 09:53 | |
*** N2TOH has joined #yosys | 09:54 | |
*** N2TOH has quit IRC | 10:02 | |
*** N2TOH has joined #yosys | 10:03 | |
*** N2TOH has quit IRC | 10:09 | |
*** N2TOH has joined #yosys | 10:14 | |
*** kraiskil has joined #yosys | 10:14 | |
*** N2TOH has quit IRC | 10:28 | |
*** N2TOH has joined #yosys | 10:32 | |
*** N2TOH has quit IRC | 10:42 | |
*** N2TOH has joined #yosys | 10:55 | |
*** N2TOH has quit IRC | 11:09 | |
*** N2TOH has joined #yosys | 11:20 | |
*** BinaryLust has quit IRC | 11:25 | |
*** kraiskil has quit IRC | 11:36 | |
*** N2TOH has quit IRC | 11:42 | |
*** N2TOH has joined #yosys | 11:45 | |
*** N2TOH has quit IRC | 11:58 | |
*** N2TOH has joined #yosys | 12:02 | |
*** adjtm has joined #yosys | 12:16 | |
*** adjtm_ has quit IRC | 12:18 | |
*** N2TOH has quit IRC | 12:33 | |
*** N2TOH has joined #yosys | 12:45 | |
*** N2TOH has quit IRC | 12:50 | |
*** vidbina has joined #yosys | 12:54 | |
*** N2TOH has joined #yosys | 12:55 | |
*** N2TOH has quit IRC | 13:00 | |
*** rrika has quit IRC | 13:03 | |
*** rrika_ has joined #yosys | 13:03 | |
*** N2TOH has joined #yosys | 13:07 | |
*** N2TOH_ has joined #yosys | 13:11 | |
*** N2TOH has quit IRC | 13:13 | |
*** adjtm_ has joined #yosys | 13:30 | |
*** adjtm has quit IRC | 13:32 | |
*** N2TOH has joined #yosys | 13:33 | |
*** N2TOH_ has quit IRC | 13:34 | |
*** N2TOH_ has joined #yosys | 13:34 | |
*** N2TOH has quit IRC | 13:37 | |
*** emeb has joined #yosys | 14:01 | |
*** kristianpaul has quit IRC | 14:11 | |
*** kristianpaul has joined #yosys | 14:14 | |
*** BinaryLust has joined #yosys | 14:36 | |
*** vidbina has quit IRC | 14:46 | |
*** kraiskil has joined #yosys | 14:51 | |
sensille | when yosys infers BRAM, it rejects a lot of my smallish register banks with "min efficiency 5' not met (ECP5) | 14:54 |
sensille | is that only not to waste bram, or also that the overhead to use the bram would be similar to not using it at all? | 14:54 |
sensille | (and others again get rejected with "Read port #0 is in clock domain !~async~.") | 15:04 |
*** citypw has joined #yosys | 15:24 | |
ZirconiumX | sensille: it's to not waste BRAM, but there needs to be a better heuristic for it all | 15:27 |
ZirconiumX | I think it will favour LUTRAM for it though | 15:28 |
ZirconiumX | sensille: (and others again get rejected with "Read port #0 is in clock domain !~async~.") <--- the ECP5 has synchronous read, but you're asking for asynchronous read, for which it would use LUTRAM. | 15:30 |
sensille | yeah, some get caught by DPR16X4 later on | 15:30 |
sensille | i can't find the async read though, the output is explicitly registered | 15:31 |
ZirconiumX | Generally you want BRAM for deep but narrow memories, and LUTRAM for wide but shallow memories | 15:31 |
ZirconiumX | Can I see your Verilog module for it? | 15:32 |
sensille | https://github.com/sensille/conan_fpga/blob/master/fifo.v | 15:33 |
tpb | Title: conan_fpga/fifo.v at master · sensille/conan_fpga · GitHub (at github.com) | 15:33 |
sensille | for the async read warning | 15:33 |
*** BinaryLust has quit IRC | 15:37 | |
*** jakobwenzel has quit IRC | 15:44 | |
*** kristianpaul has quit IRC | 15:45 | |
*** kristianpaul has joined #yosys | 15:49 | |
*** jfcaron has joined #yosys | 15:52 | |
ZirconiumX | sensille: can you give the exact module path of the thing you want inferred as BRAM? | 15:56 |
ZirconiumX | Like, conan.u_command.u_stepper.genstepdir[0].u_stepdir.u_fifo.ram | 15:56 |
*** kraiskil has quit IRC | 15:58 | |
ZirconiumX | Since as far as I can tell, the async read thing isn't actually a warning | 15:59 |
*** citypw has quit IRC | 16:00 | |
sensille | ZirconiumX: conan.u_framing.recv_ring for example | 16:22 |
sensille | and conan.u_framing.send_ring | 16:23 |
ZirconiumX | The error is actually this: Bram port B1.1 has incompatible clock type. | 16:24 |
*** BinaryLust has joined #yosys | 16:25 | |
ZirconiumX | By the way, you don't need to bother with `verilog -defer` if you use sensible defaults | 16:26 |
ZirconiumX | daveshah: can you take a look at this? | 16:28 |
daveshah | Are you initialising or resetting the output register? | 16:29 |
ZirconiumX | Doesn't look like it | 16:30 |
daveshah | I can have a look later | 16:31 |
sensille | indeed, "Bram port B1.1 has incompatible clock type." is in the next line | 16:36 |
sensille | at least my intention is that everything is driven by the one and only clk | 16:37 |
*** kraiskil has joined #yosys | 16:50 | |
daveshah | With data width 8, address width 12, that file infers memory fine for me | 16:53 |
ZirconiumX | The params used are data width 6 address width 5 | 16:54 |
daveshah | Oh, then yes it seems to fail efficiency criterea | 16:55 |
sensille | efficiency=22 | 16:55 |
sensille | https://pastebin.com/vmrvT4dB | 16:56 |
tpb | Title: Processing conan.u_framing.recv_ring: Properties: ports=2 bits=4096 rports=1 - Pastebin.com (at pastebin.com) | 16:56 |
daveshah | Oh, not the FIFO module | 16:56 |
sensille | it is probably how i use the fifo module | 16:56 |
sensille | it is an instance of the fifo module | 16:57 |
ZirconiumX | > reg [7:0] recv_ring [RING_SIZE-1:0]; | 16:57 |
ZirconiumX | No, it's not | 16:57 |
daveshah | That looks like an async port? | 16:58 |
daveshah | https://github.com/sensille/conan_fpga/blob/master/framing.v#L84 | 16:58 |
tpb | Title: conan_fpga/framing.v at master · sensille/conan_fpga · GitHub (at github.com) | 16:58 |
* sensille blushes with shame | 17:03 | |
sensille | ZirconiumX, daveshah: sorry, i don't know where i got the idea from it's the fifo. the fifo just fails the efficiency test | 17:04 |
sensille | thanks for looking at this | 17:05 |
ZirconiumX | No, I'm looking through the FIFO mappings, and it seems like all of them pass the efficiency test at 92% | 17:06 |
daveshah | I think it would actually have mapped (as a transparent port, with the reg on the address) without the '= 0' here: https://github.com/sensille/conan_fpga/blob/master/framing.v#L83 | 17:07 |
tpb | Title: conan_fpga/framing.v at master · sensille/conan_fpga · GitHub (at github.com) | 17:08 |
sensille | conan.u_framing.send_len_fifo.ram fails with 1% | 17:08 |
sensille | why is initializing the rptr a problem? | 17:10 |
ZirconiumX | Because Yosys can't merge flops into memories at the moment | 17:10 |
sensille | i guess i could initialize rptr with the first clk | 17:13 |
sensille | alternatively i need to register the output? | 17:13 |
ZirconiumX | You already have a clear option to initialise rptr | 17:16 |
ZirconiumX | Really though, I don't know much about memories here | 17:17 |
*** cr1901_modern has quit IRC | 17:18 | |
*** cr1901_modern has joined #yosys | 17:26 | |
*** dys has quit IRC | 17:27 | |
*** Twix has quit IRC | 17:28 | |
*** Twix has joined #yosys | 17:31 | |
*** klotz has joined #yosys | 17:42 | |
*** kraiskil has quit IRC | 18:04 | |
*** klotz has quit IRC | 18:05 | |
*** klotz has joined #yosys | 18:06 | |
*** vidbina has joined #yosys | 18:13 | |
*** klotz has quit IRC | 19:10 | |
*** vidbina has quit IRC | 19:29 | |
*** forrestv has quit IRC | 19:55 | |
*** Kamilion has quit IRC | 19:55 | |
*** az0re has quit IRC | 19:58 | |
*** dys has joined #yosys | 20:05 | |
*** forrestv has joined #yosys | 20:15 | |
*** Kamilion has joined #yosys | 20:17 | |
*** FFY00 has quit IRC | 20:20 | |
*** FFY00 has joined #yosys | 20:21 | |
*** Asuu has joined #yosys | 20:26 | |
*** Asu has quit IRC | 20:27 | |
*** emeb_mac has joined #yosys | 20:37 | |
*** forrestv has quit IRC | 20:45 | |
*** Kamilion has quit IRC | 20:45 | |
*** forrestv has joined #yosys | 20:55 | |
*** jfcaron has quit IRC | 21:01 | |
*** vidbina has joined #yosys | 21:11 | |
*** BinaryLust has quit IRC | 21:12 | |
*** kraiskil has joined #yosys | 21:36 | |
*** Kamilion has joined #yosys | 21:37 | |
*** smkz is now known as __builtin_trap | 22:01 | |
*** futarisIRCcloud has joined #yosys | 22:03 | |
*** az0re has joined #yosys | 22:10 | |
*** Cerpin has quit IRC | 22:10 | |
*** Cerpin has joined #yosys | 22:10 | |
*** kraiskil has quit IRC | 22:21 | |
*** Cerpin has quit IRC | 22:28 | |
*** Cerpin has joined #yosys | 22:28 | |
*** Cerpin has quit IRC | 22:42 | |
*** Cerpin has joined #yosys | 22:42 | |
*** Asuu has quit IRC | 23:21 | |
*** BinaryLust has joined #yosys | 23:21 |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!