projects
/
ieee754fpu.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
def9d37
)
Use styles in write_gtkw to simplify the trace description
author
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 21:18:17 +0000
(18:18 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 21:18:17 +0000
(18:18 -0300)
src/ieee754/part/formal/proof_partition.py
patch
|
blob
|
history
src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
patch
|
blob
|
history
src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
patch
|
blob
|
history
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):
class PartitionTestCase(FHDLTestCase):
def test_formal(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
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'}, [
('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',
'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
)
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',
'proof_partition_bmc.gtkw',
os.path.dirname(__file__) +
'/proof_partition_formal/engine_0/trace.vcd',
- traces,
+ traces,
style,
module='top',
zoom=-3
)
module='top',
zoom=-3
)
@@
-391,20
+395,24
@@
class PartitionTestCase(FHDLTestCase):
self.assertFormal(module, mode="cover", depth=1)
def test_generator(self):
self.assertFormal(module, mode="cover", depth=1)
def test_generator(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
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'}, [
('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',
'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
)
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',
'proof_partition_generator_bmc.gtkw',
os.path.dirname(__file__) +
'/proof_partition_generator/engine_0/trace.vcd',
- traces,
+ traces,
style,
module='top',
zoom=-3
)
module='top',
zoom=-3
)
@@
-421,19
+429,23
@@
class PartitionTestCase(FHDLTestCase):
self.assertFormal(module, mode="cover", depth=1)
def test_partsig_eq(self):
self.assertFormal(module, mode="cover", depth=1)
def test_partsig_eq(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
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'}, [
('eq_1', {'submodule': 'eq_1'}, [
- ('gates[6:0]',
{'base': 'bin'}
),
+ ('gates[6:0]',
'bin'
),
'a[63:0]', 'b[63:0]',
'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',
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
)
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',
'proof_partsig_eq_bmc.gtkw',
os.path.dirname(__file__) +
'/proof_partition_partsig_eq/engine_0/trace.vcd',
- traces,
+ traces,
style,
module='top',
zoom=-3
)
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):
class PartitionedEqTestCase(FHDLTestCase):
def test_formal(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
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'}, [
('dut', {'submodule': 'dut'}, [
- ('gates[6:0]',
{'base': 'bin'}
),
+ ('gates[6:0]',
'bin'
),
'a[63:0]', 'b[63:0]',
'a[63:0]', 'b[63:0]',
- ('output[7:0]',
{'base': 'bin'}
)]),
+ ('output[7:0]',
'bin'
)]),
('ripple', {'submodule': 'ripple'}, [
('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',
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
)
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',
'proof_partitioned_eq_bmc.gtkw',
os.path.dirname(__file__) +
'/proof_partitioned_eq_formal/engine_0/trace.vcd',
- traces,
+ traces,
style,
module='top',
zoom=-3
)
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):
class PartitionedEqTestCase(FHDLTestCase):
def test_formal(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
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'}, [
('dut', {'submodule': 'dut'}, [
- ('gates[6:0]',
{'base': 'bin'}
),
+ ('gates[6:0]',
'bin'
),
'a[63:0]', 'b[63:0]',
'a[63:0]', 'b[63:0]',
- ('output[7:0]',
{'base': 'bin'}
)]),
+ ('output[7:0]',
'bin'
)]),
('ripple', {'submodule': 'ripple'}, [
('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',
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
)
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',
'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
)
module='top',
zoom=-3
)