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

Creating dedicated choice representation for GIA.

This commit is contained in:
Alan Mishchenko 2012-10-24 12:22:46 -07:00
parent bc21cb41b4
commit 5cd1396b3d
7 changed files with 128 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -117,6 +117,7 @@ struct Gia_Man_t_
int * pReprsOld; // representatives (for CIs and ANDs)
Gia_Rpr_t * pReprs; // representatives (for CIs and ANDs)
int * pNexts; // next nodes in the equivalence classes
int * pSibls; // next nodes in the choice nodes
int * pIso; // pairs of structurally isomorphic nodes
int nTerLoop; // the state where loop begins
int nTerStates; // the total number of ternary states
@ -570,6 +571,8 @@ static inline void Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ a
static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; }
static inline int Gia_ObjHasRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr != GIA_VOID; }
static inline int Gia_ObjReprSelf( Gia_Man_t * p, int Id ) { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id; }
static inline int Gia_ObjSibl( Gia_Man_t * p, int Id ) { return p->pSibls ? p->pSibls[Id] : 0; }
static inline Gia_Obj_t * Gia_ObjSiblObj( Gia_Man_t * p, int Id ) { return (p->pSibls && p->pSibls[Id]) ? Gia_ManObj(p, p->pSibls[Id]) : NULL; }
static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
@ -920,6 +923,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;

89
src/aig/gia/giaAig.c
View File

@ -42,7 +42,7 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
/**Function*************************************************************
Synopsis [Derives combinational miter of the two AIGs.]
Synopsis [Duplicates AIG in the DFS order.]
Description []
@ -70,18 +70,6 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
pNew->pNexts[iObjNew] = iNextNew;
}
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
{
Gia_Man_t * pNew;
@ -111,6 +99,64 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj == NULL || pObj->iData )
return;
assert( Aig_ObjIsNode(pObj) );
Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
if ( Aig_ObjEquiv(p, pObj) )
{
int iObjNew, iNextNew;
iObjNew = Abc_Lit2Var(pObj->iData);
iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
assert( iObjNew > iNextNew );
assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
pNew->pSibls[iObjNew] = iNextNew;
}
}
Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
{
Gia_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
assert( p->pEquivs != NULL );
// create the new manager
pNew = Gia_ManStart( Aig_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// create room to store equivalences
pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->iData = 1;
Aig_ManForEachCi( p, pObj, i )
pObj->iData = Gia_ManAppendCi( pNew );
// add logic for the POs
Aig_ManForEachCo( p, pObj, i )
Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
@ -195,7 +241,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Derives combinational miter of the two AIGs.]
Synopsis [Duplicates AIG in the DFS order.]
Description []
@ -228,18 +274,6 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);
}
}
/**Function*************************************************************
Synopsis [Duplicates AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
{
Aig_Man_t * pNew;
@ -541,7 +575,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
Aig_Man_t * pNew;
pNew = Gia_ManToAig( p, 0 );
pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
pGia = Gia_ManFromAig( pNew );
// pGia = Gia_ManFromAig( pNew );
pGia = Gia_ManFromAigChoices( pNew );
Aig_ManStop( pNew );
return pGia;
}

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

@ -51,6 +51,7 @@ ABC_NAMESPACE_HEADER_START
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );

32
src/aig/gia/giaMan.c
View File

@ -107,6 +107,7 @@ void Gia_ManStop( Gia_Man_t * p )
ABC_FREE( p->pReprsOld );
ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts );
ABC_FREE( p->pSibls );
ABC_FREE( p->pRefs );
// ABC_FREE( p->pNodeRefs );
ABC_FREE( p->pHTable );
@ -249,6 +250,35 @@ void Gia_ManPrintTents( Gia_Man_t * p )
// Gia_ObjPrint( p, pObj );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintChoiceStats( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, nEquivs = 0, nChoices = 0;
Gia_ManMarkFanoutDrivers( p );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjSibl(p, i) )
continue;
nEquivs++;
if ( pObj->fMark0 )
nChoices++;
assert( !Gia_ObjSiblObj(p, i)->fMark0 );
assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
}
Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
}
/**Function*************************************************************
Synopsis [Prints stats for the AIG.]
@ -289,6 +319,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
// Gia_ManSatExperiment( p );
if ( p->pReprs && p->pNexts )
Gia_ManEquivPrintClasses( p, 0, 0.0 );
if ( p->pSibls )
Gia_ManPrintChoiceStats( p );
if ( p->pMapping )
Gia_ManPrintMappingStats( p );
if ( p->pPlacement )

25
src/aig/gia/giaUtil.c
View File

@ -1243,6 +1243,31 @@ int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
return 1;
}
/**Function*************************************************************
Synopsis [Marks nodes that appear as faninis of other nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
Gia_ManCleanMark0( p );
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark0 = 1;
}
else if ( Gia_ObjIsCo(pObj) )
Gia_ObjFanin0(pObj)->fMark0 = 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/proof/dch/dchChoice.c
View File

@ -95,7 +95,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
pEquiv = Aig_ObjEquiv( pAig, pObj );
if ( pEquiv == NULL )
continue;
assert( pEquiv->Id > pObj->Id );
assert( pEquiv->Id < pObj->Id );
nEquivs++;
}
return nEquivs;

4
src/proof/dch/dchCore.c
View File

@ -111,7 +111,9 @@ p->timeTotal = clock() - clkTotal;
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
// count the number of representatives
if ( pPars->fVerbose )
Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
Abc_Print( 1, "STATS: Ands:%8d ->%8d. Reprs:%7d ->%7d. Choices =%7d.\n",
Aig_ManNodeNum(pAig),
Aig_ManNodeNum(pResult),
Dch_DeriveChoiceCountReprs( pAig ),
Dch_DeriveChoiceCountEquivs( pResult ),
Aig_ManChoiceNum( pResult ) );