Skip to content

A
abc
Commit 6c9b59bf by Alan Mishchenko
Options

Updated code for lazy man's synthesis.

parent f09afdf2
Showing with 155 additions and 90 deletions
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;
......
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 );
......
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*************************************************************
......
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);
}
......
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*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment