[Libre-soc-bugs] [Bug 429] New: 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

            Bug ID: 429
           Summary: pipeline main_stage formal verification does not check
                    ctx fields fully
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: lkcl at lkcl.net
          Reporter: lkcl at lkcl.net
                CC: libre-soc-bugs at lists.libre-soc.org
   NLnet milestone: ---

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.

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