luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixing pointer-dependent behavior during BDD variable reordering.

This commit is contained in:
Alan Mishchenko 2025-07-13 20:58:34 -07:00
parent 990abc4349
commit c4c401b7a5
10 changed files with 47 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/bdd/cudd/cuddAddApply.c
View File

@ -182,7 +182,7 @@ Cudd_addPlus(
res = cuddUniqueConst(dd,value); res = cuddUniqueConst(dd,value);
return(res); return(res);
} }
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -223,7 +223,7 @@ Cudd_addTimes(
res = cuddUniqueConst(dd,value); res = cuddUniqueConst(dd,value);
return(res); return(res);
} }
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -405,7 +405,7 @@ Cudd_addMinimum(
return(G); return(G);
} }
} }
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -450,7 +450,7 @@ Cudd_addMaximum(
return(G); return(G);
} }
} }
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -590,7 +590,7 @@ Cudd_addOr(
if (cuddIsConstant(F)) return(G); if (cuddIsConstant(F)) return(G);
if (cuddIsConstant(G)) return(F); if (cuddIsConstant(G)) return(F);
if (F == G) return(F); if (F == G) return(F);
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -622,7 +622,7 @@ Cudd_addNand(
F = *f; G = *g; F = *f; G = *g;
if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd)); if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -654,7 +654,7 @@ Cudd_addNor(
F = *f; G = *g; F = *f; G = *g;
if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd)); if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -688,7 +688,7 @@ Cudd_addXor(
if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd)); if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }
@ -722,7 +722,7 @@ Cudd_addXnor(
if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd)); if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd)); if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd)); if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
if (F > G) { /* swap f and g */ if (cuddF2L(F) > cuddF2L(G)) { /* swap f and g */
*f = G; *f = G;
*g = F; *g = F;
} }

2
src/bdd/cudd/cuddAndAbs.c
View File

@ -226,7 +226,7 @@ cuddBddAndAbstractRecur(
} }
/* At this point f, g, and cube are not constant. */ /* At this point f, g, and cube are not constant. */
if (f > g) { /* Try to increase cache efficiency. */ if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */
DdNode *tmp = f; DdNode *tmp = f;
f = g; f = g;
g = tmp; g = tmp;

4
src/bdd/cudd/cuddClip.c
View File

@ -331,7 +331,7 @@ cuddBddClippingAndRecur(
/* Check cache. Try to increase cache efficiency by sorting the /* Check cache. Try to increase cache efficiency by sorting the
** pointers. */ ** pointers. */
if (f > g) { if (cuddF2L(f) > cuddF2L(g)) {
DdNode *tmp = f; DdNode *tmp = f;
f = g; g = tmp; f = g; g = tmp;
} }
@ -469,7 +469,7 @@ cuddBddClipAndAbsRecur(
distance--; distance--;
/* Check cache. */ /* Check cache. */
if (f > g) { /* Try to increase cache efficiency. */ if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */
DdNode *tmp = f; DdNode *tmp = f;
f = g; g = tmp; f = g; g = tmp;
} }

2
src/bdd/cudd/cuddInt.h
View File

@ -716,7 +716,7 @@ typedef struct DdLevelQueue {
SeeAlso [] SeeAlso []
******************************************************************************/ ******************************************************************************/
#define cuddF2L(f) ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) #define cuddF2L(f) ((Cudd_Regular(f)) ? ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) : 0)
/**Macro*********************************************************************** /**Macro***********************************************************************

12
src/bdd/cudd/cuddLinear.c
View File

@ -500,11 +500,11 @@ cuddLinearInPlace(
/* For each element newf1 in collision list ylist[posn]. */ /* For each element newf1 in collision list ylist[posn]. */
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
newf1 = *previousP; newf1 = *previousP;
while (f11 < cuddT(newf1)) { while (cuddF2L(f11) < cuddF2L(cuddT(newf1))) {
previousP = &(newf1->next); previousP = &(newf1->next);
newf1 = *previousP; newf1 = *previousP;
} }
while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) { while (f11 == cuddT(newf1) && cuddF2L(f00) < cuddF2L(cuddE(newf1))) {
previousP = &(newf1->next); previousP = &(newf1->next);
newf1 = *previousP; newf1 = *previousP;
} }
@ -554,11 +554,11 @@ cuddLinearInPlace(
/* For each element newf0 in collision list ylist[posn]. */ /* For each element newf0 in collision list ylist[posn]. */
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
newf0 = *previousP; newf0 = *previousP;
while (f01 < cuddT(newf0)) { while (cuddF2L(f01) < cuddF2L(cuddT(newf0))) {
previousP = &(newf0->next); previousP = &(newf0->next);
newf0 = *previousP; newf0 = *previousP;
} }
while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) { while (f01 == cuddT(newf0) && cuddF2L(f10) < cuddF2L(cuddE(newf0))) {
previousP = &(newf0->next); previousP = &(newf0->next);
newf0 = *previousP; newf0 = *previousP;
} }
@ -595,11 +595,11 @@ cuddLinearInPlace(
newxkeys++; newxkeys++;
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
tmp = *previousP; tmp = *previousP;
while (newf1 < cuddT(tmp)) { while (cuddF2L(newf1) < cuddF2L(cuddT(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }
while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) { while (newf1 == cuddT(tmp) && cuddF2L(newf0) < cuddF2L(cuddE(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }

2
src/bdd/cudd/cuddMatMult.c
View File

@ -583,7 +583,7 @@ addTriangleRecur(
res = cuddUniqueConst(dd, value); res = cuddUniqueConst(dd, value);
return(res); return(res);
} }
if (f < g) { if (cuddF2L(f) < cuddF2L(g)) {
DdNode *tmp = f; DdNode *tmp = f;
f = g; f = g;
g = tmp; g = tmp;

16
src/bdd/cudd/cuddReorder.c
View File

@ -937,11 +937,11 @@ cuddSwapInPlace(
/* For each element tmp in collision list xlist[posn]. */ /* For each element tmp in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
tmp = *previousP; tmp = *previousP;
while (cuddF2L(f1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) { while (cuddF2L(f1) < cuddF2L(cuddT(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }
while (f1 == cuddT(tmp) && cuddF2L(f0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) { while (f1 == cuddT(tmp) && cuddF2L(f0) < cuddF2L(cuddE(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }
@ -998,11 +998,11 @@ cuddSwapInPlace(
/* For each element newf1 in collision list xlist[posn]. */ /* For each element newf1 in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
newf1 = *previousP; newf1 = *previousP;
while (cuddF2L(f11) < (cuddT(newf1) ? cuddF2L(cuddT(newf1)) : 0)) { while (cuddF2L(f11) < cuddF2L(cuddT(newf1))) {
previousP = &(newf1->next); previousP = &(newf1->next);
newf1 = *previousP; newf1 = *previousP;
} }
while (f11 == cuddT(newf1) && cuddF2L(f01) < (cuddE(newf1) ? cuddF2L(cuddE(newf1)) : 0)) { while (f11 == cuddT(newf1) && cuddF2L(f01) < cuddF2L(cuddE(newf1))) {
previousP = &(newf1->next); previousP = &(newf1->next);
newf1 = *previousP; newf1 = *previousP;
} }
@ -1052,11 +1052,11 @@ cuddSwapInPlace(
/* For each element newf0 in collision list xlist[posn]. */ /* For each element newf0 in collision list xlist[posn]. */
previousP = &(xlist[posn]); previousP = &(xlist[posn]);
newf0 = *previousP; newf0 = *previousP;
while (cuddF2L(f10) < (cuddT(newf0) ? cuddF2L(cuddT(newf0)) : 0)) { while (cuddF2L(f10) < cuddF2L(cuddT(newf0))) {
previousP = &(newf0->next); previousP = &(newf0->next);
newf0 = *previousP; newf0 = *previousP;
} }
while (f10 == cuddT(newf0) && cuddF2L(f00) < (cuddE(newf0) ? cuddF2L(cuddE(newf0)) : 0)) { while (f10 == cuddT(newf0) && cuddF2L(f00) < cuddF2L(cuddE(newf0))) {
previousP = &(newf0->next); previousP = &(newf0->next);
newf0 = *previousP; newf0 = *previousP;
} }
@ -1093,11 +1093,11 @@ cuddSwapInPlace(
newykeys++; newykeys++;
previousP = &(ylist[posn]); previousP = &(ylist[posn]);
tmp = *previousP; tmp = *previousP;
while (cuddF2L(newf1) < (cuddT(tmp) ? cuddF2L(cuddT(tmp)) : 0)) { while (cuddF2L(newf1) < cuddF2L(cuddT(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }
while (newf1 == cuddT(tmp) && cuddF2L(newf0) < (cuddE(tmp) ? cuddF2L(cuddE(tmp)) : 0)) { while (newf1 == cuddT(tmp) && cuddF2L(newf0) < cuddF2L(cuddE(tmp))) {
previousP = &(tmp->next); previousP = &(tmp->next);
tmp = *previousP; tmp = *previousP;
} }

8
src/bdd/cudd/cuddSat.c
View File

@ -552,7 +552,7 @@ Cudd_EquivDC(
/* From now on, D is non-constant. */ /* From now on, D is non-constant. */
/* Normalize call to increase cache efficiency. */ /* Normalize call to increase cache efficiency. */
if (F > G) { if (cuddF2L(F) > cuddF2L(G)) {
tmp = F; tmp = F;
F = G; F = G;
G = tmp; G = tmp;
@ -674,7 +674,7 @@ Cudd_bddLeqUnless(
/* !g <= D unless !f or !D <= g unless !f */ /* !g <= D unless !f or !D <= g unless !f */
tmp = D; tmp = D;
D = Cudd_Not(f); D = Cudd_Not(f);
if (g < tmp) { if (cuddF2L(g) < cuddF2L(tmp)) {
f = Cudd_Not(g); f = Cudd_Not(g);
g = tmp; g = tmp;
} else { } else {
@ -717,7 +717,7 @@ Cudd_bddLeqUnless(
} }
} else { } else {
/* f <= g unless D or !g <= !f unless D */ /* f <= g unless D or !g <= !f unless D */
if (g < f) { if (cuddF2L(g) < cuddF2L(f)) {
tmp = g; tmp = g;
g = Cudd_Not(f); g = Cudd_Not(f);
f = Cudd_Not(tmp); f = Cudd_Not(tmp);
@ -725,7 +725,7 @@ Cudd_bddLeqUnless(
} }
} else { } else {
/* f <= g unless D or f <= D unless g */ /* f <= g unless D or f <= D unless g */
if (D < g) { if (cuddF2L(D) < cuddF2L(g)) {
tmp = D; tmp = D;
D = g; D = g;
g = tmp; g = tmp;

26
src/bdd/cudd/cuddTable.c
View File

@ -1162,14 +1162,14 @@ cuddUniqueInter(
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking = *previousP; looking = *previousP;
while (T < cuddT(looking)) { while (cuddF2L(T) < cuddF2L(cuddT(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
unique->uniqueLinks++; unique->uniqueLinks++;
#endif #endif
} }
while (T == cuddT(looking) && E < cuddE(looking)) { while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
@ -1220,14 +1220,14 @@ cuddUniqueInter(
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking = *previousP; looking = *previousP;
while (T < cuddT(looking)) { while (cuddF2L(T) < cuddF2L(cuddT(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
unique->uniqueLinks++; unique->uniqueLinks++;
#endif #endif
} }
while (T == cuddT(looking) && E < cuddE(looking)) { while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
@ -1251,14 +1251,14 @@ cuddUniqueInter(
previousP = &(nodelist[pos]); previousP = &(nodelist[pos]);
looking2 = *previousP; looking2 = *previousP;
while (T < cuddT(looking2)) { while (cuddF2L(T) < cuddF2L(cuddT(looking2))) {
previousP = &(looking2->next); previousP = &(looking2->next);
looking2 = *previousP; looking2 = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
unique->uniqueLinks++; unique->uniqueLinks++;
#endif #endif
} }
while (T == cuddT(looking2) && E < cuddE(looking2)) { while (T == cuddT(looking2) && cuddF2L(E) < cuddF2L(cuddE(looking2))) {
previousP = &(looking2->next); previousP = &(looking2->next);
looking2 = *previousP; looking2 = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
@ -1664,7 +1664,7 @@ cuddRehash(
while (node != NULL) { while (node != NULL) {
next = node->next; next = node->next;
split.value = cuddV(node); split.value = cuddV(node);
pos = ddHash(split.bits[0], split.bits[1], shift); pos = ddHash(cuddF2L(split.bits[0]), cuddF2L(split.bits[1]), shift);
node->next = nodelist[pos]; node->next = nodelist[pos];
nodelist[pos] = node; nodelist[pos] = node;
node = next; node = next;
@ -1748,14 +1748,14 @@ cuddShrinkSubtable(
looking = *previousP; looking = *previousP;
T = cuddT(node); T = cuddT(node);
E = cuddE(node); E = cuddE(node);
while (T < cuddT(looking)) { while (cuddF2L(T) < cuddF2L(cuddT(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
unique->uniqueLinks++; unique->uniqueLinks++;
#endif #endif
} }
while (T == cuddT(looking) && E < cuddE(looking)) { while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) {
previousP = &(looking->next); previousP = &(looking->next);
looking = *previousP; looking = *previousP;
#ifdef DD_UNIQUE_PROFILE #ifdef DD_UNIQUE_PROFILE
@ -2771,10 +2771,10 @@ cuddFindParent(
for (j = 0; j < slots; j++) { for (j = 0; j < slots; j++) {
f = nodelist[j]; f = nodelist[j];
while (cuddT(f) > node) { while (cuddF2L(cuddT(f)) > cuddF2L(node)) {
f = f->next; f = f->next;
} }
while (cuddT(f) == node && Cudd_Regular(cuddE(f)) > node) { while (cuddT(f) == node && cuddF2L(Cudd_Regular(cuddE(f))) > cuddF2L(node)) {
f = f->next; f = f->next;
} }
if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) { if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) {
@ -3126,8 +3126,8 @@ cuddCheckCollisionOrdering(
if (node == sentinel) return(1); if (node == sentinel) return(1);
next = node->next; next = node->next;
while (next != sentinel) { while (next != sentinel) {
if (cuddT(node) < cuddT(next) || if (cuddF2L(cuddT(node)) < cuddF2L(cuddT(next)) ||
(cuddT(node) == cuddT(next) && cuddE(node) < cuddE(next))) { (cuddT(node) == cuddT(next) && cuddF2L(cuddE(node)) < cuddF2L(cuddE(next)))) {
(void) fprintf(unique->err, (void) fprintf(unique->err,
"Unordered list: index %u, position %d\n", i, j); "Unordered list: index %u, position %d\n", i, j);
return(0); return(0);

4
src/bdd/cudd/cuddUtil.c
View File

@ -3357,10 +3357,10 @@ cuddUniqueLookup(
nodelist = subtable->nodelist; nodelist = subtable->nodelist;
looking = nodelist[posn]; looking = nodelist[posn];
while (T < cuddT(looking)) { while (cuddF2L(T) < cuddF2L(cuddT(looking))) {
looking = Cudd_Regular(looking->next); looking = Cudd_Regular(looking->next);
} }
while (T == cuddT(looking) && E < cuddE(looking)) { while (T == cuddT(looking) && cuddF2L(E) < cuddF2L(cuddE(looking))) {
looking = Cudd_Regular(looking->next); looking = Cudd_Regular(looking->next);
} }
if (cuddT(looking) == T && cuddE(looking) == E) { if (cuddT(looking) == T && cuddE(looking) == E) {