projects
/
ieee754fpu.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e039b6d
)
Generate shifted down input and outputs
author
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 21:33:10 +0000
(18:33 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sun, 10 Jan 2021 21:33:10 +0000
(18:33 -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 d1ba0f802095e2058c37af606b552d525fe96dd2..c2ff89ba15ad0af475a5a761be2134ebbaac88ea 100644
(file)
--- a/
src/ieee754/part/formal/proof_partition.py
+++ b/
src/ieee754/part/formal/proof_partition.py
@@
-354,8
+354,18
@@
class ComparisonOpDriver(Elaboratable):
comb += gates.eq(gen.gates)
p_offset = gen.p_offset
p_width = gen.p_width
comb += gates.eq(gen.gates)
p_offset = gen.p_offset
p_width = gen.p_width
+ # generate shifted down inputs and outputs
+ p_output = Signal(mwidth)
+ p_a = Signal(width)
+ p_b = Signal(width)
+ for pos in range(mwidth):
+ with m.If(p_offset == pos):
+ comb += p_output.eq(output[pos:])
+ comb += p_a.eq(a.sig[pos * step:])
+ comb += p_b.eq(b.sig[pos * step:])
# output a test case
# output a test case
- comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1))
+ comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) &
+ (p_a != 0) & (p_b != 0) & (p_output != 0))
return m
return m
@@
-440,7
+450,9
@@
class PartitionTestCase(FHDLTestCase):
('eq_1', {'submodule': 'eq_1'}, [
('gates[6:0]', 'bin'),
'a[63:0]', 'b[63:0]',
('eq_1', {'submodule': 'eq_1'}, [
('gates[6:0]', 'bin'),
'a[63:0]', 'b[63:0]',
- ('output[7:0]', 'bin')])]
+ ('output[7:0]', 'bin')]),
+ 'p_a[63:0]', 'p_b[63:0]',
+ ('p_output[7:0]', 'bin')]
write_gtkw(
'proof_partsig_eq_cover.gtkw',
os.path.dirname(__file__) +
write_gtkw(
'proof_partsig_eq_cover.gtkw',
os.path.dirname(__file__) +