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-06-07 12:52:23 -07:00
parent 44f3265e8b
commit 6463f11625
3 changed files with 12 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -381,6 +381,7 @@ struct DdManager { /* specialized DD symbol table */
// double allocated; /* number of nodes allocated */
ABC_INT64_T allocated; /* number of nodes allocated */
/* (not during reordering) */
ABC_INT64_T allocated2; /* number of nodes allocated */
double reclaimed; /* number of nodes brought back from the dead */
int isolated; /* isolated projection functions */
int *perm; /* current variable perm. (index to level) */

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

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

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

@ -329,7 +329,7 @@ cuddAllocNode(
unique->allocated++;
node = unique->nextFree;
unique->nextFree = node->next;
node->Id = (unique->allocated<<4);
node->Id = (++unique->allocated2<<4);
return(node);
} /* end of cuddAllocNode */
@ -398,6 +398,7 @@ cuddInitTable(
unique->looseUpTo = looseUpTo;
unique->gcEnabled = 1;
unique->allocated = 0;
unique->allocated2 = 0;
unique->reclaimed = 0;
unique->subtables = ABC_ALLOC(DdSubtable,unique->maxSize);
if (unique->subtables == NULL) {