[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

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #6)
> Due to my lack of experience with the workflow and build environment, I'm
> not confident this is a real bug just yet. 

nono, it is.  you cannot compare python object instances and expect them to
automatically enumerate the nmigen Signals or Records in them.

you had done this:

class Obj: pass

x = Obj()
y = Obj()

Assert(x == y)

which of course returns the boolean "false" which of course Assert(false)
raises the assert failure condition.

so you changed it to Assert (x != y) and of course object x is not equal to
object y so the Formal Proof passed.

what you *expected* was that the Signals inside ctx would be automatically
enumerated and compared and that simply does not happen without some
infrastructure.

what would be necessary is to add an __eq__ function and to implement it to
perform a comparison against ctx.muxid and against ctx.op

class Context
    def __eq__(self, rhs):
        return self.muxid == rhs.muxid and
               self.op == rhs.op

we might as well just do

     Assert (x.muxid == y.muxid)
     Assert (x.op == y.op)

and not worry about it.

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