projects
/
ieee754fpu.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
feadebe
)
Add the Gate Generator to the ComparisonOpDriver
author
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 20:56:29 +0000
(17:56 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 20:56:29 +0000
(17:56 -0300)
src/ieee754/part/formal/proof_partition.py
patch
|
blob
|
history
diff --git
a/src/ieee754/part/formal/proof_partition.py
b/src/ieee754/part/formal/proof_partition.py
index 54c9f98f90c8c3b794a4ec1267a565d51e3fdc62..c86f262dd471eb5edbc1b5fced6de8c508285385 100644
(file)
--- 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))
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
# output a test case
- comb += Cover(
output != 0
)
+ comb += Cover(
(p_offset != 0) & (p_width == 3) & (sum(output) > 1)
)
return m
return m
@@
-417,6
+422,9
@@
class PartitionTestCase(FHDLTestCase):
def test_partsig_eq(self):
traces = [
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]',
('eq_1', {'submodule': 'eq_1'}, [
('gates[6:0]', {'base': 'bin'}),
'a[63:0]', 'b[63:0]',