[Libre-soc-bugs] [Bug 429] pipeline main_stage formal verification does not check ctx fields fully

[bugzilla-daemon at libre-soc.org]

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

Luke Kenneth Casson Leighton <lkcl at lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           Assignee|lkcl at lkcl.net               |kc5tja at arrl.net

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #2)
> https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpcommon/
> getop.py;hb=HEAD#l66
> 
> this is the definition of FPPipeContext.

... and it is *not* a nmigen Record.  therefore it is guaranteed that
both of these would silently report "success"

        comb += Assert(dut.o.ctx == dut.i.ctx)
        comb += Assert(dut.o.ctx != dut.i.ctx)

the two members needing checking are ctx.op and ctx.muxid.  this
therefore works:

+        # check that the operation (op) is passed through (and muxid)
+        comb += Assert(dut.o.ctx.op == dut.i.ctx.op )
+        comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid )

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