summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h14
-rw-r--r--src/aig/gia/giaMan.c4
-rw-r--r--src/aig/gia/giaUtil.c169
-rw-r--r--src/base/abci/abcRec2.c54
-rw-r--r--src/misc/vec/vecStr.h4
5 files changed, 155 insertions, 90 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 7efad774..a74da4cb 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -154,11 +154,13 @@ struct Gia_Man_t_
word nHashHit; // hash table hit
word nHashMiss; // hash table miss
int fVerbose; // verbose reports
- Vec_Int_t * vObjNums; // object numbers
- Vec_Wrd_t * vTtMemory; // truth table memory
+ // truth table computation for small functions
int nTtVars; // truth table variables
int nTtWords; // truth table words
- int iTtNum; // truth table current number
+ Vec_Str_t * vTtNums; // object numbers
+ Vec_Int_t * vTtNodes; // internal nodes
+ Vec_Ptr_t * vTtInputs; // truth tables for constant and primary inputs
+ Vec_Wrd_t * vTtMemory; // truth tables for internal nodes
};
@@ -384,6 +386,9 @@ static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int
static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); }
static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
+static inline int Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (int)(unsigned char)Vec_StrGetEntry(p->vTtNums, Gia_ObjId(p,pObj)); }
+static inline void Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 && n < 254 ); Vec_StrSetEntry(p->vTtNums, Gia_ObjId(p,pObj), (char)n); }
+
static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; }
static inline int Gia_ObjRefsId( Gia_Man_t * p, int Id ) { assert( p->pRefs); return p->pRefs[Id]; }
static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; }
@@ -711,7 +716,6 @@ extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta
extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
-extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
/*=== giaAbsGla.c ===========================================================*/
extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
/*=== giaAbsVta.c ===========================================================*/
@@ -951,6 +955,8 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
+extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 037edc78..31f03d80 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -86,8 +86,10 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vObjClasses );
Vec_IntFreeP( &p->vLevels );
Vec_IntFreeP( &p->vTruths );
+ Vec_StrFreeP( &p->vTtNums );
+ Vec_IntFreeP( &p->vTtNodes );
Vec_WrdFreeP( &p->vTtMemory );
- Vec_IntFreeP( &p->vObjNums );
+ Vec_PtrFreeP( &p->vTtInputs );
Vec_IntFree( p->vCis );
Vec_IntFree( p->vCos );
ABC_FREE( p->pTravIds );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index c0e5b9ab..c212fe64 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1347,78 +1347,76 @@ unsigned * Gia_ManComputePoTruthTables( Gia_Man_t * p, int nBytesMax )
/**Function*************************************************************
- Synopsis [Computing the truth table of one PO.]
+ Synopsis [Collects internal nodes reachable from the given node.]
- Description [The truth table should be used (or saved into the user's
- storage) before this procedure is called next time!]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-int Gia_ObjComputeTruthTable_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
-{
- word * pTruth0, * pTruth1, * pTruth, * pTruthL;
- int Value0, Value1;
- if ( Gia_ObjIsTravIdCurrent(p, pObj) )
- return Vec_IntGetEntry(p->vObjNums, Gia_ObjId(p, pObj));
- Gia_ObjSetTravIdCurrent(p, pObj);
- assert( Gia_ObjIsAnd(pObj) );
- Value0 = Gia_ObjComputeTruthTable_rec( p, Gia_ObjFanin0(pObj) );
- Value1 = Gia_ObjComputeTruthTable_rec( p, Gia_ObjFanin1(pObj) );
- assert( Value0 < Vec_WrdSize(p->vTtMemory) );
- assert( Value1 < Vec_WrdSize(p->vTtMemory) );
- pTruth0 = Vec_WrdArray(p->vTtMemory) + p->nTtWords * Value0;
- pTruth1 = Vec_WrdArray(p->vTtMemory) + p->nTtWords * Value1;
- assert( p->nTtWords * p->iTtNum < Vec_WrdSize(p->vTtMemory) );
- pTruth = Vec_WrdArray(p->vTtMemory) + p->nTtWords * p->iTtNum++;
- pTruthL = Vec_WrdArray(p->vTtMemory) + p->nTtWords * p->iTtNum;
- if ( Gia_ObjFaninC0(pObj) )
- {
- if ( Gia_ObjFaninC1(pObj) )
- while ( pTruth < pTruthL )
- *pTruth++ = ~*pTruth0++ & ~*pTruth1++;
- else
- while ( pTruth < pTruthL )
- *pTruth++ = ~*pTruth0++ & *pTruth1++;
- }
- else
- {
- if ( Gia_ObjFaninC1(pObj) )
- while ( pTruth < pTruthL )
- *pTruth++ = *pTruth0++ & ~*pTruth1++;
- else
- while ( pTruth < pTruthL )
- *pTruth++ = *pTruth0++ & *pTruth1++;
- }
- Vec_IntSetEntry(p->vObjNums, Gia_ObjId(p, pObj), p->iTtNum-1);
- return p->iTtNum-1;
+void Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ if ( pObj->fMark0 )
+ return;
+ pObj->fMark0 = 1;
+ Gia_ObjCollectInternal_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ObjCollectInternal_rec( p, Gia_ObjFanin1(pObj) );
+ Gia_ObjSetNum( p, pObj, Vec_IntSize(p->vTtNodes) );
+ Vec_IntPush( p->vTtNodes, Gia_ObjId(p, pObj) );
+}
+void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ Vec_IntClear( p->vTtNodes );
+ Gia_ObjCollectInternal_rec( p, pObj );
}
+
+/**Function*************************************************************
+
+ Synopsis [Truth table manipulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word * Gla_ObjTruthElem( Gia_Man_t * p, int i ) { return (word *)Vec_PtrEntry( p->vTtInputs, i ); }
+static inline word * Gla_ObjTruthNode( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjNum(p, pObj); }
+static inline word * Gla_ObjTruthFree1( Gia_Man_t * p ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * 254; }
+static inline word * Gla_ObjTruthFree2( Gia_Man_t * p ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * 255; }
+static inline word * Gla_ObjTruthConst0( Gia_Man_t * p, word * pDst ) { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = 0; return pDst; }
+static inline word * Gla_ObjTruthDup( Gia_Man_t * p, word * pDst, word * pSrc, int c ) { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = c ? ~pSrc[w] : pSrc[w]; return pDst; }
+
+/**Function*************************************************************
+
+ Synopsis [Computing the truth table for GIA object.]
+
+ Description [The truth table should be used by the calling application
+ (or saved into the user's storage) before this procedure is called again.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
{
- Gia_Obj_t * pTemp;
- word * pTruth;
- int i, k;
+ Gia_Obj_t * pTemp, * pRoot;
+ word * pTruth, * pTruthL, * pTruth0, * pTruth1;
+ int i;
if ( p->vTtMemory == NULL )
{
- word Truth6[7] = {
- 0x0000000000000000,
- 0xAAAAAAAAAAAAAAAA,
- 0xCCCCCCCCCCCCCCCC,
- 0xF0F0F0F0F0F0F0F0,
- 0xFF00FF00FF00FF00,
- 0xFFFF0000FFFF0000,
- 0xFFFFFFFF00000000
- };
p->nTtVars = Gia_ManPiNum( p );
p->nTtWords = (p->nTtVars <= 6 ? 1 : (1 << (p->nTtVars - 6)));
+ p->vTtNums = Vec_StrAlloc( Gia_ManObjNum(p) + 1000 );
+ p->vTtNodes = Vec_IntAlloc( 256 );
+ p->vTtInputs = Vec_PtrAllocTruthTables( p->nTtVars );
p->vTtMemory = Vec_WrdStart( p->nTtWords * 256 );
- for ( i = 0; i < 7; i++ )
- for ( k = 0; k < p->nTtWords; k++ )
- Vec_WrdWriteEntry( p->vTtMemory, i * p->nTtWords + k, Truth6[i] );
- assert( p->vObjNums == NULL );
- p->vObjNums = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
}
else
{
@@ -1426,33 +1424,44 @@ unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
// since the truth table computation storage was prepared
assert( p->nTtVars == Gia_ManPiNum(p) );
}
- // mark const and PIs
- Gia_ManIncrementTravId( p );
- Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
- Vec_IntSetEntry(p->vObjNums,0, 0);
- Gia_ManForEachPi( p, pTemp, i )
- {
- Gia_ObjSetTravIdCurrent( p, pTemp );
- Vec_IntSetEntry(p->vObjNums, Gia_ObjId(p, pTemp), i+1);
- }
- p->iTtNum = 7;
- // compute truth table for the fanin node
- if ( Gia_ObjIsCo(pObj) )
+ // collect internal nodes
+ pRoot = Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj;
+ Gia_ObjCollectInternal( p, pRoot );
+ // compute the truth table for internal nodes
+ Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
{
- pTruth = Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjComputeTruthTable_rec(p, Gia_ObjFanin0(pObj));
- // complement if needed
- if ( Gia_ObjFaninC0(pObj) )
+ pTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
+ pTruth = Gla_ObjTruthNode(p, pTemp);
+ pTruthL = pTruth + p->nTtWords;
+ pTruth0 = Gia_ObjIsAnd(Gia_ObjFanin0(pTemp)) ? Gla_ObjTruthNode(p, Gia_ObjFanin0(pTemp)) : Gla_ObjTruthElem(p, Gia_ObjCioId(Gia_ObjFanin0(pTemp)) );
+ pTruth1 = Gia_ObjIsAnd(Gia_ObjFanin1(pTemp)) ? Gla_ObjTruthNode(p, Gia_ObjFanin1(pTemp)) : Gla_ObjTruthElem(p, Gia_ObjCioId(Gia_ObjFanin1(pTemp)) );
+ if ( Gia_ObjFaninC0(pTemp) )
{
- word * pTemp = pTruth;
- assert( p->nTtWords * p->iTtNum < Vec_WrdSize(p->vTtMemory) );
- pTruth = Vec_WrdArray(p->vTtMemory) + p->nTtWords * p->iTtNum;
- for ( k = 0; k < p->nTtWords; k++ )
- pTruth[k] = ~pTemp[k];
+ if ( Gia_ObjFaninC1(pTemp) )
+ while ( pTruth < pTruthL )
+ *pTruth++ = ~*pTruth0++ & ~*pTruth1++;
+ else
+ while ( pTruth < pTruthL )
+ *pTruth++ = ~*pTruth0++ & *pTruth1++;
+ }
+ else
+ {
+ if ( Gia_ObjFaninC1(pTemp) )
+ while ( pTruth < pTruthL )
+ *pTruth++ = *pTruth0++ & ~*pTruth1++;
+ else
+ while ( pTruth < pTruthL )
+ *pTruth++ = *pTruth0++ & *pTruth1++;
}
}
- else
- pTruth = Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjComputeTruthTable_rec(p, pObj);
- return (unsigned *)pTruth;
+ // compute the final table
+ if ( Gia_ObjIsConst0(pRoot) )
+ pTruth = Gla_ObjTruthConst0( p, Gla_ObjTruthFree1(p) );
+ else if ( Gia_ObjIsPi(p, pRoot) )
+ pTruth = Gla_ObjTruthElem( p, Gia_ObjCioId(pRoot) );
+ else if ( Gia_ObjIsAnd(pRoot) )
+ pTruth = Gla_ObjTruthNode( p, pRoot );
+ return (unsigned *)Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) );
}
/**Function*************************************************************
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index e0a33f0d..ed7beea5 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -1122,7 +1122,7 @@ p->timeInsert += clock() - timeInsert;
p->pTemp2 = ABC_ALLOC( unsigned, p->nWords );
p->vNodes = Vec_PtrAlloc( 100 );
p->vTtTemps = Vec_PtrAllocSimInfo( 1024, p->nWords );
- p->vLabels = Vec_PtrStart( 1000);
+ p->vLabels = Vec_PtrStart( 1000 );
p->timeTotal += clock() - clkTotal;
@@ -1930,8 +1930,8 @@ Hop_Obj_t * Abc_NtkRecBuildUp_rec2(Hop_Man_t* pMan, Gia_Obj_t* pObj, Vec_Ptr_t *
Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj )
{
Rec_Obj_t2 * pCandMin;
- Hop_Obj_t* pHopObj;
- Gia_Obj_t* pGiaObj;
+ Hop_Obj_t* pHopObj, * pFan0, * pFan1;
+ Gia_Obj_t* pGiaObj, *pGiaTemp;
Gia_Man_t * pAig = s_pMan->pGia;
int nLeaves, i;// DelayMin = ABC_INFINITY , Delay = -ABC_INFINITY
unsigned uCanonPhase;
@@ -1963,6 +1963,8 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
If_CutTruthStretch(pInOut, nLeaves, nVars);
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);
+
+/*
Vec_PtrGrow(s_pMan->vLabels, Gia_ManObjNum(pAig));
s_pMan->vLabels->nSize = s_pMan->vLabels->nCap;
for (i = 0; i < nLeaves; i++)
@@ -1976,8 +1978,54 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
Gia_ManIncrementTravId(pAig);
//derive the best structure in the library.
pHopObj = Abc_NtkRecBuildUp_rec2(pMan, Abc_NtkRecGetObj(Rec_ObjID(s_pMan, pCandMin)), s_pMan->vLabels);
+*/
+
+ // get the top-most GIA node
+ pGiaObj = Abc_NtkRecGetObj( Rec_ObjID(s_pMan, pCandMin) );
+ assert( Gia_ObjIsAnd(pGiaObj) || Gia_ObjIsPi(pAig, pGiaObj) );
+ // collect internal nodes into pAig->vTtNodes
+ if ( pAig->vTtNodes == NULL )
+ pAig->vTtNodes = Vec_IntAlloc( 256 );
+ Gia_ObjCollectInternal( pAig, pGiaObj );
+ // collect HOP nodes for leaves
+ Vec_PtrClear( s_pMan->vLabels );
+ for (i = 0; i < nLeaves; i++)
+ {
+ pHopObj = Hop_IthVar(pMan, pCanonPerm[i]);
+ pHopObj = Hop_NotCond(pHopObj, ((uCanonPhase & (1 << i)) > 0));
+ Vec_PtrPush(s_pMan->vLabels, pHopObj);
+ }
+ // compute HOP nodes for internal nodes
+ Gia_ManForEachObjVec( pAig->vTtNodes, pAig, pGiaTemp, i )
+ {
+ pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
+
+ if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
+ pFan0 = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjNum(pAig, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
+ else
+ pFan0 = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
+ pFan0 = Hop_NotCond(pFan0, Gia_ObjFaninC0(pGiaTemp));
+
+ if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
+ pFan1 = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjNum(pAig, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
+ else
+ pFan1 = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
+ pFan1 = Hop_NotCond(pFan1, Gia_ObjFaninC1(pGiaTemp));
+
+ pHopObj = Hop_And(pMan, pFan0, pFan1);
+ Vec_PtrPush(s_pMan->vLabels, pHopObj);
+ }
+ // get the final result
+ if ( Gia_ObjIsAnd(pGiaObj) )
+ pHopObj = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjNum(pAig, pGiaObj) + nLeaves);
+ else if ( Gia_ObjIsPi(pAig, pGiaObj) )
+ pHopObj = (Hop_Obj_t *)Vec_PtrEntry(s_pMan->vLabels, Gia_ObjCioId(pGiaObj));
+ else assert( 0 );
+
+
s_pMan->timeIfDerive += clock() - time;
s_pMan->timeIfTotal += clock() - time;
+ // complement the result if needed
return Hop_NotCond(pHopObj, (pCut->fCompl)^(((uCanonPhase & (1 << nLeaves)) > 0)) ^ fCompl);
}
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index cefa0ea9..cc57b2de 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -360,8 +360,8 @@ static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
{
if ( p->nCap >= nCapMin )
return;
- p->pArray = ABC_REALLOC( char, p->pArray, 2 * nCapMin );
- p->nCap = 2 * nCapMin;
+ p->pArray = ABC_REALLOC( char, p->pArray, nCapMin );
+ p->nCap = nCapMin;
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 13:48:12 +0000