From 98efb59eec8e333d72281022917c42e3d114e7b1 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Tue, 28 Jan 2020 12:38:35 -0500 Subject: [PATCH] Flesh out the formal proof for fmax --- src/ieee754/fpmax/formal/proof_fmax_mod.py | 25 +++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/ieee754/fpmax/formal/proof_fmax_mod.py b/src/ieee754/fpmax/formal/proof_fmax_mod.py index 386cd0fd..5471eee6 100644 --- a/src/ieee754/fpmax/formal/proof_fmax_mod.py +++ b/src/ieee754/fpmax/formal/proof_fmax_mod.py @@ -1,7 +1,7 @@ # Proof of correctness for FPMAX module # Copyright (C) 2020 Michael Nolan -from nmigen import Module, Signal, Elaboratable +from nmigen import Module, Signal, Elaboratable, Cat, Mux from nmigen.asserts import Assert, Assume from nmigen.cli import rtlil @@ -26,6 +26,7 @@ class FPMAXDriver(Elaboratable): def elaborate(self, platform): m = Module() + width = self.pspec.width m.submodules.dut = dut = FPMAXPipeMod(self.pspec) a1 = FPNumBaseRecord(self.pspec.width, False) @@ -41,6 +42,28 @@ class FPMAXDriver(Elaboratable): m.d.comb += Assert((z1.v == a1.v) | (z1.v == b1.v) | (z1.v == a1.fp.nan2(0))) + with m.If(a1.is_nan & b1.is_nan): + m.d.comb += Assert(z1.is_nan) + with m.Elif(a1.is_nan & ~b1.is_nan): + m.d.comb += Assert(z1.v == b1.v) + with m.Elif(b1.is_nan & ~a1.is_nan): + m.d.comb += Assert(z1.v == a1.v) + with m.Else(): + isrhs = Signal() + # if a1 is negative and b1 isn't, then we should return b1 + with m.If(a1.s != b1.s): + m.d.comb += isrhs.eq(a1.s > b1.s) + with m.Else(): + # if they both have the same sign + gt = Signal() + m.d.comb += gt.eq(self.a[0:width-1] < self.b[0:width-1]) + m.d.comb += isrhs.eq(gt ^ a1.s) + + with m.If(self.opc == 0): + m.d.comb += Assert(z1.v == + Mux(self.opc[0] ^ isrhs, + b1.v, a1.v)) + # connect up the inputs and outputs. I think these could # theoretically be $anyconst/$anysync but I'm not sure nmigen # has support for that -- 2.30.2