From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 10 Jan 2021 20:56:29 +0000 (-0300)
Subject: Add the Gate Generator to the ComparisonOpDriver
X-Git-Tag: ls180-24jan2020~13
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=def9d3725d092926eaabf8ecefb72b3510e249ee;p=ieee754fpu.git

Add the Gate Generator to the ComparisonOpDriver
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 54c9f98f..c86f262d 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -349,8 +349,13 @@ class ComparisonOpDriver(Elaboratable):
         b.set_module(m)
         # perform the operation on the partitioned signals
         comb += output.eq(self.op(a, b))
+        # instantiate the partitioned gate generator and connect the gates
+        m.submodules.gen = gen = GateGenerator(mwidth)
+        comb += gates.eq(gen.gates)
+        p_offset = gen.p_offset
+        p_width = gen.p_width
         # output a test case
-        comb += Cover(output != 0)
+        comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1))
         return m
 
 
@@ -417,6 +422,9 @@ class PartitionTestCase(FHDLTestCase):
 
     def test_partsig_eq(self):
         traces = [
+            ('p_offset[2:0]', {'base': 'dec'}),
+            ('p_width[3:0]', {'base': 'dec'}),
+            ('p_gates[8:0]', {'base': 'bin'}),
             ('eq_1', {'submodule': 'eq_1'}, [
                 ('gates[6:0]', {'base': 'bin'}),
                 'a[63:0]', 'b[63:0]',