<mwk>
pepijndevos: in gowin, why do all the FFs have the INIT parameter? it seems to me that init value is basically determined by the cell type (0 if it has reset, 1 if it has set), and thus the parameter is both unnecessary and invalid (ie. cells with set have INIT of 0 by default. and the techmap rules don't change that default, resulting in sim mismatch)
emeb_mac has quit [Ping timeout: 265 seconds]
<Lofty>
I think it's to match the vendor model, mwk
emeb has quit [Ping timeout: 240 seconds]
<mwk>
Lofty: I'd prefer correct models to vendor-matching models
<mwk>
either the synth flow is buggy and we're using the FFs with set wrong, or the sim library is
emeb has joined #yosys
emeb_mac has joined #yosys
Degi has quit [Ping timeout: 240 seconds]
Degi has joined #yosys
citypw has joined #yosys
proteusguy has quit [Ping timeout: 246 seconds]
citypw has quit [Remote host closed the connection]
emeb has left #yosys [#yosys]
az0re has joined #yosys
az0re has quit [Ping timeout: 240 seconds]
FFY00 has quit [Ping timeout: 244 seconds]
acertain has joined #yosys
emeb_mac has quit [Quit: Leaving.]
<acertain>
i'm trying to use yosys as a frontend for verification tools (& not actually for synthesis), is there a way to unset a reg/cause the generated transition rel to under some conditions not implicitly set next var = var?
<acertain>
actually seems like btor2 might not support this?
nengel has joined #yosys
jakobwenzel has joined #yosys
dys has quit [Ping timeout: 240 seconds]
dys has joined #yosys
kraiskil has joined #yosys
adjtm_ has quit [Quit: Leaving]
Asu has joined #yosys
citypw has joined #yosys
citypw has quit [Quit: Leaving]
citypw has joined #yosys
Asu has quit [Remote host closed the connection]
Asu has joined #yosys
Asu has quit [Remote host closed the connection]
X-Scale has quit [Ping timeout: 246 seconds]
X-Scale` has joined #yosys
X-Scale` is now known as X-Scale
proteusguy has joined #yosys
Asu has joined #yosys
_whitelogger has joined #yosys
Asu has quit [Read error: Connection reset by peer]
Asu has joined #yosys
Asu has quit [Remote host closed the connection]
Asu has joined #yosys
kraiskil has quit [Ping timeout: 264 seconds]
kraiskil has joined #yosys
kraiskil has quit [Max SendQ exceeded]
kraiskil has joined #yosys
kraiskil has quit [Max SendQ exceeded]
kraiskil has joined #yosys
AdamHorden has quit [Ping timeout: 246 seconds]
AdamHorden has joined #yosys
maartenBE has quit [Ping timeout: 260 seconds]
smarter has quit [Ping timeout: 260 seconds]
smarter_ has joined #yosys
ZipCPU has quit [Excess Flood]
ZipCPU has joined #yosys
FFY00 has joined #yosys
minicom has joined #yosys
<ZipCPU>
acertain: What is it you are trying to do? I'm not sure I get it, and I'm also not sure I get why it can't be done in logic in the first place
TFKyle has quit [Ping timeout: 246 seconds]
TFKyle has joined #yosys
<acertain>
in this case i want to check if an incomplete implementation is sufficient for proving a property
kraiskil has quit [Ping timeout: 256 seconds]
<acertain>
regs start as undefined? and verification tools can check if there exists a bad initial value for regs? so i want to be able to set them back to undefined to check the safety property without having to fully specify everything
<acertain>
i guess i could have a big array reg & take bits from it as needed? but i think that would be very inefficient
jakobwenzel has quit [Quit: jakobwenzel]
kraiskil has joined #yosys
jakobwenzel has joined #yosys
<FL4SHK>
So I'm doing `cover(past_rst && bus.empty)`
<FL4SHK>
this does not seem to be working
<FL4SHK>
`if (rst) begin past_rst <= 1'b1; end`
<FL4SHK>
it also won't work for `cover(past_rst)`
FFY00 has quit [Read error: Connection reset by peer]
kraiskil has quit [Read error: Connection reset by peer]
jakobwenzel has quit [Ping timeout: 260 seconds]
FFY00 has joined #yosys
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #yosys
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
jeanthom has joined #yosys
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #yosys
craigo has joined #yosys
craigo has quit [Quit: Leaving]
craigo has joined #yosys
<ZipCPU>
FL4SHK: Did you double check that past_rst was initialized to zero?
<ZipCPU>
'cause ... it should work just fine in a cover statement--it's just logic.
<FL4SHK>
ZipCPU: I'm not sure it got initialized properly given that this is nmigen
craigo has quit [Client Quit]
<ZipCPU>
In order for past_valid to work, it needs to be initialized.
<FL4SHK>
I think I initialized it wrongly
craigo has joined #yosys
<FL4SHK>
ZipCPU: so I'm probably doing this wrongly, but I'm trying to ensure that `cover` doesn't hit an invalid state
<ZipCPU>
Why not assert that the invalid state will never happen?