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

Version abc90410

This commit is contained in:
Alan Mishchenko 2009-04-10 08:01:00 -07:00
parent df6fdd1dff
commit ccd1b57264
36 changed files with 1196 additions and 171 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/aig/aig/aig.h
View File

@ -514,10 +514,10 @@ extern void Aig_ManStopMemory( Aig_Man_t * p );
/*=== aigMffc.c ==========================================================*/
extern int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
extern int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin, float * pPower, float * pProbs );
extern int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
extern int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower );
extern int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
extern int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
extern int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
extern int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower );
extern int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
extern int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
/*=== aigObj.c ==========================================================*/
extern Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p );
extern Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );

10
src/aig/aig/aigDup.c
View File

@ -476,15 +476,9 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// duplicate representation of choice nodes
if ( p->pEquivs )
{
pNew->pEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
}
pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
if ( p->pReprs )
{
pNew->pReprs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
}
pNew->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
// create the PIs
Aig_ManCleanData( p );
// duplicate internal nodes

18
src/aig/aig/aigMffc.c
View File

@ -144,7 +144,7 @@ int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin )
SeeAlso []
***********************************************************************/
void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
void Aig_NodeMffcSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
{
// skip visited nodes
if ( Aig_ObjIsTravIdCurrent(p, pNode) )
@ -158,8 +158,8 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin,
}
assert( Aig_ObjIsNode(pNode) );
// recur on the children
Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
Aig_NodeMffcSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
Aig_NodeMffcSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
}
/**Function*************************************************************
@ -173,7 +173,7 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin,
SeeAlso []
***********************************************************************/
int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
{
int ConeSize1, ConeSize2;
if ( vSupp ) Vec_PtrClear( vSupp );
@ -187,7 +187,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t
assert( Aig_ObjIsNode(pNode) );
Aig_ManIncrementTravId( p );
ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL );
Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
Aig_NodeMffcSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
assert( ConeSize1 == ConeSize2 );
assert( ConeSize1 > 0 );
@ -205,7 +205,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t
SeeAlso []
***********************************************************************/
int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
{
int ConeSize1, ConeSize2;
assert( (pPower != NULL) == (p->vProbs != NULL) );
@ -230,7 +230,7 @@ int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
SeeAlso []
***********************************************************************/
int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
{
Aig_Obj_t * pObj;
int i, ConeSize1, ConeSize2;
@ -259,7 +259,7 @@ int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
SeeAlso []
***********************************************************************/
int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
{
Aig_Obj_t * pObj, * pLeafBest;
int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
@ -294,7 +294,7 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
// collect the cut nodes
Vec_PtrClear( vResult );
Aig_ManIncrementTravId( p );
Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
Aig_NodeMffcSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
// ref the nodes
ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
assert( ConeCur1 == ConeCur2 );

2
src/aig/aig/aigPart.c
View File

@ -1520,7 +1520,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter );
for ( pTemp = pNode; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
{
Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp );
Counter = Aig_NodeMffcSupp( p, pTemp, 0, vSupp );
printf( "S=%d N=%d L=%d ", Vec_PtrSize(vSupp), Counter, pTemp->Level );
}
printf( "}\n" );

5
src/aig/cec/cec.h
View File

@ -125,6 +125,7 @@ struct Cec_ParCor_t_
int nBTLimit; // conflict limit at a node
int fLatchCorr; // consider only latch outputs
int fUseRings; // use rings
int fMakeChoices; // use equilvaences as choices
int fUseCSat; // use circuit-based solver
int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
@ -139,8 +140,8 @@ struct Cec_ParChc_t_
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nBTLimit; // conflict limit at a node
int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fUseRings; // use rings
int fUseCSat; // use circuit-based solver
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};

2
src/aig/cec/cecCec.c
View File

@ -70,7 +70,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose )
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp );
Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
int RetValue, iOut, nOuts, clkTotal = clock();
Gia_ManStop( pTemp );
// run CEC on this miter

443
src/aig/cec/cecChoice.c
View File

@ -19,15 +19,170 @@
***********************************************************************/
#include "cecInt.h"
#include "giaAig.h"
#include "dch.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the real value of the literal w/o spec reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
assert( Gia_ObjIsAnd(pObj) );
Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Recursively performs speculative reduction for the object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr;
if ( ~pObj->Value )
return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
return;
}
pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int i, iPrev, iObj, iPrevNew, iObjNew;
assert( p->pReprs != NULL );
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
if ( fRings )
{
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsConst( p, i ) )
{
iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( vXorLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
iPrev = iObj;
}
iObj = i;
iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
}
}
}
}
else
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis []
@ -39,9 +194,293 @@
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
{
return NULL;
int nItersMax = 1000;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
int r, RetValue;
int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
int clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = 0;
pParsSim->fSeqSimulate = 0;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim );
Cec_ManSimClassesPrepare( pSim );
Cec_ManSimClassesRefine( pSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
printf( "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// perform refinement of equivalence classes
for ( r = 0; r < nItersMax; r++ )
{
clk = clock();
// perform speculative reduction
clk2 = clock();
pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
clkSrm += clock() - clk2;
if ( Gia_ManCoNum(pSrm) == 0 )
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
Vec_IntFree( vOutputs );
Gia_ManStop( pSrm );
break;
}
//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
// found counter-examples to speculation
clk2 = clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
clkSat += clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 )
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
break;
}
// refine classes with these counter-examples
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
Vec_IntFree( vCexStore );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
// check the overflow
if ( r == nItersMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
return 0;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
if ( Gia_ObjIsCo(pObj) )
return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Derives the miter of several AIGs for choice computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
{
Gia_Man_t * pNew, * pGia, * pGia0;
int i, k, iNode, nNodes;
// make sure they have equal parameters
assert( Vec_PtrSize(vGias) > 0 );
pGia0 = Vec_PtrEntry( vGias, 0 );
Vec_PtrForEachEntry( vGias, pGia, i )
{
assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
Gia_ManFillValue( pGia );
Gia_ManConst0(pGia)->Value = 0;
}
// start the new manager
pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
pNew->pName = Gia_UtilStrsav( pGia0->pName );
// create new CIs and assign them to the old manager CIs
for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
{
iNode = Gia_ManAppendCi(pNew);
Vec_PtrForEachEntry( vGias, pGia, i )
Gia_ManCi( pGia, k )->Value = iNode;
}
// create internal nodes
Gia_ManHashAlloc( pNew );
for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
{
Vec_PtrForEachEntry( vGias, pGia, i )
Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
}
Gia_ManHashStop( pNew );
// check the presence of dangling nodes
nNodes = Gia_ManHasDandling( pNew );
assert( nNodes == 0 );
// finalize
// Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
return pNew;
}
/**Function*************************************************************
Synopsis [Computes choices for the vector of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
{
Gia_Man_t * pMiter, * pNew;
int RetValue;
// compute equivalences of the miter
pMiter = Gia_ManChoiceMiter( vGias );
RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
// derive AIG with choices
pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
Gia_ManHasChoices( pNew );
Gia_ManStop( pMiter );
// report the results
if ( pPars->fVerbose )
{
// printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
// 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Computes choices for one AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
{
extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
Dch_Pars_t Pars, * pPars = &Pars;
Aig_Man_t * pMan, * pManNew;
Gia_Man_t * pGia;
if ( 0 )
{
Vec_Ptr_t * vGias;
vGias = Vec_PtrAlloc( 1 );
Vec_PtrPush( vGias, pAig );
pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
Vec_PtrFree( vGias );
}
else
{
pMan = Gia_ManToAig( pAig, 0 );
Dch_ManSetDefaultParams( pPars );
pPars->fUseGia = 1;
pPars->nBTLimit = pParsChc->nBTLimit;
pPars->fUseCSat = pParsChc->fUseCSat;
pPars->fVerbose = pParsChc->fVerbose;
pManNew = Dar_ManChoiceNew( pMan, pPars );
pGia = Gia_ManFromAig( pManNew );
Aig_ManStop( pManNew );
Aig_ManStop( pMan );
}
return pGia;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description [Takes several AIGs and performs choicing.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
{
Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
Vec_Ptr_t * vGias;
Gia_Man_t * pGia;
Aig_Man_t * pAig;
int i;
if ( pPars->fVerbose )
ABC_PRT( "Synthesis time", pPars->timeSynth );
Cec_ManChcSetDefaultParams( pParsChc );
pParsChc->nBTLimit = pPars->nBTLimit;
pParsChc->fUseCSat = pPars->fUseCSat;
if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
pParsChc->nBTLimit = 100;
pParsChc->fVerbose = pPars->fVerbose;
vGias = Vec_PtrAlloc( 10 );
Vec_PtrForEachEntry( vAigs, pAig, i )
Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
Vec_PtrForEachEntry( vGias, pAig, i )
Gia_ManStop( (Gia_Man_t *)pAig );
Vec_PtrFree( vGias );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;
}
////////////////////////////////////////////////////////////////////////

4
src/aig/cec/cecCore.c
View File

@ -199,8 +199,8 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
p->nWords = 15; // the number of simulation words
p->nRounds = 15; // the number of simulation rounds
p->nBTLimit = 1000; // conflict limit at a node
p->fFirstStop = 0; // stop on the first sat output
p->fUseSmartCnf = 0; // use smart CNF computation
p->fUseRings = 1; // use rings
p->fUseCSat = 0; // use circuit-based solver
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
}

165
src/aig/cec/cecCorr.c
View File

@ -564,6 +564,35 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates counter-examples derived by the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
{
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
Gia_ManSetRefs( pSim->pAig );
pSim->pPars->nRounds = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
Cec_ManStartSimInfo( vSimInfo, 0 );
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
}
assert( iStart == Vec_IntSize(vCexStore) );
Vec_PtrFree( vSimInfo );
return RetValue;
}
/**Function*************************************************************
Synopsis [Updates equivalence classes by marking those that timed out.]
@ -613,9 +642,10 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
return 1;
}
/**Function*************************************************************
Synopsis [Marks all the nodes as proved.]
Synopsis [Duplicates the AIG in the DFS order.]
Description []
@ -624,20 +654,57 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
SeeAlso []
***********************************************************************/
void Gia_ManSetProvedNodes( Gia_Man_t * p )
void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pObj;
int i, nLits = 0;
Gia_ManForEachObj1( p, pObj, i )
Gia_Obj_t * pRepr;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjRepr(p, i) == GIA_VOID )
continue;
Gia_ObjSetProved( p, i );
nLits++;
Gia_ManCorrReduce_rec( pNew, p, pRepr );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
// printf( "Identified %d proved literals.\n", nLits );
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Prints statistics during solving.]
@ -649,7 +716,7 @@ void Gia_ManSetProvedNodes( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
{
int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
@ -685,7 +752,7 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.]
Synopsis [Internal procedure for register correspondence.]
Description []
@ -694,26 +761,26 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Gia_Man_t * pNew, * pTemp;
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
int r, RetValue;
int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
int r, RetValue, clkTotal = clock();
int clkSat = 0, clkSim = 0, clkSrm = 0;
int clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
if ( Gia_ManRegNum(pAig) == 0 )
{
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return NULL;
return 0;
}
Gia_ManRandom( 1 );
// prepare simulation manager
@ -736,10 +803,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManLCorrPrintStats( pAig, NULL, 0, clock() - clk );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// perform refinement of equivalence classes
for ( r = 0; r < 100000; r++ )
for ( r = 0; r < nIterMax; r++ )
{
clk = clock();
// perform speculative reduction
@ -776,7 +843,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
@ -811,7 +878,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc );
Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
@ -822,20 +889,55 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
else
{
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
}
// check the overflow
if ( r == 100000 )
if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
return 0;
}
/**Function*************************************************************
Synopsis [Top-level procedure for register correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
Gia_Man_t * pNew, * pTemp;
int RetValue;
RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
Gia_ManEquivImprove( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
if ( pPars->fMakeChoices )
{
pNew = Gia_ManEquivToChoices( pAig, 1 );
Gia_ManHasChoices( pNew );
}
else
{
Gia_ManEquivImprove( pAig );
pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
}
// report the results
if ( pPars->fVerbose )
{
@ -844,11 +946,6 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
ABC_PRTP( "Srm ", clkSrm, clkTotal );
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
return pNew;
}

3
src/aig/cec/cecInt.h
View File

@ -166,7 +166,8 @@ struct Cec_ManFra_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cecCore.c ============================================================*/
/*=== cecCorr.c ============================================================*/
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time );
/*=== cecClass.c ============================================================*/
extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p );

2
src/aig/cec/cecSeq.c
View File

@ -126,7 +126,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
{
unsigned * pInfo0, * pInfo1;
int f, i, k, w, RetValue = 0;
assert( Gia_ManRegNum(p->pAig) > 0 );
// assert( Gia_ManRegNum(p->pAig) > 0 );
assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
{

2
src/aig/dar/darLib.c
View File

@ -730,7 +730,7 @@ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * p
for ( i = 0; i < nLeaves; i++ )
Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
// label MFFC with current ID
nNodes = Aig_NodeMffsLabel( p, pRoot, pPower );
nNodes = Aig_NodeMffcLabel( p, pRoot, pPower );
// unmark the cut leaves
for ( i = 0; i < nLeaves; i++ )
Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;

12
src/aig/dar/darRefact.c
View File

@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
{
p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
p->pGraphBest = Kit_GraphCreateConst0();
Vec_PtrCopy( p->vLeavesBest, vCut );
return p->GainBest;
}
if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
{
p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
p->pGraphBest = Kit_GraphCreateConst1();
Vec_PtrCopy( p->vLeavesBest, vCut );
return p->GainBest;
@ -528,7 +528,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
// get the bounded MFFC size
clk = clock();
nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 );
nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
{
p->timeCuts += clock() - clk;
@ -538,15 +538,15 @@ p->timeCuts += clock() - clk;
if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
{
Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
}
else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
{
if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
{
if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) )
{
nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
assert( nNodesSaved2 == nNodesSaved );
}
if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )

16
src/aig/dar/darScript.c
View File

@ -435,6 +435,7 @@ ABC_PRT( "Choicing time ", clock() - clk );
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
int fVerbose = pPars->fVerbose;
int fConstruct = 0;
@ -444,7 +445,8 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
clk = clock();
// vAigs = Dar_ManChoiceSynthesisExt();
vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
// vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
// swap the first and last network
// this should lead to the primary choice being "better" because of synthesis
@ -458,9 +460,9 @@ clk = clock();
if ( fVerbose )
{
ABC_PRT( "Synthesis time", clock() - clk );
//ABC_PRT( "Synthesis time", clock() - clk );
}
// pPars->timeSynth = clock() - clk;
pPars->timeSynth = clock() - clk;
clk = clock();
/*
@ -469,7 +471,11 @@ clk = clock();
else
pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
*/
pMan = Dch_ComputeChoices( vAigs, pPars );
// perform choice computation
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( vAigs, pPars );
else
pMan = Dch_ComputeChoices( vAigs, pPars );
// reconstruct the network
pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
@ -483,6 +489,8 @@ clk = clock();
}
// reset levels
Aig_ManChoiceLevel( pMan );
ABC_FREE( pMan->pName );
ABC_FREE( pMan->pSpec );
pMan->pName = Aig_UtilStrsav( pTemp->pName );
pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );

4
src/aig/dch/dch.h
View File

@ -46,8 +46,10 @@ struct Dch_Pars_t_
int nSatVarMax; // the max number of SAT variables
int fSynthesis; // set to 1 to perform synthesis
int fPolarFlip; // uses polarity adjustment
int fSimulateTfo; // uses simulatin of TFO classes
int fSimulateTfo; // uses simulation of TFO classes
int fPower; // uses power-aware rewriting
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
int fVerbose; // verbose stats
int timeSynth; // synthesis runtime
int nNodesAhead; // the lookahead in terms of nodes

2
src/aig/dch/dchAig.c
View File

@ -72,7 +72,7 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
{
assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
nNodes += Aig_ManNodeNum(pAig);
nNodes += Aig_ManNodeNum(pAig2);
Aig_ManCleanData( pAig2 );
}
// map constant nodes

6
src/aig/gia/gia.h
View File

@ -418,6 +418,7 @@ static inline int Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c ) { i
static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id ) { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );}
static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; }
static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
@ -535,6 +536,8 @@ extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
/*=== giaEquiv.c ==========================================================*/
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
extern void Gia_ManDeriveReprs( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
@ -544,6 +547,7 @@ extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int f
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
extern void Gia_ManEquivImprove( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
/*=== giaFanout.c =========================================================*/
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@ -629,6 +633,8 @@ extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis,
extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_ManHasChoices( Gia_Man_t * p );
extern int Gia_ManHasDandling( Gia_Man_t * p );
#ifdef __cplusplus
}

94
src/aig/gia/giaAig.c
View File

@ -45,19 +45,24 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
SeeAlso []
***********************************************************************/
void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Obj_t * pObj )
void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj->pData )
Aig_Obj_t * pNext;
if ( pObj->iData )
return;
if ( Aig_ObjIsPi(pObj) )
{
pObj->iData = Gia_ManAppendCi( pNew );
return;
}
assert( Aig_ObjIsNode(pObj) );
Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
Gia_ManFromAig_rec( pNew, Aig_ObjFanin1(pObj) );
Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
{
int iObjNew, iNextNew;
Gia_ManFromAig_rec( pNew, p, pNext );
iObjNew = Gia_Lit2Var(pObj->iData);
iNextNew = Gia_Lit2Var(pNext->iData);
if ( pNew->pNexts )
pNew->pNexts[iObjNew] = iNextNew;
}
}
/**Function*************************************************************
@ -76,26 +81,25 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
Gia_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// add fake POs to all the dangling nodes (choices)
Aig_ManForEachNode( p, pObj, i )
assert( Aig_ObjRefs(pObj) > 0 );
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
// create room to store equivalences
if ( p->pEquivs )
pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->iData = 1;
Aig_ManForEachPi( p, pObj, i )
{
// if ( Aig_ObjRefs(pObj) == 0 )
pObj->iData = Gia_ManAppendCi( pNew );
}
pObj->iData = Gia_ManAppendCi( pNew );
// add logic for the POs
Aig_ManForEachPo( p, pObj, i )
Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
if ( pNew->pNexts )
Gia_ManDeriveReprs( pNew );
return pNew;
}
@ -117,7 +121,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
int i;
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->iData = 1;
@ -127,12 +131,12 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
Aig_ManForEachNode( p, pObj, i )
if ( Aig_ObjRefs(pObj) == 0 )
{
Gia_ManFromAig_rec( pNew, pObj );
Gia_ManFromAig_rec( pNew, p, pObj );
Gia_ManAppendCo( pNew, pObj->iData );
}
// add logic for the POs
Aig_ManForEachPo( p, pObj, i )
Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
@ -152,17 +156,27 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
***********************************************************************/
void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pNext;
if ( ppNodes[Gia_ObjId(p, pObj)] )
return;
if ( Gia_ObjIsCi(pObj) )
{
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
return;
else
{
assert( Gia_ObjIsAnd(pObj) );
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
}
if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
{
Aig_Obj_t * pObjNew, * pNextNew;
Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
pObjNew = ppNodes[Gia_ObjId(p, pObj)];
pNextNew = ppNodes[Gia_ObjId(p, pNext)];
if ( pNew->pEquivs )
pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);
}
assert( Gia_ObjIsAnd(pObj) );
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
}
/**Function*************************************************************
@ -176,37 +190,31 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
{
Aig_Man_t * pNew;
Aig_Obj_t ** ppNodes;
Gia_Obj_t * pObj;
int i;
assert( !fChoices || (p->pNexts && p->pReprs) );
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
// pNew->pSpec = Gia_UtilStrsav( p->pName );
// duplicate representation of choice nodes
if ( fChoices )
pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
// create the PIs
ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
ppNodes[0] = Aig_ManConst0(pNew);
Gia_ManForEachCi( p, pObj, i )
{
// if ( Aig_ObjRefs(pObj) == 0 )
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
}
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
// add logic for the POs
Gia_ManForEachCo( p, pObj, i )
{
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
}
/*
Gia_ManForEachCo( p, pObj, i )
Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
*/
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
ABC_FREE( ppNodes );
return pNew;
@ -230,7 +238,7 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
pGia = Gia_ManFromAig( p );
pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
Gia_ManStop( pTemp );
pMan = Gia_ManToAig( pGia );
pMan = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );
return pMan;
}

2
src/aig/gia/giaAig.h
View File

@ -48,7 +48,7 @@
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
#ifdef __cplusplus
}

2
src/aig/gia/giaAiger.c
View File

@ -413,7 +413,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Aig_UtilStrsav( pFileName );
// pNew->pSpec = Gia_UtilStrsav( pFileName );
ABC_FREE( pName );
// prepare the array of nodes

23
src/aig/gia/giaDup.c
View File

@ -387,6 +387,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
{
if ( pObj->fMark0 )
continue;
pObj->fMark0 = 0;
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
@ -396,14 +397,32 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
}
else if ( Gia_ObjIsCo(pObj) )
{
Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
// Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
nRis += Gia_ObjIsRi(p, pObj);
}
}
assert( nRos == nRis );
Gia_ManSetRegNum( pNew, nRos );
if ( p->pReprs && p->pNexts )
{
Gia_Obj_t * pRepr;
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
Gia_ManForEachObj1( p, pObj, i )
{
if ( !~pObj->Value )
continue;
pRepr = Gia_ObjReprObj( p, i );
if ( pRepr == NULL )
continue;
assert( ~pRepr->Value );
if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) )
Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) );
}
pNew->pNexts = Gia_ManDeriveNexts( pNew );
}
return pNew;
}

293
src/aig/gia/giaEquiv.c
View File

@ -94,7 +94,8 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
{
unsigned * pNexts, * pTails;
int i;
assert( p->pReprs );
assert( p->pReprs != NULL );
assert( p->pNexts == NULL );
pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
@ -110,6 +111,37 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
return (int *)pNexts;
}
/**Function*************************************************************
Synopsis [Given points to the next objects, derives representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDeriveReprs( Gia_Man_t * p )
{
int i, iObj;
assert( p->pReprs == NULL );
assert( p->pNexts != NULL );
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
Gia_ObjSetRepr( p, i, GIA_VOID );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
{
if ( p->pNexts[i] == 0 )
continue;
if ( p->pReprs[i].iRepr != GIA_VOID )
continue;
// next is set, repr is not set
for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
p->pReprs[iObj].iRepr = i;
}
}
/**Function*************************************************************
Synopsis []
@ -175,6 +207,25 @@ int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
return nLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManEquivCountClasses( Gia_Man_t * p )
{
int i, Counter = 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
Counter += Gia_ObjIsHead(p, i);
return Counter;
}
/**Function*************************************************************
Synopsis []
@ -966,6 +1017,246 @@ void Gia_ManEquivImprove( Gia_Man_t * p )
// p->pNexts = Gia_ManDeriveNexts( p );
}
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNode.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
{
// check the trivial cases
if ( pNode == NULL )
return 0;
if ( Gia_ObjIsCi(pNode) )
return 0;
// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
// return 0;
if ( pNode == pOld )
return 1;
// skip the visited node
if ( pNode->fMark0 )
return 0;
pNode->fMark0 = 1;
Vec_PtrPush( vVisited, pNode );
// check the children
if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
return 1;
if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
return 1;
// check equivalent nodes
return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
}
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNode.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
{
Vec_Ptr_t * vVisited;
Gia_Obj_t * pObj;
int RetValue, i;
assert( !Gia_IsComplement(pOld) );
assert( !Gia_IsComplement(pNode) );
vVisited = Vec_PtrAlloc( 100 );
RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
Vec_PtrForEachEntry( vVisited, pObj, i )
pObj->fMark0 = 0;
Vec_PtrFree( vVisited );
return RetValue;
}
/**Function*************************************************************
Synopsis [Adds the next entry while making choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
{
if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
{
Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
return;
}
Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
if ( ~pObj->Value )
return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjIsConst0(pRepr) )
{
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
Gia_ManEquivToChoices_rec( pNew, p, pRepr );
assert( Gia_ObjIsAnd(pObj) );
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
{
assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
{
assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
{
assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
}
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Removes choices, which contain fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManRemoveBadChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iObj, iPrev, Counter = 0;
// mark nodes with fanout
Gia_ManForEachObj( p, pObj, i )
{
pObj->fMark0 = 0;
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark0 = 1;
}
else if ( Gia_ObjIsCo(pObj) )
Gia_ObjFanin0(pObj)->fMark0 = 1;
}
// go through the classes and remove
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
{
if ( !Gia_ManObj(p, iObj)->fMark0 )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
}
// remove the marks
Gia_ManCleanMark0( p );
// printf( "Removed %d bad choices.\n", Counter );
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
int i;
assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
for ( i = 0; i < Gia_ManObjNum(p); i++ )
Gia_ObjSetRepr( pNew, i, GIA_VOID );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
pObj->Value = pRepr->Value;
}
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
if ( i % nSnapshots == 0 )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Gia_ManRemoveBadChoices( pNew );
// Gia_ManEquivPrintClasses( pNew, 0, 0 );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
// Gia_ManEquivPrintClasses( pNew, 0, 0 );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/gia/giaMan.c
View File

@ -158,7 +158,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p )
void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
{
if ( p->pName )
printf( "%8s : ", p->pName );
printf( "%-8s : ", p->pName );
printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
if ( Gia_ManRegNum(p) )
printf( " ff =%7d", Gia_ManRegNum(p) );
@ -166,6 +166,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
printf( " lev =%5d", Gia_ManLevelNum(p) );
printf( " cut =%5d", Gia_ManCrossCut(p) );
printf( " mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
if ( Gia_ManHasDandling(p) )
printf( " ch =%5d", Gia_ManEquivCountClasses(p) );
if ( fSwitch )
{
if ( p->pSwitching )

6
src/aig/gia/giaScl.c
View File

@ -41,12 +41,15 @@
***********************************************************************/
int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( pObj == NULL )
return 0;
if ( !pObj->fMark0 )
return 0;
pObj->fMark0 = 0;
assert( Gia_ObjIsAnd(pObj) );
return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
+ Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) );
+ Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) )
+ (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0);
}
/**Function*************************************************************
@ -88,6 +91,7 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
return Gia_ManDupMarked( p );
}
/**Function*************************************************************
Synopsis [Marks CIs/COs/ANDs unreachable from POs.]

108
src/aig/gia/giaUtil.c
View File

@ -858,6 +858,114 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
return ConeSize1;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter1 = 0, Counter2 = 0;
int nFailNoRepr = 0;
int nFailHaveRepr = 0;
int nChoiceNodes = 0;
int nChoices = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
// check if there are any representatives
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
Counter1++;
if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
Counter2++;
}
if ( Counter1 == 0 )
{
printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
return 0;
}
// printf( "%d nodes have reprs.\n", Counter1 );
// printf( "%d nodes have nexts.\n", Counter2 );
// check if there are any internal nodes without fanout
// make sure all nodes without fanout have representatives
// make sure all nodes with fanout have no representatives
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Gia_ObjRefs(p, pObj) == 0 )
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
nFailNoRepr++;
else
nChoices++;
}
else
{
if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
nFailHaveRepr++;
if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
nChoiceNodes++;
}
if ( Gia_ObjReprObj( p, i ) )
assert( Gia_ObjRepr(p, i) < i );
}
if ( nChoices == 0 )
return 0;
if ( nFailNoRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
// return 0;
}
if ( nFailHaveRepr )
{
printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
// return 0;
}
// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasDandling( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachObj( p, pObj, i )
{
pObj->fMark0 = 0;
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark0 = 1;
}
else if ( Gia_ObjIsCo(pObj) )
Gia_ObjFanin0(pObj)->fMark0 = 1;
}
Gia_ManForEachAnd( p, pObj, i )
Counter += !pObj->fMark0;
Gia_ManCleanMark0( p );
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/ivy/ivyRwr.c
View File

@ -96,9 +96,9 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
}
if ( nGain > 0 )
{ // print stats on the MFFC
extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode );
extern void Ivy_NodeMffcConeSuppPrint( Ivy_Obj_t * pNode );
printf( "Node %6d : Gain = %4d ", pNode->Id, nGain );
Ivy_NodeMffsConeSuppPrint( pNode );
Ivy_NodeMffcConeSuppPrint( pNode );
}
*/
// complement the FF if needed

4
src/aig/ssw/sswClass.c
View File

@ -392,7 +392,7 @@ void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
printf( "{ " );
Ssw_ClassForEachNode( p, pRepr, pObj, i )
printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
printf( "}\n" );
}
@ -420,7 +420,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
Aig_ManForEachObj( p->pAig, pObj, i )
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
printf( "}\n" );
Ssw_ManForEachClass( p, ppClass, i )
{

2
src/base/abc/abc.h
View File

@ -779,7 +779,7 @@ extern ABC_DLL int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
extern ABC_DLL int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
extern ABC_DLL int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
extern ABC_DLL int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
extern ABC_DLL void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode );
extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode );
/*=== abcRefactor.c ==========================================================*/

2
src/base/abc/abcNtk.c
View File

@ -741,7 +741,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
vCone = Vec_PtrAlloc( 100 );
vSupp = Vec_PtrAlloc( 100 );
Abc_NodeDeref_rec( pNode );
Abc_NodeMffsConeSupp( pNode, vCone, vSupp );
Abc_NodeMffcConeSupp( pNode, vCone, vSupp );
Abc_NodeRef_rec( pNode );
// create the PIs
Vec_PtrForEachEntry( vSupp, pObj, i )

20
src/base/abc/abcRefs.c
View File

@ -260,7 +260,7 @@ int Abc_NodeRef_rec( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
void Abc_NodeMffcConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
{
Abc_Obj_t * pFanin;
int i;
@ -276,7 +276,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t *
}
// recur on the children
Abc_ObjForEachFanin( pNode, pFanin, i )
Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 );
Abc_NodeMffcConeSupp_rec( pFanin, vCone, vSupp, 0 );
// collect the internal node
if ( vCone ) Vec_PtrPush( vCone, pNode );
// printf( "%d ", pNode->Id );
@ -293,14 +293,14 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t *
SeeAlso []
***********************************************************************/
void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
{
assert( Abc_ObjIsNode(pNode) );
assert( !Abc_ObjIsComplement(pNode) );
if ( vCone ) Vec_PtrClear( vCone );
if ( vSupp ) Vec_PtrClear( vSupp );
Abc_NtkIncrementTravId( pNode->pNtk );
Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
Abc_NodeMffcConeSupp_rec( pNode, vCone, vSupp, 1 );
// printf( "\n" );
}
@ -315,7 +315,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
SeeAlso []
***********************************************************************/
void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode )
{
Vec_Ptr_t * vCone, * vSupp;
Abc_Obj_t * pObj;
@ -323,7 +323,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
vCone = Vec_PtrAlloc( 100 );
vSupp = Vec_PtrAlloc( 100 );
Abc_NodeDeref_rec( pNode );
Abc_NodeMffsConeSupp( pNode, vCone, vSupp );
Abc_NodeMffcConeSupp( pNode, vCone, vSupp );
Abc_NodeRef_rec( pNode );
printf( "Node = %6s : Supp = %3d Cone = %3d (",
Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) );
@ -345,7 +345,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside )
int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside )
{
Abc_Obj_t * pObj;
int i, Count1, Count2;
@ -355,7 +355,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns
// dereference the node
Count1 = Abc_NodeDeref_rec( pNode );
// collect the nodes inside the MFFC
Abc_NodeMffsConeSupp( pNode, vInside, NULL );
Abc_NodeMffcConeSupp( pNode, vInside, NULL );
// reference it back
Count2 = Abc_NodeRef_rec( pNode );
assert( Count1 == Count2 );
@ -376,7 +376,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode )
Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode )
{
Vec_Ptr_t * vInside;
int Count1, Count2;
@ -384,7 +384,7 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode )
Count1 = Abc_NodeDeref_rec( pNode );
// collect the nodes inside the MFFC
vInside = Vec_PtrAlloc( 10 );
Abc_NodeMffsConeSupp( pNode, vInside, NULL );
Abc_NodeMffcConeSupp( pNode, vInside, NULL );
// reference it back
Count2 = Abc_NodeRef_rec( pNode );
assert( Count1 == Count2 );

75
src/base/abci/abc.c
View File

@ -9515,7 +9515,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF )
{
switch ( c )
{
@ -9561,6 +9561,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fSimulateTfo ^= 1;
break;
case 'g':
pPars->fUseGia ^= 1;
break;
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -9591,7 +9597,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" );
fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" );
fprintf( pErr, "\t computes structural choices using a new approach\n" );
fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@ -9599,6 +9605,8 @@ usage:
fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
fprintf( pErr, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( pErr, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
fprintf( pErr, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -21820,6 +21828,7 @@ usage:
int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
Gia_Man_t * pAig;
Aig_Man_t * pMan;
int c, fVerbose = 0;
@ -21845,12 +21854,15 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "The current network should be strashed.\n" );
return 1;
}
// if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
// {
// printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
// Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
// }
if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
{
printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
}
pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
pMan = Abc_NtkToDarChoices( pAbc->pNtkCur );
else
pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
pAig = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
if ( pAig == NULL )
@ -21886,6 +21898,7 @@ usage:
int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
extern Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
Aig_Man_t * pMan;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
@ -21917,9 +21930,27 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
pMan = Gia_ManToAig( pAbc->pAig );
pNtk = Abc_NtkFromAigPhase( pMan );
Aig_ManStop( pMan );
if ( Gia_ManHasDandling(pAbc->pAig) == 0 )
{
pMan = Gia_ManToAig( pAbc->pAig, 0 );
pNtk = Abc_NtkFromAigPhase( pMan );
Aig_ManStop( pMan );
}
else
{
Abc_Ntk_t * pNtkNoCh;
// printf( "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pAig) );
// create network without choices
pMan = Gia_ManToAig( pAbc->pAig, 0 );
pNtkNoCh = Abc_NtkFromAigPhase( pMan );
pNtkNoCh->pName = Extra_UtilStrsav(pMan->pName);
Aig_ManStop( pMan );
// derive network with choices
pMan = Gia_ManToAig( pAbc->pAig, 1 );
pNtk = Abc_NtkFromDarChoices( pNtkNoCh, pMan );
Abc_NtkDelete( pNtkNoCh );
Aig_ManStop( pMan );
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
@ -22204,7 +22235,7 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Show(): There is no AIG.\n" );
return 1;
}
pMan = Gia_ManToAig( pAbc->pAig );
pMan = Gia_ManToAig( pAbc->pAig, 0 );
Aig_ManShow( pMan, 0, NULL );
Aig_ManStop( pMan );
return 0;
@ -23400,7 +23431,7 @@ usage:
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@ -23425,7 +23456,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_ManCorSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF )
{
switch ( c )
{
@ -23457,6 +23488,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fUseRings ^= 1;
break;
case 'e':
pPars->fMakeChoices ^= 1;
break;
case 'c':
pPars->fUseCSat ^= 1;
break;
@ -23483,12 +23517,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: &scorr [-FC num] [-frcvh]\n" );
fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" );
fprintf( stdout, "\t performs signal correpondence computation\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@ -23513,7 +23548,7 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_ManChcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Ccvh" ) ) != EOF )
{
switch ( c )
{
@ -23528,6 +23563,9 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'c':
pPars->fUseCSat ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -23540,8 +23578,6 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Choice(): There is no AIG.\n" );
return 1;
}
printf("The command is not yet ready.\n" );
return 0;
pAbc->pAig = Cec_ManChoiceComputation( pTemp = pAbc->pAig, pPars );
if ( pAbc->pAig == NULL )
{
@ -23553,9 +23589,10 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( stdout, "usage: &choice [-C num] [-vh]\n" );
fprintf( stdout, "usage: &choice [-C num] [-cvh]\n" );
fprintf( stdout, "\t performs computation of structural choices\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;

4
src/base/abci/abcCut.c
View File

@ -586,7 +586,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk )
Abc_Obj_t * pObj;//, * pTemp;
int i;//, k;
int nNodesTotal = 0, nMffcsTotal = 0;
extern Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode );
extern Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode );
vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
// Abc_NtkForEachCi( pNtk, pObj, i )
@ -615,7 +615,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk )
{
if ( Vec_IntEntry( vAttrs, pObj->Id ) )
{
vNodes = Abc_NodeMffsInsideCollect( pObj );
vNodes = Abc_NodeMffcInsideCollect( pObj );
Vec_PtrForEachEntry( vNodes, pTemp, k )
if ( pTemp != pObj )
Vec_IntWriteEntry( vAttrs, pTemp->Id, 0 );

10
src/base/abci/abcDar.c
View File

@ -896,6 +896,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
Vec_Ptr_t * vAigs;
Aig_Man_t * pMan, * pTemp;
@ -911,6 +912,10 @@ clk = clock();
// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
Aig_ManStop( pMan );
// swap around the first and the last
pTemp = Vec_PtrPop( vAigs );
Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
Vec_PtrWriteEntry( vAigs, 0, pTemp );
}
else
{
@ -918,7 +923,10 @@ clk = clock();
Vec_PtrPush( vAigs, pMan );
}
pPars->timeSynth = clock() - clk;
pMan = Dch_ComputeChoices( vAigs, pPars );
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( vAigs, pPars );
else
pMan = Dch_ComputeChoices( vAigs, pPars );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
// pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );

4
src/base/abci/abcPrint.c
View File

@ -704,9 +704,9 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i;
extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
extern void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode );
Abc_NtkForEachNode( pNtk, pNode, i )
Abc_NodeMffsConeSuppPrint( pNode );
Abc_NodeMffcConeSuppPrint( pNode );
}
/**Function*************************************************************

4
src/base/abci/abcResub.c
View File

@ -1624,7 +1624,7 @@ void Abc_ManResubCleanup( Abc_ManRes_t * p )
***********************************************************************/
Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, bool fVerbose )
{
extern int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
Dec_Graph_t * pGraph;
int Required;
int clk;
@ -1639,7 +1639,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
// collect the MFFC
clk = clock();
p->nMffc = Abc_NodeMffsInside( pRoot, vLeaves, p->vTemp );
p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp );
p->timeMffc += clock() - clk;
assert( p->nMffc > 0 );

2
src/base/io/ioWriteAiger.c
View File

@ -728,7 +728,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
// write the comment
fprintfBz2Aig( &b, "c" );
if ( pNtk->pName && strlen(pNtk->pName) > 0 )
fprintfBz2Aig( &b, "n%s%c", pNtk->pName, '\0' );
fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );