luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Separated truth table computation for GIA manager and added new procedures.

This commit is contained in:
Alan Mishchenko 2012-10-02 15:20:11 -07:00
parent b612db977c
commit b71d4425d0
3 changed files with 89 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -884,6 +884,7 @@ extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int De
extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
/*=== giaTruth.c ===========================================================*/
extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax );

56
src/aig/gia/giaTruth.c
View File

@ -38,6 +38,62 @@ static inline word * Gla_ObjTruthDup( Gia_Man_t * p, word * pDst, word * pSrc, i
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes truth table up to 6 inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ObjComputeTruthTable6_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Wrd_t * vTruths )
{
word uTruth0, uTruth1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( !pObj->fMark0 );
assert( Gia_ObjIsAnd(pObj) );
Gia_ObjComputeTruthTable6_rec( p, Gia_ObjFanin0(pObj), vTruths );
Gia_ObjComputeTruthTable6_rec( p, Gia_ObjFanin1(pObj), vTruths );
uTruth0 = Vec_WrdEntry( vTruths, Gia_ObjFanin0(pObj)->Value );
uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
uTruth1 = Vec_WrdEntry( vTruths, Gia_ObjFanin1(pObj)->Value );
uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
pObj->Value = Vec_WrdSize(vTruths);
Vec_WrdPush( vTruths, uTruth0 & uTruth1 );
}
word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths )
{
static word s_Truth6[6] = {
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
Gia_Obj_t * pLeaf;
int i;
assert( Vec_IntSize(vSupp) <= 6 );
assert( Gia_ObjIsAnd(pObj) );
assert( !pObj->fMark0 );
Vec_WrdClear( vTruths );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vSupp, p, pLeaf, i )
{
assert( pLeaf->fMark0 || Gia_ObjIsRo(p, pLeaf) );
pLeaf->Value = Vec_WrdSize(vTruths);
Vec_WrdPush( vTruths, s_Truth6[i] );
Gia_ObjSetTravIdCurrent(p, pLeaf);
}
Gia_ObjComputeTruthTable6_rec( p, pObj, vTruths );
return Vec_WrdEntryLast( vTruths );
}
/**Function*************************************************************
Synopsis [Collects internal nodes reachable from the given node.]

102
src/proof/abs/absRpm.c
View File

@ -52,7 +52,7 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
{
Vec_Int_t * vNodes;
Gia_Obj_t * pObj;
int Level, LevelMax = 2;
int Lev, LevMax = 2;
int i, iDom, iDomNext;
vNodes = Vec_IntAlloc( 100 );
Gia_ManForEachObj( p, pObj, i )
@ -60,9 +60,9 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
if ( !pObj->fMark0 )
continue;
iDom = Gia_ObjDom(p, pObj);
if ( iDom == Gia_ObjId(p, pObj) )
if ( iDom == i )
continue;
for ( Level = 0; Level < LevelMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Level++ )
for ( Lev = 0; Lev < LevMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Lev++ )
{
Vec_IntPush( vNodes, iDom );
iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom) );
@ -189,25 +189,44 @@ void Gia_ManTestDoms2( Gia_Man_t * p )
Gia_ManCleanMark0( p );
}
/**Function*************************************************************
Synopsis [Collect PI doms.]
Description [Assumes that some PIs and ANDs are marked with fMark0.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManComputePiDoms( Gia_Man_t * p )
{
Vec_Int_t * vNodes;
Gia_ManComputeDoms( p );
vNodes = Gia_ManCollectDoms( p );
// Vec_IntPrint( vNodes );
printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) );
return vNodes;
}
void Gia_ManTestDoms( Gia_Man_t * p )
{
Vec_Int_t * vNodes;
Gia_Obj_t * pObj;
int i;
assert( p->vDoms == NULL );
Gia_ManComputeDoms( p );
// for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
// mark PIs
Gia_ManCleanMark0( p );
Gia_ManForEachPi( p, pObj, i )
pObj->fMark0 = 1;
vNodes = Gia_ManCollectDoms( p );
// Vec_IntPrint( vNodes );
printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) );
// compute dominators
vNodes = Gia_ManComputePiDoms( p );
Vec_IntFree( vNodes );
// unmark PIs
Gia_ManCleanMark0( p );
}
/**Function*************************************************************
Synopsis []
@ -444,62 +463,6 @@ int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 )
return (int)( i == nStr );
}
/**Function*************************************************************
Synopsis [Computes truth table up to 6 inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abs_GiaComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Wrd_t * vTruths )
{
word uTruth0, uTruth1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( !pObj->fMark0 );
assert( Gia_ObjIsAnd(pObj) );
Abs_GiaComputeTruth_rec( p, Gia_ObjFanin0(pObj), vTruths );
Abs_GiaComputeTruth_rec( p, Gia_ObjFanin1(pObj), vTruths );
uTruth0 = Vec_WrdEntry( vTruths, Gia_ObjFanin0(pObj)->Value );
uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
uTruth1 = Vec_WrdEntry( vTruths, Gia_ObjFanin1(pObj)->Value );
uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
pObj->Value = Vec_WrdSize(vTruths);
Vec_WrdPush( vTruths, uTruth0 & uTruth1 );
}
word Abs_GiaComputeTruth( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths )
{
static word s_Truth6[6] = {
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
Gia_Obj_t * pLeaf;
int i;
assert( Vec_IntSize(vSupp) <= 6 );
assert( Gia_ObjIsAnd(pObj) );
assert( !pObj->fMark0 );
Vec_WrdClear( vTruths );
Gia_ManIncrementTravId( p );
Gia_ManForEachObjVec( vSupp, p, pLeaf, i )
{
assert( pLeaf->fMark0 || Gia_ObjIsRo(p, pLeaf) );
pLeaf->Value = Vec_WrdSize(vTruths);
Vec_WrdPush( vTruths, s_Truth6[i] );
Gia_ObjSetTravIdCurrent(p, pLeaf);
}
Abs_GiaComputeTruth_rec( p, pObj, vTruths );
return Vec_WrdEntryLast( vTruths );
}
/**Function*************************************************************
Synopsis [Returns 1 if truth table has const cofactors.]
@ -575,7 +538,7 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose )
}
// compute truth table
uTruth = Abs_GiaComputeTruth( p, pObj, vSupp, vTruths );
uTruth = Gia_ObjComputeTruthTable6( p, pObj, vSupp, vTruths );
// check if truth table has const cofs
if ( !Abs_GiaCheckTruth( &uTruth, Vec_IntSize(vSupp), nSize0 ) ) // has const
@ -658,10 +621,9 @@ Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p )
Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose )
{
Gia_Man_t * pNew;
Gia_ManTestDoms( p );
return NULL;
Gia_ObjComputeTruthTableStart( p, nCutMax );
// Gia_ManTestDoms( p );
// return NULL;
Abs_RpmPerformMark( p, nCutMax, 1 );
pNew = Gia_ManDupRpm( p );
Gia_ManCleanMark0( p );