From e039b6d881e589d89c7812863f84519ca08ca4e2 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 10 Jan 2021 18:18:17 -0300 Subject: [PATCH] Use styles in write_gtkw to simplify the trace description --- src/ieee754/part/formal/proof_partition.py | 54 +++++++++++-------- .../formal/proof_partitioned_eq.py | 24 +++++---- .../formal/proof_partitioned_eq_gt_ge.py | 24 +++++---- 3 files changed, 61 insertions(+), 41 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index c86f262d..d1ba0f80 100644 --- 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 bc464d8a..8acecf82 100644 --- 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 c8d527f9..dbdbc58b 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 @@ -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 ) -- 2.30.2