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

Version abc80410

This commit is contained in:
Alan Mishchenko 2008-04-10 08:01:00 -07:00
parent 9d6b12ddfd
commit c645bac366
29 changed files with 2054 additions and 144 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abc.dsp
View File

@ -3066,6 +3066,10 @@ SOURCE=.\src\aig\ntl\ntlCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlEc.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlExtract.c
# End Source File
# Begin Source File
@ -3094,6 +3098,10 @@ SOURCE=.\src\aig\ntl\ntlReadBlif.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlSweep.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntl\ntlTable.c
# End Source File
# Begin Source File

5
copyright.txt
View File

@ -1,3 +1,8 @@
ABC: System for Sequential Synthesis and Verification
http://www.eecs.berkeley.edu/~alanmi/abc/
Copyright (c) The Regents of the University of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or

5
src/aig/aig/aig.h
View File

@ -140,6 +140,7 @@ struct Aig_Man_t_
void * pManCuts;
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
Vec_Int_t * vFlopReprs;
void * pSeqModel;
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
@ -314,7 +315,7 @@ static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; }
static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; }
static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext; }
static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
@ -461,6 +462,7 @@ extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t
extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
/*=== aigDup.c ==========================================================*/
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
@ -560,6 +562,7 @@ extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
extern void Aig_ManComputeSccs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
/*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/

6
src/aig/aig/aigDfs.c
View File

@ -449,10 +449,10 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
LevelMax = Aig_ObjLevel(pObj);
}
Aig_ManCleanPioNumbers( p );
Aig_ManForEachNode( p, pObj, i )
assert( Aig_ObjLevel(pObj) > 0 );
// Aig_ManForEachNode( p, pObj, i )
// assert( Aig_ObjLevel(pObj) > 0 );
return LevelMax;
}
}
//#endif

70
src/aig/aig/aigDup.c
View File

@ -29,6 +29,72 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description [Orders nodes as follows: PIs, ANDs, POs.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachPi( p, pObj, i )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
// duplicate internal nodes
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
{
pObjNew = Aig_ObjChild0Copy(pObj);
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachPo( p, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
@ -543,7 +609,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
}
// check the new manager
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupReprentative: Check has failed.\n" );
printf( "Aig_ManDupRepres: Check has failed.\n" );
return pNew;
}
@ -616,7 +682,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
}
// check the new manager
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupReprentative: Check has failed.\n" );
printf( "Aig_ManDupRepresDfs: Check has failed.\n" );
return pNew;
}

1
src/aig/aig/aigMan.c
View File

@ -206,6 +206,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
if ( p->vFlopReprs)Vec_IntFree( p->vFlopReprs );
if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
FREE( p->pData );

2
src/aig/aig/aigObj.c
View File

@ -258,6 +258,8 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
Aig_ObjDeref( pFaninOld );
// update the fanin
pObj->pFanin0 = pFaninNew;
pObj->Level = Aig_ObjLevelNew( pObj );
pObj->fPhase = Aig_ObjPhaseReal(pObj->pFanin0);
// increment ref and add fanout
if ( p->pFanData )
Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );

2
src/aig/aig/aigRepr.c
View File

@ -278,6 +278,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// Aig_ManForEachPi( p, pObj, i )
// pObj->pData = Aig_ObjGetRepr( p, pObj );
// map the internal nodes
if ( fOrdered )
{

96
src/aig/aig/aigScl.c
View File

@ -44,25 +44,52 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjMapped;
int i;
int i, nTruePis;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
if ( p->vFlopReprs )
pNew->vFlopReprs = Vec_IntDup( p->vFlopReprs );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// implement the mapping
nTruePis = Aig_ManPiNum(p)-Aig_ManRegNum(p);
if ( p->vFlopReprs )
{
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i-nTruePis );
}
Aig_ManForEachPi( p, pObj, i )
{
pObjMapped = Vec_PtrEntry( vMap, i );
pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped )
{
Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) );
if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) )
Vec_IntPush( pNew->vFlopReprs, -1 );
else
{
assert( !Aig_IsComplement(pObjMapped) );
assert( Aig_ObjIsPi(pObjMapped) );
assert( Aig_ObjPioNum(pObj) != Aig_ObjPioNum(pObjMapped) );
Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObjMapped) );
}
}
}
if ( p->vFlopReprs )
{
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pNext = NULL;
}
// duplicate internal nodes
Aig_ManForEachObj( p, pObj, i )
@ -158,16 +185,15 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
if ( p->vFlopNums )
{
int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p);
// remember numbers of flops in the flops
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i - nTruePos );
// reset the flop numbers
Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos )
Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)(long)pObj->pNext );
Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos );
// clean the next pointer
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pNext = NULL;
int iNum, k = 0;
Aig_ManForEachPo( p, pObj, i )
if ( i >= nTruePos && Aig_ObjIsTravIdCurrent(p, pObj) )
{
iNum = Vec_IntEntry( p->vFlopNums, i - nTruePos );
Vec_IntWriteEntry( p->vFlopNums, k++, iNum );
}
assert( k == Vec_PtrSize(vNodes) - nTruePos );
Vec_IntShrink( p->vFlopNums, k );
}
// collect new CIs/COs
vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
@ -505,6 +531,54 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
Vec_VecFree( (Vec_Vec_t *)vSupports );
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
{
Aig_Man_t * pAigInit, * pAigNew;
Aig_Obj_t * pFlop1, * pFlop2;
int i, Entry1, Entry2, nTruePis;
// store the original AIG
assert( pAig->vFlopNums == NULL );
pAigInit = pAig;
pAig = Aig_ManDup( pAig );
// create storage for latch numbers
pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs );
pAig->vFlopReprs = Vec_IntAlloc( 100 );
Aig_ManSeqCleanup( pAig );
if ( fLatchConst && pAig->nRegs )
pAig = Aig_ManConstReduce( pAig, fVerbose );
if ( fLatchEqual && pAig->nRegs )
pAig = Aig_ManReduceLaches( pAig, fVerbose );
// translate pairs into reprs
nTruePis = Aig_ManPiNum(pAigInit)-Aig_ManRegNum(pAigInit);
Aig_ManReprStart( pAigInit, Aig_ManObjNumMax(pAigInit) );
Vec_IntForEachEntry( pAig->vFlopReprs, Entry1, i )
{
Entry2 = Vec_IntEntry( pAig->vFlopReprs, ++i );
pFlop1 = Aig_ManPi( pAigInit, nTruePis + Entry1 );
pFlop2 = (Entry2 == -1)? Aig_ManConst1(pAigInit) : Aig_ManPi( pAigInit, nTruePis + Entry2 );
assert( pFlop1 != pFlop2 );
if ( pFlop1->Id > pFlop2->Id )
pAigInit->pReprs[pFlop1->Id] = pFlop2;
else
pAigInit->pReprs[pFlop2->Id] = pFlop1;
}
Aig_ManStop( pAig );
// Aig_ManSeqCleanup( pAigInit );
pAigNew = Aig_ManDupRepr( pAigInit, 0 );
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

10
src/aig/fra/fraSec.c
View File

@ -47,13 +47,18 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
// try the miter before solving
RetValue = Fra_FraigMiterStatus( p );
if ( RetValue == 0 || RetValue == 1 )
goto finish;
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = fVeryVerbose;
pNew = Aig_ManDupOrdered( p );
// pNew = Aig_ManDupDfs( p );
pNew = Aig_ManDup( p );
if ( fVerbose )
{
printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
@ -208,6 +213,7 @@ PRT( "Time", clock() - clkTotal );
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
finish:
// report the miter
if ( RetValue == 1 )
{

6
src/aig/ioa/ioaWriteAig.c
View File

@ -145,7 +145,7 @@ static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->iD
SeeAlso []
***********************************************************************/
int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
int Ioa_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
{
unsigned char ch;
while (x & ~0x7f)
@ -332,8 +332,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
assert( uLit0 < uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
if ( Pos > nBufferSize - 10 )
{
printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );

2
src/aig/ntl/module.make
View File

@ -1,5 +1,6 @@
SRC += src/aig/ntl/ntlCheck.c \
src/aig/ntl/ntlCore.c \
src/aig/ntl/ntlEc.c \
src/aig/ntl/ntlExtract.c \
src/aig/ntl/ntlFraig.c \
src/aig/ntl/ntlInsert.c \
@ -7,6 +8,7 @@ SRC += src/aig/ntl/ntlCheck.c \
src/aig/ntl/ntlMap.c \
src/aig/ntl/ntlObj.c \
src/aig/ntl/ntlReadBlif.c \
src/aig/ntl/ntlSweep.c \
src/aig/ntl/ntlTable.c \
src/aig/ntl/ntlTime.c \
src/aig/ntl/ntlUtil.c \

34
src/aig/ntl/ntl.h
View File

@ -54,8 +54,9 @@ typedef enum {
NTL_OBJ_PO, // 2: primary output
NTL_OBJ_LATCH, // 3: latch node
NTL_OBJ_NODE, // 4: logic node
NTL_OBJ_BOX, // 5: white box or black box
NTL_OBJ_VOID // 6: unused object
NTL_OBJ_LUT1, // 5: inverter/buffer
NTL_OBJ_BOX, // 6: white box or black box
NTL_OBJ_VOID // 7: unused object
} Ntl_Type_t;
struct Ntl_Man_t_
@ -122,7 +123,7 @@ struct Ntl_Net_t_
Ntl_Obj_t * pDriver; // driver of the net
char nVisits; // the number of times the net is visited
char fMark; // temporary mark
char fCompl; // complemented attribue
char fCompl; // complemented attribute
char pName[0]; // the name of this net
};
@ -148,6 +149,7 @@ static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return Vec_P
static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; }
static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; }
static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_NODE]; }
static inline int Ntl_ModelLut1Num( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LUT1]; }
static inline int Ntl_ModelLatchNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LATCH]; }
static inline int Ntl_ModelBoxNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_BOX]; }
static inline int Ntl_ModelCiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; }
@ -228,27 +230,35 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
/*=== ntlCore.c ==========================================================*/
extern int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
extern int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
/*=== ntlEc.c ==========================================================*/
extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
/*=== ntlExtract.c ==========================================================*/
extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p );
extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p );
extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
extern char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
/*=== ntlInsert.c ==========================================================*/
extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
extern int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
extern Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
extern Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
extern Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
/*=== ntlCheck.c ==========================================================*/
extern int Ntl_ManCheck( Ntl_Man_t * pMan );
extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
/*=== ntlMan.c ============================================================*/
extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName );
extern void Ntl_ManCleanup( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
extern void Ntl_ManFree( Ntl_Man_t * p );
extern int Ntl_ManIsComb( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
extern void Ntl_ManPrintStats( Ntl_Man_t * p );
extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
extern Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern void Ntl_ModelFree( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
@ -263,15 +273,19 @@ extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
extern Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
extern Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
extern char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
/*=== ntlSweep.c ==========================================================*/
extern Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose );
/*=== ntlTable.c ==========================================================*/
extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
extern void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
extern int Ntl_ModelCountNets( Ntl_Mod_t * p );
/*=== ntlTime.c ==========================================================*/
extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
/*=== ntlReadBlif.c ==========================================================*/
@ -279,9 +293,15 @@ extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
/*=== ntlUtil.c ==========================================================*/
extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
extern int Ntl_ManTransformCoDrivers( Ntl_Man_t * p );
extern int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p );
extern Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p );
extern Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p );
extern void Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
extern void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
extern int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
#ifdef __cplusplus
}

10
src/aig/ntl/ntlCheck.c
View File

@ -31,7 +31,7 @@
/**Function*************************************************************
Synopsis []
Synopsis [Checks one model.]
Description []
@ -49,12 +49,12 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
{
if ( pNet->pName == NULL )
{
printf( "Net %d does not have a name\n", i );
printf( "Net in bin %d does not have a name\n", i );
fStatus = 0;
}
if ( pNet->pDriver == NULL )
{
printf( "Net %d (%s) does not have a driver\n", i, pNet->pName );
printf( "Net %s does not have a driver\n", pNet->pName );
fStatus = 0;
}
}
@ -78,7 +78,7 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
/**Function*************************************************************
Synopsis []
Synopsis [Checks the netlist.]
Description []
@ -131,7 +131,7 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
/**Function*************************************************************
Synopsis [Reads the verilog file.]
Synopsis [Fixed problems with non-driven nets in the model.]
Description []

10
src/aig/ntl/ntlCore.c
View File

@ -69,10 +69,13 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate
***********************************************************************/
int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
{
Ntl_Man_t * pNew;
Vec_Ptr_t * vMapping;
int RetValue;
vMapping = Ntl_MappingFromAig( pAig );
RetValue = Ntl_ManInsert( p, vMapping, pAig );
pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
RetValue = (pNew != NULL);
Ntl_ManFree( pNew );
Vec_PtrFree( vMapping );
return RetValue;
}
@ -90,10 +93,13 @@ int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
***********************************************************************/
int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig )
{
Ntl_Man_t * pNew;
Vec_Ptr_t * vMapping;
int RetValue;
vMapping = Ntl_MappingIf( p, pAig );
RetValue = Ntl_ManInsert( p, vMapping, pAig );
pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
RetValue = (pNew != NULL);
Ntl_ManFree( pNew );
Vec_PtrFree( vMapping );
return RetValue;
}

317
src/aig/ntl/ntlEc.c Normal file
View File

@ -0,0 +1,317 @@
/**CFile****************************************************************
FileName [ntlEc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Equivalence checking procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlEc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds PIs to both models, so that they have the same PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i;
Ntl_ModelForEachPi( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
}
Ntl_ModelForEachPi( p2, pObj, i )
{
pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
}
if ( !fSeq )
{
Ntl_ModelForEachLatch( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
}
Ntl_ModelForEachLatch( p2, pObj, i )
{
pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
}
}
}
/**Function*************************************************************
Synopsis [Creates arrays of combinational inputs in the same order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
{
Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i;
if ( fSeq )
assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) );
else
assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) );
// order the CIs
Vec_PtrClear( pMan1->vCis );
Vec_PtrClear( pMan2->vCis );
Ntl_ModelForEachPi( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
{
printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
return;
}
Vec_PtrPush( pMan1->vCis, pObj );
Vec_PtrPush( pMan2->vCis, pNet->pDriver );
}
if ( !fSeq )
{
Ntl_ModelForEachLatch( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
if ( pNet == NULL )
{
printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
return;
}
Vec_PtrPush( pMan1->vCis, pObj );
Vec_PtrPush( pMan2->vCis, pNet->pDriver );
}
}
}
/**Function*************************************************************
Synopsis [Creates arrays of combinational outputs in the same order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
{
Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i;
// if ( fSeq )
// assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) );
// else
// assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) );
// remember PO in the corresponding net of the second design
Ntl_ModelForEachPo( p2, pObj, i )
Ntl_ObjFanin0(pObj)->pCopy = pObj;
// order the COs
Vec_PtrClear( pMan1->vCos );
Vec_PtrClear( pMan2->vCos );
Ntl_ModelForEachPo( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
if ( pNet == NULL )
{
printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n",
Ntl_ObjFanin0(pObj)->pName );
continue;
}
Vec_PtrPush( pMan1->vCos, pObj );
Vec_PtrPush( pMan2->vCos, pNet->pCopy );
}
if ( !fSeq )
{
Ntl_ModelForEachLatch( p2, pObj, i )
Ntl_ObjFanin0(pObj)->pCopy = pObj;
Ntl_ModelForEachLatch( p1, pObj, i )
{
pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
if ( pNet == NULL )
{
printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n",
Ntl_ObjFanin0(pObj)->pName );
continue;
}
Vec_PtrPush( pMan1->vCos, pObj );
Vec_PtrPush( pMan2->vCos, pNet->pCopy );
}
}
}
/**Function*************************************************************
Synopsis [Prepares AIGs for combinational equivalence checking.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 )
{
Ntl_Man_t * pMan1, * pMan2;
Ntl_Mod_t * pModel1, * pModel2;
*ppMan1 = NULL;
*ppMan2 = NULL;
// read the netlists
pMan1 = Ioa_ReadBlif( pFileName1, 1 );
pMan2 = Ioa_ReadBlif( pFileName2, 1 );
if ( !pMan1 || !pMan2 )
{
if ( pMan1 ) Ntl_ManFree( pMan1 );
if ( pMan2 ) Ntl_ManFree( pMan2 );
printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" );
return;
}
// make sure they are compatible
pModel1 = Ntl_ManRootModel( pMan1 );
pModel2 = Ntl_ManRootModel( pMan2 );
if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
{
printf( "Warning: The number of inputs in the designs is different (%d and %d).\n",
Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) );
}
if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) )
{
printf( "Warning: The number of outputs in the designs is different (%d and %d).\n",
Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) );
}
// normalize inputs/outputs
Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 );
Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 );
if ( Vec_PtrSize(pMan1->vCos) == 0 )
{
printf( "Ntl_ManPrepareCec(): There is no identically-named primary outputs to compare.\n" );
if ( pMan1 ) Ntl_ManFree( pMan1 );
if ( pMan2 ) Ntl_ManFree( pMan2 );
return;
}
// derive AIGs
*ppMan1 = Ntl_ManCollapseForCec( pMan1 );
*ppMan2 = Ntl_ManCollapseForCec( pMan2 );
// cleanup
Ntl_ManFree( pMan1 );
Ntl_ManFree( pMan2 );
}
/**Function*************************************************************
Synopsis [Prepares AIGs for sequential equivalence checking.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
{
Aig_Man_t * pAig;
Ntl_Man_t * pMan1, * pMan2;
Ntl_Mod_t * pModel1, * pModel2;
// read the netlists
pMan1 = Ioa_ReadBlif( pFileName1, 1 );
pMan2 = Ioa_ReadBlif( pFileName2, 1 );
if ( !pMan1 || !pMan2 )
{
if ( pMan1 ) Ntl_ManFree( pMan1 );
if ( pMan2 ) Ntl_ManFree( pMan2 );
printf( "Ntl_ManPrepareSec(): Reading designs from file has failed.\n" );
return NULL;
}
// make sure they are compatible
pModel1 = Ntl_ManRootModel( pMan1 );
pModel2 = Ntl_ManRootModel( pMan2 );
if ( Ntl_ModelLatchNum(pModel1) == 0 || Ntl_ModelLatchNum(pModel2) == 0 )
{
if ( pMan1 ) Ntl_ManFree( pMan1 );
if ( pMan2 ) Ntl_ManFree( pMan2 );
printf( "Ntl_ManPrepareSec(): The designs have no latches. Used combinational command \"*cec\".\n" );
return NULL;
}
if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
{
printf( "Warning: The number of inputs in the designs is different (%d and %d).\n",
Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) );
}
if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) )
{
printf( "Warning: The number of outputs in the designs is different (%d and %d).\n",
Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) );
}
// normalize inputs/outputs
Ntl_ManCreateMissingInputs( pModel1, pModel2, 1 );
Ntl_ManDeriveCommonCis( pMan1, pMan2, 1 );
Ntl_ManDeriveCommonCos( pMan1, pMan2, 1 );
if ( Vec_PtrSize(pMan1->vCos) == 0 )
{
printf( "Ntl_ManPrepareSec(): There is no identically-named primary outputs to compare.\n" );
if ( pMan1 ) Ntl_ManFree( pMan1 );
if ( pMan2 ) Ntl_ManFree( pMan2 );
return NULL;
}
// derive AIGs
pAig = Ntl_ManCollapseForSec( pMan1, pMan2 );
// cleanup
pMan1->pAig = pMan2->pAig = NULL;
Ntl_ManFree( pMan1 );
Ntl_ManFree( pMan2 );
return pAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

219
src/aig/ntl/ntlExtract.c
View File

@ -467,6 +467,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i, nUselessObjects;
Ntl_ManCleanup( p );
assert( Vec_PtrSize(p->vCis) == 0 );
assert( Vec_PtrSize(p->vCos) == 0 );
assert( Vec_PtrSize(p->vNodes) == 0 );
@ -540,7 +541,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// report the number of dangling objects
nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
if ( nUselessObjects )
printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
// cleanup the AIG
@ -658,7 +659,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
{
Aig_Man_t * pAig;
Ntl_Mod_t * pRoot;
@ -694,6 +695,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( p->pAig );
if ( fSeq && (pObj->LatchId & 3) == 1 )
pNet->pCopy = Aig_Not(pNet->pCopy);
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@ -721,6 +724,60 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
return 0;
}
if ( fSeq && (pObj->LatchId & 3) == 1 )
Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
else
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// cleanup the AIG
Aig_ManCleanup( p->pAig );
pAig = p->pAig; p->pAig = NULL;
return pAig;
}
/**Function*************************************************************
Synopsis [Derives AIG for CEC.]
Description [Uses CIs/COs collected in the internal arrays.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
{
Aig_Man_t * pAig;
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i;
// create the manager
p->pAig = Aig_ManStart( 10000 );
p->pAig->pName = Aig_UtilStrsav( p->pName );
p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
// set the inputs
Ntl_ManForEachCiNet( p, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( p->pAig );
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
return 0;
}
pNet->nVisits = 2;
}
// derive the outputs
Ntl_ManForEachCoNet( p, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManCollapse_rec( p, pNet ) )
{
printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
return 0;
}
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// cleanup the AIG
@ -729,6 +786,164 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
return pAig;
}
/**Function*************************************************************
Synopsis [Performs DFS.]
Description [Checks for combinational loops. Collects PI/PO nets.
Collects nodes in the topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
{
Aig_Man_t * pAig;
Aig_Obj_t * pMiter;
Ntl_Mod_t * pRoot1, * pRoot2;
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
Vec_Ptr_t * vPairs;
int i;
assert( Vec_PtrSize(p1->vCis) > 0 );
assert( Vec_PtrSize(p1->vCos) > 0 );
assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) );
assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) );
// create the manager
pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 );
pAig->pName = Aig_UtilStrsav( p1->pName );
pAig->pSpec = Aig_UtilStrsav( p1->pSpec );
vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) );
// placehoder output to be used later for the miter output
Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
/////////////////////////////////////////////////////
// primary inputs
Ntl_ManForEachCiNet( p1, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( pAig );
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
return 0;
}
pNet->nVisits = 2;
}
// latch outputs
pRoot1 = Ntl_ManRootModel(p1);
Ntl_ModelForEachLatch( pRoot1, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( pAig );
if ( (pObj->LatchId & 3) == 1 )
pNet->pCopy = Aig_Not(pNet->pCopy);
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
return 0;
}
pNet->nVisits = 2;
}
// derive the outputs
Ntl_ManForEachCoNet( p1, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManCollapse_rec( p1, pNet ) )
{
printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
return 0;
}
// Aig_ObjCreatePo( pAig, pNet->pCopy );
Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy );
}
// visit the nodes starting from latch inputs outputs
Ntl_ModelForEachLatch( pRoot1, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManCollapse_rec( p1, pNet ) )
{
printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
return 0;
}
if ( (pObj->LatchId & 3) == 1 )
Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
else
Aig_ObjCreatePo( pAig, pNet->pCopy );
}
/////////////////////////////////////////////////////
// primary inputs
Ntl_ManForEachCiNet( p2, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ManPi( pAig, i );
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
return 0;
}
pNet->nVisits = 2;
}
// latch outputs
pRoot2 = Ntl_ManRootModel(p2);
Ntl_ModelForEachLatch( pRoot2, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( pAig );
if ( (pObj->LatchId & 3) == 1 )
pNet->pCopy = Aig_Not(pNet->pCopy);
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
return 0;
}
pNet->nVisits = 2;
}
// derive the outputs
Ntl_ManForEachCoNet( p2, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManCollapse_rec( p2, pNet ) )
{
printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
return 0;
}
// Aig_ObjCreatePo( pAig, pNet->pCopy );
Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy );
}
// visit the nodes starting from latch inputs outputs
Ntl_ModelForEachLatch( pRoot2, pObj, i )
{
pNet = Ntl_ObjFanin0(pObj);
if ( !Ntl_ManCollapse_rec( p2, pNet ) )
{
printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
return 0;
}
if ( (pObj->LatchId & 3) == 1 )
Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
else
Aig_ObjCreatePo( pAig, pNet->pCopy );
}
/////////////////////////////////////////////////////
pMiter = Aig_Miter(pAig, vPairs);
Vec_PtrFree( vPairs );
Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter );
pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 );
Aig_ManCleanup( pAig );
return pAig;
}
/**Function*************************************************************
Synopsis [Increments reference counter of the net.]

164
src/aig/ntl/ntlFraig.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "ntl.h"
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -30,10 +31,10 @@
/**Function*************************************************************
Synopsis [Returns AIG with WB after fraiging.]
Synopsis [Transfers equivalence class info from pAigCol to pAig.]
Description [pAig points to the nodes of pNew derived using it.
pNew points to the nodes of pAigCol derived using it.]
Description [pAig points to the nodes of netlist (pNew) derived using it.
pNew points to the nodes of the collapsed AIG (pAigCol) derived using it.]
SideEffects []
@ -59,6 +60,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
}
// create mapping from the collapsed manager into the original manager
// (each node in the collapsed manager may have more than one equivalent node
// in the original manager; this procedure finds the first node in the original
// manager that is equivalent to the given node in the collapsed manager)
pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) );
memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) );
Aig_ManForEachObj( pAig, pObj, i )
@ -115,16 +119,15 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
assert( pAig->pReprs == NULL );
// create a new netlist whose nodes are in 1-to-1 relationship with AIG
pNew = Ntl_ManDup( p );
if ( !Ntl_ManInsertAig( pNew, pAig ) )
pNew = Ntl_ManInsertAig( p, pAig );
if ( pNew == NULL )
{
Ntl_ManFree( pNew );
printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
return NULL;
}
// collapse the AIG
pAigCol = Ntl_ManCollapse( pNew );
pAigCol = Ntl_ManCollapse( pNew, 0 );
// perform fraiging for the given design
if ( nPartSize == 0 )
nPartSize = Aig_ManPoNum(pAigCol);
@ -148,6 +151,153 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
return pTemp;
}
/**Function*************************************************************
Synopsis [Performs sequential cleanup.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
{
Ntl_Man_t * pNew;
Aig_Man_t * pAigCol, * pTemp;
assert( pAig->pReprs == NULL );
// create a new netlist whose nodes are in 1-to-1 relationship with AIG
pNew = Ntl_ManInsertAig( p, pAig );
if ( pNew == NULL )
{
printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
return NULL;
}
// collapse the AIG
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform fraiging for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
// transfer equivalence classes to the original AIG
pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
// cleanup
Aig_ManStop( pAigCol );
Ntl_ManFree( pNew );
// derive the new AIG
pTemp = Aig_ManDupRepresDfs( pAig );
// duplicate the timing manager
if ( pAig->pManTime )
pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
// reset levels
Aig_ManChoiceLevel( pTemp );
return pTemp;
}
/**Function*************************************************************
Synopsis [Returns AIG with WB after fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose )
{
Ntl_Man_t * pNew;
Aig_Man_t * pAigCol, * pTemp;
assert( pAig->pReprs == NULL );
// create a new netlist whose nodes are in 1-to-1 relationship with AIG
pNew = Ntl_ManInsertAig( p, pAig );
if ( pNew == NULL )
{
printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
return NULL;
}
// collapse the AIG
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform fraiging for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
Aig_ManStop( pTemp );
// transfer equivalence classes to the original AIG
pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
// cleanup
Aig_ManStop( pAigCol );
Ntl_ManFree( pNew );
// derive the new AIG
pTemp = Aig_ManDupRepresDfs( pAig );
// duplicate the timing manager
if ( pAig->pManTime )
pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
// reset levels
Aig_ManChoiceLevel( pTemp );
return pTemp;
}
/**Function*************************************************************
Synopsis [Returns AIG with WB after fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
{
Ntl_Man_t * pNew;
Aig_Man_t * pAigCol, * pTemp;
assert( pAig->pReprs == NULL );
// create a new netlist whose nodes are in 1-to-1 relationship with AIG
pNew = Ntl_ManInsertAig( p, pAig );
if ( pNew == NULL )
{
printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
return NULL;
}
// collapse the AIG
pAigCol = Ntl_ManCollapse( pNew, 1 );
// perform fraiging for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Fra_FraigInduction( pAigCol, pPars );
Aig_ManStop( pTemp );
// transfer equivalence classes to the original AIG
pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
// cleanup
Aig_ManStop( pAigCol );
Ntl_ManFree( pNew );
// derive the new AIG
pTemp = Aig_ManDupRepresDfs( pAig );
// duplicate the timing manager
if ( pAig->pManTime )
pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
// reset levels
Aig_ManChoiceLevel( pTemp );
return pTemp;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

90
src/aig/ntl/ntlInsert.c
View File

@ -40,7 +40,7 @@
SeeAlso []
***********************************************************************/
int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
{
char Buffer[100];
Vec_Ptr_t * vCopies;
@ -50,16 +50,14 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
Ntl_Net_t * pNet, * pNetCo;
Ntl_Lut_t * pLut;
int i, k, nDigits;
assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
p = Ntl_ManStartFrom( p );
pRoot = Ntl_ManRootModel( p );
assert( Ntl_ModelNodeNum(pRoot) == 0 );
// map the AIG back onto the design
Ntl_ManForEachCiNet( p, pNet, i )
pNet->pCopy = Aig_ManPi( pAig, i );
Ntl_ManForEachCoNet( p, pNet, i )
pNet->pCopy = Aig_ObjChild0( Aig_ManPo( pAig, i ) );
// remove old nodes
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachNode( pRoot, pNode, i )
Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
pRoot->nObjs[NTL_OBJ_NODE] = 0;
// start mapping of AIG nodes into their copies
vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
Ntl_ManForEachCiNet( p, pNet, i )
@ -101,19 +99,19 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
Vec_IntFree( vCover );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
pNetCo->nVisits = 101; // using "101" is harmless because nVisits can only be 0, 1 or 2
pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
if ( pNetCo->nVisits == 101 )
if ( pNetCo->fMark )
continue;
pNetCo->nVisits = 101;
pNetCo->fMark = 1;
pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
pNode = Ntl_ModelCreateNode( pRoot, 1 );
pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
pNetCo->pDriver = NULL;
assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
@ -121,7 +119,11 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
}
}
Vec_PtrFree( vCopies );
return 1;
// clean CI/CO marks
Ntl_ManUnmarkCiCoNets( p );
if ( !Ntl_ManCheck( p ) )
printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
return p;
}
/**Function*************************************************************
@ -135,7 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
{
char Buffer[100];
Ntl_Mod_t * pRoot;
@ -145,17 +147,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
int i, nDigits, Counter;
assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
p = Ntl_ManStartFrom( p );
pRoot = Ntl_ManRootModel( p );
assert( Ntl_ModelNodeNum(pRoot) == 0 );
// set the correspondence between the PI/PO nodes
Aig_ManCleanData( pAig );
Ntl_ManForEachCiNet( p, pNet, i )
Aig_ManPi( pAig, i )->pData = pNet;
// Ntl_ManForEachCoNet( p, pNet, i )
// Nwk_ManCo( pNtk, i )->pCopy = pNet;
// remove old nodes
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachNode( pRoot, pNode, i )
Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
pRoot->nObjs[NTL_OBJ_NODE] = 0;
// create constant node if needed
if ( Aig_ManConst1(pAig)->nRefs > 0 )
{
@ -213,13 +211,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
}
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
pNetCo->nVisits = 101;
pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
if ( pNetCo->nVisits == 101 )
if ( pNetCo->fMark )
continue;
pNetCo->nVisits = 101;
pNetCo->fMark = 1;
// get the corresponding PO and its driver
pObj = Aig_ManPo( pAig, i );
pFanin = Aig_ObjFanin0( pObj );
@ -229,14 +227,18 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
pNetCo->pDriver = NULL;
assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
printf( "Ntl_ManInsertAig(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
return 1;
// clean CI/CO marks
Ntl_ManUnmarkCiCoNets( p );
if ( !Ntl_ManCheck( p ) )
printf( "Ntl_ManInsertAig: The check has failed for design %s.\n", p->pName );
return p;
}
@ -251,7 +253,7 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
{
char Buffer[100];
Vec_Ptr_t * vObjs;
@ -265,16 +267,12 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
unsigned * pTruth;
assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
p = Ntl_ManStartFrom( p );
pRoot = Ntl_ManRootModel( p );
assert( Ntl_ModelNodeNum(pRoot) == 0 );
// set the correspondence between the PI/PO nodes
Ntl_ManForEachCiNet( p, pNet, i )
Nwk_ManCi( pNtk, i )->pCopy = pNet;
// Ntl_ManForEachCoNet( p, pNet, i )
// Nwk_ManCo( pNtk, i )->pCopy = pNet;
// remove old nodes
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachNode( pRoot, pNode, i )
Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
pRoot->nObjs[NTL_OBJ_NODE] = 0;
// create a new node for each LUT
vTruth = Vec_IntAlloc( 1 << 16 );
vCover = Vec_IntAlloc( 1 << 16 );
@ -298,7 +296,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pNet = pFanin->pCopy;
if ( pNet == NULL )
{
printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
return 0;
}
Ntl_ObjSetFanin( pNode, pNet, k );
@ -307,13 +305,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
sprintf( Buffer, "lut%0*d", nDigits, i );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
return 0;
}
pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
{
printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
return 0;
}
pObj->pCopy = pNet;
@ -323,13 +321,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
Vec_IntFree( vTruth );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
pNetCo->nVisits = 101;
pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
if ( pNetCo->nVisits == 101 )
if ( pNetCo->fMark )
continue;
pNetCo->nVisits = 101;
pNetCo->fMark = 1;
// get the corresponding PO and its driver
pObj = Nwk_ManCo( pNtk, i );
pFanin = Nwk_ObjFanin0( pObj );
@ -339,14 +337,18 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
pNetCo->pDriver = NULL;
assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
return 1;
// clean CI/CO marks
Ntl_ManUnmarkCiCoNets( p );
if ( !Ntl_ManCheck( p ) )
printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
return p;
}

137
src/aig/ntl/ntlMan.c
View File

@ -61,7 +61,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
/**Function*************************************************************
Synopsis [Duplicates the interface of the top level model.]
Synopsis [Cleanups extended representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManCleanup( Ntl_Man_t * p )
{
Vec_PtrClear( p->vCis );
Vec_PtrClear( p->vCos );
Vec_PtrClear( p->vNodes );
Vec_IntClear( p->vBox1Cos );
if ( p->pAig )
{
Aig_ManStop( p->pAig );
p->pAig = NULL;
}
if ( p->pManTime )
{
Tim_ManStop( p->pManTime );
p->pManTime = NULL;
}
}
/**Function*************************************************************
Synopsis [Duplicates the design without the nodes of the root model.]
Description []
@ -72,12 +101,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
***********************************************************************/
Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
{
return NULL;
Ntl_Man_t * pNew;
Ntl_Mod_t * pModel;
Ntl_Obj_t * pBox;
Ntl_Net_t * pNet;
int i, k;
pNew = Ntl_ManAlloc( pOld->pSpec );
Vec_PtrForEachEntry( pOld->vModels, pModel, i )
if ( i == 0 )
{
Ntl_ManMarkCiCoNets( pOld );
pModel->pCopy = Ntl_ModelStartFrom( pNew, pModel );
Ntl_ManUnmarkCiCoNets( pOld );
}
else
pModel->pCopy = Ntl_ModelDup( pNew, pModel );
Vec_PtrForEachEntry( pOld->vModels, pModel, i )
Ntl_ModelForEachBox( pModel, pBox, k )
((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
Ntl_ManForEachCiNet( pOld, pNet, i )
Vec_PtrPush( pNew->vCis, pNet->pCopy );
Ntl_ManForEachCoNet( pOld, pNet, i )
Vec_PtrPush( pNew->vCos, pNet->pCopy );
if ( pOld->pManTime )
pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the interface of the top level model.]
Synopsis [Duplicates the design.]
Description []
@ -142,6 +195,22 @@ void Ntl_ManFree( Ntl_Man_t * p )
free( p );
}
/**Function*************************************************************
Synopsis [Returns 1 if the design is combinational.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManIsComb( Ntl_Man_t * p )
{
return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0;
}
/**Function*************************************************************
Synopsis [Find the model with the given name.]
@ -178,15 +247,18 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
pRoot = Ntl_ManRootModel( p );
printf( "%-15s : ", p->pName );
printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) );
printf( "po = %5d ", Ntl_ModelPoNum(pRoot) );
printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) );
printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) );
printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) );
printf( "mod = %3d", Vec_PtrSize(p->vModels) );
printf( "%-15s : ", p->pName );
printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) );
printf( "po = %5d ", Ntl_ModelPoNum(pRoot) );
printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) );
printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) );
printf( "inv/buf = %5d ", Ntl_ModelLut1Num(pRoot) );
printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) );
printf( "mod = %3d ", Vec_PtrSize(p->vModels) );
printf( "net = %d", Ntl_ModelCountNets(pRoot) );
printf( "\n" );
fflush( stdout );
assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
}
/**Function*************************************************************
@ -235,6 +307,50 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the model without nodes but with CI/CO nets.]
Description [The CI/CO nets of the old model should be marked before
calling this procedure.]
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
{
Ntl_Mod_t * pModelNew;
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
int i, k;
pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
Ntl_ModelForEachNet( pModelOld, pNet, i )
if ( pNet->fMark )
pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
else
pNet->pCopy = NULL;
Ntl_ModelForEachObj( pModelOld, pObj, i )
{
if ( Ntl_ObjIsNode(pObj) )
continue;
pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
Ntl_ObjForEachFanin( pObj, pNet, k )
if ( pNet->pCopy != NULL )
Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
Ntl_ObjForEachFanout( pObj, pNet, k )
if ( pNet->pCopy != NULL )
Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
if ( Ntl_ObjIsLatch(pObj) )
((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
}
pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
return pModelNew;
}
/**Function*************************************************************
Synopsis [Duplicates the model.]
@ -286,6 +402,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
assert( Ntl_ManCheckNetsAreNotMarked(p) );
if ( p->vRequireds ) Vec_IntFree( p->vRequireds );
if ( p->vArrivals ) Vec_IntFree( p->vArrivals );
if ( p->vDelays ) Vec_IntFree( p->vDelays );

29
src/aig/ntl/ntlObj.c
View File

@ -131,7 +131,10 @@ Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins )
p->Type = NTL_OBJ_NODE;
p->nFanins = nFanins;
p->nFanouts = 1;
pModel->nObjs[NTL_OBJ_NODE]++;
if ( nFanins == 1 )
pModel->nObjs[NTL_OBJ_LUT1]++;
else
pModel->nObjs[NTL_OBJ_NODE]++;
return p;
}
@ -188,6 +191,30 @@ Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld )
return pNew;
}
/**Function*************************************************************
Synopsis [Creates the primary input with the given name.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName )
{
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
pNet = Ntl_ModelFindOrCreateNet( pModel, pName );
if ( pNet->pDriver )
return NULL;
pObj = Ntl_ModelCreatePi( pModel );
Ntl_ModelSetNetDriver( pObj, pNet );
return pObj;
}
/**Function*************************************************************
Synopsis [Allocates memory and copies the name into it.]

6
src/aig/ntl/ntlReadBlif.c
View File

@ -109,7 +109,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
FILE * pFile;
Ioa_ReadMan_t * p;
Ntl_Man_t * pDesign;
int nNodes;
// int nNodes;
// check that the file is available
pFile = fopen( pFileName, "rb" );
@ -166,8 +166,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
}
// transform the design by removing the CO drivers
if ( (nNodes = Ntl_ManTransformCoDrivers(pDesign)) )
printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
// if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) )
// printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
//Ioa_WriteBlif( pDesign, "_temp_.blif" );
return pDesign;
}

165
src/aig/ntl/ntlSweep.c Normal file
View File

@ -0,0 +1,165 @@
/**CFile****************************************************************
FileName [ntlSweep.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Performs structural sweep of the netlist.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntl.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Detects logic that does not fanout into POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManSweepMark_rec( Ntl_Man_t * p, Ntl_Obj_t * pObj )
{
Ntl_Net_t * pNet;
int i;
if ( pObj->fMark )
return;
pObj->fMark = 1;
Ntl_ObjForEachFanin( pObj, pNet, i )
Ntl_ManSweepMark_rec( p, pNet->pDriver );
}
/**Function*************************************************************
Synopsis [Detects logic that does not fanout into POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManSweepMark( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pObj;
int i;
// get the root model
pRoot = Ntl_ManRootModel( p );
// clear net visited flags
Ntl_ModelForEachObj( pRoot, pObj, i )
assert( pObj->fMark == 0 );
// label the primary inputs
Ntl_ModelForEachPi( pRoot, pObj, i )
pObj->fMark = 1;
// start from the primary outputs
Ntl_ModelForEachPo( pRoot, pObj, i )
Ntl_ManSweepMark_rec( p, pObj );
}
/**Function*************************************************************
Synopsis [Derives new netlist by sweeping current netlist with the current AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
{
int nObjsOld[NTL_OBJ_VOID];
Ntl_Man_t * pNew;
Ntl_Mod_t * pRoot;
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
int i, k, nNetsOld;
// insert the AIG into the netlist
pNew = Ntl_ManInsertAig( p, pAig );
if ( pNew == NULL )
{
printf( "Ntl_ManSweep(): Inserting AIG has failed.\n" );
return NULL;
}
// remember the number of objects
pRoot = Ntl_ManRootModel( pNew );
for ( i = 0; i < NTL_OBJ_VOID; i++ )
nObjsOld[i] = pRoot->nObjs[i];
nNetsOld = Ntl_ModelCountNets(pRoot);
// mark the nets that do not fanout into POs
Ntl_ManSweepMark( pNew );
// remove the useless objects and their nets
Ntl_ModelForEachObj( pRoot, pObj, i )
{
if ( pObj->fMark )
{
pObj->fMark = 0;
continue;
}
// remove the fanout nets
Ntl_ObjForEachFanout( pObj, pNet, k )
Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) );
// remove the object
if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
pRoot->nObjs[NTL_OBJ_LUT1]--;
else
pRoot->nObjs[pObj->Type]--;
Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL );
pObj->Id = NTL_OBJ_NONE;
}
// print detailed statistics of sweeping
if ( fVerbose )
{
printf( "Sweep:" );
printf( " Node = %d (%4.1f %%)",
nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE],
!nObjsOld[NTL_OBJ_NODE]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE]) / nObjsOld[NTL_OBJ_NODE] );
printf( " Buf/Inv = %d (%4.1f %%)",
nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1],
!nObjsOld[NTL_OBJ_LUT1]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1]) / nObjsOld[NTL_OBJ_LUT1] );
printf( " Lat = %d (%4.1f %%)",
nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH],
!nObjsOld[NTL_OBJ_LATCH]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH]) / nObjsOld[NTL_OBJ_LATCH] );
printf( " Box = %d (%4.1f %%)",
nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX],
!nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] );
printf( "\n" );
// printf( "Also, sweep reduced %d nets.\n", nNetsOld - Ntl_ModelCountNets(pRoot) );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

20
src/aig/ntl/ntlTable.c
View File

@ -239,6 +239,26 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
return 1;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountNets( Ntl_Mod_t * p )
{
Ntl_Net_t * pNet;
int i, Counter = 0;
Ntl_ModelForEachNet( p, pNet, i )
Counter++;
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

208
src/aig/ntl/ntlUtil.c
View File

@ -30,7 +30,28 @@
/**Function*************************************************************
Synopsis [Returns 1 if netlist was written by ABC with added bufs/invs.]
Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
{
Ntl_Obj_t * pObj;
int i, Counter = 0;
Ntl_ModelForEachNode( pRoot, pObj, i )
if ( Ntl_ObjFaninNum(pObj) == 1 )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Connects COs to the internal nodes other than inv/bufs.]
Description [Should be called immediately after reading from file.]
@ -38,6 +59,63 @@
SeeAlso []
***********************************************************************/
int Ntl_ManCountSimpleCoDriversOne( Ntl_Net_t * pNetCo )
{
Ntl_Net_t * pNetFanin;
// skip the case when the net is not driven by a node
if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
return 0;
// skip the case when the node is not an inv/buf
if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
return 0;
// skip the case when the second-generation driver is not a node
pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p )
{
Ntl_Net_t * pNetCo;
Ntl_Obj_t * pObj;
Ntl_Mod_t * pRoot;
int i, k, Counter;
Counter = 0;
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachPo( pRoot, pObj, i )
Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
Ntl_ModelForEachLatch( pRoot, pObj, i )
Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
Ntl_ModelForEachBox( pRoot, pObj, i )
Ntl_ObjForEachFanin( pObj, pNetCo, k )
Counter += Ntl_ManCountSimpleCoDriversOne( pNetCo );
return Counter;
}
/**Function*************************************************************
Synopsis [Removes the CO drivers that are bufs/invs.]
Description [Should be called immediately after reading from file.]
SideEffects [This procedure does not work because the internal net
(pNetFanin) may have other drivers.]
SeeAlso []
***********************************************************************/
int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
{
@ -110,7 +188,71 @@ int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
Counter++;
}
Vec_PtrFree( vCoNets );
pRoot->nObjs[NTL_OBJ_NODE] -= Counter;
pRoot->nObjs[NTL_OBJ_LUT1] -= Counter;
return Counter;
}
/**Function*************************************************************
Synopsis [Connects COs to the internal nodes other than inv/bufs.]
Description [Should be called immediately after reading from file.]
SideEffects [This procedure does not work because the internal net
(pNetFanin) may have other drivers.]
SeeAlso []
***********************************************************************/
int Ntl_ManReconnectCoDriverOne( Ntl_Net_t * pNetCo )
{
Ntl_Net_t * pNetFanin;
// skip the case when the net is not driven by a node
if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
return 0;
// skip the case when the node is not an inv/buf
if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
return 0;
// skip the case when the second-generation driver is not a node
pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
return 0;
// set the complemented attribute of the net
pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
// drive the CO net with the second-generation driver
pNetCo->pDriver = NULL;
pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
if ( !Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo ) )
printf( "Ntl_ManReconnectCoDriverOne(): Cannot connect the net.\n" );
return 1;
}
/**Function*************************************************************
Synopsis [Connects COs to the internal nodes other than inv/bufs.]
Description [Should be called immediately after reading from file.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p )
{
Ntl_Net_t * pNetCo;
Ntl_Obj_t * pObj;
Ntl_Mod_t * pRoot;
int i, k, Counter;
Counter = 0;
pRoot = Ntl_ManRootModel( p );
Ntl_ModelForEachPo( pRoot, pObj, i )
Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
Ntl_ModelForEachLatch( pRoot, pObj, i )
Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
Ntl_ModelForEachBox( pRoot, pObj, i )
Ntl_ObjForEachFanin( pObj, pNetCo, k )
Counter += Ntl_ManReconnectCoDriverOne( pNetCo );
return Counter;
}
@ -158,6 +300,68 @@ Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p )
return vNames;
}
/**Function*************************************************************
Synopsis [Marks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManMarkCiCoNets( Ntl_Man_t * p )
{
Ntl_Net_t * pNet;
int i;
Ntl_ManForEachCiNet( p, pNet, i )
pNet->fMark = 1;
Ntl_ManForEachCoNet( p, pNet, i )
pNet->fMark = 1;
}
/**Function*************************************************************
Synopsis [Unmarks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
{
Ntl_Net_t * pNet;
int i;
Ntl_ManForEachCiNet( p, pNet, i )
pNet->fMark = 0;
Ntl_ManForEachCoNet( p, pNet, i )
pNet->fMark = 0;
}
/**Function*************************************************************
Synopsis [Unmarks the CI/CO nets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
{
Ntl_Net_t * pNet;
int i;
Ntl_ModelForEachNet( pModel, pNet, i )
assert( pNet->fMark == 0 );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/nwk/nwkMan.c
View File

@ -100,7 +100,6 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
printf( "LUTs by size: " );
for ( i = 0; i <= pLutLib->LutMax; i++ )
printf( "%d:%d ", i, Counters[i] );
printf( "\n" );
}
/**Function*************************************************************
@ -124,6 +123,7 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
printf( "co = %5d ", Nwk_ManCoNum(p) );
printf( "lat = %5d ", Nwk_ManLatchNum(p) );
printf( "node = %5d ", Nwk_ManNodeNum(p) );
printf( "edge = %5d ", Nwk_ManGetTotalFanins(p) );
printf( "aig = %6d ", Nwk_ManGetAigNodeNum(p) );
printf( "lev = %3d ", Nwk_ManLevel(p) );
// printf( "lev2 = %3d ", Nwk_ManLevelBackup(p) );

3
src/base/abc/abcCheck.c
View File

@ -725,7 +725,8 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
Description []
SideEffects []
SideEffects [Ordering POs by name is a very bad idea! It destroys
the natural order of the logic in the circuit.]
SeeAlso []

554
src/base/abci/abc.c
View File

@ -218,6 +218,7 @@ static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -456,6 +457,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*b", Abc_CommandAbc8Balance, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*speedup", Abc_CommandAbc8Speedup, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*fraig", Abc_CommandAbc8Fraig, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*sw", Abc_CommandAbc8Sweep, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*cec", Abc_CommandAbc8Cec, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*lcorr", Abc_CommandAbc8Lcorr, 0 );
@ -14868,8 +14870,8 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAig;
int c;
extern void Ioa_WriteBlif( void * p, char * pFileName );
extern int Ntl_ManInsertNtk( void * p, void * pNtk );
extern int Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
extern void * Ntl_ManDup( void * pOld );
extern void Ntl_ManFree( void * p );
@ -14895,16 +14897,19 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
// create the design to write
pTemp = Ntl_ManDup( pAbc->pAbc8Ntl );
pFileName = argv[globalUtilOptind];
if ( fAig )
{
if ( pAbc->pAbc8Aig != NULL )
{
if ( !Ntl_ManInsertAig( pTemp, pAbc->pAbc8Aig ) )
pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
if ( pTemp == NULL )
{
printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
return 1;
}
Ioa_WriteBlif( pTemp, pFileName );
Ntl_ManFree( pTemp );
}
else
{
@ -14916,19 +14921,22 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( pAbc->pAbc8Nwk != NULL )
{
if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
if ( pTemp == NULL )
{
printf( "Abc_CommandAbc8Write(): Inserting mapped network has failed.\n" );
return 1;
}
Ioa_WriteBlif( pTemp, pFileName );
Ntl_ManFree( pTemp );
}
else
{
pTemp = pAbc->pAbc8Ntl;
printf( "Writing the original design.\n" );
Ioa_WriteBlif( pTemp, pFileName );
}
}
// get the input file name
pFileName = argv[globalUtilOptind];
Ioa_WriteBlif( pTemp, pFileName );
Ntl_ManFree( pTemp );
return 0;
usage:
@ -15093,8 +15101,6 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
If_Par_t Pars, * pPars = &Pars;
void * pNtkNew;
int c;
extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig );
extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig );
extern void * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
extern If_Lib_t * If_SetSimpleLutLib( int nLutSize );
@ -15126,15 +15132,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
return 1;
}
/*
// get the input file name
if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
// if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
{
printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" );
return 1;
}
*/
pNtkNew = Nwk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
if ( pNtkNew == NULL )
{
@ -16042,6 +16040,78 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
{
void * pNtlNew;
int fVerbose;
int c;
extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
extern Aig_Man_t * Ntl_ManExtract( void * p );
// set defaults
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
return 1;
}
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
return 1;
}
// sweep the current design
pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
if ( pNtlNew == NULL )
{
printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
return 1;
}
// replace
Abc_FrameClearDesign();
pAbc->pAbc8Ntl = pNtlNew;
pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
return 1;
}
return 0;
usage:
fprintf( stdout, "usage: *sw [-h]\n" );
fprintf( stdout, "\t reads the design with whiteboxes\n" );
fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -16064,11 +16134,12 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfLimit;
int fSmart;
int nPartSize;
extern Aig_Man_t * Ntl_ManCollapse( void * p );
extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
extern void * Ntl_ManDup( void * pOld );
extern void Ntl_ManFree( void * p );
extern int Ntl_ManInsertNtk( void * p, void * pNtk );
extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
// set defaults
@ -16116,31 +16187,42 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 0 )
if ( nArgcNew != 0 && nArgcNew != 2 )
{
printf( "Currently can only compare current network against the spec.\n" );
printf( "Currently can only compare current mapped network against the spec, or designs derived from two files.\n" );
return 0;
}
if ( nArgcNew == 2 )
{
Ntl_ManPrepareCec( pArgvNew[0], pArgvNew[1], &pAig1, &pAig2 );
if ( !pAig1 || !pAig2 )
return 1;
Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
Aig_ManStop( pAig1 );
Aig_ManStop( pAig2 );
return 0;
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Cec(): There is no design to verify.\n" );
return 0;
return 1;
}
if ( pAbc->pAbc8Nwk == NULL )
{
printf( "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
return 0;
return 1;
}
// derive AIGs
pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl );
pTemp = Ntl_ManDup( pAbc->pAbc8Ntl );
if ( !Ntl_ManInsertNtk( pTemp, pAbc->pAbc8Nwk ) )
pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
if ( pTemp == NULL )
{
printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
return 1;
}
pAig2 = Ntl_ManCollapse( pTemp );
pAig2 = Ntl_ManCollapse( pTemp, 0 );
Ntl_ManFree( pTemp );
// perform verification
@ -16160,7 +16242,7 @@ usage:
fprintf( stdout, "\tfile1 : (optional) the file with the first network\n");
fprintf( stdout, "\tfile2 : (optional) the file with the second network\n");
fprintf( stdout, "\t if no files are given, uses the current network and its spec\n");
fprintf( stdout, "\t if one file is given, uses the current network and the file\n");
fprintf( stdout, "\t if two files are given, compares designs derived from files\n");
return 1;
}
@ -16177,7 +16259,77 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAigNew;
int c;
int fLatchConst;
int fLatchEqual;
int fVerbose;
extern Aig_Man_t * Ntl_ManScl( void * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
extern int Ntl_ManIsComb( void * p );
// set defaults
fLatchConst = 1;
fLatchEqual = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fLatchConst ^= 1;
break;
case 'e':
fLatchEqual ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Scl(): There is no design to SAT sweep.\n" );
return 1;
}
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Scl(): There is no AIG to SAT sweep.\n" );
return 1;
}
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
return 0;
}
// get the input file name
pAigNew = Ntl_ManScl( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fLatchConst, fLatchEqual, fVerbose );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8Scl(): Tranformation of the AIG has failed.\n" );
return 1;
}
if ( pAbc->pAbc8Aig )
Aig_ManStop( pAbc->pAbc8Aig );
pAbc->pAbc8Aig = pAigNew;
return 0;
usage:
fprintf( stdout, "usage: *scl [-cevh]\n" );
fprintf( stdout, "\t performs sequential cleanup of the current network\n" );
fprintf( stdout, "\t by removing nodes and latches that do not feed into POs\n" );
fprintf( stdout, "\t-c : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
fprintf( stdout, "\t-e : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -16193,7 +16345,92 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAigNew;
int c;
int nFramesP;
int nConfMax;
int fVerbose;
extern Aig_Man_t * Ntl_ManLcorr( void * p, Aig_Man_t * pAig, int nConfMax, int fVerbose );
extern int Ntl_ManIsComb( void * p );
// set defaults
nFramesP = 0;
nConfMax = 10000;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nFramesP = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesP < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
return 1;
}
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
return 1;
}
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
return 0;
}
// get the input file name
pAigNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nConfMax, fVerbose );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
return 1;
}
if ( pAbc->pAbc8Aig )
Aig_ManStop( pAbc->pAbc8Aig );
pAbc->pAbc8Aig = pAigNew;
return 0;
usage:
fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" );
fprintf( stdout, "\t computes latch correspondence using 1-step induction\n" );
// fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -16209,7 +16446,184 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAigNew;
Fra_Ssw_t Pars, * pPars = &Pars;
int c;
extern Aig_Man_t * Ntl_ManSsw( void * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars );
extern int Ntl_ManIsComb( void * p );
// set defaults
pPars->nPartSize = 0;
pPars->nOverSize = 0;
pPars->nFramesP = 0;
pPars->nFramesK = 1;
pPars->nMaxImps = 5000;
pPars->nMaxLevs = 0;
pPars->fUseImps = 0;
pPars->fRewrite = 0;
pPars->fFraiging = 0;
pPars->fLatchCorr = 0;
pPars->fWriteImps = 0;
pPars->fUse1Hot = 0;
pPars->fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPartSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPartSize < 2 )
goto usage;
break;
case 'Q':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
goto usage;
}
pPars->nOverSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nOverSize < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesP = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesP < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesK = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesK <= 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMaxImps = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMaxImps <= 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMaxLevs <= 0 )
goto usage;
break;
case 'i':
pPars->fUseImps ^= 1;
break;
case 'r':
pPars->fRewrite ^= 1;
break;
case 'f':
pPars->fFraiging ^= 1;
break;
case 'l':
pPars->fLatchCorr ^= 1;
break;
case 'e':
pPars->fWriteImps ^= 1;
break;
case 't':
pPars->fUse1Hot ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pAbc8Ntl == NULL )
{
printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
return 1;
}
if ( pAbc->pAbc8Aig == NULL )
{
printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
return 1;
}
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
return 0;
}
if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
{
printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
return 0;
}
if ( pPars->nFramesP && pPars->fUse1Hot )
{
printf( "Currrently can only use one-hotness without prefix.\n" );
return 0;
}
// get the input file name
pAigNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pPars );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
return 1;
}
if ( pAbc->pAbc8Aig )
Aig_ManStop( pAbc->pAbc8Aig );
pAbc->pAbc8Aig = pAigNew;
return 0;
usage:
fprintf( stdout, "usage: *ssw [-PQNFL num] [-lrfetvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
// fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
// fprintf( stdout, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( stdout, "\t-r : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
fprintf( stdout, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
fprintf( stdout, "\t-e : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
fprintf( stdout, "\t-t : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -16225,7 +16639,85 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAig;
char ** pArgvNew;
int nArgcNew;
int c;
int fRetimeFirst;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
// set defaults
nFrames = 16;
fRetimeFirst = 1;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'r':
fRetimeFirst ^= 1;
break;
case 'f':
fFraiging ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
default:
goto usage;
}
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 2 )
{
printf( "Only works for two designs written from files specified on the command line.\n" );
return 1;
}
pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
Fra_FraigSec( pAig, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
Aig_ManStop( pAig );
return 0;
usage:
fprintf( stdout, "usage: *dsec [-K num] [-rfwvh] <file1> <file2>\n" );
fprintf( stdout, "\t performs sequential equivalence checking for two designs\n" );
fprintf( stdout, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( stdout, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( stdout, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
fprintf( stdout, "\tfile1 : the file with the first design\n");
fprintf( stdout, "\tfile2 : the file with the second design\n");
// fprintf( stdout, "\t if no files are given, uses the current network and its spec\n");
// fprintf( stdout, "\t if one file is given, uses the current network and the file\n");
return 1;
}

17
src/base/abci/abcDar.c
View File

@ -1288,15 +1288,20 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
Aig_ManSeqCleanup( pMan );
if ( fLatchConst && pMan->nRegs )
pMan = Aig_ManConstReduce( pMan, fVerbose );
if ( fLatchEqual && pMan->nRegs )
pMan = Aig_ManReduceLaches( pMan, fVerbose );
// Aig_ManSeqCleanup( pMan );
// if ( fLatchConst && pMan->nRegs )
// pMan = Aig_ManConstReduce( pMan, fVerbose );
// if ( fLatchEqual && pMan->nRegs )
// pMan = Aig_ManReduceLaches( pMan, fVerbose );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;