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

Fixing bugs in the new procedures added to the library.

This commit is contained in:
Alan Mishchenko 2011-03-05 16:17:12 -08:00
parent edcb769b3e
commit badbb5a6cc
3 changed files with 44 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/aig/llb/llb3Nonlin.c
View File

@ -529,6 +529,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
clk3 = clock();
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );
// p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) );
if ( p->ddG->bFunc2 == NULL )
{
if ( !p->pPars->fSilent )
@ -552,6 +553,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
Llb_NonlinImageQuit();
p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 );
//Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );
// derive new states
clk3 = clock();
@ -567,9 +569,12 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
}
Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->ddG, bTemp );
p->timeGloba += clock() - clk3;
if ( Cudd_IsConstant(p->ddG->bFunc2) )
break;
// add to the reached set
clk3 = clock();
p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );
if ( p->ddG->bFunc == NULL )
{

3
src/misc/extra/extra.h
View File

@ -199,8 +199,7 @@ extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int
extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
extern DdNode * Extra_bddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG );
extern DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG );
extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")

52
src/misc/extra/extraBddMisc.c
View File

@ -55,6 +55,8 @@ static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdN
static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) );
static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
// file "cuddUtils.c"
static void ddSupportStep(DdNode *f, int *support);
static void ddClearFlag(DdNode *f);
@ -1072,27 +1074,39 @@ int Extra_bddVarIsInCube( DdNode * bCube, int iVar )
}
return -1;
}
/**Function*************************************************************
Synopsis [Computes the AND of two BDD with different orders.]
Description []
Description [Derives the result of Boolean AND of bF and bG in ddF.
The array pPermute gives the mapping of variables of ddG into that of ddF.]
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_bddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG )
DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
{
DdHashTable * table;
DdNode * bRes;
do
{
ddF->reordered = 0;
bRes = extraBddAndPerm( ddF, bF, ddG, bG );
table = cuddHashTableInit( ddF, 2, 256 );
if (table == NULL) return NULL;
bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute );
if ( bRes ) cuddRef( bRes );
cuddHashTableQuit( table );
if ( bRes ) cuddDeref( bRes );
//if ( ddF->reordered == 1 )
//printf( "Reordering happened\n" );
}
while ( ddF->reordered == 1 );
//printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n",
// Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes),
// Cudd_DagSize(bF) * Cudd_DagSize(bG) );
return ( bRes );
}
@ -1876,7 +1890,7 @@ static int Counter = 0;
SeeAlso []
***********************************************************************/
DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG )
DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
{
DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar;
int LevF, LevG, Lev;
@ -1893,14 +1907,19 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode
// cannot use F == 1, because the var order of G has to be changed
// check cache
if ( (Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) &&
(bRes = cuddCacheLookup2(ddF, (DD_CTFP)extraBddAndPerm, bF, bG)) )
if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) &&
(bRes = cuddHashTableLookup2(table, bF, bG)) )
return bRes;
Counter++;
if ( ddF->TimeStop && ddF->TimeStop < clock() )
return NULL;
if ( ddG->TimeStop && ddG->TimeStop < clock() )
return NULL;
// find the topmost variable in F and G using var order of F
LevF = cuddI( ddF, Cudd_Regular(bF)->index );
LevG = cuddI( ddF, Cudd_Regular(bG)->index );
LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index );
Lev = ABC_MIN( LevF, LevG );
assert( Lev < ddF->size );
bVar = ddF->vars[ddF->invperm[Lev]];
@ -1912,12 +1931,12 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode
bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) );
// call for cofactors
bRes0 = extraBddAndPerm( ddF, bF0, ddG, bG0 );
bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute );
if ( bRes0 == NULL )
return NULL;
cuddRef( bRes0 );
// call for cofactors
bRes1 = extraBddAndPerm( ddF, bF1, ddG, bG1 );
bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute );
if ( bRes1 == NULL )
{
Cudd_IterDerefBdd( ddF, bRes0 );
@ -1931,17 +1950,22 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode
{
Cudd_IterDerefBdd( ddF, bRes0 );
Cudd_IterDerefBdd( ddF, bRes1 );
return NULL;
}
cuddRef( bRes );
Cudd_IterDerefBdd( ddF, bRes0 );
Cudd_IterDerefBdd( ddF, bRes1 );
// cache the result
if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 )
cuddCacheInsert2( ddF, (DD_CTFP)extraBddAndPerm, bF, bG, bRes );
// if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 )
{
ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref;
cuddSatDec(fanout);
cuddHashTableInsert2( table, bF, bG, bRes, fanout );
}
cuddDeref( bRes );
return bRes;
}
}
/**Function*************************************************************
@ -1981,7 +2005,7 @@ Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", clock() - clk );
// compute the result
Counter = 0;
clk = clock();
bRes2 = Extra_bddAndPerm( ddF, bF, ddG, bG2 ); Cudd_Ref( bRes2 );
bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 );
Abc_PrintTime( 1, "Runtime of new procedure", clock() - clk );
printf( "Recursive calls = %d\n", Counter );
printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ",