summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h14
-rw-r--r--src/aig/gia/giaEnable.c5
-rw-r--r--src/aig/gia/giaEquiv.c4
-rw-r--r--src/aig/gia/giaIf.c68
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 21:57:45 +0000