You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
=== equiv ===
Number of wires: 3283
Number of wire bits: 3283
Number of public wires: 2696
Number of public wire bits: 2696
Number of memories: 0
Number of memory bits: 0
Number of processes: 0
Number of cells: 1006
$_AND_ 401
$_DFF_PN0_ 1
$_DFF_PP0_ 126
$_NOT_ 250
$_OR_ 220
$equiv 8
27.13. Executing CHECK pass (checking for obvious problems).
Checking module equiv...
Found and reported 0 problems.
28. Executing EQUIV_SIMPLE pass.
Found 3 unproven $equiv cells (3 groups) in equiv:
Trying to prove $equiv cell $auto$equiv_make.cc:359:find_same_cells$13331:
A = \_023__gold, B = \_023__gate, Y = \_505_.D
Adding 13 new cells to the problem (11 A, 11 B, 9 shared).
Problem size at t=10: 72 literals, 169 clauses
Failed to prove equivalence with sequence length 0.
No nets to continue in previous time step.
Trying to prove $equiv cell $auto$equiv_make.cc:251:find_same_wires$13028:
A = \_444__gold.IQ, B = \_444__gate.IQ, Y = \p
Adding 0 new cells to the problem (0 A, 0 B, 0 shared).
Problem size at t=10: 8 literals, 12 clauses
Failed to prove equivalence with sequence length 0.
No nets to continue in previous time step.
Trying to prove $equiv cell $auto$equiv_make.cc:359:find_same_cells$13465:
A = \_446__gold.IQ, B = \_446__gate.IQ, Y = \_367_.B
Adding 0 new cells to the problem (0 A, 0 B, 0 shared).
Problem size at t=10: 8 literals, 12 clauses
Failed to prove equivalence with sequence length 0.
No nets to continue in previous time step.
Proved 0 previously unproven $equiv cells.
I'm not sure how to... read these results entirely. There was an issue previously that caused a lot more cells to not be equivalent, but I figured that was probably setattr -set keep 1 that's responsible for that, as the number of cells also included many tap cells and other such nonsense. So I went ahead and removed it from the script.
I've attached a full reproducible if someone wants to help me take a look; I'm at a total loss here so any pointers would be appreciated.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
I'm trying to get a long-neglected ASIC LEC script working again. I'm this close to getting it working, but I'm running into a weird issue:
(
Yosys 0.20+70 (git sha1 6e907acf86d, gcc 8.3.1 -fPIC -Os)
btw)I'm not sure how to... read these results entirely. There was an issue previously that caused a lot more cells to not be equivalent, but I figured that was probably
setattr -set keep 1
that's responsible for that, as the number of cells also included many tap cells and other such nonsense. So I went ahead and removed it from the script.I've attached a full reproducible if someone wants to help me take a look; I'm at a total loss here so any pointers would be appreciated.
reproducible.tar.gz
Beta Was this translation helpful? Give feedback.
All reactions