diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/aig/aig.h | 4 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 8 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 5 | ||||
-rw-r--r-- | src/aig/saig/saigConstr2.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigUnfold2.c | 558 | ||||
-rw-r--r-- | src/base/abci/abc.c | 5 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcDarUnfold2.c | 69 | ||||
-rw-r--r-- | src/base/abci/abciUnfold2.c | 121 |
9 files changed, 771 insertions, 3 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index db7d380d..e92e512c 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -165,6 +165,10 @@ struct Aig_Man_t_ // timing statistics abctime time1; abctime time2; + //-- jlong -- begin + Vec_Ptr_t * unfold2_type_I; + Vec_Ptr_t * unfold2_type_II; + //-- jlong -- end }; // cut computation diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 230a2b18..246e0501 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -60,6 +60,10 @@ Aig_Man_t * Aig_ManStart( int nNodesMax ) p->vCos = Vec_PtrAlloc( 100 ); p->vObjs = Vec_PtrAlloc( 1000 ); p->vBufs = Vec_PtrAlloc( 100 ); + //--jlong -- begin + p->unfold2_type_I = Vec_PtrAlloc( 4); + p->unfold2_type_II = Vec_PtrAlloc( 4); + //--jlong -- end // prepare the internal memory manager p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax ); // create the constant node @@ -200,6 +204,10 @@ void Aig_ManStop( Aig_Man_t * p ) Vec_PtrFreeP( &p->vCos ); Vec_PtrFreeP( &p->vObjs ); Vec_PtrFreeP( &p->vBufs ); + //--jlong -- begin + Vec_PtrFreeP( &p->unfold2_type_I ); + Vec_PtrFreeP( &p->unfold2_type_II ); + //--jlong -- end Vec_IntFreeP( &p->vLevelR ); Vec_VecFreeP( &p->vLevels ); Vec_IntFreeP( &p->vFlopNums ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 475f476d..380af64b 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -116,6 +116,11 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame /*=== saigConstr2.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ); extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ); +// -- jlong -- begin +extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt ); +extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt); +// --jlong -- end + /*=== saigDual.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne ); extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles ); diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 8ab5df51..6e560b59 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -1008,6 +1008,6 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - +#include "saigUnfold2.c" ABC_NAMESPACE_IMPL_END diff --git a/src/aig/saig/saigUnfold2.c b/src/aig/saig/saigUnfold2.c new file mode 100644 index 00000000..72558ab8 --- /dev/null +++ b/src/aig/saig/saigUnfold2.c @@ -0,0 +1,558 @@ + +int Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter + , int type_ /* jlong -- */ + ) +{ + Aig_Obj_t * pObj; + int Lit, status; + pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */ + Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 ); + if ( status == l_False ) /* unsat */ + return status; + if ( status == l_Undef ) + { + printf( "Solver returned undecided.\n" ); + return status; + } + assert( status == l_True ); + return status; +} + +Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands ) +{ + int nFrames = 3; + Vec_Ptr_t * vNodes; + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; + Aig_Obj_t ** pObjMap; + int i, f, k; + + // create mapping for the frames nodes + pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); + + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); + // map constant nodes + for ( f = 0; f < nFrames; f++ ) + Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); + // create PI nodes for the frames + for ( f = 0; f < nFrames; f++ ) + Aig_ManForEachPiSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) ); + // set initial state for the latches + Aig_ManForEachLoSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) ); + + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + { + pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) ); + Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); + } + // set the latch inputs and copy them into the latch outputs of the next frame + Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i ) + { + pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f); + if ( f < nFrames - 1 ) + Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew ); + } + } + + // go through the candidates + Vec_VecForEachLevel( vCands, vNodes, i ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) + { + Aig_Obj_t * pObjR = Aig_Regular(pObj); + Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0]; + Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1]; + { + Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) ); + Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) ); + Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 ); + Aig_ObjCreateCo( pFrames, pMiter ); + + /* need to check p & Xp is satisfiable */ + /* jlong -- begin */ + Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1)); + Aig_ObjCreateCo( pFrames, pMiter2 ); /* jlong -- end */ + } + + { /* jlong -- begin */ + Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2]; + Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) ); + Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, Aig_IsComplement(pObj) ); + Aig_Obj_t * pFan2 = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) ); + Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2); + Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end */ + } + + } + } + Aig_ManCleanup( pFrames ); + ABC_FREE( pObjMap ); + +//Aig_ManShow( pAig, 0, NULL ); +//Aig_ManShow( pFrames, 0, NULL ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Detects constraints functionally.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManFilterUsingInd2( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + Aig_Man_t * pFrames; + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int i, k, k2, Counter; + /* + Vec_VecForEachLevel( vCands, vNodes, i ) + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) + printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) ); + printf( "\n" ); + */ + // create timeframes + // pFrames = Saig_ManUnrollInd( p ); + pFrames = Saig_ManCreateIndMiter2( p, vCands ); + assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 ); + // start the SAT solver + pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // check candidates + if ( fVerbose ) + printf( "Filtered cands: \n" ); + Counter = 0; + Vec_VecForEachLevel( vCands, vNodes, i ) + { + assert(i==0); /* only one item */ + k2 = 0; + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) + { + if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False) + // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) ) + { + Vec_PtrWriteEntry( vNodes, k2++, pObj ); + if ( fVerbose ) + printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + Vec_PtrPush(p->unfold2_type_I, pObj); + } + /* jlong -- begin */ + else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */ + { + if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){ + //Vec_PtrWriteEntry( vNodes, k2++, pObj ); + if ( fVerbose ) + printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + printf( " type II: %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */ + Vec_PtrPush(p->unfold2_type_II, pObj); + } + } + /* jlong -- end */ + } + Vec_PtrShrink( vNodes, k2 ); + } + + // clean up + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + if ( fVerbose ) + Aig_ManPrintStats( pFrames ); + Aig_ManStop( pFrames ); +} + + +/**Function************************************************************* + + Synopsis [Returns the number of variables implied by the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Ssw_ManFindDirectImplications2( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose ) +{ + Vec_Vec_t * vCands = NULL; + Vec_Ptr_t * vNodes; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pRepr, * pReprR; + int i, f, k, value; + assert(nFrames == 1); + vCands = Vec_VecAlloc( nFrames ); + assert(nFrames == 1); + // perform unrolling + pFrames = Saig_ManUnrollCOI( p, nFrames ); + assert( Aig_ManCoNum(pFrames) == 1 ); + // start the SAT solver + pCnf = Cnf_DeriveSimple( pFrames, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat != NULL ) + { + Aig_ManIncrementTravId( p ); + for ( f = 0; f < nFrames; f++ ) + { + Aig_ManForEachObj( p, pObj, i ) + { + if ( !Aig_ObjIsCand(pObj) ) + continue; + //--jlong : also use internal nodes as well + /* if ( !Aig_ObjIsCi(pObj) ) */ + /* continue; */ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + continue; + // get the node from timeframes + pRepr = p->pObjCopies[nFrames*i + nFrames-1-f]; + pReprR = Aig_Regular(pRepr); + if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 ) + continue; + // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ]; + value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] ); + if ( value == l_Undef ) + continue; + // label this node as taken + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Saig_ObjIsLo(p, pObj) ) + Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) ); + // remember the node + Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) ); + // printf( "%s%d ", (value == l_False)? "":"!", i ); + } + } + // printf( "\n" ); + sat_solver_delete( pSat ); + } + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + + if ( fVerbose ) + { + printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) ); + Vec_VecForEachLevel( vCands, vNodes, k ) + { + printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) ); + // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + printf( "\n" ); + } + } + + ABC_FREE( p->pObjCopies ); + /* -- jlong -- this does the SAT proof of the constraints */ + Saig_ManFilterUsingInd2( p, vCands, nConfs, nProps, fVerbose ); + if ( Vec_VecSizeSize(vCands) ) + printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) ); + if ( fVerbose ) + { + Vec_VecForEachLevel( vCands, vNodes, k ) + { + printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) ); + // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); + printf( "\n" ); + } + } + + return vCands; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG while unfolding constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){ + Aig_Man_t * pNew; + Vec_Vec_t * vCands; + Vec_Ptr_t * vNodes, * vNewFlops; + Aig_Obj_t * pObj; + int i, j, k, nNewFlops; + if ( fOldAlgo ) + vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose ); + else + vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose ); + if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 ) + { + Vec_VecFreeP( &vCands ); + return Aig_ManDupDfs( pAig ); + } + // create new manager + pNew = Aig_ManDupWithoutPos( pAig ); + pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands); + // pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II); + *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II); + // add normal POs + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); + // create constraint outputs + vNewFlops = Vec_PtrAlloc( 100 ); + + + Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){ + Aig_Obj_t * x = Aig_ObjRealCopy(pObj); + Aig_ObjCreateCo(pNew, x); + } + + Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){ + Aig_Obj_t * x = Aig_ObjRealCopy(pObj); + Aig_ObjCreateCo(pNew, x); + } + + + if(0) Vec_VecForEachLevel( vCands, vNodes, i ) + { + assert(i==0); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) + { + Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) ); + for ( j = 0; j < i; j++ ) + Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) ); + Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) ); + } + } + // add latch outputs + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); + // add new latch outputs + nNewFlops = 0;//Vec_VecSizeSize(vCands); + + if(0)Vec_VecForEachLevel( vCands, vNodes, i ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) + { + for ( j = 0; j < i; j++ ) + Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) ); + } + } + //assert( nNewFlops == Vec_PtrSize(vNewFlops) ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops ); + Vec_VecFreeP( &vCands ); + Vec_PtrFree( vNewFlops ); + return pNew; + +} +Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2_( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ) +{ + Aig_Man_t * pNew; + Vec_Vec_t * vCands; + // Vec_Ptr_t * vNodes, * vNewFlops; + Aig_Obj_t * pObj; + int i, k; + Aig_Obj_t * pMiter = NULL; + const int fCompl = 0; + + + if ( fOldAlgo ) + vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose ); + else + vCands = Ssw_ManFindDirectImplications2( pAig, nFrames, nConfs, nProps, fVerbose ); + if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 ) + { + Vec_VecFreeP( &vCands ); + return Aig_ManDupDfs( pAig ); + } + // create new manager + pNew = Aig_ManDupWithoutPos( pAig ); + + pMiter = Aig_ManConst0( pNew ); + + Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){ + + pMiter = Aig_Or( pNew, pMiter, + Aig_NotCond( Aig_ObjRealCopy(pObj), fCompl ) ); + printf("new id: %d\n", Aig_ObjId(pMiter)); + } + + Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){ + Aig_Obj_t * type_II_latch + = Aig_ObjCreateCi(pNew); /* will get connected later; */ + Aig_Obj_t *kk = Aig_And(pNew, + Aig_NotCond(type_II_latch, fCompl), + Aig_NotCond(Aig_ObjRealCopy(pObj), fCompl) + ); + + pMiter = Aig_Or(pNew, pMiter, kk + ); + } + { + Aig_Obj_t * pObjLi, *pObjLo; + Aig_Obj_t * pFlopOut = Aig_ObjCreateCi(pNew); + Aig_Obj_t * pFlopIn = Aig_Or(pNew, pMiter, pFlopOut); + + Saig_ManForEachPo(pAig, pObj, i){ + Aig_Obj_t *p = Aig_And( pNew, Aig_ObjChild0(pObj), Aig_Not(pFlopIn) ); + printf("new id: %d\n", Aig_ObjId(p)); + Aig_ObjCreateCo(pNew, p); + } + + // add latch outputs + + Saig_ManForEachLiLo(pAig, pObjLi, pObjLo, i){ + Aig_Obj_t *c = Aig_Mux(pNew, Aig_Not(pFlopIn), + Aig_ObjChild0Copy(pObjLi) , + Aig_ObjRealCopy(pObjLo));//->pData); + Aig_ObjCreateCo(pNew, c); + printf("new id: %d\n", Aig_ObjId(c)); + } + + + + Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){ + Aig_ObjCreateCo( pNew, Aig_ObjRealCopy(pObj)); + } + Aig_ObjCreateCo(pNew, pFlopIn); + } + Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + Vec_PtrSize(pAig->unfold2_type_II) + 1); + Vec_VecFreeP( &vCands ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG while unfolding constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose , + int typeII_cnt) +{ + Aig_Man_t * pAigNew; + Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj; + int i; + if ( Aig_ManConstrNum(pAig) == 0 ) + return Aig_ManDupDfs( pAig ); + assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) ); + // start the new manager + pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); + pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + // create variables for PIs + Aig_ManForEachCi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreateCi( pAigNew ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + + // OR the constraint outputs + pMiter = Aig_ManConst0( pAigNew ); + + int type_II = 0; + + Saig_ManForEachPo( pAig, pObj, i ) + { + + if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) + continue; + if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) { + type_II = 1; + } + /* now we got the constraint */ + if (type_II) { + printf("modeling typeII \n"); + Aig_Obj_t * type_II_latch + = Aig_ObjCreateCi(pAigNew); /* will get connected later; */ + pMiter = Aig_Or(pAigNew, pMiter, + Aig_And(pAigNew, + Aig_NotCond(type_II_latch, fCompl), + Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ) + ); + } else + pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); + } + + // create additional flop + if ( Saig_ManRegNum(pAig) > 0 ) + { + pFlopOut = Aig_ObjCreateCi( pAigNew ); + pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut ); + } + else + pFlopIn = pMiter; + + // create primary output + Saig_ManForEachPo( pAig, pObj, i ) + { + if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) + continue; + pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) ); + Aig_ObjCreateCo( pAigNew, pMiter ); + } + + // transfer to register outputs + { + /* the same for type I and type II */ + Aig_Obj_t * pObjLi, *pObjLo; + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) { + Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), + Aig_ObjChild0Copy(pObjLi) , + pObjLo->pData); + Aig_ObjCreateCo( pAigNew, c); + } + + } + if(0)Saig_ManForEachLi( pAig, pObj, i ) { + Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); + + Saig_ManForEachPo( pAig, pObj, i ) + { + + if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) + continue; + /* now we got the constraint */ + if (type_II) { + Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj)); + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 ); + } + } + + + // create additional flop + + if ( Saig_ManRegNum(pAig) > 0 ) + { + Aig_ObjCreateCo( pAigNew, pFlopIn ); + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 ); + } + + // perform cleanup + Aig_ManCleanup( pAigNew ); + Aig_ManSeqCleanup( pAigNew ); + return pAigNew; +} diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2323ac36..63cc04b8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -294,6 +294,7 @@ static int Abc_CommandTempor ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -870,6 +871,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 ); Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); + + Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 ); @@ -35347,5 +35350,5 @@ usage: /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - +#include "abciUnfold2.c" ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1870e713..894c9d17 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -4560,6 +4560,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - +#include "abcDarUnfold2.c" ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c new file mode 100644 index 00000000..bacda407 --- /dev/null +++ b/src/base/abci/abcDarUnfold2.c @@ -0,0 +1,69 @@ +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int); +Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + int typeII_cnt = 0; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + if ( fStruct ){ + assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan ); + }else + pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt); + Aig_ManStop( pTemp ); + if ( pMan == NULL ) + return NULL; + // typeII_cnt = pMan->nConstrsTypeII; + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pMan->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec); + Aig_ManStop( pMan ); + + return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt); + + //return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose + , int typeII_cnt + ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Saig_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt ); + Aig_ManStop( pTemp ); + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pMan->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec); + Aig_ManStop( pMan ); + return pNtkAig; +} + diff --git a/src/base/abci/abciUnfold2.c b/src/base/abci/abciUnfold2.c new file mode 100644 index 00000000..ec5047d2 --- /dev/null +++ b/src/base/abci/abciUnfold2.c @@ -0,0 +1,121 @@ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk, * pNtkRes; + int nFrames; + int nConfs; + int nProps; + int fStruct = 0; + int fOldAlgo = 0; + int fVerbose; + int c; + extern Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose ); + pNtk = Abc_FrameReadNtk(pAbc); + // set defaults + nFrames = 1; + nConfs = 1000; + nProps = 1000; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CPvh" ) ) != EOF ) + { + switch ( c ) + { + /* case 'F': */ + /* if ( globalUtilOptind >= argc ) */ + /* { */ + /* Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); */ + /* goto usage; */ + /* } */ + /* nFrames = atoi(argv[globalUtilOptind]); */ + /* globalUtilOptind++; */ + /* if ( nFrames < 0 ) */ + /* goto usage; */ + /* break; */ + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfs < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nProps = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProps < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + if ( Abc_NtkConstrNum(pNtk) > 0 ) + { + Abc_Print( -1, "Constraints are already extracted.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) > 1 && !fStruct ) + { + Abc_Print( -1, "Functional constraint extraction works for single-output miters (use \"orpos\").\n" ); + return 0; + } + // modify the current network + pNtkRes = Abc_NtkDarUnfold2( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose ); + if ( pNtkRes == NULL ) + { + Abc_Print( 1,"Transformation has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; +usage: + Abc_Print( -2, "usage: unfold [-FCP num] [-savh]\n" ); + Abc_Print( -2, "\t unfold hidden constraints as separate outputs\n" ); + Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs ); + Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + |