mirror of https://github.com/YosysHQ/abc.git
Merge
This commit is contained in:
commit
e353c4b75c
12
abclib.dsp
12
abclib.dsp
|
|
@ -391,6 +391,10 @@ SOURCE=.\src\base\abci\abcRec2.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abci\abcRec3.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abci\abcReconv.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
@ -1979,6 +1983,10 @@ SOURCE=.\src\opt\dau\dauDsd.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\dau\dauEnum.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\dau\dauInt.h
|
||||
# End Source File
|
||||
# End Group
|
||||
|
|
@ -2705,6 +2713,10 @@ SOURCE=.\src\misc\util\utilSignal.h
|
|||
|
||||
SOURCE=.\src\misc\util\utilSort.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\misc\util\utilTruth.h
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "nm"
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -481,6 +482,13 @@ static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 )
|
|||
{
|
||||
return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 );
|
||||
}
|
||||
static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 )
|
||||
{
|
||||
Gia_Obj_t * pObjCo = Gia_ManCo( p, iCoIndex );
|
||||
assert( Gia_ObjId(p, pObjCo) > Abc_Lit2Var(iLit0) );
|
||||
pObjCo->iDiff0 = Gia_ObjId(p, pObjCo) - Abc_Lit2Var(iLit0);
|
||||
pObjCo->fCompl0 = Abc_LitIsCompl(iLit0);
|
||||
}
|
||||
|
||||
#define GIA_ZER 1
|
||||
#define GIA_ONE 2
|
||||
|
|
@ -570,6 +578,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; }
|
||||
|
|
@ -697,6 +707,7 @@ extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i
|
|||
extern void Gia_ManVerifyChoices( Gia_Man_t * p );
|
||||
extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
|
||||
extern int Gia_ManHasChoices( Gia_Man_t * p );
|
||||
extern int Gia_ManChoiceLevel( Gia_Man_t * p );
|
||||
/*=== giaCsatOld.c ============================================================*/
|
||||
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
|
||||
/*=== giaCsat.c ============================================================*/
|
||||
|
|
@ -807,7 +818,14 @@ extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
|
|||
extern void Gia_ManHashProfile( Gia_Man_t * p );
|
||||
extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
|
||||
/*=== giaIf.c ===========================================================*/
|
||||
extern void Gia_ManPrintNpnClasses( Gia_Man_t * p );
|
||||
extern void Gia_ManPrintMappingStats( Gia_Man_t * p );
|
||||
extern int Gia_ManLutFaninCount( Gia_Man_t * p );
|
||||
extern int Gia_ManLutSizeMax( Gia_Man_t * p );
|
||||
extern int Gia_ManLutNum( Gia_Man_t * p );
|
||||
extern int Gia_ManLutLevel( Gia_Man_t * p );
|
||||
extern void Gia_ManSetRefsMapped( Gia_Man_t * p );
|
||||
extern void Gia_ManSetIfParsDefault( void * pIfPars );
|
||||
extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
|
||||
/*=== giaIso.c ===========================================================*/
|
||||
extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
|
||||
extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fDualOut, int fVerbose );
|
||||
|
|
@ -823,12 +841,7 @@ extern void Gia_ManPrintStatsShort( Gia_Man_t * p );
|
|||
extern void Gia_ManPrintMiterStatus( Gia_Man_t * p );
|
||||
extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
|
||||
extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
|
||||
/*=== giaMap.c ===========================================================*/
|
||||
extern void Gia_ManPrintMappingStats( Gia_Man_t * p );
|
||||
extern int Gia_ManLutFaninCount( Gia_Man_t * p );
|
||||
extern int Gia_ManLutSizeMax( Gia_Man_t * p );
|
||||
extern int Gia_ManLutNum( Gia_Man_t * p );
|
||||
extern int Gia_ManLutLevel( Gia_Man_t * p );
|
||||
extern void Gia_ManPrintNpnClasses( Gia_Man_t * p );
|
||||
/*=== giaMem.c ===========================================================*/
|
||||
extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
|
||||
extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
|
||||
|
|
@ -857,6 +870,7 @@ extern int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int
|
|||
extern int Gia_ManSeqMarkUsed( Gia_Man_t * p );
|
||||
extern int Gia_ManCombMarkUsed( Gia_Man_t * p );
|
||||
extern Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p );
|
||||
extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs );
|
||||
extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p );
|
||||
extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
|
||||
/*=== giaShrink.c ===========================================================*/
|
||||
|
|
@ -906,7 +920,7 @@ extern int Gia_ManLevelNum( Gia_Man_t * p );
|
|||
extern void Gia_ManCreateValueRefs( Gia_Man_t * p );
|
||||
extern void Gia_ManCreateRefs( Gia_Man_t * p );
|
||||
extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p );
|
||||
extern int Gia_ManCrossCut( Gia_Man_t * p );
|
||||
extern int Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
|
||||
extern int Gia_ManIsNormalized( Gia_Man_t * p );
|
||||
extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
|
||||
extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode );
|
||||
|
|
@ -920,6 +934,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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@
|
|||
|
||||
#include "gia.h"
|
||||
#include "giaAig.h"
|
||||
#include "misc/tim/tim.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -261,6 +262,108 @@ int Gia_ManHasChoices( Gia_Man_t * p )
|
|||
return 1;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes levels for AIG with choices and white boxes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
|
||||
Gia_Obj_t * pNext;
|
||||
int i, iBox, iTerm1, nTerms, LevelMax = 0;
|
||||
if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
|
||||
return;
|
||||
Gia_ObjSetTravIdCurrent( p, pObj );
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
if ( pManTime )
|
||||
{
|
||||
iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
|
||||
if ( iBox >= 0 ) // this is not a true PI
|
||||
{
|
||||
iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
|
||||
nTerms = Tim_ManBoxInputNum( pManTime, iBox );
|
||||
for ( i = 0; i < nTerms; i++ )
|
||||
{
|
||||
pNext = Gia_ManCo( p, iTerm1 + i );
|
||||
Gia_ManChoiceLevel_rec( p, pNext );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pNext) )
|
||||
LevelMax = Gia_ObjLevel(p, pNext);
|
||||
}
|
||||
LevelMax++;
|
||||
}
|
||||
}
|
||||
// Abc_Print( 1, "%d ", pObj->Level );
|
||||
}
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
pNext = Gia_ObjFanin0(pObj);
|
||||
Gia_ManChoiceLevel_rec( p, pNext );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pNext) )
|
||||
LevelMax = Gia_ObjLevel(p, pNext);
|
||||
}
|
||||
else if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
// get the maximum level of the two fanins
|
||||
pNext = Gia_ObjFanin0(pObj);
|
||||
Gia_ManChoiceLevel_rec( p, pNext );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pNext) )
|
||||
LevelMax = Gia_ObjLevel(p, pNext);
|
||||
pNext = Gia_ObjFanin1(pObj);
|
||||
Gia_ManChoiceLevel_rec( p, pNext );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pNext) )
|
||||
LevelMax = Gia_ObjLevel(p, pNext);
|
||||
LevelMax++;
|
||||
|
||||
// get the level of the nodes in the choice node
|
||||
if ( p->pSibls && (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
|
||||
{
|
||||
Gia_ManChoiceLevel_rec( p, pNext );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pNext) )
|
||||
LevelMax = Gia_ObjLevel(p, pNext);
|
||||
}
|
||||
}
|
||||
else if ( !Gia_ObjIsConst0(pObj) )
|
||||
assert( 0 );
|
||||
Gia_ObjSetLevel( p, pObj, LevelMax );
|
||||
}
|
||||
int Gia_ManChoiceLevel( Gia_Man_t * p )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, LevelMax = 0;
|
||||
// assert( Gia_ManRegNum(p) == 0 );
|
||||
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
|
||||
Gia_ManIncrementTravId( p );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
Gia_ManChoiceLevel_rec( p, pObj );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pObj) )
|
||||
LevelMax = Gia_ObjLevel(p, pObj);
|
||||
}
|
||||
// account for dangling boxes
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
{
|
||||
Gia_ManChoiceLevel_rec( p, pObj );
|
||||
if ( LevelMax < Gia_ObjLevel(p, pObj) )
|
||||
LevelMax = Gia_ObjLevel(p, pObj);
|
||||
// Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
|
||||
}
|
||||
// Abc_Print( 1, "\n" );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
assert( Gia_ObjLevel(p, pObj) > 0 );
|
||||
// printf( "Max level %d\n", LevelMax );
|
||||
return LevelMax;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -92,6 +92,47 @@ void Gia_ManFrontTransform( Gia_Man_t * p )
|
|||
ABC_FREE( pFrontToId );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Determine the frontier.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManCrossCutSimple( Gia_Man_t * p )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, nCutCur = 0, nCutMax = 0;
|
||||
Gia_ManCreateValueRefs( p );
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
{
|
||||
if ( pObj->Value )
|
||||
nCutCur++;
|
||||
if ( nCutMax < nCutCur )
|
||||
nCutMax = nCutCur;
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
if ( --Gia_ObjFanin0(pObj)->Value == 0 )
|
||||
nCutCur--;
|
||||
if ( --Gia_ObjFanin1(pObj)->Value == 0 )
|
||||
nCutCur--;
|
||||
}
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
if ( --Gia_ObjFanin0(pObj)->Value == 0 )
|
||||
nCutCur--;
|
||||
}
|
||||
}
|
||||
// Gia_ManForEachObj( p, pObj, i )
|
||||
// assert( pObj->Value == 0 );
|
||||
return nCutMax;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Determine the frontier.]
|
||||
|
|
@ -109,7 +150,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
|
|||
Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
|
||||
char * pFront; // places used for the frontier
|
||||
int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
|
||||
int nCrossCutMaxInit = Gia_ManCrossCut( p );
|
||||
int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
|
||||
int iFront = 0;//, clk = clock();
|
||||
// set references for all objects
|
||||
Gia_ManCreateValueRefs( p );
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@
|
|||
#include "gia.h"
|
||||
#include "aig/aig/aig.h"
|
||||
#include "map/if/if.h"
|
||||
#include "opt/dar/dar.h"
|
||||
#include "bool/kit/kit.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START
|
|||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
|
||||
extern int Abc_RecToGia2( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
@ -45,282 +48,44 @@ ABC_NAMESPACE_IMPL_START
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManSetIfParsDefault( If_Par_t * pPars )
|
||||
void Gia_ManSetIfParsDefault( void * pp )
|
||||
{
|
||||
If_Par_t * pPars = (If_Par_t *)pp;
|
||||
// extern void * Abc_FrameReadLibLut();
|
||||
If_Par_t * p = (If_Par_t *)pPars;
|
||||
// set defaults
|
||||
memset( pPars, 0, sizeof(If_Par_t) );
|
||||
memset( p, 0, sizeof(If_Par_t) );
|
||||
// user-controlable paramters
|
||||
// pPars->nLutSize = -1;
|
||||
pPars->nLutSize = 6;
|
||||
pPars->nCutsMax = 8;
|
||||
pPars->nFlowIters = 1;
|
||||
pPars->nAreaIters = 2;
|
||||
pPars->DelayTarget = -1;
|
||||
pPars->Epsilon = (float)0.005;
|
||||
pPars->fPreprocess = 1;
|
||||
pPars->fArea = 0;
|
||||
pPars->fFancy = 0;
|
||||
pPars->fExpRed = 1; ////
|
||||
pPars->fLatchPaths = 0;
|
||||
pPars->fEdge = 1;
|
||||
pPars->fPower = 0;
|
||||
pPars->fCutMin = 0;
|
||||
pPars->fSeqMap = 0;
|
||||
pPars->fVerbose = 0;
|
||||
p->nLutSize = -1;
|
||||
// p->nLutSize = 6;
|
||||
p->nCutsMax = 8;
|
||||
p->nFlowIters = 1;
|
||||
p->nAreaIters = 2;
|
||||
p->DelayTarget = -1;
|
||||
p->Epsilon = (float)0.005;
|
||||
p->fPreprocess = 1;
|
||||
p->fArea = 0;
|
||||
p->fFancy = 0;
|
||||
p->fExpRed = 0; ////
|
||||
p->fLatchPaths = 0;
|
||||
p->fEdge = 1;
|
||||
p->fPower = 0;
|
||||
p->fCutMin = 0;
|
||||
p->fSeqMap = 0;
|
||||
p->fVerbose = 0;
|
||||
p->pLutStruct = NULL;
|
||||
// internal parameters
|
||||
pPars->fTruth = 0;
|
||||
pPars->nLatchesCi = 0;
|
||||
pPars->nLatchesCo = 0;
|
||||
pPars->fLiftLeaves = 0;
|
||||
// pPars->pLutLib = Abc_FrameReadLibLut();
|
||||
pPars->pLutLib = NULL;
|
||||
pPars->pTimesArr = NULL;
|
||||
pPars->pTimesArr = NULL;
|
||||
pPars->pFuncCost = NULL;
|
||||
p->fTruth = 0;
|
||||
p->nLatchesCi = 0;
|
||||
p->nLatchesCo = 0;
|
||||
p->fLiftLeaves = 0;
|
||||
p->fUseCoAttrs = 1; // use CO attributes
|
||||
p->pLutLib = NULL;
|
||||
p->pTimesArr = NULL;
|
||||
p->pTimesArr = NULL;
|
||||
p->pFuncCost = NULL;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Load the network into FPGA manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
|
||||
{
|
||||
// extern Vec_Int_t * SGia_ManComputeSwitchProbs( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
|
||||
// Vec_Int_t * vSwitching = NULL, * vSwitching2 = NULL;
|
||||
// float * pSwitching, * pSwitching2;
|
||||
If_Man_t * pIfMan;
|
||||
If_Obj_t * pIfObj;
|
||||
Gia_Obj_t * pNode;
|
||||
int i;//, clk = clock();
|
||||
Gia_ManLevelNum( p );
|
||||
// assert( p->pReprs == NULL );
|
||||
/*
|
||||
// set the number of registers (switch activity will be combinational)
|
||||
Gia_ManSetRegNum( p, 0 );
|
||||
if ( pPars->fPower )
|
||||
{
|
||||
vSwitching = SGia_ManComputeSwitchProbs( p, 48, 16, 0 );
|
||||
if ( pPars->fVerbose )
|
||||
{
|
||||
ABC_PRT( "Computing switching activity", clock() - clk );
|
||||
}
|
||||
pSwitching = (float *)vSwitching->pArray;
|
||||
vSwitching2 = Vec_IntStart( Gia_ManObjNumMax(p) );
|
||||
pSwitching2 = (float *)vSwitching2->pArray;
|
||||
}
|
||||
*/
|
||||
// start the mapping manager and set its parameters
|
||||
pIfMan = If_ManStart( pPars );
|
||||
// pIfMan->vSwitching = vSwitching2;
|
||||
// load the AIG into the mapper
|
||||
Gia_ManCreateRefs( p );
|
||||
Gia_ManForEachObj( p, pNode, i )
|
||||
{
|
||||
if ( Gia_ObjIsAnd(pNode) )
|
||||
pIfObj = If_ManCreateAnd( pIfMan,
|
||||
If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ),
|
||||
If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId1(pNode, i)), Gia_ObjFaninC1(pNode) ) );
|
||||
else if ( Gia_ObjIsCi(pNode) )
|
||||
{
|
||||
pIfObj = If_ManCreateCi( pIfMan );
|
||||
If_ObjSetLevel( pIfObj, Gia_ObjLevel(p,pNode) );
|
||||
// Abc_Print( 1, "pi=%d ", pIfObj->Level );
|
||||
if ( pIfMan->nLevelMax < (int)pIfObj->Level )
|
||||
pIfMan->nLevelMax = (int)pIfObj->Level;
|
||||
}
|
||||
else if ( Gia_ObjIsCo(pNode) )
|
||||
{
|
||||
pIfObj = If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ) );
|
||||
// Abc_Print( 1, "po=%d ", pIfObj->Level );
|
||||
}
|
||||
else if ( Gia_ObjIsConst0(pNode) )
|
||||
pIfObj = If_Not(If_ManConst1( pIfMan ));
|
||||
else // add the node to the mapper
|
||||
assert( 0 );
|
||||
// save the result
|
||||
assert( Vec_PtrEntry(vAigToIf, i) == NULL );
|
||||
Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
|
||||
// if ( vSwitching2 )
|
||||
// pSwitching2[pIfObj->Id] = pSwitching[pNode->Id];
|
||||
// set up the choice node
|
||||
/*
|
||||
// if ( p->pReprs && p->pNexts && Gia_ObjIsHead( p, i ) )
|
||||
if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefNumId(p, i) )
|
||||
{
|
||||
int iPrev, iFanin;
|
||||
pIfMan->nChoices++;
|
||||
for ( iPrev = i, iFanin = Gia_ObjNext(p, i); iFanin; iPrev = iFanin, iFanin = Gia_ObjNext(p, iFanin) )
|
||||
If_ObjSetChoice( Vec_PtrEntry(vAigToIf,iPrev), Vec_PtrEntry(vAigToIf,iFanin) );
|
||||
If_ManCreateChoice( pIfMan, Vec_PtrEntry(vAigToIf,i) );
|
||||
}
|
||||
*/
|
||||
/* // set up the choice node
|
||||
if ( Gia_ObjIsChoice( p, pNode ) )
|
||||
{
|
||||
pIfMan->nChoices++;
|
||||
for ( pPrev = pNode, pFanin = Gia_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Gia_ObjEquiv(p, pFanin) )
|
||||
If_ObjSetChoice( pPrev->pData, pFanin->pData );
|
||||
If_ManCreateChoice( pIfMan, pNode->pData );
|
||||
}
|
||||
// assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
|
||||
*/
|
||||
}
|
||||
// if ( vSwitching )
|
||||
// Vec_IntFree( vSwitching );
|
||||
return pIfMan;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int * Gia_ManFromIf( If_Man_t * pIfMan, Gia_Man_t * p, Vec_Ptr_t * vAigToIf )
|
||||
{
|
||||
int * pMapping, iOffset;
|
||||
Vec_Ptr_t * vIfToAig;
|
||||
Gia_Obj_t * pObj, * pObjRepr;
|
||||
If_Obj_t * pIfObj;
|
||||
If_Cut_t * pCutBest;
|
||||
int i, k, j, nLeaves, * ppLeaves;
|
||||
int nItems = 0;
|
||||
assert( Gia_ManCiNum(p) == If_ManCiNum(pIfMan) );
|
||||
assert( Gia_ManCoNum(p) == If_ManCoNum(pIfMan) );
|
||||
assert( Gia_ManAndNum(p) == If_ManAndNum(pIfMan) );
|
||||
// create mapping of IF to AIG
|
||||
vIfToAig = Vec_PtrStart( If_ManObjNum(pIfMan) );
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
{
|
||||
pIfObj = (If_Obj_t *)Vec_PtrEntry( vAigToIf, i );
|
||||
Vec_PtrWriteEntry( vIfToAig, pIfObj->Id, pObj );
|
||||
if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
|
||||
continue;
|
||||
nItems += 2 + If_CutLeaveNum( If_ObjCutBest(pIfObj) );
|
||||
}
|
||||
// construct the network
|
||||
pMapping = ABC_CALLOC( int, Gia_ManObjNum(p) + nItems );
|
||||
iOffset = Gia_ManObjNum(p);
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
{
|
||||
pIfObj = (If_Obj_t *)Vec_PtrEntry( vAigToIf, i );
|
||||
if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
|
||||
continue;
|
||||
pCutBest = If_ObjCutBest( pIfObj );
|
||||
nLeaves = If_CutLeaveNum( pCutBest );
|
||||
ppLeaves = If_CutLeaves( pCutBest );
|
||||
// create node
|
||||
k = iOffset;
|
||||
pMapping[k++] = nLeaves;
|
||||
for ( j = 0; j < nLeaves; j++ )
|
||||
{
|
||||
pObjRepr = (Gia_Obj_t *)Vec_PtrEntry( vIfToAig, ppLeaves[j] );
|
||||
pMapping[k++] = Gia_ObjId( p, pObjRepr );
|
||||
}
|
||||
pMapping[k++] = i;
|
||||
pMapping[i] = iOffset;
|
||||
iOffset = k;
|
||||
}
|
||||
assert( iOffset <= Gia_ManObjNum(p) + nItems );
|
||||
Vec_PtrFree( vIfToAig );
|
||||
// pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
|
||||
return pMapping;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Interface with the FPGA mapping package.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars )
|
||||
{
|
||||
If_Man_t * pIfMan;
|
||||
Vec_Ptr_t * vAigToIf;
|
||||
// set the arrival times
|
||||
pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
|
||||
memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
|
||||
// translate into the mapper
|
||||
vAigToIf = Vec_PtrStart( Gia_ManObjNum(p) );
|
||||
pIfMan = Gia_ManToIf( p, pPars, vAigToIf );
|
||||
if ( pIfMan == NULL )
|
||||
{
|
||||
Vec_PtrFree( vAigToIf );
|
||||
return 0;
|
||||
}
|
||||
// pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
|
||||
if ( !If_ManPerformMapping( pIfMan ) )
|
||||
{
|
||||
Vec_PtrFree( vAigToIf );
|
||||
If_ManStop( pIfMan );
|
||||
return 0;
|
||||
}
|
||||
// transform the result of mapping into the new network
|
||||
ABC_FREE( p->pMapping );
|
||||
p->pMapping = Gia_ManFromIf( pIfMan, p, vAigToIf );
|
||||
// if ( pPars->fBidec && pPars->nLutSize <= 8 )
|
||||
// Gia_ManBidecResyn( pNtk, 0 );
|
||||
If_ManStop( pIfMan );
|
||||
Vec_PtrFree( vAigToIf );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints mapping statistics.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManPrintMappingStats( Gia_Man_t * p )
|
||||
{
|
||||
int * pLevels;
|
||||
int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
|
||||
if ( !p->pMapping )
|
||||
return;
|
||||
pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
nLuts++;
|
||||
nFanins += Gia_ObjLutSize(p, i);
|
||||
nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
|
||||
pLevels[i]++;
|
||||
LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
|
||||
}
|
||||
ABC_FREE( pLevels );
|
||||
Abc_Print( 1, "mapping (K=%d) : ", nLutSize );
|
||||
Abc_Print( 1, "lut =%7d ", nLuts );
|
||||
Abc_Print( 1, "edge =%8d ", nFanins );
|
||||
Abc_Print( 1, "lev =%5d ", LevelMax );
|
||||
Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
|
||||
Abc_Print( 1, "\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
@ -437,7 +202,7 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p )
|
|||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints NPN class statistics.]
|
||||
Synopsis [Prints mapping statistics.]
|
||||
|
||||
Description []
|
||||
|
||||
|
|
@ -446,83 +211,444 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManPrintNpnClasses( Gia_Man_t * p )
|
||||
void Gia_ManPrintMappingStats( Gia_Man_t * p )
|
||||
{
|
||||
extern char ** Kit_DsdNpn4ClassNames();
|
||||
char ** pNames = Kit_DsdNpn4ClassNames();
|
||||
Vec_Int_t * vLeaves, * vTruth, * vVisited;
|
||||
int * pLutClass, ClassCounts[222] = {0};
|
||||
int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
|
||||
unsigned * pTruth;
|
||||
assert( p->pMapping != NULL );
|
||||
assert( Gia_ManLutSizeMax( p ) <= 4 );
|
||||
vLeaves = Vec_IntAlloc( 100 );
|
||||
vVisited = Vec_IntAlloc( 100 );
|
||||
vTruth = Vec_IntAlloc( (1<<16) );
|
||||
pLutClass = ABC_CALLOC( int, Gia_ManObjNum(p) );
|
||||
Gia_ManCleanTruth( p );
|
||||
int * pLevels;
|
||||
int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
|
||||
if ( !p->pMapping )
|
||||
return;
|
||||
pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
if ( Gia_ObjLutSize(p,i) > 4 )
|
||||
continue;
|
||||
Vec_IntClear( vLeaves );
|
||||
nLuts++;
|
||||
nFanins += Gia_ObjLutSize(p, i);
|
||||
nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
Vec_IntPush( vLeaves, iFan );
|
||||
for ( ; k < 4; k++ )
|
||||
Vec_IntPush( vLeaves, 0 );
|
||||
pTruth = Gia_ManConvertAigToTruth( p, Gia_ManObj(p, i), vLeaves, vTruth, vVisited );
|
||||
Class = Dar_LibReturnClass( *pTruth );
|
||||
ClassCounts[ Class ]++;
|
||||
pLutClass[i] = Class;
|
||||
pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
|
||||
pLevels[i]++;
|
||||
LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
|
||||
}
|
||||
Vec_IntFree( vLeaves );
|
||||
Vec_IntFree( vTruth );
|
||||
Vec_IntFree( vVisited );
|
||||
Vec_IntFreeP( &p->vTruths );
|
||||
nTotal = 0;
|
||||
for ( i = 0; i < 222; i++ )
|
||||
nTotal += ClassCounts[i];
|
||||
Abc_Print( 1, "NPN CLASS STATISTICS (for %d LUT4 present in the current mapping):\n", nTotal );
|
||||
OtherClasses = 0;
|
||||
for ( i = 0; i < 222; i++ )
|
||||
ABC_FREE( pLevels );
|
||||
Abc_Print( 1, "mapping (K=%d) : ", nLutSize );
|
||||
Abc_Print( 1, "lut =%7d ", nLuts );
|
||||
Abc_Print( 1, "edge =%8d ", nFanins );
|
||||
Abc_Print( 1, "lev =%5d ", LevelMax );
|
||||
Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
|
||||
Abc_Print( 1, "\n" );
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts GIA into IF manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline If_Obj_t * If_ManFanin0Copy( If_Man_t * pIfMan, Gia_Obj_t * pObj ) { return If_NotCond( If_ManObj(pIfMan, Gia_ObjValue(Gia_ObjFanin0(pObj))), Gia_ObjFaninC0(pObj) ); }
|
||||
static inline If_Obj_t * If_ManFanin1Copy( If_Man_t * pIfMan, Gia_Obj_t * pObj ) { return If_NotCond( If_ManObj(pIfMan, Gia_ObjValue(Gia_ObjFanin1(pObj))), Gia_ObjFaninC1(pObj) ); }
|
||||
If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars )
|
||||
{
|
||||
If_Man_t * pIfMan;
|
||||
If_Obj_t * pIfObj;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
// create levels with choices
|
||||
Gia_ManChoiceLevel( p );
|
||||
// mark representative nodes
|
||||
Gia_ManMarkFanoutDrivers( p );
|
||||
// start the mapping manager and set its parameters
|
||||
pIfMan = If_ManStart( pPars );
|
||||
pIfMan->pName = Abc_UtilStrsav( Gia_ManName(p) );
|
||||
// print warning about excessive memory usage
|
||||
if ( 1.0 * Gia_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
|
||||
printf( "Warning: The mapper will allocate %.1f GB for to represent the subject graph with %d AIG nodes.\n",
|
||||
1.0 * Gia_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Gia_ManObjNum(p) );
|
||||
// load the AIG into the mapper
|
||||
Gia_ManFillValue( p );
|
||||
Gia_ManConst0(p)->Value = If_ObjId( If_ManConst1(pIfMan) );
|
||||
Gia_ManForEachObj1( p, pObj, i )
|
||||
{
|
||||
if ( ClassCounts[i] == 0 )
|
||||
continue;
|
||||
if ( 100.0 * ClassCounts[i] / (nTotal+1) < 0.1 ) // do not show anything below 0.1 percent
|
||||
continue;
|
||||
OtherClasses += ClassCounts[i];
|
||||
Abc_Print( 1, "Class %3d : Count = %6d (%7.2f %%) %s\n",
|
||||
i, ClassCounts[i], 100.0 * ClassCounts[i] / (nTotal+1), pNames[i] );
|
||||
}
|
||||
OtherClasses = nTotal - OtherClasses;
|
||||
Abc_Print( 1, "Other : Count = %6d (%7.2f %%)\n",
|
||||
OtherClasses, 100.0 * OtherClasses / (nTotal+1) );
|
||||
// count the number of LUTs that have MUX function and two fanins with MUX functions
|
||||
OtherClasses = OtherClasses2 = 0;
|
||||
ABC_FREE( p->pRefs );
|
||||
Gia_ManSetRefsMapped( p );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
if ( pLutClass[i] != 109 )
|
||||
continue;
|
||||
Counter = Counter2 = 0;
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
pIfObj = If_ManCreateAnd( pIfMan, If_ManFanin0Copy(pIfMan, pObj), If_ManFanin1Copy(pIfMan, pObj) );
|
||||
else if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
Counter += (pLutClass[iFan] == 109);
|
||||
Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
|
||||
pIfObj = If_ManCreateCi( pIfMan );
|
||||
If_ObjSetLevel( pIfObj, Gia_ObjLevel(p, pObj) );
|
||||
// Abc_Print( 1, "pi%d=%d\n ", If_ObjId(pIfObj), If_ObjLevel(pIfObj) );
|
||||
if ( pIfMan->nLevelMax < (int)pIfObj->Level )
|
||||
pIfMan->nLevelMax = (int)pIfObj->Level;
|
||||
}
|
||||
OtherClasses += (Counter > 1);
|
||||
OtherClasses2 += (Counter2 > 1);
|
||||
// Abc_Print( 1, "%d -- ", pLutClass[i] );
|
||||
// Gia_LutForEachFanin( p, i, iFan, k )
|
||||
// Abc_Print( 1, "%d ", pLutClass[iFan] );
|
||||
// Abc_Print( 1, "\n" );
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
pIfObj = If_ManCreateCo( pIfMan, If_NotCond( If_ManFanin0Copy(pIfMan, pObj), Gia_ObjIsConst0(Gia_ObjFanin0(pObj))) );
|
||||
// Abc_Print( 1, "po%d=%d\n ", If_ObjId(pIfObj), If_ObjLevel(pIfObj) );
|
||||
}
|
||||
else assert( 0 );
|
||||
assert( i == If_ObjId(pIfObj) );
|
||||
Gia_ObjSetValue( pObj, If_ObjId(pIfObj) );
|
||||
// set up the choice node
|
||||
if ( Gia_ObjSibl(p, i) && pObj->fMark0 )
|
||||
{
|
||||
Gia_Obj_t * pSibl, * pPrev;
|
||||
for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) )
|
||||
If_ObjSetChoice( If_ManObj(pIfMan, Gia_ObjValue(pObj)), If_ManObj(pIfMan, Gia_ObjValue(pSibl)) );
|
||||
If_ManCreateChoice( pIfMan, If_ManObj(pIfMan, Gia_ObjValue(pObj)) );
|
||||
}
|
||||
// assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
|
||||
}
|
||||
ABC_FREE( p->pRefs );
|
||||
Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d (%7.2f %%) MFFC = %6d (%7.2f %%)\n",
|
||||
OtherClasses, 100.0 * OtherClasses / (nTotal+1),
|
||||
OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
|
||||
ABC_FREE( pLutClass );
|
||||
Gia_ManCleanMark0( p );
|
||||
return pIfMan;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives node's AIG after SOP balancing]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManNodeIfSopToGiaInt( Gia_Man_t * pNew, Vec_Wrd_t * vAnds, int nVars, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
Vec_Int_t * vResults;
|
||||
int iRes0, iRes1, iRes = -1;
|
||||
If_And_t This;
|
||||
word Entry;
|
||||
int i;
|
||||
if ( Vec_WrdSize(vAnds) == 0 )
|
||||
return 0;
|
||||
if ( Vec_WrdSize(vAnds) == 1 && Vec_WrdEntry(vAnds,0) == 0 )
|
||||
return 1;
|
||||
vResults = Vec_IntAlloc( Vec_WrdSize(vAnds) );
|
||||
for ( i = 0; i < nVars; i++ )
|
||||
Vec_IntPush( vResults, Vec_IntEntry(vLeaves, i) );
|
||||
Vec_WrdForEachEntryStart( vAnds, Entry, i, nVars )
|
||||
{
|
||||
This = If_WrdToAnd( Entry );
|
||||
iRes0 = Abc_LitNotCond( Vec_IntEntry(vResults, This.iFan0), This.fCompl0 );
|
||||
iRes1 = Abc_LitNotCond( Vec_IntEntry(vResults, This.iFan1), This.fCompl1 );
|
||||
if ( fHash )
|
||||
iRes = Gia_ManHashAnd( pNew, iRes0, iRes1 );
|
||||
else
|
||||
iRes = Gia_ManAppendAnd( pNew, iRes0, iRes1 );
|
||||
Vec_IntPush( vResults, iRes );
|
||||
}
|
||||
Vec_IntFree( vResults );
|
||||
return Abc_LitNotCond( iRes, This.fCompl );
|
||||
}
|
||||
int Gia_ManNodeIfSopToGia( Gia_Man_t * pNew, If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
int iResult;
|
||||
Vec_Wrd_t * vArray;
|
||||
vArray = If_CutDelaySopArray( p, pCut );
|
||||
iResult = Gia_ManNodeIfSopToGiaInt( pNew, vArray, If_CutLeaveNum(pCut), vLeaves, fHash );
|
||||
// Vec_WrdFree( vArray );
|
||||
return iResult;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Recursively derives the local AIG for the cut.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, int fHash )
|
||||
{
|
||||
If_Cut_t * pCut;
|
||||
If_Obj_t * pTemp;
|
||||
int iFunc, iFunc0, iFunc1;
|
||||
// get the best cut
|
||||
pCut = If_ObjCutBest(pIfObj);
|
||||
// if the cut is visited, return the result
|
||||
if ( If_CutDataInt(pCut) )
|
||||
return If_CutDataInt(pCut);
|
||||
// mark the node as visited
|
||||
Vec_PtrPush( vVisited, pCut );
|
||||
// insert the worst case
|
||||
If_CutSetDataInt( pCut, ~0 );
|
||||
// skip in case of primary input
|
||||
if ( If_ObjIsCi(pIfObj) )
|
||||
return If_CutDataInt(pCut);
|
||||
// compute the functions of the children
|
||||
for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
|
||||
{
|
||||
iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited, fHash );
|
||||
if ( iFunc0 == ~0 )
|
||||
continue;
|
||||
iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
|
||||
if ( iFunc1 == ~0 )
|
||||
continue;
|
||||
// both branches are solved
|
||||
if ( fHash )
|
||||
iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
|
||||
else
|
||||
iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) );
|
||||
if ( pTemp->fPhase != pIfObj->fPhase )
|
||||
iFunc = Abc_LitNot(iFunc);
|
||||
If_CutSetDataInt( pCut, iFunc );
|
||||
break;
|
||||
}
|
||||
return If_CutDataInt(pCut);
|
||||
}
|
||||
int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
If_Cut_t * pCut;
|
||||
If_Obj_t * pLeaf;
|
||||
int i, iRes;
|
||||
// get the best cut
|
||||
pCut = If_ObjCutBest(pIfObj);
|
||||
assert( pCut->nLeaves > 1 );
|
||||
// set the leaf variables
|
||||
If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
|
||||
If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
|
||||
// recursively compute the function while collecting visited cuts
|
||||
Vec_PtrClear( pIfMan->vTemp );
|
||||
iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp, fHash );
|
||||
if ( iRes == ~0 )
|
||||
{
|
||||
Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
|
||||
return ~0;
|
||||
}
|
||||
// clean the cuts
|
||||
If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
|
||||
If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
|
||||
Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
|
||||
If_CutSetDataInt( pCut, 0 );
|
||||
return iRes;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts IF into GIA manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
|
||||
{
|
||||
int fHash = 0;
|
||||
Gia_Man_t * pNew;
|
||||
If_Obj_t * pIfObj, * pIfLeaf;
|
||||
If_Cut_t * pCutBest;
|
||||
Vec_Int_t * vLeaves;
|
||||
Vec_Int_t * vCover;
|
||||
unsigned * pTruth;
|
||||
int Counter, iOffset, nItems = 0;
|
||||
int i, k, w, GiaId;
|
||||
// create new manager
|
||||
pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
|
||||
Gia_ManHashAlloc( pNew );
|
||||
// iterate through nodes used in the mapping
|
||||
vCover = Vec_IntAlloc( 1 << 16 );
|
||||
vLeaves = Vec_IntAlloc( 16 );
|
||||
If_ManCleanCutData( pIfMan );
|
||||
If_ManForEachObj( pIfMan, pIfObj, i )
|
||||
{
|
||||
if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
|
||||
continue;
|
||||
if ( If_ObjIsAnd(pIfObj) )
|
||||
{
|
||||
pCutBest = If_ObjCutBest( pIfObj );
|
||||
// collect leaves of the best cut
|
||||
Vec_IntClear( vLeaves );
|
||||
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
|
||||
Vec_IntPush( vLeaves, pIfLeaf->iCopy );
|
||||
// get the functionality
|
||||
if ( pIfMan->pPars->pLutStruct )
|
||||
pIfObj->iCopy = Kit_TruthToGia( pNew, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, vLeaves, fHash );
|
||||
else if ( pIfMan->pPars->fDelayOpt )
|
||||
pIfObj->iCopy = Gia_ManNodeIfSopToGia( pNew, pIfMan, pCutBest, vLeaves, fHash );
|
||||
else if ( pIfMan->pPars->fUserRecLib )
|
||||
pIfObj->iCopy = Abc_RecToGia2( pNew, pIfMan, pCutBest, pIfObj, vLeaves, fHash );
|
||||
else
|
||||
pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, fHash );
|
||||
// complement the node if the TT was used and the cut was complemented
|
||||
if ( pIfMan->pPars->pLutStruct )
|
||||
pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
|
||||
// count entries in the mapping array
|
||||
nItems += 2 + If_CutLeaveNum( pCutBest );
|
||||
}
|
||||
else if ( If_ObjIsCi(pIfObj) )
|
||||
pIfObj->iCopy = Gia_ManAppendCi(pNew);
|
||||
else if ( If_ObjIsCo(pIfObj) )
|
||||
pIfObj->iCopy = Gia_ManAppendCo( pNew, Abc_LitNotCond(If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj)) );
|
||||
else if ( If_ObjIsConst1(pIfObj) )
|
||||
{
|
||||
pIfObj->iCopy = 1;
|
||||
nItems += 2;
|
||||
}
|
||||
else assert( 0 );
|
||||
}
|
||||
Vec_IntFree( vCover );
|
||||
Vec_IntFree( vLeaves );
|
||||
Gia_ManHashStop( pNew );
|
||||
|
||||
// GIA after mapping with choices may end up with dangling nodes
|
||||
// which participate as leaves of some cuts used in the mapping
|
||||
// such nodes are marked here and skipped when mapping is derived
|
||||
Counter = Gia_ManMarkDangling(pNew);
|
||||
// if ( pIfMan->pPars->fVerbose && Counter )
|
||||
if ( Counter )
|
||||
printf( "GIA after mapping has %d dangling nodes.\n", Counter );
|
||||
|
||||
// create mapping
|
||||
iOffset = Gia_ManObjNum(pNew);
|
||||
pNew->pMapping = ABC_CALLOC( int, iOffset + nItems );
|
||||
assert( pNew->vTruths == NULL );
|
||||
if ( pIfMan->pPars->pLutStruct )
|
||||
pNew->vTruths = Vec_IntAlloc( 1000 );
|
||||
If_ManForEachObj( pIfMan, pIfObj, i )
|
||||
{
|
||||
if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
|
||||
continue;
|
||||
if ( If_ObjIsAnd(pIfObj) )
|
||||
{
|
||||
GiaId = Abc_Lit2Var( pIfObj->iCopy );
|
||||
if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) ) // skip trivial node
|
||||
continue;
|
||||
assert( Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) );
|
||||
if ( !Gia_ManObj(pNew, GiaId)->fMark0 ) // skip dangling node
|
||||
continue;
|
||||
// get the best cut
|
||||
pCutBest = If_ObjCutBest( pIfObj );
|
||||
// copy the truth tables
|
||||
pTruth = NULL;
|
||||
if ( pNew->vTruths )
|
||||
{
|
||||
// copy truth table
|
||||
for ( w = 0; w < pIfMan->nTruthWords; w++ )
|
||||
Vec_IntPush( pNew->vTruths, If_CutTruth(pCutBest)[w] );
|
||||
pTruth = (unsigned *)(Vec_IntArray(pNew->vTruths) + Vec_IntSize(pNew->vTruths) - pIfMan->nTruthWords);
|
||||
// complement
|
||||
if ( pCutBest->fCompl ^ Abc_LitIsCompl(pIfObj->iCopy) )
|
||||
for ( w = 0; w < pIfMan->nTruthWords; w++ )
|
||||
pTruth[w] = ~pTruth[w];
|
||||
}
|
||||
// create node
|
||||
pNew->pMapping[GiaId] = iOffset;
|
||||
pNew->pMapping[iOffset++] = If_CutLeaveNum(pCutBest);
|
||||
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
|
||||
{
|
||||
int FaninId = Abc_Lit2Var(pIfLeaf->iCopy);
|
||||
if ( pTruth && Abc_LitIsCompl(pIfLeaf->iCopy) )
|
||||
Kit_TruthChangePhase( pTruth, If_CutLeaveNum(pCutBest), k );
|
||||
if ( !Gia_ManObj(pNew, FaninId)->fMark0 ) // skip dangling node
|
||||
{
|
||||
// update truth table
|
||||
if ( pTruth )
|
||||
{
|
||||
extern void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar );
|
||||
if ( If_CutLeaveNum(pCutBest) >= 6 )
|
||||
If_CluSwapVars( (word*)pTruth, If_CutLeaveNum(pCutBest), NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
|
||||
else
|
||||
{
|
||||
word Truth = ((word)pTruth[0] << 32) | (word)pTruth[0];
|
||||
If_CluSwapVars( &Truth, 6, NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
|
||||
pTruth[0] = (Truth & 0xFFFFFFFF);
|
||||
}
|
||||
}
|
||||
pNew->pMapping[iOffset-k-1]--;
|
||||
continue;
|
||||
}
|
||||
assert( FaninId < GiaId );
|
||||
pNew->pMapping[iOffset++] = FaninId;
|
||||
}
|
||||
pNew->pMapping[iOffset++] = GiaId;
|
||||
}
|
||||
else if ( If_ObjIsConst1(pIfObj) )
|
||||
{
|
||||
// create node
|
||||
pNew->pMapping[0] = iOffset;
|
||||
pNew->pMapping[iOffset++] = 0;
|
||||
pNew->pMapping[iOffset++] = 0;
|
||||
/*
|
||||
if ( pNew->vTruths )
|
||||
{
|
||||
printf( "%d ", nLeaves );
|
||||
for ( w = 0; w < pIfMan->nTruthWords; w++ )
|
||||
Vec_IntPush( pNew->vTruths, 0 );
|
||||
}
|
||||
*/
|
||||
}
|
||||
}
|
||||
Gia_ManCleanMark0( pNew );
|
||||
// assert( iOffset == Gia_ManObjNum(pNew) + nItems );
|
||||
if ( pIfMan->pManTim )
|
||||
pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
|
||||
// verify that COs have mapping
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Gia_ManForEachCo( pNew, pObj, i )
|
||||
{
|
||||
if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
|
||||
assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
|
||||
}
|
||||
}
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Interface of LUT mapping package.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
|
||||
{
|
||||
Gia_Man_t * pNew;
|
||||
If_Man_t * pIfMan;
|
||||
If_Par_t * pPars = (If_Par_t *)pp;
|
||||
// set the arrival times
|
||||
assert( pPars->pTimesArr == NULL );
|
||||
pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
|
||||
memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
|
||||
// translate into the mapper
|
||||
pIfMan = Gia_ManToIf( p, pPars );
|
||||
if ( pIfMan == NULL )
|
||||
return NULL;
|
||||
if ( p->pManTime )
|
||||
pIfMan->pManTim = Tim_ManDup( p->pManTime, 0 );
|
||||
if ( !If_ManPerformMapping( pIfMan ) )
|
||||
{
|
||||
If_ManStop( pIfMan );
|
||||
return NULL;
|
||||
}
|
||||
// transform the result of mapping into the new network
|
||||
pNew = Gia_ManFromIf( pIfMan );
|
||||
If_ManStop( pIfMan );
|
||||
// transfer name
|
||||
assert( pNew->pName == NULL );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
|
||||
// unmap in case of SOP balancing
|
||||
// if ( pIfMan->pPars->fDelayOpt )
|
||||
// Vec_IntFreeP( &pNew->vMapping );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@
|
|||
#include "gia.h"
|
||||
#include "misc/tim/tim.h"
|
||||
#include "proof/abs/abs.h"
|
||||
#include "opt/dar/dar.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -107,6 +108,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 +251,36 @@ 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 );
|
||||
Gia_ManCleanMark0( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints stats for the AIG.]
|
||||
|
|
@ -271,7 +303,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
|
|||
printf( " ff =%7d", Gia_ManRegNum(p) );
|
||||
printf( " and =%8d", Gia_ManAndNum(p) );
|
||||
printf( " lev =%5d", Gia_ManLevelNum(p) ); Vec_IntFreeP( &p->vLevels );
|
||||
printf( " cut =%5d", Gia_ManCrossCut(p) );
|
||||
printf( " cut = %d(%d)", Gia_ManCrossCut(p, 0), Gia_ManCrossCut(p, 1) );
|
||||
// printf( " mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
|
||||
printf( " mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
|
||||
if ( Gia_ManHasDangling(p) )
|
||||
|
|
@ -289,6 +321,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 )
|
||||
|
|
@ -427,6 +461,96 @@ void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew )
|
|||
printf( "\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints NPN class statistics.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManPrintNpnClasses( Gia_Man_t * p )
|
||||
{
|
||||
extern char ** Kit_DsdNpn4ClassNames();
|
||||
char ** pNames = Kit_DsdNpn4ClassNames();
|
||||
Vec_Int_t * vLeaves, * vTruth, * vVisited;
|
||||
int * pLutClass, ClassCounts[222] = {0};
|
||||
int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
|
||||
unsigned * pTruth;
|
||||
assert( p->pMapping != NULL );
|
||||
assert( Gia_ManLutSizeMax( p ) <= 4 );
|
||||
vLeaves = Vec_IntAlloc( 100 );
|
||||
vVisited = Vec_IntAlloc( 100 );
|
||||
vTruth = Vec_IntAlloc( (1<<16) );
|
||||
pLutClass = ABC_CALLOC( int, Gia_ManObjNum(p) );
|
||||
Gia_ManCleanTruth( p );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
if ( Gia_ObjLutSize(p,i) > 4 )
|
||||
continue;
|
||||
Vec_IntClear( vLeaves );
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
Vec_IntPush( vLeaves, iFan );
|
||||
for ( ; k < 4; k++ )
|
||||
Vec_IntPush( vLeaves, 0 );
|
||||
pTruth = Gia_ManConvertAigToTruth( p, Gia_ManObj(p, i), vLeaves, vTruth, vVisited );
|
||||
Class = Dar_LibReturnClass( *pTruth );
|
||||
ClassCounts[ Class ]++;
|
||||
pLutClass[i] = Class;
|
||||
}
|
||||
Vec_IntFree( vLeaves );
|
||||
Vec_IntFree( vTruth );
|
||||
Vec_IntFree( vVisited );
|
||||
Vec_IntFreeP( &p->vTruths );
|
||||
nTotal = 0;
|
||||
for ( i = 0; i < 222; i++ )
|
||||
nTotal += ClassCounts[i];
|
||||
Abc_Print( 1, "NPN CLASS STATISTICS (for %d LUT4 present in the current mapping):\n", nTotal );
|
||||
OtherClasses = 0;
|
||||
for ( i = 0; i < 222; i++ )
|
||||
{
|
||||
if ( ClassCounts[i] == 0 )
|
||||
continue;
|
||||
if ( 100.0 * ClassCounts[i] / (nTotal+1) < 0.1 ) // do not show anything below 0.1 percent
|
||||
continue;
|
||||
OtherClasses += ClassCounts[i];
|
||||
Abc_Print( 1, "Class %3d : Count = %6d (%7.2f %%) %s\n",
|
||||
i, ClassCounts[i], 100.0 * ClassCounts[i] / (nTotal+1), pNames[i] );
|
||||
}
|
||||
OtherClasses = nTotal - OtherClasses;
|
||||
Abc_Print( 1, "Other : Count = %6d (%7.2f %%)\n",
|
||||
OtherClasses, 100.0 * OtherClasses / (nTotal+1) );
|
||||
// count the number of LUTs that have MUX function and two fanins with MUX functions
|
||||
OtherClasses = OtherClasses2 = 0;
|
||||
ABC_FREE( p->pRefs );
|
||||
Gia_ManSetRefsMapped( p );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
if ( pLutClass[i] != 109 )
|
||||
continue;
|
||||
Counter = Counter2 = 0;
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
{
|
||||
Counter += (pLutClass[iFan] == 109);
|
||||
Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
|
||||
}
|
||||
OtherClasses += (Counter > 1);
|
||||
OtherClasses2 += (Counter2 > 1);
|
||||
// Abc_Print( 1, "%d -- ", pLutClass[i] );
|
||||
// Gia_LutForEachFanin( p, i, iFan, k )
|
||||
// Abc_Print( 1, "%d ", pLutClass[iFan] );
|
||||
// Abc_Print( 1, "\n" );
|
||||
}
|
||||
ABC_FREE( p->pRefs );
|
||||
Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d (%7.2f %%) MFFC = %6d (%7.2f %%)\n",
|
||||
OtherClasses, 100.0 * OtherClasses / (nTotal+1),
|
||||
OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
|
||||
ABC_FREE( pLutClass );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -94,6 +94,32 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
|
|||
return Gia_ManDupMarked( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Skip the first outputs during cleanup.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
assert( Gia_ManRegNum(p) == 0 );
|
||||
assert( nOutputs < Gia_ManCoNum(p) );
|
||||
Gia_ManCombMarkUsed( p );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
if ( i < nOutputs )
|
||||
pObj->fMark0 = 1;
|
||||
else
|
||||
break;
|
||||
return Gia_ManDupMarked( p );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
|
|||
|
|
@ -550,12 +550,59 @@ int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManCrossCut( Gia_Man_t * p )
|
||||
void Gia_ManDfsForCrossCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
|
||||
{
|
||||
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
||||
return;
|
||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
|
||||
return;
|
||||
}
|
||||
if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
Gia_ObjFanin0(pObj)->Value++;
|
||||
Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
|
||||
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
|
||||
return;
|
||||
}
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Gia_ObjFanin0(pObj)->Value++;
|
||||
Gia_ObjFanin1(pObj)->Value++;
|
||||
Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
|
||||
Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
|
||||
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
|
||||
}
|
||||
Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p, int fReverse )
|
||||
{
|
||||
Vec_Int_t * vNodes;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
Gia_ManCleanValue( p );
|
||||
vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
|
||||
Gia_ManIncrementTravId( p );
|
||||
if ( fReverse )
|
||||
{
|
||||
Gia_ManForEachCoReverse( p, pObj, i )
|
||||
if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
|
||||
Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
|
||||
}
|
||||
else
|
||||
{
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
|
||||
Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
|
||||
}
|
||||
return vNodes;
|
||||
}
|
||||
int Gia_ManCrossCut( Gia_Man_t * p, int fReverse )
|
||||
{
|
||||
Vec_Int_t * vNodes;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, nCutCur = 0, nCutMax = 0;
|
||||
Gia_ManCreateValueRefs( p );
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
vNodes = Gia_ManDfsForCrossCut( p, fReverse );
|
||||
Gia_ManForEachObjVec( vNodes, p, pObj, i )
|
||||
{
|
||||
if ( pObj->Value )
|
||||
nCutCur++;
|
||||
|
|
@ -574,8 +621,9 @@ int Gia_ManCrossCut( Gia_Man_t * p )
|
|||
nCutCur--;
|
||||
}
|
||||
}
|
||||
// Gia_ManForEachObj( p, pObj, i )
|
||||
// assert( pObj->Value == 0 );
|
||||
Vec_IntFree( vNodes );
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
assert( pObj->Value == 0 );
|
||||
return nCutMax;
|
||||
}
|
||||
|
||||
|
|
@ -1195,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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -789,7 +789,7 @@ extern ABC_DLL int Abc_NtkRecVarNum();
|
|||
extern ABC_DLL Vec_Int_t * Abc_NtkRecMemory();
|
||||
extern ABC_DLL int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
|
||||
/*=== abcRec2.c ==========================================================*/
|
||||
extern ABC_DLL void Abc_NtkRecStart2( Gia_Man_t *p, int nVars, int nCuts, int fTrim );
|
||||
extern ABC_DLL void Abc_NtkRecStart2( Gia_Man_t * p, int nVars, int nCuts, int fTrim );
|
||||
extern ABC_DLL void Abc_NtkRecStop2();
|
||||
extern ABC_DLL void Abc_NtkRecAdd2( Abc_Ntk_t * pNtk, int fUseSOPB );
|
||||
extern ABC_DLL void Abc_NtkRecPs2(int fPrintLib);
|
||||
|
|
@ -798,6 +798,15 @@ extern ABC_DLL void Abc_NtkRecLibMerge2(Gia_Man_t * pGia);
|
|||
extern ABC_DLL int Abc_NtkRecIsRunning2();
|
||||
extern ABC_DLL int Abc_NtkRecIsInTrimMode2();
|
||||
extern ABC_DLL void Abc_NtkRecFilter2(int nLimit);
|
||||
/*=== abcRec3.c ==========================================================*/
|
||||
extern ABC_DLL void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose );
|
||||
extern ABC_DLL void Abc_NtkRecStop3();
|
||||
extern ABC_DLL void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB );
|
||||
extern ABC_DLL void Abc_NtkRecPs3(int fPrintLib);
|
||||
extern ABC_DLL Gia_Man_t * Abc_NtkRecGetGia3();
|
||||
extern ABC_DLL int Abc_NtkRecIsRunning3();
|
||||
extern ABC_DLL void Abc_NtkRecLibMerge3(Gia_Man_t * pGia);
|
||||
//extern ABC_DLL void Abc_NtkRecFilter3(int nLimit);
|
||||
/*=== abcReconv.c ==========================================================*/
|
||||
extern ABC_DLL Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
|
||||
extern ABC_DLL void Abc_NtkManCutStop( Abc_ManCut_t * p );
|
||||
|
|
|
|||
|
|
@ -377,12 +377,12 @@ int Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
|
|||
}
|
||||
if ( Abc_ObjFaninNum(pObj) != 1 )
|
||||
{
|
||||
fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin.\n", Abc_ObjName(pObj) );
|
||||
fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin (but %d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj) );
|
||||
return 0;
|
||||
}
|
||||
if ( Abc_ObjFanoutNum(pObj) > 0 )
|
||||
{
|
||||
fprintf( stdout, "NetworkCheck: A PO \"%s\" has fanouts.\n", Abc_ObjName(pObj) );
|
||||
fprintf( stdout, "NetworkCheck: A PO \"%s\" has %d fanout(s).\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
|
||||
return 0;
|
||||
}
|
||||
pObj->pCopy = (Abc_Obj_t *)1;
|
||||
|
|
|
|||
|
|
@ -87,20 +87,13 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
|
|||
assert( !Abc_ObjIsComplement(pObj) );
|
||||
assert( pObj->pNtk == pFaninR->pNtk );
|
||||
assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
|
||||
assert( !Abc_ObjIsPi(pObj) && !Abc_ObjIsPo(pFanin) ); // fanin of PI or fanout of PO
|
||||
assert( !Abc_ObjIsCo(pObj) || !Abc_ObjFaninNum(pObj) ); // CO with two fanins
|
||||
assert( !Abc_ObjIsNet(pObj) || !Abc_ObjFaninNum(pObj) ); // net with two fanins
|
||||
Vec_IntPushMem( pObj->pNtk->pMmStep, &pObj->vFanins, pFaninR->Id );
|
||||
Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id );
|
||||
if ( Abc_ObjIsComplement(pFanin) )
|
||||
Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
|
||||
if ( Abc_ObjIsNet(pObj) && Abc_ObjFaninNum(pObj) > 1 )
|
||||
{
|
||||
printf( "Abc_ObjAddFanin(): Error! Creating net \"%s\" with two fanins.\n", Abc_ObjName(pObj) );
|
||||
}
|
||||
/*
|
||||
if ( Abc_ObjIsCo(pFanin) )
|
||||
{
|
||||
printf( "Abc_ObjAddFanin(): Error! Creating fanout of a CO.\n", Abc_ObjName(pFanin) );
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
1023
src/base/abci/abc.c
1023
src/base/abci/abc.c
File diff suppressed because it is too large
Load Diff
|
|
@ -620,6 +620,150 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
|
|||
return pNtkNew;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates local function of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
|
||||
if ( Gia_ObjIsTravIdCurrentId(p, Id) )
|
||||
return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
|
||||
Gia_ObjSetTravIdCurrentId(p, Id);
|
||||
pObj = Gia_ManObj(p, Id);
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
// compute the functions of the children
|
||||
gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
|
||||
gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
|
||||
// get the function of the cut
|
||||
gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );
|
||||
Vec_PtrWriteEntry( vCopies, Id, gFunc );
|
||||
return gFunc;
|
||||
}
|
||||
Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
|
||||
{
|
||||
int k, iFan;
|
||||
assert( Gia_ObjIsLut(p, GiaId) );
|
||||
assert( Gia_ObjLutSize(p, GiaId) > 0 );
|
||||
Gia_ManIncrementTravId( p );
|
||||
Gia_LutForEachFanin( p, GiaId, iFan, k )
|
||||
{
|
||||
Gia_ObjSetTravIdCurrentId(p, iFan);
|
||||
Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
|
||||
}
|
||||
return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts the network from the mapped GIA manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
|
||||
{
|
||||
int fVerbose = 0;
|
||||
int fDuplicate = 0;
|
||||
Abc_Ntk_t * pNtkNew;
|
||||
Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
|
||||
Gia_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||
Vec_Ptr_t * vReflect;
|
||||
int i, k, iFan, nDupGates;
|
||||
assert( p->pMapping != NULL );
|
||||
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
|
||||
// duplicate the name and the spec
|
||||
pNtkNew->pName = Extra_UtilStrsav(p->pName);
|
||||
pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
|
||||
Gia_ManFillValue( p );
|
||||
// create constant
|
||||
pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
|
||||
Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
|
||||
// create PIs
|
||||
Gia_ManForEachPi( p, pObj, i )
|
||||
pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
|
||||
// create POs
|
||||
Gia_ManForEachPo( p, pObj, i )
|
||||
pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
|
||||
// create as many latches as there are registers in the manager
|
||||
Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
|
||||
{
|
||||
pObjNew = Abc_NtkCreateLatch( pNtkNew );
|
||||
pObjNewLi = Abc_NtkCreateBi( pNtkNew );
|
||||
pObjNewLo = Abc_NtkCreateBo( pNtkNew );
|
||||
Abc_ObjAddFanin( pObjNew, pObjNewLi );
|
||||
Abc_ObjAddFanin( pObjNewLo, pObjNew );
|
||||
pObjLi->Value = Abc_ObjId( pObjNewLi );
|
||||
pObjLo->Value = Abc_ObjId( pObjNewLo );
|
||||
Abc_LatchSetInit0( pObjNew );
|
||||
}
|
||||
// rebuild the AIG
|
||||
vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
|
||||
Gia_ManForEachLut( p, i )
|
||||
{
|
||||
pObj = Gia_ManObj(p, i);
|
||||
assert( pObj->Value == ~0 );
|
||||
if ( Gia_ObjLutSize(p, i) == 0 )
|
||||
{
|
||||
pObj->Value = Abc_ObjId(pConst0);
|
||||
continue;
|
||||
}
|
||||
pObjNew = Abc_NtkCreateNode( pNtkNew );
|
||||
Gia_LutForEachFanin( p, i, iFan, k )
|
||||
Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
|
||||
pObjNew->pData = Abc_ObjHopFromGia( pNtkNew->pManFunc, p, i, vReflect );
|
||||
pObj->Value = Abc_ObjId( pObjNew );
|
||||
}
|
||||
Vec_PtrFree( vReflect );
|
||||
// connect the PO nodes
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
|
||||
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
|
||||
}
|
||||
// create names
|
||||
Abc_NtkAddDummyPiNames( pNtkNew );
|
||||
Abc_NtkAddDummyPoNames( pNtkNew );
|
||||
Abc_NtkAddDummyBoxNames( pNtkNew );
|
||||
|
||||
// decouple the PO driver nodes to reduce the number of levels
|
||||
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
|
||||
if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
|
||||
{
|
||||
if ( !fDuplicate )
|
||||
printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
|
||||
else
|
||||
printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
|
||||
}
|
||||
// remove const node if it is not used
|
||||
if ( Abc_ObjFanoutNum(pConst0) == 0 )
|
||||
Abc_NtkDeleteObj( pConst0 );
|
||||
|
||||
assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
|
||||
assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
|
||||
assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
|
||||
|
||||
// check the resulting AIG
|
||||
if ( !Abc_NtkCheck( pNtkNew ) )
|
||||
Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
|
||||
return pNtkNew;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts the network from the AIG manager into ABC.]
|
||||
|
|
|
|||
|
|
@ -353,10 +353,10 @@ void Abc_TruthStoreRead( char * pFileName, Abc_TtStore_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p )
|
||||
void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p, int fBinary )
|
||||
{
|
||||
FILE * pFile;
|
||||
int i;
|
||||
int i, nBytes = 8 * Abc_Truth6WordNum( p->nVars );
|
||||
pFile = fopen( pFileName, "wb" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
|
|
@ -365,8 +365,10 @@ void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p )
|
|||
}
|
||||
for ( i = 0; i < p->nFuncs; i++ )
|
||||
{
|
||||
Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars );
|
||||
fprintf( pFile, "\n" );
|
||||
if ( fBinary )
|
||||
fwrite( p->pFuncs[i], nBytes, 1, pFile );
|
||||
else
|
||||
Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars ), fprintf( pFile, "\n" );
|
||||
}
|
||||
fclose( pFile );
|
||||
}
|
||||
|
|
@ -441,7 +443,7 @@ void Abc_TtStoreTest( char * pFileName )
|
|||
return;
|
||||
|
||||
// write into another file
|
||||
Abc_TtStoreWrite( pFileOutput, p );
|
||||
Abc_TtStoreWrite( pFileOutput, p, 0 );
|
||||
|
||||
// delete data-structure
|
||||
Abc_TtStoreFree( p, -1 );
|
||||
|
|
@ -471,6 +473,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
|
|||
pAlgoName = "bi-decomp";
|
||||
else if ( DecType == 3 )
|
||||
pAlgoName = "DSD";
|
||||
else if ( DecType == 4 )
|
||||
pAlgoName = "fast DSD";
|
||||
|
||||
if ( pAlgoName )
|
||||
printf( "Applying %-10s to %8d func%s of %2d vars... ",
|
||||
|
|
@ -535,6 +539,24 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
|
|||
Kit_DsdNtkFree( pNtk );
|
||||
}
|
||||
}
|
||||
else if ( DecType == 4 )
|
||||
{
|
||||
extern void Dau_DsdTestOne( word t, int i );
|
||||
if ( p->nVars != 6 )
|
||||
{
|
||||
printf( "Currently only works for 6 variables.\n" );
|
||||
return;
|
||||
}
|
||||
// perform disjoint-support decomposition and count AIG nodes
|
||||
// (non-DSD blocks are decomposed into 2:1 MUXes, each counting as 3 AIG nodes)
|
||||
assert( p->nVars == 6 );
|
||||
for ( i = 0; i < p->nFuncs; i++ )
|
||||
{
|
||||
if ( fVerbose )
|
||||
printf( "%7d : ", i );
|
||||
Dau_DsdTestOne( *p->pFuncs[i], i );
|
||||
}
|
||||
}
|
||||
else assert( 0 );
|
||||
|
||||
printf( "AIG nodes =%9d ", nNodes );
|
||||
|
|
@ -585,7 +607,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose )
|
|||
printf( "Using truth tables from file \"%s\"...\n", pFileName );
|
||||
if ( DecType == 0 )
|
||||
{ if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); }
|
||||
else if ( DecType >= 1 && DecType <= 3 )
|
||||
else if ( DecType >= 1 && DecType <= 4 )
|
||||
Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose );
|
||||
else
|
||||
printf( "Unknown decomposition type value (%d).\n", DecType );
|
||||
|
|
|
|||
|
|
@ -228,7 +228,6 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
|
|||
// set up the choice node
|
||||
if ( Abc_AigNodeIsChoice( pNode ) )
|
||||
{
|
||||
pIfMan->nChoices++;
|
||||
for ( pPrev = pNode, pFanin = (Abc_Obj_t *)pNode->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
|
||||
If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
|
||||
If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
|
||||
|
|
@ -495,10 +494,13 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
|
|||
{
|
||||
extern Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj );
|
||||
extern Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj );
|
||||
if(Abc_NtkRecIsRunning())
|
||||
pNodeNew->pData = Abc_RecToHop( (Hop_Man_t *)pNtkNew->pManFunc, pIfMan, pCutBest, pIfObj);
|
||||
else
|
||||
extern Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj );
|
||||
if(Abc_NtkRecIsRunning3())
|
||||
pNodeNew->pData = Abc_RecToHop3( (Hop_Man_t *)pNtkNew->pManFunc, pIfMan, pCutBest, pIfObj);
|
||||
else if(Abc_NtkRecIsRunning2())
|
||||
pNodeNew->pData = Abc_RecToHop2( (Hop_Man_t *)pNtkNew->pManFunc, pIfMan, pCutBest, pIfObj);
|
||||
else
|
||||
pNodeNew->pData = Abc_RecToHop( (Hop_Man_t *)pNtkNew->pManFunc, pIfMan, pCutBest, pIfObj);
|
||||
|
||||
}
|
||||
else
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ struct Abc_TtStore_t_
|
|||
|
||||
extern Abc_TtStore_t * Abc_TtStoreLoad( char * pFileName, int nVarNum );
|
||||
extern void Abc_TtStoreFree( Abc_TtStore_t * p, int nVarNum );
|
||||
extern void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p );
|
||||
extern void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p, int fBinary );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
|
|
@ -276,7 +276,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Abc_TruthNpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fVerbose )
|
||||
void Abc_TruthNpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose )
|
||||
{
|
||||
Abc_TtStore_t * p;
|
||||
char * pFileNameOut;
|
||||
|
|
@ -292,8 +292,11 @@ void Abc_TruthNpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes,
|
|||
// write the result
|
||||
if ( fDumpRes )
|
||||
{
|
||||
pFileNameOut = Extra_FileNameGenericAppend( pFileName, "_out.txt" );
|
||||
Abc_TtStoreWrite( pFileNameOut, p );
|
||||
if ( fBinary )
|
||||
pFileNameOut = Extra_FileNameGenericAppend( pFileName, "_out.tt" );
|
||||
else
|
||||
pFileNameOut = Extra_FileNameGenericAppend( pFileName, "_out.txt" );
|
||||
Abc_TtStoreWrite( pFileNameOut, p, fBinary );
|
||||
if ( fVerbose )
|
||||
printf( "The resulting functions are written into file \"%s\".\n", pFileNameOut );
|
||||
}
|
||||
|
|
@ -315,12 +318,12 @@ void Abc_TruthNpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes,
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fVerbose )
|
||||
int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int fBinary, int fVerbose )
|
||||
{
|
||||
if ( fVerbose )
|
||||
printf( "Using truth tables from file \"%s\"...\n", pFileName );
|
||||
if ( NpnType >= 0 && NpnType <= 4 )
|
||||
Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fVerbose );
|
||||
Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
|
||||
else
|
||||
printf( "Unknown canonical form value (%d).\n", NpnType );
|
||||
fflush( stdout );
|
||||
|
|
|
|||
|
|
@ -86,6 +86,7 @@ struct Abc_ManRec_t_2
|
|||
Vec_Ptr_t * vNodes; // the temporary nodes
|
||||
Vec_Ptr_t * vTtTemps; // the truth tables for the internal nodes of the cut
|
||||
Vec_Ptr_t * vLabels; // temporary storage for AIG node labels
|
||||
Vec_Int_t * vLabelsInt; // temporary storage for AIG node labels
|
||||
Vec_Int_t * vUselessPos;
|
||||
// statistics
|
||||
int nTried; // the number of cuts tried
|
||||
|
|
@ -1144,6 +1145,7 @@ p->timeInsert += clock() - timeInsert;
|
|||
p->vNodes = Vec_PtrAlloc( 100 );
|
||||
p->vTtTemps = Vec_PtrAllocSimInfo( 1024, p->nWords );
|
||||
p->vLabels = Vec_PtrStart( 1000 );
|
||||
p->vLabelsInt = Vec_IntStart( 1000 );
|
||||
|
||||
|
||||
p->timeTotal += clock() - clkTotal;
|
||||
|
|
@ -2063,6 +2065,105 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
|
|||
return Hop_NotCond(pHopObj, (pCut->fCompl)^(((uCanonPhase & (1 << nLeaves)) > 0)) ^ fCompl);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derive the final network from the library.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_RecToGia2( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
Rec_Obj_t2 * pCandMin;
|
||||
int 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;
|
||||
int nVars = s_pMan->nVars;
|
||||
char pCanonPerm[16];
|
||||
unsigned *pInOut = s_pMan->pTemp1;
|
||||
unsigned *pTemp = s_pMan->pTemp2;
|
||||
int time = clock();
|
||||
int fCompl;
|
||||
int * pCompl = &fCompl;
|
||||
nLeaves = If_CutLeaveNum(pCut);
|
||||
// if (nLeaves < 3)
|
||||
// return Abc_NodeTruthToHop(pMan, pIfMan, pCut);
|
||||
Kit_TruthCopy(pInOut, If_CutTruth(pCut), pCut->nLimit);
|
||||
//special cases when cut-minimization return 2, that means there is only one leaf in the cut.
|
||||
if ((Kit_TruthIsConst0(pInOut, nLeaves) && pCut->fCompl == 0) || (Kit_TruthIsConst1(pInOut, nLeaves) && pCut->fCompl == 1))
|
||||
return 0;
|
||||
if ((Kit_TruthIsConst0(pInOut, nLeaves) && pCut->fCompl == 1) || (Kit_TruthIsConst1(pInOut, nLeaves) && pCut->fCompl == 0))
|
||||
return 1;
|
||||
if (Kit_TruthSupport(pInOut, nLeaves) != Kit_BitMask(nLeaves))
|
||||
{
|
||||
for (i = 0; i < nLeaves; i++)
|
||||
if(Kit_TruthVarInSupport( pInOut, nLeaves, i ))
|
||||
return Abc_LitNotCond( Vec_IntEntry(vLeaves, i), (pCut->fCompl ^ ((*pInOut & 0x01) > 0)) );
|
||||
}
|
||||
|
||||
for (i = 0; i < nLeaves; i++)
|
||||
pCanonPerm[i] = i;
|
||||
uCanonPhase = Kit_TruthSemiCanonicize_new(pInOut, pTemp, nLeaves, pCanonPerm);
|
||||
If_CutTruthStretch(pInOut, nLeaves, nVars);
|
||||
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);
|
||||
|
||||
// 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_IntClear( s_pMan->vLabelsInt );
|
||||
for (i = 0; i < nLeaves; i++)
|
||||
{
|
||||
pHopObj = Vec_IntEntry(vLeaves, pCanonPerm[i]);
|
||||
pHopObj = Abc_LitNotCond(pHopObj, ((uCanonPhase & (1 << i)) > 0));
|
||||
Vec_IntPush(s_pMan->vLabelsInt, 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 = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjNum(pAig, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
|
||||
else
|
||||
pFan0 = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
|
||||
pFan0 = Abc_LitNotCond(pFan0, Gia_ObjFaninC0(pGiaTemp));
|
||||
|
||||
if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
|
||||
pFan1 = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjNum(pAig, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
|
||||
else
|
||||
pFan1 = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
|
||||
pFan1 = Abc_LitNotCond(pFan1, Gia_ObjFaninC1(pGiaTemp));
|
||||
|
||||
if ( fHash )
|
||||
pHopObj = Gia_ManHashAnd(pMan, pFan0, pFan1);
|
||||
else
|
||||
pHopObj = Gia_ManAppendAnd(pMan, pFan0, pFan1);
|
||||
Vec_IntPush(s_pMan->vLabelsInt, pHopObj);
|
||||
}
|
||||
// get the final result
|
||||
if ( Gia_ObjIsAnd(pGiaObj) )
|
||||
pHopObj = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjNum(pAig, pGiaObj) + nLeaves);
|
||||
else if ( Gia_ObjIsPi(pAig, pGiaObj) )
|
||||
pHopObj = Vec_IntEntry(s_pMan->vLabelsInt, Gia_ObjCioId(pGiaObj));
|
||||
else assert( 0 );
|
||||
|
||||
s_pMan->timeIfDerive += clock() - time;
|
||||
s_pMan->timeIfTotal += clock() - time;
|
||||
// complement the result if needed
|
||||
return Abc_LitNotCond(pHopObj, (pCut->fCompl)^(((uCanonPhase & (1 << nLeaves)) > 0)) ^ fCompl);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the given record.]
|
||||
|
|
@ -2097,8 +2198,8 @@ void Abc_NtkRecStop2()
|
|||
ABC_FREE( s_pMan->pTemp2 );
|
||||
Vec_PtrFree( s_pMan->vNodes );
|
||||
Vec_PtrFree( s_pMan->vTtTemps );
|
||||
if ( s_pMan->vLabels )
|
||||
Vec_PtrFree( s_pMan->vLabels );
|
||||
Vec_PtrFree( s_pMan->vLabels );
|
||||
Vec_IntFree( s_pMan->vLabelsInt );
|
||||
//if(s_pMan->pMemObj)
|
||||
// Mem_FixedStop(s_pMan->pMemObj, 0);
|
||||
Vec_IntFree( s_pMan->vUselessPos);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -46,6 +46,7 @@ SRC += src/base/abci/abc.c \
|
|||
src/base/abci/abcQuant.c \
|
||||
src/base/abci/abcRec.c \
|
||||
src/base/abci/abcRec2.c \
|
||||
src/base/abci/abcRec3.c \
|
||||
src/base/abci/abcReconv.c \
|
||||
src/base/abci/abcReach.c \
|
||||
src/base/abci/abcRefactor.c \
|
||||
|
|
|
|||
|
|
@ -1654,9 +1654,10 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
char * pFileName;
|
||||
char * pLutStruct = NULL;
|
||||
int c, fSpecial = 0;
|
||||
int fUseHie = 0;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Sjh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Sjah" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -1677,6 +1678,9 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
case 'j':
|
||||
fSpecial ^= 1;
|
||||
break;
|
||||
case 'a':
|
||||
fUseHie ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
|
|
@ -1694,16 +1698,17 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
pFileName = argv[globalUtilOptind];
|
||||
// call the corresponding file writer
|
||||
if ( fSpecial || pLutStruct )
|
||||
Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName, pLutStruct );
|
||||
Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName, pLutStruct, fUseHie );
|
||||
else
|
||||
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: write_blif [-S str] [-jh] <file>\n" );
|
||||
fprintf( pAbc->Err, "usage: write_blif [-S str] [-jah] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
|
||||
fprintf( pAbc->Err, "\t-S str : string representing the LUT structure [default = %s]\n", pLutStruct ? pLutStruct : "not used" );
|
||||
fprintf( pAbc->Err, "\t-j : enables special BLIF writing [default = %s]\n", fSpecial? "yes" : "no" );;
|
||||
fprintf( pAbc->Err, "\t-a : enables hierarchical BLIF writing for LUT structures [default = %s]\n", fUseHie? "yes" : "no" );;
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
|
||||
return 1;
|
||||
|
|
@ -2734,17 +2739,22 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
char * pFileName;
|
||||
FILE * pFile;
|
||||
unsigned * pTruth;
|
||||
int nBytes;
|
||||
int fReverse = 0;
|
||||
int fBinary = 0;
|
||||
int c, i;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "rbh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'r':
|
||||
fReverse ^= 1;
|
||||
break;
|
||||
case 'b':
|
||||
fBinary ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
|
|
@ -2761,30 +2771,39 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables up to 16 inputs.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( Gia_ManPiNum(pAbc->pGia) < 3 )
|
||||
{
|
||||
Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables for 3 inputs or more.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( argc != globalUtilOptind + 1 )
|
||||
goto usage;
|
||||
// get the input file name
|
||||
pFileName = argv[globalUtilOptind];
|
||||
// convert to logic
|
||||
pFile = fopen( pFileName, "w" );
|
||||
pFile = fopen( pFileName, "wb" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
|
||||
return 0;
|
||||
}
|
||||
nBytes = 8 * Abc_Truth6WordNum( Gia_ManPiNum(pAbc->pGia) );
|
||||
Gia_ManForEachCo( pAbc->pGia, pObj, i )
|
||||
{
|
||||
pTruth = Gia_ObjComputeTruthTable( pAbc->pGia, pObj );
|
||||
Extra_PrintHex( pFile, pTruth, Gia_ManPiNum(pAbc->pGia) );
|
||||
fprintf( pFile, "\n" );
|
||||
if ( fBinary )
|
||||
fwrite( pTruth, nBytes, 1, pFile );
|
||||
else
|
||||
Extra_PrintHex( pFile, pTruth, Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
|
||||
}
|
||||
fclose( pFile );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: &write_truths [-rh] <file>\n" );
|
||||
fprintf( pAbc->Err, "usage: &write_truths [-rbh] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t writes truth tables of each PO of GIA manager into a file\n" );
|
||||
fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-b : toggle using binary format [default = %s]\n", fBinary? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -106,7 +106,7 @@ extern void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName );
|
|||
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
|
||||
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches, int fBb2Wb, int fSeq );
|
||||
extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
|
||||
extern void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct );
|
||||
extern void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct, int fUseHie );
|
||||
/*=== abcWriteBlifMv.c ==========================================================*/
|
||||
extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
|
||||
/*=== abcWriteBench.c =========================================================*/
|
||||
|
|
|
|||
|
|
@ -1272,7 +1272,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
|
|||
return 0;
|
||||
}
|
||||
*/
|
||||
if ( k == nEquals )
|
||||
if ( pName2 == NULL )
|
||||
{
|
||||
Abc_Obj_t * pNode = Abc_NtkCreateNode( p->pNtk );
|
||||
pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, " 0\n" );
|
||||
|
|
@ -1313,11 +1313,10 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
|
|||
return 0;
|
||||
}
|
||||
*/
|
||||
assert( pName2 != NULL );
|
||||
|
||||
// create the BI with the actual name
|
||||
pTerm = Abc_NtkCreateBo( p->pNtk );
|
||||
pNet = Abc_NtkFindOrCreateNet( p->pNtk, k == nEquals ? Abc_ObjNameSuffix(pTerm, "abc") : pName2 );
|
||||
pNet = Abc_NtkFindOrCreateNet( p->pNtk, pName2 == NULL ? Abc_ObjNameSuffix(pTerm, "abc") : pName2 );
|
||||
Abc_ObjAddFanin( pNet, pTerm );
|
||||
Abc_ObjAddFanin( pTerm, pBox );
|
||||
}
|
||||
|
|
|
|||
|
|
@ -514,6 +514,68 @@ void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode )
|
|||
fprintf( pFile, " %s", pName );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes the primary input list.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_NtkWriteSubcktFanins( FILE * pFile, Abc_Obj_t * pNode )
|
||||
{
|
||||
Abc_Obj_t * pNet;
|
||||
int LineLength;
|
||||
int AddedLength;
|
||||
int NameCounter;
|
||||
char * pName;
|
||||
int i;
|
||||
|
||||
LineLength = 6;
|
||||
NameCounter = 0;
|
||||
|
||||
// get the output name
|
||||
pName = Abc_ObjName(Abc_ObjFanout0(pNode));
|
||||
// get the line length after the output name is written
|
||||
AddedLength = strlen(pName) + 1;
|
||||
fprintf( pFile, " m%d", Abc_ObjId(pNode) );
|
||||
|
||||
// get the input names
|
||||
Abc_ObjForEachFanin( pNode, pNet, i )
|
||||
{
|
||||
// get the fanin name
|
||||
pName = Abc_ObjName(pNet);
|
||||
// get the line length after the fanin name is written
|
||||
AddedLength = strlen(pName) + 3;
|
||||
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
|
||||
{ // write the line extender
|
||||
fprintf( pFile, " \\\n" );
|
||||
// reset the line length
|
||||
LineLength = 0;
|
||||
NameCounter = 0;
|
||||
}
|
||||
fprintf( pFile, " %c=%s", 'a'+i, pName );
|
||||
LineLength += AddedLength;
|
||||
NameCounter++;
|
||||
}
|
||||
|
||||
// get the output name
|
||||
pName = Abc_ObjName(Abc_ObjFanout0(pNode));
|
||||
// get the line length after the output name is written
|
||||
AddedLength = strlen(pName) + 3;
|
||||
if ( NameCounter && LineLength + AddedLength > 75 )
|
||||
{ // write the line extender
|
||||
fprintf( pFile, " \\\n" );
|
||||
// reset the line length
|
||||
LineLength = 0;
|
||||
NameCounter = 0;
|
||||
}
|
||||
fprintf( pFile, " %c=%s", 'o', pName );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
@ -584,6 +646,26 @@ int Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length )
|
|||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the node into a file.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Io_NtkWriteNodeSubckt( FILE * pFile, Abc_Obj_t * pNode, int Length )
|
||||
{
|
||||
int RetValue = 0;
|
||||
fprintf( pFile, ".subckt" );
|
||||
Io_NtkWriteSubcktFanins( pFile, pNode );
|
||||
fprintf( pFile, "\n" );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes the timing info.]
|
||||
|
|
@ -1020,6 +1102,182 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov
|
|||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the node into a file.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_NtkWriteModelIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover, char * pStr )
|
||||
{
|
||||
Abc_Obj_t * pNet;
|
||||
int nLeaves = Abc_ObjFaninNum(pNode);
|
||||
int i, nLutLeaf, nLutLeaf2, nLutRoot, Length;
|
||||
|
||||
// write the header
|
||||
fprintf( pFile, "\n" );
|
||||
fprintf( pFile, ".model m%d\n", Abc_ObjId(pNode) );
|
||||
fprintf( pFile, ".inputs" );
|
||||
for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
|
||||
fprintf( pFile, " %c", 'a' + i );
|
||||
fprintf( pFile, "\n" );
|
||||
fprintf( pFile, ".outputs o\n" );
|
||||
|
||||
// quit if parameters are wrong
|
||||
Length = strlen(pStr);
|
||||
if ( Length != 2 && Length != 3 )
|
||||
{
|
||||
printf( "Wrong LUT struct (%s)\n", pStr );
|
||||
return;
|
||||
}
|
||||
for ( i = 0; i < Length; i++ )
|
||||
if ( pStr[i] - '0' < 3 || pStr[i] - '0' > 6 )
|
||||
{
|
||||
printf( "The LUT size (%d) should belong to {3,4,5,6}.\n", pStr[i] - '0' );
|
||||
return;
|
||||
}
|
||||
|
||||
nLutLeaf = pStr[0] - '0';
|
||||
nLutLeaf2 = ( Length == 3 ) ? pStr[1] - '0' : 0;
|
||||
nLutRoot = pStr[Length-1] - '0';
|
||||
if ( nLeaves > nLutLeaf - 1 + (nLutLeaf2 ? nLutLeaf2 - 1 : 0) + nLutRoot )
|
||||
{
|
||||
printf( "The node size (%d) is too large for the LUT structure %s.\n", nLeaves, pStr );
|
||||
return;
|
||||
}
|
||||
|
||||
// consider easy case
|
||||
if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) )
|
||||
{
|
||||
// write the .names line
|
||||
fprintf( pFile, ".names" );
|
||||
Abc_ObjForEachFanin( pNode, pNet, i )
|
||||
fprintf( pFile, " %c", 'a' + i );
|
||||
// get the output name
|
||||
fprintf( pFile, " %s\n", "o" );
|
||||
// write the cubes
|
||||
fprintf( pFile, "%s", (char*)Abc_ObjData(pNode) );
|
||||
fprintf( pFile, ".end\n" );
|
||||
return;
|
||||
}
|
||||
else
|
||||
{
|
||||
extern int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars );
|
||||
|
||||
static word TruthStore[16][1<<10] = {{0}}, * pTruths[16];
|
||||
word pCube[1<<10], pRes[1<<10], Func0, Func1, Func2;
|
||||
char pLut0[32], pLut1[32], pLut2[32] = {0}, * pSop;
|
||||
// int nVarsMin[3], pVars[3][20];
|
||||
|
||||
if ( TruthStore[0][0] == 0 )
|
||||
{
|
||||
static word Truth6[6] = {
|
||||
0xAAAAAAAAAAAAAAAA,
|
||||
0xCCCCCCCCCCCCCCCC,
|
||||
0xF0F0F0F0F0F0F0F0,
|
||||
0xFF00FF00FF00FF00,
|
||||
0xFFFF0000FFFF0000,
|
||||
0xFFFFFFFF00000000
|
||||
};
|
||||
int nVarsMax = 16;
|
||||
int nWordsMax = (1 << 10);
|
||||
int i, k;
|
||||
assert( nVarsMax <= 16 );
|
||||
for ( i = 0; i < nVarsMax; i++ )
|
||||
pTruths[i] = TruthStore[i];
|
||||
for ( i = 0; i < 6; i++ )
|
||||
for ( k = 0; k < nWordsMax; k++ )
|
||||
pTruths[i][k] = Truth6[i];
|
||||
for ( i = 6; i < nVarsMax; i++ )
|
||||
for ( k = 0; k < nWordsMax; k++ )
|
||||
pTruths[i][k] = ((k >> (i-6)) & 1) ? ~(word)0 : 0;
|
||||
}
|
||||
|
||||
// collect variables
|
||||
// Abc_ObjForEachFanin( pNode, pNet, i )
|
||||
// pVars[0][i] = pVars[1][i] = pVars[2][i] = i;
|
||||
|
||||
// derive truth table
|
||||
Abc_SopToTruthBig( (char*)Abc_ObjData(pNode), nLeaves, pTruths, pCube, pRes );
|
||||
if ( Kit_TruthIsConst0((unsigned *)pRes, nLeaves) || Kit_TruthIsConst1((unsigned *)pRes, nLeaves) )
|
||||
{
|
||||
fprintf( pFile, ".names %s\n %d\n", "o", Kit_TruthIsConst1((unsigned *)pRes, nLeaves) );
|
||||
fprintf( pFile, ".end\n" );
|
||||
return;
|
||||
}
|
||||
|
||||
// Extra_PrintHex( stdout, (unsigned *)pRes, nLeaves ); printf( " " );
|
||||
// Kit_DsdPrintFromTruth( (unsigned*)pRes, nLeaves ); printf( "\n" );
|
||||
|
||||
// perform decomposition
|
||||
if ( Length == 2 )
|
||||
{
|
||||
if ( !If_CluCheckExt( NULL, pRes, nLeaves, nLutLeaf, nLutRoot, pLut0, pLut1, &Func0, &Func1 ) )
|
||||
{
|
||||
Extra_PrintHex( stdout, (unsigned *)pRes, nLeaves ); printf( " " );
|
||||
Kit_DsdPrintFromTruth( (unsigned*)pRes, nLeaves ); printf( "\n" );
|
||||
printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
return;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( !If_CluCheckExt3( NULL, pRes, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, pLut0, pLut1, pLut2, &Func0, &Func1, &Func2 ) )
|
||||
{
|
||||
Extra_PrintHex( stdout, (unsigned *)pRes, nLeaves ); printf( " " );
|
||||
Kit_DsdPrintFromTruth( (unsigned*)pRes, nLeaves ); printf( "\n" );
|
||||
printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
// write leaf node
|
||||
fprintf( pFile, ".names" );
|
||||
for ( i = 0; i < pLut1[0]; i++ )
|
||||
fprintf( pFile, " %c", 'a' + pLut1[2+i] );
|
||||
fprintf( pFile, " lut1\n" );
|
||||
// write SOP
|
||||
pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func1, pLut1[0], vCover );
|
||||
fprintf( pFile, "%s", pSop );
|
||||
|
||||
if ( Length == 3 && pLut2[0] > 0 )
|
||||
{
|
||||
// write leaf node
|
||||
fprintf( pFile, ".names" );
|
||||
for ( i = 0; i < pLut2[0]; i++ )
|
||||
if ( pLut2[2+i] == nLeaves )
|
||||
fprintf( pFile, " lut1" );
|
||||
else
|
||||
fprintf( pFile, " %c", 'a' + pLut2[2+i] );
|
||||
fprintf( pFile, " lut2\n" );
|
||||
// write SOP
|
||||
pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func2, pLut2[0], vCover );
|
||||
fprintf( pFile, "%s", pSop );
|
||||
}
|
||||
|
||||
// write root node
|
||||
fprintf( pFile, ".names" );
|
||||
for ( i = 0; i < pLut0[0]; i++ )
|
||||
if ( pLut0[2+i] == nLeaves )
|
||||
fprintf( pFile, " lut1" );
|
||||
else if ( pLut0[2+i] == nLeaves+1 )
|
||||
fprintf( pFile, " lut2" );
|
||||
else
|
||||
fprintf( pFile, " %c", 'a' + pLut0[2+i] );
|
||||
fprintf( pFile, " %s\n", "o" );
|
||||
// write SOP
|
||||
pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, Func0, pLut0[0], vCover );
|
||||
fprintf( pFile, "%s", pSop );
|
||||
fprintf( pFile, ".end\n" );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the network into a BLIF file with the given name.]
|
||||
|
|
@ -1031,7 +1289,7 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
|
||||
void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct, int fUseHie )
|
||||
{
|
||||
FILE * pFile;
|
||||
Vec_Int_t * vCover;
|
||||
|
|
@ -1063,18 +1321,33 @@ void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
|
|||
Io_NtkWriteLatch( pFile, pLatch );
|
||||
if ( Abc_NtkLatchNum(pNtk) )
|
||||
fprintf( pFile, "\n" );
|
||||
// write each internal node
|
||||
// write the hierarchy
|
||||
vCover = Vec_IntAlloc( (1<<16) );
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
if ( fUseHie )
|
||||
{
|
||||
if ( pLutStruct )
|
||||
Io_NtkWriteNodeIntStruct( pFile, pNode, vCover, pLutStruct );
|
||||
else
|
||||
Io_NtkWriteNodeInt( pFile, pNode, vCover );
|
||||
// write each internal node
|
||||
fprintf( pFile, "\n" );
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
Io_NtkWriteNodeSubckt( pFile, pNode, 0 );
|
||||
fprintf( pFile, ".end\n\n" );
|
||||
// write models
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
Io_NtkWriteModelIntStruct( pFile, pNode, vCover, pLutStruct );
|
||||
fprintf( pFile, "\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
// write each internal node
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
{
|
||||
if ( pLutStruct )
|
||||
Io_NtkWriteNodeIntStruct( pFile, pNode, vCover, pLutStruct );
|
||||
else
|
||||
Io_NtkWriteNodeInt( pFile, pNode, vCover );
|
||||
}
|
||||
fprintf( pFile, ".end\n\n" );
|
||||
}
|
||||
Vec_IntFree( vCover );
|
||||
// write the end
|
||||
fprintf( pFile, ".end\n\n" );
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
|
|
@ -1089,7 +1362,7 @@ void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
|
||||
void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct, int fUseHie )
|
||||
{
|
||||
Abc_Ntk_t * pNtkTemp;
|
||||
assert( Abc_NtkIsLogic(pNtk) );
|
||||
|
|
@ -1101,7 +1374,10 @@ void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct )
|
|||
fprintf( stdout, "Writing BLIF has failed.\n" );
|
||||
return;
|
||||
}
|
||||
Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct );
|
||||
if ( pLutStruct && fUseHie )
|
||||
Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct, 1 );
|
||||
else
|
||||
Io_WriteBlifInt( pNtkTemp, FileName, pLutStruct, 0 );
|
||||
Abc_NtkDelete( pNtkTemp );
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -111,7 +111,7 @@ struct Abc_Frame_t_
|
|||
void * pAbc85Ntl2;
|
||||
void * pAbc85Best;
|
||||
void * pAbc85Delay;
|
||||
If_Lib_t * pAbc85Lib;
|
||||
// If_Lib_t * pAbc85Lib;
|
||||
|
||||
EXT_ABC_FRAME // plugin for external functionality
|
||||
};
|
||||
|
|
|
|||
|
|
@ -68,7 +68,8 @@ struct Kit_Node_t_
|
|||
Kit_Edge_t eEdge0; // the left child of the node
|
||||
Kit_Edge_t eEdge1; // the right child of the node
|
||||
// other info
|
||||
void * pFunc; // the function of the node (BDD or AIG)
|
||||
union { int iFunc; // the function of the node (BDD or AIG)
|
||||
void * pFunc; }; // the function of the node (BDD or AIG)
|
||||
unsigned Level : 14; // the level of this node in the global AIG
|
||||
// printing info
|
||||
unsigned fNodeOr : 1; // marks the original OR node
|
||||
|
|
@ -561,6 +562,7 @@ extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
|
|||
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
|
||||
extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
|
||||
/*=== kitHop.c ==========================================================*/
|
||||
//extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
|
||||
//extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
|
||||
//extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
|
||||
//extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@
|
|||
|
||||
#include "kit.h"
|
||||
#include "aig/hop/hop.h"
|
||||
#include "aig/gia/gia.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -32,6 +33,74 @@ ABC_NAMESPACE_IMPL_START
|
|||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Transforms the decomposition graph into the AIG.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Kit_GraphToGiaInternal( Gia_Man_t * pMan, Kit_Graph_t * pGraph, int fHash )
|
||||
{
|
||||
Kit_Node_t * pNode = NULL;
|
||||
int i, pAnd0, pAnd1;
|
||||
// check for constant function
|
||||
if ( Kit_GraphIsConst(pGraph) )
|
||||
return Abc_LitNotCond( 1, Kit_GraphIsComplement(pGraph) );
|
||||
// check for a literal
|
||||
if ( Kit_GraphIsVar(pGraph) )
|
||||
return Abc_LitNotCond( Kit_GraphVar(pGraph)->iFunc, Kit_GraphIsComplement(pGraph) );
|
||||
// build the AIG nodes corresponding to the AND gates of the graph
|
||||
Kit_GraphForEachNode( pGraph, pNode, i )
|
||||
{
|
||||
pAnd0 = Abc_LitNotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->iFunc, pNode->eEdge0.fCompl );
|
||||
pAnd1 = Abc_LitNotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->iFunc, pNode->eEdge1.fCompl );
|
||||
if ( fHash )
|
||||
pNode->iFunc = Gia_ManHashAnd( pMan, pAnd0, pAnd1 );
|
||||
else
|
||||
pNode->iFunc = Gia_ManAppendAnd( pMan, pAnd0, pAnd1 );
|
||||
}
|
||||
// complement the result if necessary
|
||||
return Abc_LitNotCond( pNode->iFunc, Kit_GraphIsComplement(pGraph) );
|
||||
}
|
||||
int Kit_GraphToGia( Gia_Man_t * pMan, Kit_Graph_t * pGraph, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
Kit_Node_t * pNode = NULL;
|
||||
int i;
|
||||
// collect the fanins
|
||||
Kit_GraphForEachLeaf( pGraph, pNode, i )
|
||||
pNode->iFunc = Vec_IntEntry( vLeaves, i );
|
||||
// perform strashing
|
||||
return Kit_GraphToGiaInternal( pMan, pGraph, fHash );
|
||||
}
|
||||
int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash )
|
||||
{
|
||||
int iLit;
|
||||
Kit_Graph_t * pGraph;
|
||||
// transform truth table into the decomposition tree
|
||||
if ( vMemory == NULL )
|
||||
{
|
||||
vMemory = Vec_IntAlloc( 0 );
|
||||
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
|
||||
Vec_IntFree( vMemory );
|
||||
}
|
||||
else
|
||||
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
|
||||
if ( pGraph == NULL )
|
||||
{
|
||||
printf( "Kit_TruthToGia(): Converting truth table to AIG has failed for function:\n" );
|
||||
Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
|
||||
}
|
||||
// derive the AIG for the decomposition tree
|
||||
iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash );
|
||||
Kit_GraphFree( pGraph );
|
||||
return iLit;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Transforms the decomposition graph into the AIG.]
|
||||
|
|
@ -64,18 +133,6 @@ Hop_Obj_t * Kit_GraphToHopInternal( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
|
|||
// complement the result if necessary
|
||||
return Hop_NotCond( (Hop_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Strashes one logic node using its SOP.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
|
||||
{
|
||||
Kit_Node_t * pNode = NULL;
|
||||
|
|
@ -86,18 +143,6 @@ Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
|
|||
// perform strashing
|
||||
return Kit_GraphToHopInternal( pMan, pGraph );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Strashed onen logic nodes using its truth table.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
|
||||
{
|
||||
Hop_Obj_t * pObj;
|
||||
|
|
|
|||
|
|
@ -1664,6 +1664,8 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
|
|||
|
||||
// canonicize output
|
||||
uCanonPhase = 0;
|
||||
for ( i = 0; i < nVars; i++ )
|
||||
pCanonPerm[i] = i;
|
||||
|
||||
nOnes = Kit_TruthCountOnes(pIn, nVars);
|
||||
//if(pIn[0] & 1)
|
||||
|
|
|
|||
|
|
@ -333,7 +333,7 @@ static inline void * If_ObjCopy( If_Obj_t * pObj ) { r
|
|||
static inline int If_ObjLevel( If_Obj_t * pObj ) { return pObj->Level; }
|
||||
static inline void If_ObjSetLevel( If_Obj_t * pObj, int Level ) { pObj->Level = Level; }
|
||||
static inline void If_ObjSetCopy( If_Obj_t * pObj, void * pCopy ) { pObj->pCopy = pCopy; }
|
||||
static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu; }
|
||||
static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { assert( pObj->Id > pEqu->Id ); pObj->pEquiv = pEqu; }
|
||||
|
||||
static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return &pObj->CutBest; }
|
||||
static inline unsigned If_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); }
|
||||
|
|
@ -353,8 +353,9 @@ static inline void If_CutSetDataInt( If_Cut_t * pCut, int Data ) { *
|
|||
static inline int If_CutLeaveNum( If_Cut_t * pCut ) { return pCut->nLeaves; }
|
||||
static inline int * If_CutLeaves( If_Cut_t * pCut ) { return pCut->pLeaves; }
|
||||
static inline unsigned * If_CutTruth( If_Cut_t * pCut ) { return pCut->pTruth; }
|
||||
static inline word * If_CutTruthW( If_Cut_t * pCut ) { return (word *)pCut->pTruth; }
|
||||
static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); }
|
||||
static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
|
||||
static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); }
|
||||
static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
|
||||
|
||||
static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { return pCut->fUser? (float)pCut->Cost : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves] : (float)1.0); }
|
||||
|
|
@ -505,8 +506,9 @@ extern void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, I
|
|||
extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
|
||||
/*=== ifTruth.c ===========================================================*/
|
||||
extern int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut );
|
||||
extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
|
||||
extern void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars );
|
||||
extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
|
||||
extern int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
|
||||
/*=== ifUtil.c ============================================================*/
|
||||
extern void If_ManCleanNodeCopy( If_Man_t * p );
|
||||
extern void If_ManCleanCutData( If_Man_t * p );
|
||||
|
|
@ -525,13 +527,18 @@ extern Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p );
|
|||
extern Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p );
|
||||
|
||||
extern int If_ManCountSpecialPos( If_Man_t * p );
|
||||
extern void If_CutTraverse( If_Man_t * p, If_Obj_t * pRoot, If_Cut_t * pCut, Vec_Ptr_t * vNodes );
|
||||
extern void If_ObjPrint( If_Obj_t * pObj );
|
||||
|
||||
/*=== abcRec.c ============================================================*/
|
||||
/*=== abcRec2.c ============================================================*/
|
||||
/*=== abcRec3.c ============================================================*/
|
||||
extern int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj);
|
||||
extern int If_CutDelayRecCost2(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj);
|
||||
/*=== abcRec2.c ============================================================*/
|
||||
extern int If_CutDelayRecCost3(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj);
|
||||
extern ABC_DLL int Abc_NtkRecIsRunning();
|
||||
extern ABC_DLL int Abc_NtkRecIsRunning2();
|
||||
extern ABC_DLL int Abc_NtkRecIsRunning3();
|
||||
|
||||
// othe packages
|
||||
extern int Bat_ManCellFuncLookup( unsigned * pTruth, int nVars, int nLeaves );
|
||||
|
|
|
|||
|
|
@ -337,6 +337,7 @@ void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
|
|||
// mark the largest level
|
||||
if ( p->nLevelMax < (int)pObj->Level )
|
||||
p->nLevelMax = (int)pObj->Level;
|
||||
p->nChoices++;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -410,8 +411,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
|
|||
// set up elementary truth table of the unit cut
|
||||
if ( p->pPars->fTruth )
|
||||
{
|
||||
int i, nTruthWords;
|
||||
nTruthWords = pCut->nLimit <= 5 ? 1 : (1 << (pCut->nLimit - 5));
|
||||
int i, nTruthWords = If_CutTruthWords(pCut->nLimit);
|
||||
for ( i = 0; i < nTruthWords; i++ )
|
||||
If_CutTruth(pCut)[i] = 0xAAAAAAAA;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -75,7 +75,8 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry )
|
|||
Delay = IF_MAX( Delay, Pin2Pin[fCarry][i] + DelayCur );
|
||||
}
|
||||
return Delay;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
@ -157,12 +158,13 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
|
|||
/// pCut->Delay = If_CutDelayLutStruct( p, pCut, p->pPars->pLutStruct, p->pPars->WireDelay );
|
||||
if ( p->pPars->fUserRecLib )
|
||||
{
|
||||
if((Abc_NtkRecIsRunning2()&& Abc_NtkRecIsRunning()) || (!Abc_NtkRecIsRunning2()&& !Abc_NtkRecIsRunning()))
|
||||
assert(0);
|
||||
else if(Abc_NtkRecIsRunning())
|
||||
pCut->Delay = If_CutDelayRecCost(p, pCut, pObj);
|
||||
assert( Abc_NtkRecIsRunning() + Abc_NtkRecIsRunning2() + Abc_NtkRecIsRunning3() == 1 );
|
||||
if ( Abc_NtkRecIsRunning3() )
|
||||
pCut->Delay = If_CutDelayRecCost3(p, pCut, pObj);
|
||||
else if( Abc_NtkRecIsRunning2() )
|
||||
pCut->Delay = If_CutDelayRecCost2(p, pCut, pObj);
|
||||
else
|
||||
pCut->Delay = If_CutDelayRecCost2(p, pCut, pObj);
|
||||
pCut->Delay = If_CutDelayRecCost(p, pCut, pObj);
|
||||
}
|
||||
else if(p->pPars->fDelayOpt)
|
||||
pCut->Delay = If_CutDelaySopCost(p,pCut);
|
||||
|
|
@ -211,8 +213,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
|
|||
if ( p->pPars->fTruth )
|
||||
{
|
||||
// clock_t clk = clock();
|
||||
int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
|
||||
// int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
|
||||
int RetValue = If_CutComputeTruth2( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
|
||||
// p->timeTruth += clock() - clk;
|
||||
|
||||
pCut->fUseless = 0;
|
||||
if ( p->pPars->pFuncCell && RetValue < 2 )
|
||||
{
|
||||
|
|
@ -236,12 +240,13 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
|
|||
/// pCut->Delay = If_CutDelayLutStruct( p, pCut, p->pPars->pLutStruct, p->pPars->WireDelay );
|
||||
if ( p->pPars->fUserRecLib )
|
||||
{
|
||||
if((Abc_NtkRecIsRunning2()&& Abc_NtkRecIsRunning()) || (!Abc_NtkRecIsRunning2()&& !Abc_NtkRecIsRunning()))
|
||||
assert(0);
|
||||
else if(Abc_NtkRecIsRunning())
|
||||
pCut->Delay = If_CutDelayRecCost(p, pCut, pObj);
|
||||
else
|
||||
assert( Abc_NtkRecIsRunning() + Abc_NtkRecIsRunning2() + Abc_NtkRecIsRunning3() == 1 );
|
||||
if ( Abc_NtkRecIsRunning3() )
|
||||
pCut->Delay = If_CutDelayRecCost3(p, pCut, pObj);
|
||||
else if( Abc_NtkRecIsRunning2() )
|
||||
pCut->Delay = If_CutDelayRecCost2(p, pCut, pObj);
|
||||
else
|
||||
pCut->Delay = If_CutDelayRecCost(p, pCut, pObj);
|
||||
}
|
||||
else if (p->pPars->fDelayOpt)
|
||||
pCut->Delay = If_CutDelaySopCost(p, pCut);
|
||||
|
|
@ -263,6 +268,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
|
|||
pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
|
||||
// insert the cut into storage
|
||||
If_CutSort( p, pCutSet, pCut );
|
||||
// If_CutTraverse( p, pObj, pCut );
|
||||
}
|
||||
assert( pCutSet->nCuts > 0 );
|
||||
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "if.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -43,29 +44,28 @@ ABC_NAMESPACE_IMPL_START
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int If_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
|
||||
static inline void If_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
|
||||
{
|
||||
int w;
|
||||
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
|
||||
for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
|
||||
pOut[w] = ~pIn[w];
|
||||
}
|
||||
static inline void If_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
|
||||
{
|
||||
int w;
|
||||
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
|
||||
for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
|
||||
pOut[w] = pIn[w];
|
||||
}
|
||||
static inline void If_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
|
||||
{
|
||||
int w;
|
||||
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
|
||||
for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
|
||||
pOut[w] = ~(pIn0[w] & pIn1[w]);
|
||||
}
|
||||
static inline void If_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
|
||||
{
|
||||
int w;
|
||||
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
|
||||
for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
|
||||
pOut[w] = pIn0[w] & pIn1[w];
|
||||
}
|
||||
|
||||
|
|
@ -89,7 +89,7 @@ void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int i
|
|||
{ 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
|
||||
{ 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
|
||||
};
|
||||
int nWords = If_TruthWordNum( nVars );
|
||||
int nWords = If_CutTruthWords( nVars );
|
||||
int i, k, Step, Shift;
|
||||
|
||||
assert( iVar < nVars - 1 );
|
||||
|
|
@ -245,7 +245,7 @@ void If_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, u
|
|||
***********************************************************************/
|
||||
int If_CutTruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
|
||||
{
|
||||
int nWords = If_TruthWordNum( nVars );
|
||||
int nWords = If_CutTruthWords( nVars );
|
||||
int i, k, Step;
|
||||
|
||||
assert( iVar < nVars );
|
||||
|
|
@ -449,6 +449,191 @@ int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut )
|
|||
}
|
||||
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs truth table computation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut )
|
||||
{
|
||||
unsigned uSupport;
|
||||
int i, k, nSuppSize;
|
||||
int nVars = If_CutLeaveNum(pCut);
|
||||
// compute the support of the cut's function
|
||||
uSupport = Abc_Tt6SupportAndSize( *If_CutTruthW(pCut), nVars, &nSuppSize );
|
||||
if ( nSuppSize == If_CutLeaveNum(pCut) )
|
||||
return 0;
|
||||
// TEMPORARY
|
||||
if ( nSuppSize < 2 )
|
||||
{
|
||||
p->nSmallSupp++;
|
||||
return 2;
|
||||
}
|
||||
// update leaves and signature
|
||||
pCut->uSign = 0;
|
||||
for ( i = k = 0; i < nVars; i++ )
|
||||
{
|
||||
if ( !(uSupport & (1 << i)) )
|
||||
continue;
|
||||
pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
|
||||
if ( k < i )
|
||||
{
|
||||
pCut->pLeaves[k] = pCut->pLeaves[i];
|
||||
Abc_TtSwapVars( If_CutTruthW(pCut), pCut->nLimit, k, i );
|
||||
}
|
||||
k++;
|
||||
}
|
||||
assert( k == nSuppSize );
|
||||
pCut->nLeaves = nSuppSize;
|
||||
// verify the result
|
||||
// assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
|
||||
return 1;
|
||||
}
|
||||
static inline word If_TruthStretch6( word Truth, If_Cut_t * pCut, If_Cut_t * pCut0 )
|
||||
{
|
||||
int i, k;
|
||||
for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
|
||||
{
|
||||
if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
|
||||
continue;
|
||||
assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
|
||||
if ( k < i )
|
||||
Abc_TtSwapVars( &Truth, pCut->nLimit, k, i );
|
||||
k--;
|
||||
}
|
||||
return Truth;
|
||||
}
|
||||
static inline int If_CutComputeTruth6( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
|
||||
{
|
||||
word t0 = (fCompl0 ^ pCut0->fCompl) ? ~*If_CutTruthW(pCut0) : *If_CutTruthW(pCut0);
|
||||
word t1 = (fCompl1 ^ pCut1->fCompl) ? ~*If_CutTruthW(pCut1) : *If_CutTruthW(pCut1);
|
||||
assert( pCut->nLimit <= 6 );
|
||||
t0 = If_TruthStretch6( t0, pCut, pCut0 );
|
||||
t1 = If_TruthStretch6( t1, pCut, pCut1 );
|
||||
*If_CutTruthW(pCut) = t0 & t1;
|
||||
if ( p->pPars->fCutMin )
|
||||
return If_CutTruthMinimize6( p, pCut );
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs truth table computation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
// this procedure handles special case reductions
|
||||
static inline int If_CutTruthMinimize21( If_Man_t * p, If_Cut_t * pCut )
|
||||
{
|
||||
word * pTruth = If_CutTruthW(pCut);
|
||||
int i, k, nVars = If_CutLeaveNum(pCut);
|
||||
unsigned uSign = 0;
|
||||
for ( i = k = 0; i < nVars; i++ )
|
||||
{
|
||||
if ( !Abc_TtHasVar( pTruth, nVars, i ) )
|
||||
continue;
|
||||
uSign |= If_ObjCutSign( pCut->pLeaves[i] );
|
||||
if ( k < i )
|
||||
{
|
||||
pCut->pLeaves[k] = pCut->pLeaves[i];
|
||||
Abc_TtSwapVars( pTruth, nVars, k, i );
|
||||
}
|
||||
k++;
|
||||
}
|
||||
if ( k == nVars )
|
||||
return 0;
|
||||
assert( k < nVars );
|
||||
pCut->nLeaves = k;
|
||||
pCut->uSign = uSign;
|
||||
// TEMPORARY
|
||||
if ( pCut->nLeaves < 2 )
|
||||
{
|
||||
p->nSmallSupp++;
|
||||
return 2;
|
||||
}
|
||||
// verify the result
|
||||
assert( If_CutLeaveNum(pCut) == Abc_TtSupportSize(pTruth, nVars) );
|
||||
return 1;
|
||||
}
|
||||
static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut )
|
||||
{
|
||||
unsigned uSupport;
|
||||
int i, k, nSuppSize;
|
||||
int nVars = If_CutLeaveNum(pCut);
|
||||
// compute the support of the cut's function
|
||||
uSupport = Abc_TtSupportAndSize( If_CutTruthW(pCut), nVars, &nSuppSize );
|
||||
if ( nSuppSize == If_CutLeaveNum(pCut) )
|
||||
return 0;
|
||||
// TEMPORARY
|
||||
if ( nSuppSize < 2 )
|
||||
{
|
||||
p->nSmallSupp++;
|
||||
return 2;
|
||||
}
|
||||
// update leaves and signature
|
||||
pCut->uSign = 0;
|
||||
for ( i = k = 0; i < nVars; i++ )
|
||||
{
|
||||
if ( !(uSupport & (1 << i)) )
|
||||
continue;
|
||||
pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
|
||||
if ( k < i )
|
||||
{
|
||||
pCut->pLeaves[k] = pCut->pLeaves[i];
|
||||
Abc_TtSwapVars( If_CutTruthW(pCut), pCut->nLimit, k, i );
|
||||
}
|
||||
k++;
|
||||
}
|
||||
assert( k == nSuppSize );
|
||||
pCut->nLeaves = nSuppSize;
|
||||
// verify the result
|
||||
// assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
|
||||
return 1;
|
||||
}
|
||||
static inline void If_TruthStretch2( word * pTruth, If_Cut_t * pCut, If_Cut_t * pCut0 )
|
||||
{
|
||||
int i, k;
|
||||
for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
|
||||
{
|
||||
if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
|
||||
continue;
|
||||
assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
|
||||
if ( k < i )
|
||||
Abc_TtSwapVars( pTruth, pCut->nLimit, k, i );
|
||||
k--;
|
||||
}
|
||||
}
|
||||
inline int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
|
||||
{
|
||||
int nWords;
|
||||
if ( pCut->nLimit < 7 )
|
||||
return If_CutComputeTruth6( p, pCut, pCut0, pCut1, fCompl0, fCompl1 );
|
||||
nWords = Abc_TtWordNum( pCut->nLimit );
|
||||
Abc_TtCopy( (word *)p->puTemp[0], If_CutTruthW(pCut0), nWords, fCompl0 ^ pCut0->fCompl );
|
||||
Abc_TtCopy( (word *)p->puTemp[1], If_CutTruthW(pCut1), nWords, fCompl1 ^ pCut1->fCompl );
|
||||
If_TruthStretch2( (word *)p->puTemp[0], pCut, pCut0 );
|
||||
If_TruthStretch2( (word *)p->puTemp[1], pCut, pCut1 );
|
||||
Abc_TtAnd( If_CutTruthW(pCut), (word *)p->puTemp[0], (word *)p->puTemp[1], nWords, 0 );
|
||||
if ( p->pPars->fCutMin )
|
||||
return If_CutTruthMinimize2( p, pCut );
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -769,6 +769,90 @@ int If_ManCountSpecialPos( If_Man_t * p )
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Traverse the cut and counts its volume.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static void If_CutTraverse_rec( If_Obj_t * pNode, Vec_Ptr_t * vNodes )
|
||||
{
|
||||
if ( pNode->fMark )
|
||||
return;
|
||||
pNode->fMark = 1;
|
||||
// assert( !If_ObjIsCi(pNode) ); // does not hold with cut minimization
|
||||
if ( If_ObjIsAnd(pNode) )
|
||||
If_CutTraverse_rec( If_ObjFanin0(pNode), vNodes );
|
||||
if ( If_ObjIsAnd(pNode) )
|
||||
If_CutTraverse_rec( If_ObjFanin1(pNode), vNodes );
|
||||
Vec_PtrPush( vNodes, pNode );
|
||||
}
|
||||
void If_CutTraverse( If_Man_t * p, If_Obj_t * pRoot, If_Cut_t * pCut, Vec_Ptr_t * vNodes )
|
||||
{
|
||||
If_Obj_t * pLeaf;
|
||||
int i;
|
||||
// collect the internal nodes of the cut
|
||||
Vec_PtrClear( vNodes );
|
||||
If_CutForEachLeaf( p, pCut, pLeaf, i )
|
||||
{
|
||||
Vec_PtrPush( vNodes, pLeaf );
|
||||
assert( pLeaf->fMark == 0 );
|
||||
pLeaf->fMark = 1;
|
||||
}
|
||||
// collect other nodes
|
||||
If_CutTraverse_rec( pRoot, vNodes );
|
||||
// clean the mark
|
||||
Vec_PtrForEachEntry( If_Obj_t *, vNodes, pLeaf, i )
|
||||
pLeaf->fMark = 0;
|
||||
}
|
||||
void If_CutTraverseTest( If_Man_t * p, If_Obj_t * pRoot, If_Cut_t * pCut )
|
||||
{
|
||||
Vec_Ptr_t * vNodes;
|
||||
vNodes = Vec_PtrAlloc( 1000 );
|
||||
If_CutTraverse( p, pRoot, pCut, vNodes );
|
||||
//if ( Vec_PtrSize(vNodes) > 30 )
|
||||
//printf( "%d ", Vec_PtrSize(vNodes) );
|
||||
Vec_PtrFree( vNodes );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void If_ObjPrint( If_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj == NULL )
|
||||
{
|
||||
printf( "Object is NULL." );
|
||||
return;
|
||||
}
|
||||
printf( "Obj %4d : ", If_ObjId(pObj) );
|
||||
if ( If_ObjIsConst1(pObj) )
|
||||
printf( "constant 1" );
|
||||
else if ( If_ObjIsCi(pObj) )
|
||||
printf( "PI" );
|
||||
else if ( If_ObjIsCo(pObj) )
|
||||
printf( "PO( %4d%s )", If_ObjId(If_ObjFanin0(pObj)), (If_ObjFaninC0(pObj)? "\'" : " ") );
|
||||
else
|
||||
printf( "AND( %4d%s, %4d%s )",
|
||||
If_ObjId(If_ObjFanin0(pObj)), (If_ObjFaninC0(pObj)? "\'" : " "),
|
||||
If_ObjId(If_ObjFanin1(pObj)), (If_ObjFaninC1(pObj)? "\'" : " ") );
|
||||
printf( " (refs = %3d)", pObj->nVisitsCopy );
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -109,6 +109,7 @@ static inline void Abc_SclTimeNodePrint( SC_Man * p, Abc_Obj_t * pObj, int fRise
|
|||
{
|
||||
printf( "%7d : ", Abc_ObjId(pObj) );
|
||||
printf( "%d ", Abc_ObjFaninNum(pObj) );
|
||||
printf( "%d ", Abc_ObjFanoutNum(pObj) );
|
||||
printf( "%-*s ", Length, Abc_SclObjCell(p, pObj)->pName );
|
||||
if ( fRise >= 0 )
|
||||
printf( "(%s) ", fRise ? "rise" : "fall" );
|
||||
|
|
|
|||
|
|
@ -52,9 +52,11 @@
|
|||
#endif
|
||||
|
||||
// catch memory leaks in Visual Studio
|
||||
#ifdef _DEBUG
|
||||
#define _CRTDBG_MAP_ALLOC
|
||||
#include <crtdbg.h>
|
||||
#ifdef WIN32
|
||||
#ifdef _DEBUG
|
||||
#define _CRTDBG_MAP_ALLOC
|
||||
#include <crtdbg.h>
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#if !defined(___unused)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,422 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [utilTruth.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Truth table manipulation.]
|
||||
|
||||
Synopsis [Truth table manipulation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - October 28, 2012.]
|
||||
|
||||
Revision [$Id: utilTruth.h,v 1.00 2012/10/28 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__misc__util__utilTruth_h
|
||||
#define ABC__misc__util__utilTruth_h
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static word s_Truths6[6] = {
|
||||
0xAAAAAAAAAAAAAAAA,
|
||||
0xCCCCCCCCCCCCCCCC,
|
||||
0xF0F0F0F0F0F0F0F0,
|
||||
0xFF00FF00FF00FF00,
|
||||
0xFFFF0000FFFF0000,
|
||||
0xFFFFFFFF00000000
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
|
||||
{
|
||||
int w;
|
||||
if ( fCompl )
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pOut[w] = ~pIn[w];
|
||||
else
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pOut[w] = pIn[w];
|
||||
}
|
||||
static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
|
||||
{
|
||||
int w;
|
||||
if ( fCompl )
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pOut[w] = ~(pIn1[w] & pIn2[w]);
|
||||
else
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pOut[w] = pIn1[w] & pIn2[w];
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtSuppIsMinBase( int Supp )
|
||||
{
|
||||
return (Supp & (Supp+1)) == 0;
|
||||
}
|
||||
static inline int Abc_Tt6HasVar( word t, int iVar )
|
||||
{
|
||||
return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]);
|
||||
}
|
||||
static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
|
||||
{
|
||||
int nWords = Abc_TtWordNum( nVars );
|
||||
assert( iVar < nVars );
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i, Shift = (1 << iVar);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != t[Step+i] )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtSupport( word * t, int nVars )
|
||||
{
|
||||
int v, Supp = 0;
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtHasVar( t, nVars, v ) )
|
||||
Supp |= (1 << v);
|
||||
return Supp;
|
||||
}
|
||||
static inline int Abc_TtSupportSize( word * t, int nVars )
|
||||
{
|
||||
int v, SuppSize = 0;
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtHasVar( t, nVars, v ) )
|
||||
SuppSize++;
|
||||
return SuppSize;
|
||||
}
|
||||
static inline int Abc_TtSupportAndSize( word * t, int nVars, int * pSuppSize )
|
||||
{
|
||||
int v, Supp = 0;
|
||||
*pSuppSize = 0;
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtHasVar( t, nVars, v ) )
|
||||
Supp |= (1 << v), (*pSuppSize)++;
|
||||
return Supp;
|
||||
}
|
||||
static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
|
||||
{
|
||||
int v, Supp = 0;
|
||||
*pSuppSize = 0;
|
||||
assert( nVars <= 6 );
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_Tt6HasVar( t, v ) )
|
||||
Supp |= (1 << v), (*pSuppSize)++;
|
||||
return Supp;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
|
||||
{
|
||||
static word PPMasks[5][6][3] = {
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0
|
||||
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1
|
||||
{ 0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050 }, // 0 2
|
||||
{ 0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 }, // 0 3
|
||||
{ 0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 }, // 0 4
|
||||
{ 0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 } // 0 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 1
|
||||
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, // 1 2
|
||||
{ 0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 }, // 1 3
|
||||
{ 0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 }, // 1 4
|
||||
{ 0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 } // 1 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 2
|
||||
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, // 2 3
|
||||
{ 0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 }, // 2 4
|
||||
{ 0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 } // 2 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 2
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 3
|
||||
{ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, // 3 4
|
||||
{ 0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 } // 3 5
|
||||
},
|
||||
{
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 0
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 1
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 2
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 3
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 4
|
||||
{ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } // 4 5
|
||||
}
|
||||
};
|
||||
if ( iVar == jVar )
|
||||
return;
|
||||
if ( jVar < iVar )
|
||||
ABC_SWAP( int, iVar, jVar );
|
||||
assert( iVar < jVar && jVar < nVars );
|
||||
if ( nVars <= 6 )
|
||||
{
|
||||
word * pMasks = PPMasks[iVar][jVar];
|
||||
int shift = (1 << jVar) - (1 << iVar);
|
||||
pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( jVar <= 5 )
|
||||
{
|
||||
word * pMasks = PPMasks[iVar][jVar];
|
||||
int nWords = Abc_TtWordNum(nVars);
|
||||
int w, shift = (1 << jVar) - (1 << iVar);
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
|
||||
}
|
||||
else if ( iVar <= 5 && jVar > 5 )
|
||||
{
|
||||
word low2High, high2Low;
|
||||
word * pLimit = pTruth + Abc_TtWordNum(nVars);
|
||||
int j, jStep = Abc_TtWordNum(jVar);
|
||||
int shift = 1 << iVar;
|
||||
for ( ; pTruth < pLimit; pTruth += 2*jStep )
|
||||
for ( j = 0; j < jStep; j++ )
|
||||
{
|
||||
low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
|
||||
high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
|
||||
pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
|
||||
pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
word temp, * pLimit = pTruth + Abc_TtWordNum(nVars);
|
||||
int i, iStep = Abc_TtWordNum(iVar);
|
||||
int j, jStep = Abc_TtWordNum(jVar);
|
||||
for ( ; pTruth < pLimit; pTruth += 2*jStep )
|
||||
for ( i = 0; i < jStep; i += 2*iStep )
|
||||
for ( j = 0; j < iStep; j++ )
|
||||
{
|
||||
temp = pTruth[iStep + i + j];
|
||||
pTruth[iStep + i + j] = pTruth[jStep + i + j];
|
||||
pTruth[jStep + i + j] = temp;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar )
|
||||
{
|
||||
static word PPMasks[6][6] = {
|
||||
{ 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
|
||||
{ 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
|
||||
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
|
||||
};
|
||||
if ( nVars <= 6 )
|
||||
{
|
||||
int shift;
|
||||
word low2High, high2Low;
|
||||
assert( iVar <= 5 && jVar <= 5 && iVar < jVar );
|
||||
shift = (1 << jVar) - (1 << iVar);
|
||||
low2High = (pTruth[0] & PPMasks[iVar][jVar - 1] ) << shift;
|
||||
pTruth[0] &= ~PPMasks[iVar][jVar - 1];
|
||||
high2Low = (pTruth[0] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
|
||||
pTruth[0] &= ~(PPMasks[iVar][jVar - 1] << shift);
|
||||
pTruth[0] |= low2High | high2Low;
|
||||
}
|
||||
else
|
||||
{
|
||||
word low2High, high2Low, temp;
|
||||
int nWords = Abc_TtWordNum(nVars);
|
||||
int shift, step, iStep, jStep;
|
||||
int w = 0, i = 0, j = 0;
|
||||
if ( iVar == jVar )
|
||||
return;
|
||||
if ( jVar < iVar )
|
||||
ABC_SWAP( int, iVar, jVar );
|
||||
if ( iVar <= 5 && jVar <= 5 )
|
||||
{
|
||||
shift = (1 << jVar) - (1 << iVar);
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
{
|
||||
low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
|
||||
pTruth[w] &= ~PPMasks[iVar][jVar - 1];
|
||||
high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
|
||||
pTruth[w] &= ~(PPMasks[iVar][jVar - 1] << shift);
|
||||
pTruth[w] |= low2High | high2Low;
|
||||
}
|
||||
}
|
||||
else if ( iVar <= 5 && jVar > 5 )
|
||||
{
|
||||
step = Abc_TtWordNum(jVar + 1)/2;
|
||||
shift = 1 << iVar;
|
||||
for ( w = 0; w < nWords; w += 2*step )
|
||||
{
|
||||
for (j = 0; j < step; j++)
|
||||
{
|
||||
low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
|
||||
pTruth[w + j] &= ~PPMasks[iVar][5];
|
||||
high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
|
||||
pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
|
||||
pTruth[w + j] |= high2Low;
|
||||
pTruth[w + step + j] |= low2High;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
iStep = Abc_TtWordNum(iVar + 1)/2;
|
||||
jStep = Abc_TtWordNum(jVar + 1)/2;
|
||||
for (w = 0; w < nWords; w += 2*jStep)
|
||||
{
|
||||
for (i = 0; i < jStep; i += 2*iStep)
|
||||
{
|
||||
for (j = 0; j < iStep; j++)
|
||||
{
|
||||
temp = pTruth[w + iStep + i + j];
|
||||
pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
|
||||
pTruth[w + jStep + i + j] = temp;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Stretch truthtable to have more input variables.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
|
||||
{
|
||||
int w, i, step, nWords;
|
||||
if ( nVarS == nVarB )
|
||||
return;
|
||||
assert( nVarS < nVarB );
|
||||
step = Abc_TruthWordNum(nVarS);
|
||||
nWords = Abc_TruthWordNum(nVarB);
|
||||
if ( step == nWords )
|
||||
return;
|
||||
assert( step < nWords );
|
||||
for ( w = 0; w < nWords; w += step )
|
||||
for ( i = 0; i < step; i++ )
|
||||
pInOut[w + i] = pInOut[i];
|
||||
}
|
||||
static void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
|
||||
{
|
||||
int w, i, step, nWords;
|
||||
if ( nVarS == nVarB )
|
||||
return;
|
||||
assert( nVarS < nVarB );
|
||||
step = Abc_Truth6WordNum(nVarS);
|
||||
nWords = Abc_Truth6WordNum(nVarB);
|
||||
if ( step == nWords )
|
||||
return;
|
||||
assert( step < nWords );
|
||||
for ( w = 0; w < nWords; w += step )
|
||||
for ( i = 0; i < step; i++ )
|
||||
pInOut[w + i] = pInOut[i];
|
||||
}
|
||||
|
||||
/*=== utilTruth.c ===========================================================*/
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
@ -57,14 +57,16 @@ struct Vec_Mem_t_
|
|||
int nPageAlloc; // number of pages currently allocated
|
||||
int iPage; // the number of a page currently used
|
||||
word ** ppPages; // memory pages
|
||||
Vec_Int_t * vTable; // hash table
|
||||
Vec_Int_t * vNexts; // next pointers
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#define Vec_MemForEachEntry( vVec, pEntry, i ) \
|
||||
for ( i = 0; (i < Vec_MemEntryNum(vVec)) && ((pEntry) = Vec_MemReadEntry(vVec, i)); i++ )
|
||||
#define Vec_MemForEachEntry( p, pEntry, i ) \
|
||||
for ( i = 0; (i < Vec_MemEntryNum(p)) && ((pEntry) = Vec_MemReadEntry(p, i)); i++ )
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
|
|
@ -266,12 +268,12 @@ static inline void Vec_MemShrink( Vec_Mem_t * p, int nEntriesNew )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_MemPrint( Vec_Mem_t * vVec )
|
||||
static inline void Vec_MemPrint( Vec_Mem_t * p )
|
||||
{
|
||||
word * pEntry;
|
||||
int i;
|
||||
printf( "Memory vector has %d entries: ", Vec_MemEntryNum(vVec) );
|
||||
Vec_MemForEachEntry( vVec, pEntry, i )
|
||||
printf( "Memory vector has %d entries: ", Vec_MemEntryNum(p) );
|
||||
Vec_MemForEachEntry( p, pEntry, i )
|
||||
{
|
||||
printf( "%3d : ", i );
|
||||
// add printout here
|
||||
|
|
@ -279,6 +281,76 @@ static inline void Vec_MemPrint( Vec_Mem_t * vVec )
|
|||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Hashing entries in the memory vector.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_MemHashAlloc( Vec_Mem_t * p, int nTableSize )
|
||||
{
|
||||
assert( p->vTable == NULL && p->vNexts == NULL );
|
||||
p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nTableSize) );
|
||||
p->vNexts = Vec_IntAlloc( nTableSize );
|
||||
}
|
||||
static inline void Vec_MemHashFree( Vec_Mem_t * p )
|
||||
{
|
||||
Vec_IntFreeP( &p->vTable );
|
||||
Vec_IntFreeP( &p->vNexts );
|
||||
}
|
||||
static inline unsigned Vec_MemHashKey( Vec_Mem_t * p, word * pEntry )
|
||||
{
|
||||
static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
|
||||
int i, nData = 2 * p->nEntrySize;
|
||||
unsigned * pData = (unsigned *)pEntry;
|
||||
unsigned uHash = 0;
|
||||
for ( i = 0; i < nData; i++ )
|
||||
uHash += pData[i] * s_Primes[i & 0x7];
|
||||
return uHash % Vec_IntSize(p->vTable);
|
||||
}
|
||||
static int * Vec_MemHashLookup( Vec_Mem_t * p, word * pEntry )
|
||||
{
|
||||
int * pSpot = Vec_IntEntryP( p->vTable, Vec_MemHashKey(p, pEntry) );
|
||||
for ( ; *pSpot != -1; pSpot = Vec_IntEntryP(p->vNexts, *pSpot) )
|
||||
if ( !memcmp( Vec_MemReadEntry(p, *pSpot), pEntry, sizeof(word) * p->nEntrySize ) ) // equal
|
||||
return pSpot;
|
||||
return pSpot;
|
||||
}
|
||||
static void Vec_MemHashResize( Vec_Mem_t * p )
|
||||
{
|
||||
word * pEntry;
|
||||
int i, * pSpot;
|
||||
Vec_IntFill( p->vTable, Abc_PrimeCudd(2 * Vec_IntSize(p->vTable)), -1 );
|
||||
Vec_IntClear( p->vNexts );
|
||||
Vec_MemForEachEntry( p, pEntry, i )
|
||||
{
|
||||
pSpot = Vec_MemHashLookup( p, pEntry );
|
||||
assert( *pSpot == -1 );
|
||||
*pSpot = Vec_IntSize(p->vNexts);
|
||||
Vec_IntPush( p->vNexts, -1 );
|
||||
}
|
||||
assert( p->nEntries == Vec_IntSize(p->vNexts) );
|
||||
}
|
||||
static int Vec_MemHashInsert( Vec_Mem_t * p, word * pEntry )
|
||||
{
|
||||
int * pSpot;
|
||||
if ( p->nEntries > Vec_IntSize(p->vTable) )
|
||||
Vec_MemHashResize( p );
|
||||
pSpot = Vec_MemHashLookup( p, pEntry );
|
||||
if ( *pSpot != -1 )
|
||||
return *pSpot;
|
||||
*pSpot = Vec_IntSize(p->vNexts);
|
||||
Vec_IntPush( p->vNexts, -1 );
|
||||
Vec_MemPush( p, pEntry );
|
||||
assert( p->nEntries == Vec_IntSize(p->vNexts) );
|
||||
return Vec_IntSize(p->vNexts) - 1;
|
||||
}
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "dauInt.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -443,7 +444,7 @@ void Dau_DsdTestOne( word t, int i )
|
|||
{
|
||||
word t2;
|
||||
char * p = Dau_DsdPerform( t );
|
||||
// return;
|
||||
return;
|
||||
t2 = Dau_DsdToTruth( p );
|
||||
if ( t != t2 )
|
||||
{
|
||||
|
|
@ -463,6 +464,344 @@ void Dau_DsdTestOne( word t, int i )
|
|||
Dau_DsdTestOne( *p->pFuncs[i], i );
|
||||
*/
|
||||
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; }
|
||||
static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
|
||||
|
||||
static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( t[i] & ~s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != ~(word)0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( t[i] & s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i+Step] != ~(word)0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
|
||||
{
|
||||
if ( iVar < 6 )
|
||||
{
|
||||
int i, Shift = (1 << iVar);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVar - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != ~t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ )
|
||||
{
|
||||
assert( iVarI > iVarJ );
|
||||
if ( iVarI < 6 )
|
||||
{
|
||||
int i, Shift = (1 << iVarJ);
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else if ( iVarI == 6 )
|
||||
{
|
||||
}
|
||||
else
|
||||
{
|
||||
int i, Step = (1 << (iVarJ - 6));
|
||||
word * tLimit = t + nWords;
|
||||
for ( ; t < tLimit; t += 2*Step )
|
||||
for ( i = 0; i < Step; i++ )
|
||||
if ( t[i] != t[i+Step] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdMinimize( word * p, int * pVars, int nVars )
|
||||
{
|
||||
int i, k;
|
||||
assert( nVars > 6 );
|
||||
for ( i = k = nVars - 1; i >= 0; i-- )
|
||||
{
|
||||
if ( Abc_TtHasVar( p, nVars, i ) )
|
||||
continue;
|
||||
if ( i < k )
|
||||
{
|
||||
pVars[i] = pVars[k];
|
||||
Abc_TtSwapVars( p, nVars, i, k );
|
||||
}
|
||||
k--;
|
||||
nVars--;
|
||||
}
|
||||
return nVars;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
|
||||
{
|
||||
int v, nWords = Abc_TtWordNum( nVars );
|
||||
nVars = Dau_DsdMinimize( p, pVars, nVars );
|
||||
if ( nVars <= 6 )
|
||||
return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
if ( p[0] & 1 )
|
||||
{
|
||||
// check for !(ax)
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst0( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// check for ax
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst1( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
if ( (p[nWords-1] >> 63) & 1 )
|
||||
{
|
||||
// check for !(!ax)
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof0IsConst1( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// check for !ax
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCof1IsConst0( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '(';
|
||||
pBuffer[Pos++] = '!';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ')';
|
||||
return Pos;
|
||||
}
|
||||
}
|
||||
// check for a^x
|
||||
for ( v = 0; v < nVars; v++ )
|
||||
if ( Abc_TtCofsOpposite( p, nWords, v ) )
|
||||
{
|
||||
pBuffer[Pos++] = '[';
|
||||
pBuffer[Pos++] = 'a' + pVars[v];
|
||||
Abc_TtSwapVars( p, nVars, v, nVars - 1 );
|
||||
pVars[v] = pVars[nVars-1];
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = ']';
|
||||
return Pos;
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
char * Dau_DsdRun( word * p, int nVars )
|
||||
{
|
||||
static char pBuffer[DAU_MAX_STR+20];
|
||||
static char pStore[16][16];
|
||||
int nWords = Abc_TtWordNum( nVars );
|
||||
int i, Pos = 0, Func = 0, pVars[16];
|
||||
assert( nVars <= 16 );
|
||||
for ( i = 0; i < nVars; i++ )
|
||||
pVars[i] = i;
|
||||
if ( Abc_TtTruthIsConst0( p, nWords ) )
|
||||
pBuffer[Pos++] = '0';
|
||||
else if ( Abc_TtTruthIsConst1( p, nWords ) )
|
||||
pBuffer[Pos++] = '1';
|
||||
else if ( nVars <= 6 )
|
||||
Pos = Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
else
|
||||
Pos = Dau_DsdRun_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
|
||||
pBuffer[Pos++] = 0;
|
||||
Dau_DsdCleanBraces( pBuffer );
|
||||
return pBuffer;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -0,0 +1,253 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dauEnum.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [DAG-aware unmapping.]
|
||||
|
||||
Synopsis [Enumeration of decompositions.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: dauEnum.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dauInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
char * Dau_EnumLift( char * pName, int Shift )
|
||||
{
|
||||
static char pBuffer[64];
|
||||
char * pTemp;
|
||||
for ( pTemp = pBuffer; *pName; pTemp++, pName++ )
|
||||
*pTemp = (*pName >= 'a' && *pName <= 'z') ? *pName + Shift : *pName;
|
||||
*pTemp = 0;
|
||||
return pBuffer;
|
||||
}
|
||||
char * Dau_EnumLift2( char * pName, int Shift )
|
||||
{
|
||||
static char pBuffer[64];
|
||||
char * pTemp;
|
||||
for ( pTemp = pBuffer; *pName; pTemp++, pName++ )
|
||||
*pTemp = (*pName >= 'a' && *pName <= 'z') ? *pName + Shift : *pName;
|
||||
*pTemp = 0;
|
||||
return pBuffer;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dau_EnumCombineTwo( Vec_Ptr_t * vOne, int fStar, int fXor, char * pName1, char * pName2, int Shift2, int fCompl1, int fCompl2 )
|
||||
{
|
||||
static char pBuffer[256];
|
||||
pName2 = Dau_EnumLift( pName2, Shift2 );
|
||||
sprintf( pBuffer, "%s%c%s%s%s%s%c",
|
||||
fStar?"*":"",
|
||||
fXor?'[':'(',
|
||||
fCompl1?"!":"", pName1[0] == '*' ? pName1 + 1 : pName1,
|
||||
fCompl2?"!":"", pName2[0] == '*' ? pName2 + 1 : pName2,
|
||||
fXor?']':')' );
|
||||
// printf( "%s ", pBuffer );
|
||||
Vec_PtrPush( vOne, Abc_UtilStrsav(pBuffer) );
|
||||
}
|
||||
void Dau_EnumCombineThree( Vec_Ptr_t * vOne, int fStar, char * pNameC, char * pName1, char * pName2, int Shift1, int Shift2, int fComplC, int fCompl1, int fCompl2 )
|
||||
{
|
||||
static char pBuffer[256];
|
||||
pName1 = Dau_EnumLift( pName1, Shift1 );
|
||||
pName2 = Dau_EnumLift2( pName2, Shift2 );
|
||||
sprintf( pBuffer, "%s%c%s%s%s%s%s%s%c",
|
||||
fStar?"*":"",
|
||||
'<',
|
||||
fComplC?"!":"", pNameC[0] == '*' ? pNameC + 1 : pNameC,
|
||||
fCompl1?"!":"", pName1[0] == '*' ? pName1 + 1 : pName1,
|
||||
fCompl2?"!":"", pName2[0] == '*' ? pName2 + 1 : pName2,
|
||||
'>' );
|
||||
// printf( "%s ", pBuffer );
|
||||
Vec_PtrPush( vOne, Abc_UtilStrsav(pBuffer) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dau_EnumTestDump( Vec_Ptr_t * vSets, char * pFileName )
|
||||
{
|
||||
FILE * pFile;
|
||||
Vec_Ptr_t * vOne;
|
||||
char * pName;
|
||||
int v, k;
|
||||
pFile = fopen( pFileName, "wb" );
|
||||
if ( pFile == NULL )
|
||||
return;
|
||||
Vec_PtrForEachEntry( Vec_Ptr_t *, vSets, vOne, v )
|
||||
{
|
||||
fprintf( pFile, "VARIABLE NUMBER %d:\n", v );
|
||||
Vec_PtrForEachEntry( char *, vOne, pName, k )
|
||||
fprintf( pFile, "%s\n", pName );
|
||||
}
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Dau_EnumTest()
|
||||
{
|
||||
int v, k, nVarMax = 10;
|
||||
Vec_Ptr_t * vSets;
|
||||
Vec_Ptr_t * vOne;
|
||||
char * pName;
|
||||
// 0 vars
|
||||
vSets = Vec_PtrAlloc( 16 );
|
||||
Vec_PtrPush( vSets, Vec_PtrAlloc(0) );
|
||||
// 1 vars
|
||||
vOne = Vec_PtrAlloc( 1 );
|
||||
Vec_PtrPush( vOne, Abc_UtilStrsav("*a") );
|
||||
Vec_PtrPush( vSets, vOne );
|
||||
// 2+ vars
|
||||
for ( v = 2; v <= nVarMax; v++ )
|
||||
{
|
||||
Vec_Ptr_t * vSetI, * vSetJ, * vSetK;
|
||||
char * pNameI, * pNameJ, * pNameK;
|
||||
int i, j, k, i1, j1, k1;
|
||||
vOne = Vec_PtrAlloc( 100 );
|
||||
for ( i = 1; i < v; i++ )
|
||||
for ( j = i; j < v; j++ )
|
||||
{
|
||||
if ( i + j != v )
|
||||
continue;
|
||||
vSetI = (Vec_Ptr_t *)Vec_PtrEntry( vSets, i );
|
||||
vSetJ = (Vec_Ptr_t *)Vec_PtrEntry( vSets, j );
|
||||
Vec_PtrForEachEntry( char *, vSetI, pNameI, i1 )
|
||||
Vec_PtrForEachEntry( char *, vSetJ, pNameJ, j1 )
|
||||
{
|
||||
// AND(a,b)
|
||||
Dau_EnumCombineTwo( vOne, 0, 0, pNameI, pNameJ, i, 0, 0 );
|
||||
// AND(!a,b)
|
||||
if ( pNameI[0] != '*' )
|
||||
Dau_EnumCombineTwo( vOne, 0, 0, pNameI, pNameJ, i, 1, 0 );
|
||||
// AND(a,!b)
|
||||
if ( pNameJ[0] != '*' && !(i == j && i1 == j1) )
|
||||
Dau_EnumCombineTwo( vOne, 0, 0, pNameI, pNameJ, i, 0, 1 );
|
||||
// AND(!a,!b)
|
||||
if ( pNameI[0] != '*' && pNameJ[0] != '*' )
|
||||
Dau_EnumCombineTwo( vOne, 0, 0, pNameI, pNameJ, i, 1, 1 );
|
||||
// XOR(a,b)
|
||||
Dau_EnumCombineTwo( vOne, pNameI[0] == '*' || pNameJ[0] == '*', 1, pNameI, pNameJ, i, 0, 0 );
|
||||
}
|
||||
}
|
||||
for ( k = 1; k < v; k++ )
|
||||
for ( i = 1; i < v; i++ )
|
||||
for ( j = i; j < v; j++ )
|
||||
{
|
||||
if ( k + i + j != v )
|
||||
continue;
|
||||
vSetK = (Vec_Ptr_t *)Vec_PtrEntry( vSets, k );
|
||||
vSetI = (Vec_Ptr_t *)Vec_PtrEntry( vSets, i );
|
||||
vSetJ = (Vec_Ptr_t *)Vec_PtrEntry( vSets, j );
|
||||
Vec_PtrForEachEntry( char *, vSetK, pNameK, k1 )
|
||||
Vec_PtrForEachEntry( char *, vSetI, pNameI, i1 )
|
||||
Vec_PtrForEachEntry( char *, vSetJ, pNameJ, j1 )
|
||||
{
|
||||
int fStar = pNameI[0] == '*' && pNameJ[0] == '*';
|
||||
|
||||
// MUX(c,a,b)
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 0, 0, 0 );
|
||||
// MUX(c,!a,b)
|
||||
if ( pNameI[0] != '*' )
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 0, 1, 0 );
|
||||
// MUX(c,a,!b)
|
||||
if ( pNameJ[0] != '*' && !(i == j && i1 == j1) )
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 0, 0, 1 );
|
||||
|
||||
if ( pNameK[0] != '*' && !(i == j && i1 == j1) )
|
||||
{
|
||||
// MUX(!c,a,b)
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 1, 0, 0 );
|
||||
// MUX(!c,!a,b)
|
||||
if ( pNameI[0] != '*' )
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 1, 1, 0 );
|
||||
// MUX(!c,a,!b)
|
||||
if ( pNameJ[0] != '*' )
|
||||
Dau_EnumCombineThree( vOne, fStar, pNameK, pNameI, pNameJ, k, k+i, 1, 0, 1 );
|
||||
}
|
||||
}
|
||||
}
|
||||
Vec_PtrPush( vSets, vOne );
|
||||
}
|
||||
Dau_EnumTestDump( vSets, "_npn/npn/dsd10.txt" );
|
||||
|
||||
Vec_PtrForEachEntry( Vec_Ptr_t *, vSets, vOne, v )
|
||||
{
|
||||
printf( "VARIABLE NUMBER %d:\n", v );
|
||||
Vec_PtrForEachEntry( char *, vOne, pName, k )
|
||||
printf( "%s\n", pName );
|
||||
if ( v == 4 )
|
||||
break;
|
||||
}
|
||||
Vec_PtrForEachEntry( Vec_Ptr_t *, vSets, vOne, v )
|
||||
{
|
||||
printf( "%d=%d ", v, Vec_PtrSize(vOne) );
|
||||
Vec_PtrFreeFree( vOne );
|
||||
}
|
||||
Vec_PtrFree( vSets );
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -1,3 +1,4 @@
|
|||
SRC += src/opt/dau/dau.c \
|
||||
src/opt/dau/dauCore.c \
|
||||
src/opt/dau/dauDsd.c
|
||||
src/opt/dau/dauDsd.c \
|
||||
src/opt/dau/dauEnum.c
|
||||
|
|
|
|||
|
|
@ -163,7 +163,6 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
|
|||
// set up the choice node
|
||||
if ( Aig_ObjIsChoice( p, pNode ) )
|
||||
{
|
||||
pIfMan->nChoices++;
|
||||
for ( pPrev = pNode, pFanin = Aig_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Aig_ObjEquiv(p, pFanin) )
|
||||
If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
|
||||
If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
|
||||
|
|
|
|||
|
|
@ -144,6 +144,7 @@ struct Cec_ParCor_t_
|
|||
int fUseCSat; // use circuit-based solver
|
||||
// int fFirstStop; // stop on the first sat output
|
||||
int fUseSmartCnf; // use smart CNF computation
|
||||
int fStopWhenGone; // quit when PO is not a candidate constant
|
||||
int fVerboseFlops; // verbose stats
|
||||
int fVeryVerbose; // verbose stats
|
||||
int fVerbose; // verbose stats
|
||||
|
|
|
|||
|
|
@ -753,6 +753,7 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
|
|||
nFail++;
|
||||
}
|
||||
Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
|
||||
Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
|
||||
Abc_PrintTime( 1, "T", Time );
|
||||
}
|
||||
|
||||
|
|
@ -950,6 +951,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
|
||||
if ( pPars->pFunc )
|
||||
((int (*)(void *))pPars->pFunc)( pPars->pData );
|
||||
// quit if const is no longer there
|
||||
if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
|
||||
{
|
||||
printf( "Iterative refinement is stopped after iteration %d\n", r );
|
||||
printf( "because the property output is no longer a candidate constant.\n" );
|
||||
Cec_ManSimStop( pSim );
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
if ( pPars->fVerbose )
|
||||
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
|
||||
|
|
@ -1071,7 +1080,11 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
ABC_FREE( pAig->pReprs );
|
||||
ABC_FREE( pAig->pNexts );
|
||||
if ( pPars->nPrefix == 0 )
|
||||
{
|
||||
RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
|
||||
if ( RetValue == 0 )
|
||||
return Gia_ManDup( pAig );
|
||||
}
|
||||
else
|
||||
{
|
||||
// compute the cycles AIG
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 ) );
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
|
|||
{
|
||||
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
|
||||
extern If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
|
||||
extern void Gia_ManSetIfParsDefault( If_Par_t * pPars );
|
||||
extern void Gia_ManSetIfParsDefault( void * pPars );
|
||||
If_Par_t Pars, * pPars = &Pars;
|
||||
If_Man_t * pIfMan;
|
||||
If_Obj_t * pAnd;
|
||||
|
|
|
|||
|
|
@ -70,6 +70,7 @@ struct Ssw_Pars_t_
|
|||
int fVerbose; // verbose stats
|
||||
int fFlopVerbose; // verbose printout of redundant flops
|
||||
int fEquivDump; // enables dumping equivalences
|
||||
int fStopWhenGone; // stop when PO output is not a candidate constant
|
||||
// optimized latch correspondence
|
||||
int fLatchCorrOpt; // perform register correspondence (optimized)
|
||||
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
|
||||
|
|
|
|||
|
|
@ -346,6 +346,24 @@ clk = clock();
|
|||
}
|
||||
// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
|
||||
// p->pPars->nBTLimit = 10000;
|
||||
|
||||
if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
|
||||
{
|
||||
printf( "Iterative refinement is stopped after iteration %d\n", nIter );
|
||||
printf( "because the property output is no longer a candidate constant.\n" );
|
||||
// prepare to quite
|
||||
p->nLitsEnd = p->nLitsBeg;
|
||||
p->nNodesEnd = p->nNodesBeg;
|
||||
p->nRegsEnd = p->nRegsBeg;
|
||||
// cleanup
|
||||
Ssw_SatStop( p->pMSat );
|
||||
p->pMSat = NULL;
|
||||
Ssw_ManCleanup( p );
|
||||
// cleanup
|
||||
Aig_ManSetPhase( p->pAig );
|
||||
Aig_ManCleanMarkB( p->pAig );
|
||||
return Aig_ManDupSimple( p->pAig );
|
||||
}
|
||||
}
|
||||
nSatProof = p->nSatProof;
|
||||
nSatCallsSat = p->nSatCallsSat;
|
||||
|
|
|
|||
Loading…
Reference in New Issue