az0re has quit [Remote host closed the connection]
az0re has joined #yosys
Asu has joined #yosys
vidbina has joined #yosys
DaKnig has joined #yosys
vidbina has quit [Ping timeout: 258 seconds]
Forty-Bot has quit [Read error: Connection reset by peer]
Forty-Bot has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
citypw has joined #yosys
vidbina has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
wiizzard has quit [*.net *.split]
MoeIcenowy has quit [*.net *.split]
MoeIcenowy has joined #yosys
wiizzard has joined #yosys
emeb has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
vidbina has quit [Ping timeout: 260 seconds]
<tnt>
:/ Is there something more to do that adding 'multiclock on' in the .sby for riscv formal to behavre properly with @negedge in the design ?
<tnt>
without it I get 'FAIL' for the reg_ch0 test. With it on, I get 'PASS' ... but I get PASS also if I voluntarely add a bug in my register implementation so that doesn't inspire much confidence that the testing is working.
<daveshah>
You may need to double all the bmc depths too
<daveshah>
With multiclock on, it will be two solver steps per clock cycle
<tnt>
ok, I doubled `depth` and `skip`
<tnt>
Ok, it failed on the purposefully buggy implementation, good first step. Lets see how it does on the (hopefully) correct one.
<tnt>
Arf, failed :/
<tnt>
And the trace vcd is showing me nothing AFAICT. I mean the register write enable is low for the entire trace so not sure what's it expecting there.
<daveshah>
It might be to do with skip and the fact that multiclock gives it the freedom to keep the clock stuck not toggling
<daveshah>
You might need to constrain the clock, although this is slightly beyond my formal experience
<tnt>
In the vcd at least I see it toggling regularely.
<daveshah>
Ah, that probably isn't the problem then