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

From: bugzilla-daemon@libre-soc.org
To: libre-riscv-dev@lists.libre-riscv.org
Subject: [libre-riscv-dev] [Bug 342] formal proof of soc.fu.compunits.FunctionUnitBaseSingle needed
Date: Tue, 26 May 2020 17:52:49 +0000
Message-ID: <bug-342-13-hxCyxltHdD@https.bugs.libre-soc.org/> (raw)
In-Reply-To: <bug-342-13@https.bugs.libre-soc.org/>

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

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl@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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev