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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 26 18:35:49 BST 2020


--- 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.

More information about the libre-riscv-dev mailing list