Skip to content

A
abc
Commit a8d75dcc by Alan Mishchenko
Options

Version abc70710

parent 39bc4842
Showing with 421 additions and 128 deletions
abc.rc
......@@ -160,8 +160,9 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
#alias t "r c.blif; st; wc c.cnf"
#alias t "r test/dsdmap6.blif; lutpack -vw; cec"
alias t "r i10_if4.blif; lp"
alias t1 "r pj1_if4.blif; lp"
alias t2 "r pj1_if6.blif; lp"
#alias t "r i10_if4.blif; lp"
#alias t1 "r pj1_if4.blif; lp"
#alias t2 "r pj1_if6.blif; lp"
alias t "r pj/pj1.blif; st; dfraig -v"
src/aig/dar/darCore.c
......@@ -64,10 +64,6 @@ int Dar_ManRewrite( Dar_Man_t * p )
continue;
if ( i > nNodesOld )
break;
if ( pObj->Id == 654 )
{
int x = 0;
}
// compute cuts for the node
clk = clock();
pCutSet = Dar_ObjComputeCuts_rec( p, pObj );
......
src/aig/dar/darMan.c
......@@ -94,7 +94,7 @@ Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p )
Dar_Obj_t * pObj;
int i;
// create the new manager
pNew = Dar_ManStart();
pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
// create the PIs
Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
Dar_ManForEachPi( p, pObj, i )
......@@ -119,7 +119,7 @@ Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
Dar_Obj_t * pObj;
int i;
// create the new manager
pNew = Dar_ManStart();
pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
// create the PIs
Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
Dar_ManForEachPi( p, pObj, i )
......
src/aig/dar/module.make
......@@ -9,5 +9,7 @@ SRC += src/aig/dar/darBalance.c \
src/aig/dar/darMem.c \
src/aig/dar/darObj.c \
src/aig/dar/darOper.c \
src/aig/dar/darSeq.c \
src/aig/dar/darTable.c \
src/aig/dar/darTruth.c \
src/aig/dar/darUtil.c
src/aig/fra/fra.h
......@@ -142,14 +142,14 @@ static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj )
static inline Vec_Ptr_t * Fra_ObjFaninVec( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
static inline int Fra_ObjSatNum( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; }
static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; }
static inline void Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
static inline void Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
static inline void Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; }
static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
......@@ -161,6 +161,7 @@ static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )
/*=== fraAnd.c ========================================================*/
extern void Fra_Sweep( Fra_Man_t * p );
/*=== fraClass.c ========================================================*/
extern void Fra_PrintClasses( Fra_Man_t * p );
extern void Fra_CreateClasses( Fra_Man_t * p );
extern int Fra_RefineClasses( Fra_Man_t * p );
extern int Fra_RefineClasses1( Fra_Man_t * p );
......@@ -171,6 +172,7 @@ extern Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
extern void Fra_ManPrepare( Fra_Man_t * p );
extern void Fra_ManStop( Fra_Man_t * p );
extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
......
src/aig/fra/fraAnd.c
......@@ -51,14 +51,15 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
// get the fraiged node
pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
Dar_Regular(pObjFraig)->pData = p;
// get representative of this class
pObjOldRepr = Fra_ObjRepr(pObjOld);
if ( pObjOldRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
{
assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
assert( pObjFraig != Dar_Regular(pFanin0Fraig) );
assert( pObjFraig != Dar_Regular(pFanin1Fraig) );
assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) );
assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) );
return pObjFraig;
}
// get the fraiged representative
......@@ -67,11 +68,13 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
return pObjFraig;
assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
// if they are proved different, the c-ex will be in p->pPatWords
RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
pObjOld->fMarkA = 1;
// pObjOld->fMarkA = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
if ( RetValue == -1 ) // failed
......@@ -79,11 +82,12 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
if ( !p->pPars->fSpeculate )
return pObjFraig;
// substitute the node
pObjOld->fMarkB = 1;
// pObjOld->fMarkB = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
// simulate the counter-example and return the Fraig node
Fra_Resimulate( p );
assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
return pObjFraig;
}
......@@ -103,7 +107,7 @@ void Fra_Sweep( Fra_Man_t * p )
Dar_Obj_t * pObj, * pObjNew;
int i, k = 0;
p->nClassesZero = Vec_PtrSize(p->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->vClasses);
p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
// duplicate internal nodes
// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
Dar_ManForEachNode( p->pManAig, pObj, i )
......@@ -114,11 +118,11 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses);
pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
assert( Fra_ObjFraig(pObj) != NULL );
Fra_ObjSetFraig( pObj, pObjNew );
assert( Fra_ObjFraig(pObj) != NULL );
}
// Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = Vec_PtrSize(p->vClasses);
p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
// try to prove the outputs of the miter
p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
......
src/aig/fra/fraClass.c
......@@ -25,6 +25,7 @@
to the array of pointers to the nodes in each class.
The first node of the class is its representative node.
The representative has the smallest topological order among the class nodes.
The nodes inside each class are ordered according to their topological order.
The classes are ordered according to the topological order of their representatives.
The array of pointers to the class nodes is terminated with a NULL pointer.
To enable dynamic addition of new classes (during class refinement),
......@@ -35,12 +36,55 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Dar_Obj_t * Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj ) { return ppNexts[pObj->Id]; }
static inline void Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_PrintClass( Dar_Obj_t ** pClass )
{
Dar_Obj_t * pTemp;
int i;
printf( "{ " );
for ( i = 0; pTemp = pClass[i]; i++ )
printf( "%d ", pTemp->Id );
printf( "}\n" );
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_CountClass( Dar_Obj_t ** pClass )
{
Dar_Obj_t * pTemp;
int i;
for ( i = 0; pTemp = pClass[i]; i++ );
return i;
}
/**Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
......@@ -56,22 +100,40 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
int i, nNodes, nPairs = 0;
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
for ( nNodes = 0; pClass[nNodes]; nNodes++ )
{
if ( nNodes > DAR_INFINITY )
{
printf( "Error in equivalence classes.\n" );
break;
}
}
nPairs += (nNodes - 1) * (nNodes - 2) / 2;
nNodes = Fra_CountClass( pClass );
assert( nNodes > 1 );
nPairs += nNodes * (nNodes - 1) / 2;
}
return nPairs;
}
/**Function*************************************************************
Synopsis [Computes hash value using simulation info.]
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_PrintClasses( Fra_Man_t * p )
{
Dar_Obj_t ** pClass;
int i;
printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
// printf( "%3d (%3d) : ", Fra_CountClass(pClass) );
// Fra_PrintClass( pClass );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
......@@ -102,7 +164,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
int i;
assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Fra_ObjSim(pObj);
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
uHash ^= pSims[i] * s_FPrimes[i];
return uHash;
......@@ -110,7 +172,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
/**Function********************************************************************
Synopsis [Returns the next prime &gt;= p.]
Synopsis [Returns the next prime >= p.]
Description [Copied from CUDD, for stand-aloneness.]
......@@ -158,18 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p )
***********************************************************************/
void Fra_CreateClasses( Fra_Man_t * p )
{
Dar_Obj_t ** pTable;
Dar_Obj_t * pObj;
int i, k, k2, nTableSize, nEntries, iEntry;
// allocate the table
nTableSize = Cudd_PrimeFra( Dar_ManNodeNum(p->pManAig) );
pTable = ALLOC( Dar_Obj_t *, nTableSize );
memset( pTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
// collect nodes into the table
Dar_Obj_t ** ppTable, ** ppNexts;
Dar_Obj_t * pObj, * pTemp;
int i, k, nTableSize, nEntries, nNodes, iEntry;
// allocate the hash table hashing simulation info into nodes
nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 );
ppTable = ALLOC( Dar_Obj_t *, nTableSize );
ppNexts = ALLOC( Dar_Obj_t *, nTableSize );
memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
// add all the nodes to the hash table
Vec_PtrClear( p->vClasses1 );
Dar_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Dar_ObjIsPi(pObj) && !Dar_ObjIsNode(pObj) )
if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
continue;
// hash the node by its simulation info
iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
......@@ -177,52 +242,80 @@ void Fra_CreateClasses( Fra_Man_t * p )
if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
{
Vec_PtrPush( p->vClasses1, pObj );
Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) );
continue;
}
// add the node to the table
pObj->pData = pTable[iEntry];
pTable[iEntry] = pObj;
// add the node to the class
if ( ppTable[iEntry] == NULL )
{
ppTable[iEntry] = pObj;
Fra_ObjSetNext( ppNexts, pObj, pObj );
}
else
{
Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
}
}
// count the total number of nodes in the non-trivial classes
// mark the representative nodes of each equivalence class
nEntries = 0;
for ( i = 0; i < nTableSize; i++ )
if ( pTable[i] && pTable[i]->pData )
if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
{
k = 0;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
k++;
nEntries += 2*k;
for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1;
pTemp != ppTable[i];
pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
assert( k > 1 );
nEntries += k;
// mark the node
assert( ppTable[i]->fMarkA == 0 );
ppTable[i]->fMarkA = 1;
}
// allocate room for classes
p->pMemClasses = ALLOC( Dar_Obj_t *, nEntries + 2*Vec_PtrSize(p->vClasses1) );
p->pMemClassesFree = p->pMemClasses + nEntries;
// copy the entries into storage
p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
p->pMemClassesFree = p->pMemClasses + 2*nEntries;
// copy the entries into storage in the topological order
Vec_PtrClear( p->vClasses );
nEntries = 0;
for ( i = 0; i < nTableSize; i++ )
if ( pTable[i] && pTable[i]->pData )
Dar_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
continue;
// skip the nodes that are not representatives of non-trivial classes
if ( pObj->fMarkA == 0 )
continue;
pObj->fMarkA = 0;
// add the class of nodes
Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
// count the number of entries in this class
for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1;
pTemp != pObj;
pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
nNodes = k;
assert( nNodes > 1 );
// add the nodes to the class in the topological order
p->pMemClasses[2*nEntries] = pObj;
for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1;
pTemp != pObj;
pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
{
k = 0;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
k++;
// write entries in the topological order
k2 = k;
for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
{
k2--;
p->pMemClasses[nEntries+k2] = pObj;
p->pMemClasses[nEntries+k+k2] = NULL;
}
assert( k2 == 0 );
Vec_PtrPush( p->vClasses, p->pMemClasses + nEntries );
nEntries += 2*k;
p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
Fra_ObjSetRepr( pTemp, pObj );
}
free( pTable );
// add as many empty entries
// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes );
p->pMemClasses[2*nEntries + nNodes] = NULL;
// increment the number of entries
nEntries += k;
}
free( ppTable );
free( ppNexts );
// now it is time to refine the classes
Fra_RefineClasses( p );
// set the pointer to the manager
Dar_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p->pManAig;
}
/**Function*************************************************************
......@@ -236,40 +329,42 @@ void Fra_CreateClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** pClass )
Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
{
Dar_Obj_t * pObj;
Dar_Obj_t * pObj, ** ppThis;
int i;
assert( pClass[1] != NULL );
assert( ppClass[0] != NULL && ppClass[1] != NULL );
// check if the class is going to be refined
for ( pObj = pClass[1]; pObj; pObj++ )
if ( !Fra_NodeCompareSims(p, pClass[0], pObj) )
for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )
if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
break;
if ( pObj == NULL )
return NULL;
// split the class
Vec_PtrClear( p->vClassOld );
Vec_PtrClear( p->vClassNew );
Vec_PtrPush( p->vClassOld, pClass[0] );
for ( pObj = pClass[1]; pObj; pObj++ )
if ( Fra_NodeCompareSims(p, pClass[0], pObj) )
Vec_PtrPush( p->vClassOld, ppClass[0] );
for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )
if ( Fra_NodeCompareSims(p, ppClass[0], pObj) )
Vec_PtrPush( p->vClassOld, pObj );
else
Vec_PtrPush( p->vClassNew, pObj );
// put the nodes back into the class memory
Vec_PtrForEachEntry( p->vClassOld, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
}
pClass += 2*Vec_PtrSize(p->vClassOld);
ppClass += 2*Vec_PtrSize(p->vClassOld);
// put the new nodes into the class memory
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
}
return pClass;
return ppClass;
}
/**Function*************************************************************
......@@ -295,7 +390,10 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
Vec_PtrPop( vClasses );
// if the new class is trivial, stop
if ( pClass2[1] == NULL )
{
nRefis++;
break;
}
// othewise, add the class and continue
Vec_PtrPush( vClasses, pClass2 );
pClass = pClass2;
......@@ -319,7 +417,7 @@ int Fra_RefineClasses( Fra_Man_t * p )
{
Vec_Ptr_t * vTemp;
Dar_Obj_t ** pClass;
int clk, i, nRefis = 0;
int clk, i, nRefis;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
if ( p->pPars->fProve )
......@@ -328,12 +426,13 @@ int Fra_RefineClasses( Fra_Man_t * p )
return 0;
// refine the classes
clk = clock();
nRefis = 0;
Vec_PtrClear( p->vClassesTemp );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
// add the class to the new array
Vec_PtrPush( p->vClassesTemp, pClass );
// refine the class interatively
// refine the class iteratively
nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
}
// exchange the class representation
......@@ -357,11 +456,17 @@ p->timeRef += clock() - clk;
***********************************************************************/
int Fra_RefineClasses1( Fra_Man_t * p )
{
Dar_Obj_t * pObj, ** pClass;
int i, k;
Dar_Obj_t * pObj, ** ppClass;
int i, k, nRefis, clk;
// check if there is anything to refine
if ( Vec_PtrSize(p->vClasses1) == 0 )
return 0;
clk = clock();
// make sure constant 1 class contains only non-constant nodes
assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) );
// collect all the nodes to be refined
Vec_PtrClear( p->vClassNew );
k = 0;
Vec_PtrClear( p->vClassNew );
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
{
if ( Fra_NodeHasZeroSim( p, pObj ) )
......@@ -373,18 +478,24 @@ int Fra_RefineClasses1( Fra_Man_t * p )
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
if ( Vec_PtrSize(p->vClassNew) == 1 )
{
Fra_ObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
return 1;
}
// create a new class composed of these nodes
pClass = p->pMemClassesFree;
ppClass = p->pMemClassesFree;
p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
{
pClass[i] = pObj;
pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
}
Vec_PtrPush( p->vClasses, pClass );
Vec_PtrPush( p->vClasses, ppClass );
// iteratively refine this class
return 1 + Fra_RefineClassLastIter( p, p->vClasses );
nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
p->timeRef += clock() - clk;
return nRefis;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fraCnf.c
......@@ -209,6 +209,7 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
***********************************************************************/
void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
Fra_Man_t * pTemp = pObj->pData;
assert( !Dar_IsComplement(pObj) );
if ( Fra_ObjSatNum(pObj) )
return;
......
src/aig/fra/fraMan.c
......@@ -69,8 +69,6 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Dar_Obj_t * pObj;
int i;
// allocate the fraiging manager
p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
......@@ -82,13 +80,17 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
p->nSimWords = pPars->nSimWords;
p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
// clean simulation info of the constant node
memset( p->pSimWords, 0, p->nSimWords * sizeof(unsigned) );
memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) );
// allocate storage for sim pattern
p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
// allocate other members
p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
p->pMemFraig = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
......@@ -98,17 +100,41 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc );
memset( p->pMemSatNums, 0xff, p->nSizeAlloc * sizeof(int) );
memset( p->pMemSatNums, 0, p->nSizeAlloc * sizeof(int) );
// set random number generator
srand( 0xABCABC );
// make sure the satisfying assignment is node assigned
assert( p->pManFraig->pData == NULL );
// connect AIG managers to the FRAIG manager
Fra_ManPrepare( p );
return p;
}
/**Function*************************************************************
Synopsis [Prepares managers by transfering pointers to the objects.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManPrepare( Fra_Man_t * p )
{
Dar_Obj_t * pObj;
int i;
// set the pointers to the manager
Dar_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
// set the pointer to the manager
Dar_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
// set the pointers to the available fraig nodes
Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
Dar_ManForEachPi( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
// set the pointers to the manager
Dar_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p->pManFraig;
// set random number generator
srand( 0xABCABC );
return p;
}
/**Function*************************************************************
......
src/aig/fra/fraSim.c
......@@ -105,7 +105,11 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
Dar_Obj_t * pObj;
int i, Limit;
Dar_ManForEachPi( p->pManAig, pObj, i )
{
Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
// printf( "%d", Dar_InfoHasBit(pPat, i) );
}
// printf( "\n" );
Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
......@@ -441,7 +445,7 @@ void Fra_Resimulate( Fra_Man_t * p )
if ( nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
if ( !p->pPars->fPatScores )
return;
......@@ -487,7 +491,7 @@ void Fra_Simulate( Fra_Man_t * p )
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
Fra_SavePattern1( p );
......@@ -495,7 +499,7 @@ void Fra_Simulate( Fra_Man_t * p )
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
// refine classes by random simulation
......@@ -505,11 +509,11 @@ void Fra_Simulate( Fra_Man_t * p )
nClasses = Vec_PtrSize(p->vClasses);
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig )
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
// Fra_PrintSimClasses( p );
// Fra_PrintClasses( p );
}
/**Function*************************************************************
......
src/aig/ivy/ivyFraig.c
......@@ -733,7 +733,12 @@ void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
Ivy_Obj_t * pObj;
int i, Limit;
Ivy_ManForEachPi( p->pManAig, pObj, i )
{
Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
// printf( "%d", Ivy_InfoHasBit(pPat, i) );
}
// printf( "\n" );
Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
......@@ -1742,7 +1747,6 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
if ( !p->pParams->fPatScores )
return;
......@@ -2018,6 +2022,8 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
return pObjNew;
assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id );
// they are different (the counter-example is in p->pPatWords)
RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
if ( RetValue == 1 ) // proved equivalent
......
src/base/abc/abcUtil.c
......@@ -1490,7 +1490,8 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk )
static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj )
{
// pObj->pCopy = (void *)(((int)pObj->pCopy)++);
((char*)pObj->pCopy)++;
int Value = (int)pObj->pCopy;
pObj->pCopy = (void *)(Value + 1);
return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj);
}
......
src/base/abci/abc.c
......@@ -112,6 +112,7 @@ static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -267,6 +268,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
......@@ -333,7 +335,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
{
extern void Dar_LibStart();
Dar_LibStart();
// Dar_LibStart();
}
}
......@@ -352,7 +354,7 @@ void Abc_End()
{
{
extern void Dar_LibStop();
Dar_LibStop();
// Dar_LibStop();
}
Abc_NtkFraigStoreClean();
......@@ -6077,14 +6079,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk4VarTable( pNtk );
// Dar_NtkGenerateArrays( pNtk );
// Dar_ManDeriveCnfTest2();
/*
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Network should be strashed. Command has failed.\n" );
return 1;
}
*/
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
// pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -6911,6 +6915,93 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, fProve, fVerbose, fDoSparse;
int nConfLimit;
extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nConfLimit = 100;
fDoSparse = 0;
fProve = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfLimit < 0 )
goto usage;
break;
case 's':
fDoSparse ^= 1;
break;
case 'p':
fProve ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: dfraig [-C num] [-spvh]\n" );
fprintf( pErr, "\t performs fraiging using a new method\n" );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Prove_Params_t Params, * pParams = &Params;
......
src/base/abci/abcDar.c
......@@ -21,6 +21,7 @@
#include "abc.h"
#include "dar.h"
#include "cnf.h"
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -443,6 +444,37 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
{
Fra_Par_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
Dar_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
Fra_ParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose;
pParams->fProve = fProve;
pParams->fDoSparse = fDoSparse;
pMan = Fra_Perform( pTemp = pMan, pParams );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Dar_ManStop( pTemp );
Dar_ManStop( pMan );
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/kit/kitGraph.c
......@@ -357,6 +357,8 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
if ( RetValue == -1 )
return NULL;
if ( Vec_IntSize(vMemory) > 128 )
return NULL;
// printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
assert( RetValue == 0 || RetValue == 1 );
// derive factored form
......
src/opt/lpk/lpkCore.c
......@@ -229,7 +229,6 @@ p->timeMap += clock() - clk;
int Lpk_ResynthesizeNode( Lpk_Man_t * p )
{
static int Count = 0;
char * pFileName;
Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut;
unsigned * pTruth;
......@@ -245,6 +244,8 @@ p->timeCuts += clock() - clk;
}
p->timeCuts += clock() - clk;
//return 0;
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts
......@@ -289,12 +290,13 @@ p->timeTruth += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
// char * pFileName;
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk );
// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
printf( "Saved truth table in file \"%s\".\n", pFileName );
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}
// update the network
......
src/opt/lpk/lpkCut.c
......@@ -474,12 +474,16 @@ if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
assert( p->nCuts < LPK_CUTS_MAX );
p->nCuts++;
assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
// assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
/*
printf( " Creating cut: " );
Lpk_NodePrintCut( p, pCutNew, 1 );
printf( "\n" );
*/
// if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) )
// printf( "Assertion in line 477 failed.\n" );
}
/**Function*************************************************************
......@@ -519,9 +523,17 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
pCut = p->pCuts + i;
if ( pCut->nLeaves == 0 )
continue;
// try to expand the fanins of this cut
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
if ( p->pObj->Id == 28 && i == 273 && k == 13 )
{
Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]);
int s = 0;
}
// create a new cut
Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
// quit if the number of cuts has exceeded the limit
......
src/opt/lpk/lpkMan.c
......@@ -50,7 +50,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->pPars = pPars;
p->nCutsMax = LPK_CUTS_MAX;
p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
......
src/opt/lpk/module.make
SRC += src/aig/lpk/lpkCore.c \
src/aig/lpk/lpkCut.c \
src/aig/lpk/lpkMan.c \
src/aig/lpk/lpkMap.c \
src/aig/lpk/lpkMulti.c \
src/aig/lpk/lpkMux.c \
src/aig/lpk/lpkSets.c
SRC += src/opt/lpk/lpkCore.c \
src/opt/lpk/lpkCut.c \
src/opt/lpk/lpkMan.c \
src/opt/lpk/lpkMap.c \
src/opt/lpk/lpkMulti.c \
src/opt/lpk/lpkMux.c \
src/opt/lpk/lpkSets.c
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment