Use styles in write_gtkw to simplify the trace description

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index c86f262dd471eb5edbc1b5fced6de8c508285385..d1ba0f802095e2058c37af606b552d525fe96dd2 100644 (file)
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -361,20 +361,24 @@ class ComparisonOpDriver(Elaboratable):
 
 class PartitionTestCase(FHDLTestCase):
     def test_formal(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
         traces = [
-            ('p_offset[2:0]', {'base': 'dec'}),
-            ('p_width[3:0]', {'base': 'dec'}),
-            ('p_finish[3:0]', {'base': 'dec'}),
-            ('p_gates[8:0]', {'base': 'bin'}),
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_finish[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
             ('dut', {'submodule': 'dut'}, [
-                ('gates[6:0]', {'base': 'bin'}),
+                ('gates[6:0]', 'bin'),
                 'output[63:0]']),
             'p_output[63:0]', 'expected_3[21:0]']
         write_gtkw(
             'proof_partition_cover.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_formal/engine_0/trace0.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -382,7 +386,7 @@ class PartitionTestCase(FHDLTestCase):
             'proof_partition_bmc.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_formal/engine_0/trace.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -391,20 +395,24 @@ class PartitionTestCase(FHDLTestCase):
         self.assertFormal(module, mode="cover", depth=1)
 
     def test_generator(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
         traces = [
-            ('p_offset[2:0]', {'base': 'dec'}),
-            ('p_width[3:0]', {'base': 'dec'}),
-            ('p_finish[3:0]', {'base': 'dec'}),
-            ('p_gates[8:0]', {'base': 'bin'}),
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_finish[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
             ('dut', {'submodule': 'dut'}, [
-                ('gates[6:0]', {'base': 'bin'}),
+                ('gates[6:0]', 'bin'),
                 'output[63:0]']),
             'p_output[63:0]', 'expected_3[21:0]']
         write_gtkw(
             'proof_partition_generator_cover.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_generator/engine_0/trace0.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -412,7 +420,7 @@ class PartitionTestCase(FHDLTestCase):
             'proof_partition_generator_bmc.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_generator/engine_0/trace.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -421,19 +429,23 @@ class PartitionTestCase(FHDLTestCase):
         self.assertFormal(module, mode="cover", depth=1)
 
     def test_partsig_eq(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
         traces = [
-            ('p_offset[2:0]', {'base': 'dec'}),
-            ('p_width[3:0]', {'base': 'dec'}),
-            ('p_gates[8:0]', {'base': 'bin'}),
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
             ('eq_1', {'submodule': 'eq_1'}, [
-                ('gates[6:0]', {'base': 'bin'}),
+                ('gates[6:0]', 'bin'),
                 'a[63:0]', 'b[63:0]',
-                ('output[7:0]', {'base': 'bin'})])]
+                ('output[7:0]', 'bin')])]
         write_gtkw(
             'proof_partsig_eq_cover.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_partsig_eq/engine_0/trace0.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -441,7 +453,7 @@ class PartitionTestCase(FHDLTestCase):
             'proof_partsig_eq_bmc.gtkw',
             os.path.dirname(__file__) +
             '/proof_partition_partsig_eq/engine_0/trace.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )

diff --git a/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py b/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
index bc464d8ab0fc08df3a51b8bdbb27a250a4a68787..8acecf82c4095e33f15b8e915879a82cc555d605 100644 (file)
--- a/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
+++ b/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
@@ -70,23 +70,27 @@ class Driver(Elaboratable):
 class PartitionedEqTestCase(FHDLTestCase):
 
     def test_formal(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
         traces = [
-            ('p_offset[2:0]', {'base': 'dec'}),
-            ('p_width[3:0]', {'base': 'dec'}),
-            ('p_gates[8:0]', {'base': 'bin'}),
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
             ('dut', {'submodule': 'dut'}, [
-                ('gates[6:0]', {'base': 'bin'}),
+                ('gates[6:0]', 'bin'),
                 'a[63:0]', 'b[63:0]',
-                ('output[7:0]', {'base': 'bin'})]),
+                ('output[7:0]', 'bin')]),
             ('ripple', {'submodule': 'ripple'}, [
-                ('output[7:0]', {'base': 'bin'})]),
-            ('p_output[7:0]', {'base': 'bin'}),
-            ('expected_3[2:0]', {'base': 'bin'})]
+                ('output[7:0]', 'bin')]),
+            ('p_output[7:0]', 'bin'),
+            ('expected_3[2:0]', 'bin')]
         write_gtkw(
             'proof_partitioned_eq_cover.gtkw',
             os.path.dirname(__file__) +
             '/proof_partitioned_eq_formal/engine_0/trace0.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -94,7 +98,7 @@ class PartitionedEqTestCase(FHDLTestCase):
             'proof_partitioned_eq_bmc.gtkw',
             os.path.dirname(__file__) +
             '/proof_partitioned_eq_formal/engine_0/trace.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )

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 c8d527f9d37f0e2011394b0718bbbde44a0d3393..dbdbc58b2f578bc4a8e8883878e70f882d090436 100644 (file)
--- a/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
+++ b/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
@@ -79,23 +79,27 @@ class Driver(Elaboratable):
 class PartitionedEqTestCase(FHDLTestCase):
 
     def test_formal(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
         traces = [
-            ('p_offset[2:0]', {'base': 'dec'}),
-            ('p_width[3:0]', {'base': 'dec'}),
-            ('p_gates[8:0]', {'base': 'bin'}),
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
             ('dut', {'submodule': 'dut'}, [
-                ('gates[6:0]', {'base': 'bin'}),
+                ('gates[6:0]', 'bin'),
                 'a[63:0]', 'b[63:0]',
-                ('output[7:0]', {'base': 'bin'})]),
+                ('output[7:0]', 'bin')]),
             ('ripple', {'submodule': 'ripple'}, [
-                ('output[7:0]', {'base': 'bin'})]),
-            ('p_output[7:0]', {'base': 'bin'}),
-            ('expected_3[2:0]', {'base': 'bin'})]
+                ('output[7:0]', 'bin')]),
+            ('p_output[7:0]', 'bin'),
+            ('expected_3[2:0]', 'bin')]
         write_gtkw(
             'proof_partitioned_eq_gt_ge_cover.gtkw',
             os.path.dirname(__file__) +
             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace0.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )
@@ -103,7 +107,7 @@ class PartitionedEqTestCase(FHDLTestCase):
             'proof_partitioned_eq_gt_ge_bmc.gtkw',
             os.path.dirname(__file__) +
             '/proof_partitioned_eq_gt_ge_formal/engine_0/trace.vcd',
-            traces,
+            traces, style,
             module='top',
             zoom=-3
         )