alu/spr/etc. main_stage.py: comb += self.o.ctx.eq(self.i.ctx) however the formal correctness proofs only do this: comb += dut.i.ctx.op.eq(rec) # Assert that op gets copied from the input to output for rec_sig in rec.ports(): name = rec_sig.name dut_sig = getattr(dut.o.ctx.op, name) comb += Assert(dut_sig == rec_sig) the remainder of the ctx fields also need verifying.
hm i asked on irc #nmigen and Assert on Record instances should work, straight. it therefore should not be necessary to walk the fields of the Record: simply assign the Record and assert it.
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. FPPipeContext is the base for ReservationStations context information. it therefore contains muxid and an op. Samuel when you ran the proof and found that ctx was not working, which Signal failed in the counterexample?
(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 )
commit b9bf80737f94469f387ae3df24e223f505c9c2bc (HEAD -> master) Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net> Date: Wed Jul 15 11:49:52 2020 +0100 use Record Assert and also check muxid see https://bugs.libre-soc.org/show_bug.cgi?id=429#c3
https://freenode.irclog.whitequark.org/nmigen/2020-07-15#27508083; really needs a nmigen bugreport
Due to my lack of experience with the workflow and build environment, I'm not confident this is a real bug just yet. Let me gain some more experience with different parts of the ALU; I could have been doing something wrong.
(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.