[libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=342

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #7)
> with m.If(Past(wr_rel) & Past(go_wr)):
>     # the alu data is output
>     comb += Assert(dut.data_o == alu_temp)
>     # wr_rel is dropped
>     comb += Assert(wr_rel == 0)
>     # busy is dropped.
>     with m.If(~Past(go_die)):
> 	comb += Assert(busy == 0)
> 
> 
> Shouldn't the module drop busy after go_die is asserted? If I delete the
> m.If(~Past(go_die)) the proof fails.

annoyingly, it's one cycle after, because of the syncs setting the latches.

fascinatingly, in practice, we get away with it.  the code is complex enough
that i am not sure why.

-- 
You are receiving this mail because:
You are on the CC list for the bug.