From e811eb8cf4055455f487fd8c58b33662935701ce Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 10 Jan 2021 18:42:58 -0300 Subject: [PATCH] Generate and check expected values for all possible partition sizes --- src/ieee754/part/formal/proof_partition.py | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index c2ff89ba..4df92e7f 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -33,7 +33,7 @@ import os import unittest import operator -from nmigen import Elaboratable, Signal, Module, Const +from nmigen import Elaboratable, Signal, Module, Const, Repl from nmigen.asserts import Assert, Cover from nmigen.hdl.ast import Assume @@ -363,6 +363,23 @@ class ComparisonOpDriver(Elaboratable): comb += p_output.eq(output[pos:]) comb += p_a.eq(a.sig[pos * step:]) comb += p_b.eq(b.sig[pos * step:]) + # generate and check expected values for all possible partition sizes + for w in range(1, mwidth+1): + with m.If(p_width == w): + # calculate the expected output, for the given bit width, + # truncating the inputs to the partition size + input_bit_width = w * step + output_bit_width = w + expected = Signal(output_bit_width, name=f"expected_{w}") + 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]) + comb += lsb.eq(self.op(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 a test case comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) & (p_a != 0) & (p_b != 0) & (p_output != 0)) @@ -417,7 +434,8 @@ class PartitionTestCase(FHDLTestCase): ('dut', {'submodule': 'dut'}, [ ('gates[6:0]', 'bin'), 'output[63:0]']), - 'p_output[63:0]', 'expected_3[21:0]'] + 'p_output[63:0]', 'expected_3[21:0]', + 'a_3[23:0]', 'b_3[32:0]', 'expected_3[2:0]'] write_gtkw( 'proof_partition_generator_cover.gtkw', os.path.dirname(__file__) + -- 2.30.2