<awygle>
are there any good examples of throughput-based formal properties?
<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]"
<awygle>
and i can't really figure out how to do that...
<awygle>
i guess i can do a cover trace fairly easily actually
BinaryLust has quit [Ping timeout: 256 seconds]
<az0re>
Do you have a signal for "able to accept a transaction"?
<az0re>
then it should be not(redor(exception_bitvector)) -> able_to_accept_transaction, no?
<az0re>
so "or(not(redor(exception_bitvector)), able_to_accept_transaction)"
BinaryLust has joined #yosys
Cerpin has quit [Ping timeout: 256 seconds]
emeb_mac has quit [Quit: Leaving.]
N2TOH has quit [Ping timeout: 272 seconds]
N2TOH has joined #yosys
jakobwenzel has joined #yosys
dys has quit [Ping timeout: 260 seconds]
N2TOH has quit [Ping timeout: 260 seconds]
dys has joined #yosys
N2TOH has joined #yosys
Cerpin has joined #yosys
Thorn has quit [Ping timeout: 272 seconds]
vidbina has joined #yosys
N2TOH has quit [Read error: Connection reset by peer]
vidbina has quit [Ping timeout: 258 seconds]
N2TOH has joined #yosys
Thorn has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 256 seconds]
N2TOH has joined #yosys
Asu has joined #yosys
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
N2TOH has quit [Ping timeout: 264 seconds]
captain_morgan has quit [Quit: Ping timeout (120 seconds)]
captain_morgan has joined #yosys
N2TOH has joined #yosys
N2TOH has quit [Read error: Connection reset by peer]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
N2TOH has joined #yosys
kraiskil has joined #yosys
N2TOH has quit [Ping timeout: 246 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 240 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
N2TOH has joined #yosys
BinaryLust has quit [Ping timeout: 246 seconds]
kraiskil has quit [Ping timeout: 256 seconds]
N2TOH has quit [Ping timeout: 246 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
N2TOH has joined #yosys
adjtm has joined #yosys
adjtm_ has quit [Ping timeout: 256 seconds]
N2TOH has quit [Ping timeout: 258 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
vidbina has joined #yosys
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 272 seconds]
rrika has quit [Ping timeout: 256 seconds]
rrika_ has joined #yosys
N2TOH has joined #yosys
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
adjtm_ has joined #yosys
adjtm has quit [Ping timeout: 256 seconds]
N2TOH has joined #yosys
N2TOH_ has quit [Read error: Connection reset by peer]
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 240 seconds]
emeb has joined #yosys
kristianpaul has quit [Quit: WeeChat 1.9.1]
kristianpaul has joined #yosys
BinaryLust has joined #yosys
vidbina has quit [Ping timeout: 256 seconds]
kraiskil has joined #yosys
<sensille>
when yosys infers BRAM, it rejects a lot of my smallish register banks with "min efficiency 5' not met (ECP5)
<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?
<sensille>
(and others again get rejected with "Read port #0 is in clock domain !~async~.")
citypw has joined #yosys
<ZirconiumX>
sensille: it's to not waste BRAM, but there needs to be a better heuristic for it all
<ZirconiumX>
I think it will favour LUTRAM for it though
<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.
<sensille>
yeah, some get caught by DPR16X4 later on
<sensille>
i can't find the async read though, the output is explicitly registered
<ZirconiumX>
Generally you want BRAM for deep but narrow memories, and LUTRAM for wide but shallow memories
<ZirconiumX>
Can I see your Verilog module for it?