[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 #7 from Michael Nolan <mtnolan2640 at gmail.com> ---
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.

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