From: Cesar Strauss Date: Sat, 9 Jan 2021 17:23:03 +0000 (-0300) Subject: Check all possible opcodes for PartitionedEqGtGe X-Git-Tag: ls180-24jan2020~19 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd6b30621da8f64a626bca78f366961431deed72;p=ieee754fpu.git Check all possible opcodes for PartitionedEqGtGe --- diff --git a/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py b/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py index 59231845..9e906353 100644 --- a/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py +++ b/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py @@ -32,7 +32,6 @@ class Driver(Elaboratable): points[(i+1)*step] = gates[i] # instantiate the DUT m.submodules.dut = dut = PartitionedEqGtGe(width, points) - comb += dut.opcode.eq(PartitionedEqGtGe.EQ) # post-process the output to ripple the LSB # TODO: remove this once PartitionedEq is conformant m.submodules.ripple = ripple = RippleLSB(mwidth) @@ -61,9 +60,18 @@ class Driver(Elaboratable): input_bit_width = w * step output_bit_width = w expected = Signal(output_bit_width, name=f"expected_{w}") - comb += expected[0].eq( - p_a[:input_bit_width] == p_b[:input_bit_width]) - comb += expected[1:].eq(Repl(expected[0], output_bit_width-1)) + a = Signal(input_bit_width, name=f"a_{w}") + b = Signal(input_bit_width, name=f"b_{w}") + lsb = Signal(name=f"lsb_{w}") + comb += a.eq(p_a[:input_bit_width]) + comb += b.eq(p_b[:input_bit_width]) + with m.If(dut.opcode == PartitionedEqGtGe.EQ): + comb += lsb.eq(a == b) + with m.Elif(dut.opcode == PartitionedEqGtGe.GT): + comb += lsb.eq(a > b) + with m.Elif(dut.opcode == PartitionedEqGtGe.GE): + comb += lsb.eq(a >= b) + comb += expected.eq(Repl(lsb, output_bit_width)) # truncate the output, compare and assert comb += Assert(p_output[:output_bit_width] == expected) # output an example