diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-10-04 19:18:34 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-10-04 19:18:34 -0700 |
commit | 24083998ab2e6abdb0cacd90a8f45a01201aa7ce (patch) | |
tree | 5afd80e046fbb2391ebe5502863378a15e66f202 /src/aig/gia | |
parent | 4c7165a4f75a647dd61c5f09f51131d8ed99924d (diff) | |
download | abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.tar.gz abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.tar.bz2 abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.zip |
Deriving cell mapping with &if -kz.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 14 | ||||
-rw-r--r-- | src/aig/gia/giaEnable.c | 5 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaIf.c | 68 |
4 files changed, 73 insertions, 18 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1dda7dc0..28d65b35 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -135,7 +135,7 @@ struct Gia_Man_t_ Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexSeq; // sequential counter-example Vec_Ptr_t * vSeqModelVec; // sequential counter-examples - int * pCopies; // intermediate copies + Vec_Int_t vCopies; // intermediate copies Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vGateClasses; // classes of gates for abstraction @@ -465,11 +465,15 @@ static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); } -static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } -static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } +static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Vec_IntEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)); } +static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit); } +static inline int Gia_ObjCopyArray( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); } +static inline void Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); } -static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } -static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } +static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } +static inline int Gia_ObjFanin0CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p,pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjFanin1CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId1p(p,pObj)), Gia_ObjFaninC1(pObj)); } static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c index 9cb0dce5..03d1a390 100644 --- a/src/aig/gia/giaEnable.c +++ b/src/aig/gia/giaEnable.c @@ -362,8 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames ) Gia_Man_t * pNew; Gia_Obj_t * pObj, * pObjRi, * pObjRo; int f, i; - ABC_FREE( p->pCopies ); - p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); + Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); @@ -413,7 +412,7 @@ Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, i vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs ); Vec_IntFree( vTemp ); Gia_ManStop( pFrames ); - ABC_FREE( p->pCopies ); + ABC_FREE( p->vCopies.pArray ); // cofactor all these variables pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose ); Vec_IntFree( vCofSigs ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index c5dba25b..61290da2 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1017,7 +1017,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames } */ assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); - p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); + Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) ); vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); if ( fDualOut ) @@ -1052,7 +1052,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames // Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" ); Gia_ManAppendCo( pNew, 0 ); } - ABC_FREE( p->pCopies ); + ABC_FREE( p->vCopies.pArray ); Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 1c4ae9c0..a5eafb5f 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1425,9 +1425,51 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p SeeAlso [] ***********************************************************************/ -int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, void * pNtkCell, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) +int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) { - return 0; + int iLit; + if ( Vec_IntSize(vLeaves) <= nLutMax ) + iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 ); + else + { + Gia_Obj_t * pObj; + int i, Id; + // extract variable permutation + word Perm = If_DsdManGetFuncPerm( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); + assert( Perm > 0 ); + // perform boolean matching + if ( !If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, If_CutTruthW(pIfMan, pCutBest), Vec_IntSize(vLeaves), Perm, Ifn_NtkInputNum(pNtkCell), vLits ) ) + { + printf( "Boolean matching does not exist.\n" ); + return -1; + } + // use config bits to generate the network + iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, vLits, vCover ); + // copy GIA back into the manager + Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 ); + Gia_ObjSetCopyArray( pTemp, 0, 0 ); + Gia_ManForEachCiId( pTemp, Id, i ) + Gia_ObjSetCopyArray( pTemp, Id, Vec_IntEntry(vLeaves, i) ); + // collect nodes + Gia_ManIncrementTravId( pTemp ); + Id = Abc_Lit2Var( iLit ); + Gia_ManCollectAnds( pTemp, &Id, 1, vCover ); + // copy GIA + Gia_ManForEachObjVec( vCover, pTemp, pObj, i ) + { + iLit = Gia_ManAppendAnd( pNew, Gia_ObjFanin0CopyArray(pTemp, pObj), Gia_ObjFanin1CopyArray(pTemp, pObj) ); + Gia_ObjSetCopyArray( pTemp, Gia_ObjId(pTemp, pObj), iLit ); + } + iLit = Abc_LitNotCond( Gia_ObjCopyArray(pTemp, Id), Abc_LitIsCompl(iLit) ); + } + // write packing + if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 ) + { + Vec_IntPush( vPacking, 1 ); + Vec_IntPush( vPacking, Abc_Lit2Var(iLit) ); + Vec_IntAddToEntry( vPacking, 0, 1 ); + } + return iLit; } /**Function************************************************************* @@ -1443,15 +1485,15 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * ***********************************************************************/ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) { - Gia_Man_t * pNew; + Gia_Man_t * pNew, * pHashed = NULL; If_Cut_t * pCutBest; If_Obj_t * pIfObj, * pIfLeaf; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; Vec_Int_t * vPiVars = NULL, * vPoVars = NULL; sat_solver * pSat = NULL; - void * pNtkCell = NULL; - int i, k, Entry; + Ifn_Ntk_t * pNtkCell = NULL; + int i, k, nLutMax, Entry; assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth ); // if ( pIfMan->pPars->fEnableCheck07 ) // pIfMan->pPars->fDeriveLuts = 0; @@ -1499,8 +1541,16 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts ) { if ( pSat == NULL ) - pSat = (sat_solver *)If_ManSatBuildFromCell( NULL, &vPiVars, &vPoVars, (void **)&pNtkCell ); - pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking ); + { + pSat = (sat_solver *)If_ManSatBuildFromCell( If_DsdManGetCellStr(pIfMan->pIfDsdMan), &vPiVars, &vPoVars, &pNtkCell ); + nLutMax = Ifn_NtkLutSizeMax( pNtkCell ); + pHashed = Gia_ManStart( 10000 ); + Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 ); + for ( k = 0; k < pIfMan->pPars->nLutSize; k++ ) + Gia_ManAppendCi( pHashed ); + Gia_ManHashAlloc( pHashed ); + } + pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pHashed, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, nLutMax, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); } else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm ) @@ -1549,8 +1599,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Vec_IntFreeP( &vPoVars ); if ( pNtkCell ) ABC_FREE( pNtkCell ); - if ( pSat != NULL ) + if ( pSat ) sat_solver_delete(pSat); + if ( pHashed ) + Gia_ManStop( pHashed ); // printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n", // If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) ); // finish mapping |