From e94ccfd3fb07d22ed426e0386ccf536e470744b7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 8 May 2008 08:01:00 -0700 Subject: Version abc80508 --- abc.dsp | 6 +- src/aig/aig/aig.h | 1 + src/aig/aig/aigDup.c | 2 + src/aig/aig/aigMan.c | 2 +- src/aig/aig/aigObj.c | 6 +- src/aig/aig/aigTsim.c | 4 +- src/aig/aig/aigUtil.c | 88 +++++++++++++++++++ src/aig/bbr/bbrImage.c | 6 +- src/aig/bbr/module.make | 2 +- src/aig/cnf/cnf.h | 1 + src/aig/cnf/cnfMan.c | 24 +++++ src/aig/cnf/cnfWrite.c | 15 +++- src/aig/dar/darBalance.c | 2 +- src/aig/fra/fra.h | 2 +- src/aig/fra/fraCec.c | 8 +- src/aig/fra/fraClaus.c | 15 ++-- src/aig/fra/fraHot.c | 3 +- src/aig/fra/fraMan.c | 3 +- src/aig/fra/fraSec.c | 24 +++-- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 2 + src/aig/saig/saigPhase.c | 14 ++- src/aig/saig/saigRetMin.c | 6 ++ src/aig/saig/saigRetStep.c | 202 +++++++++++++++++++++++++++++++++++++++++++ src/base/abc/abcShow.c | 2 +- src/base/abci/abc.c | 26 ++++-- src/base/abci/abcDar.c | 36 ++++++++ src/base/abci/abcDress.c | 2 +- src/base/cmd/cmd.c | 2 +- src/base/io/io.c | 2 +- src/base/io/io.h | 146 ------------------------------- src/base/io/ioAbc.h | 146 +++++++++++++++++++++++++++++++ src/base/io/ioReadAiger.c | 4 +- src/base/io/ioReadBaf.c | 2 +- src/base/io/ioReadBench.c | 2 +- src/base/io/ioReadBlif.c | 2 +- src/base/io/ioReadBlifMv.c | 2 +- src/base/io/ioReadDsd.c | 2 +- src/base/io/ioReadEdif.c | 2 +- src/base/io/ioReadEqn.c | 2 +- src/base/io/ioReadPla.c | 2 +- src/base/io/ioReadVerilog.c | 2 +- src/base/io/ioUtil.c | 2 +- src/base/io/ioWriteAiger.c | 2 +- src/base/io/ioWriteBaf.c | 2 +- src/base/io/ioWriteBench.c | 2 +- src/base/io/ioWriteBlif.c | 2 +- src/base/io/ioWriteBlifMv.c | 2 +- src/base/io/ioWriteCnf.c | 2 +- src/base/io/ioWriteDot.c | 2 +- src/base/io/ioWriteEqn.c | 2 +- src/base/io/ioWriteGml.c | 2 +- src/base/io/ioWriteList.c | 2 +- src/base/io/ioWritePla.c | 2 +- src/base/io/ioWriteVerilog.c | 2 +- src/base/io/io_.c | 2 +- src/base/main/main.h | 2 +- src/opt/fret/fretInit.c | 2 +- 58 files changed, 632 insertions(+), 223 deletions(-) create mode 100644 src/aig/saig/saigRetStep.c delete mode 100644 src/base/io/io.h create mode 100644 src/base/io/ioAbc.h diff --git a/abc.dsp b/abc.dsp index 4fababfe..a484406a 100644 --- a/abc.dsp +++ b/abc.dsp @@ -462,7 +462,7 @@ SOURCE=.\src\base\io\io.c # End Source File # Begin Source File -SOURCE=.\src\base\io\io.h +SOURCE=.\src\base\io\ioabc.h # End Source File # Begin Source File @@ -3266,6 +3266,10 @@ SOURCE=.\src\aig\saig\saigRetMin.c # End Source File # Begin Source File +SOURCE=.\src\aig\saig\saigRetStep.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\saig\saigScl.c # End Source File # End Group diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 47696a41..6ecec3f8 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -622,6 +622,7 @@ extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ); extern void Aig_ManSetPioNumbers( Aig_Man_t * p ); extern void Aig_ManCleanPioNumbers( Aig_Man_t * p ); extern int Aig_ManCountChoices( Aig_Man_t * p ); +extern unsigned Aig_ManRandom( int fReset ); /*=== aigWin.c =========================================================*/ extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index e7623739..9dfa2ddf 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -118,6 +118,8 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ) pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = p->nTruePos; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 47ee8d4d..2e68e93c 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -216,7 +216,7 @@ void Aig_ManStop( Aig_Man_t * p ) FREE( p->pObjCopies ); FREE( p->pReprs ); FREE( p->pEquivs ); - free( p->pTable ); +// free( p->pTable ); free( p ); } diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 9c7cf2c4..88fb9c9d 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -361,7 +361,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in // the object to be replaced cannot be complemented assert( !Aig_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal - assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) ); +// assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) ); + assert( !Aig_ObjIsPo(pObjOld) ); // the object to be used cannot be a buffer or a PO assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) ); // the object cannot be the same @@ -371,7 +372,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in assert( pObjOld != Aig_ObjFanin1(pObjNewR) ); // recursively delete the old node - but leave the object there pObjNewR->nRefs++; - Aig_ObjDelete_rec( p, pObjOld, 0 ); + if ( !Aig_ObjIsPi(pObjOld) ) + Aig_ObjDelete_rec( p, pObjOld, 0 ); pObjNewR->nRefs--; // if the new object is complemented or already used, create a buffer p->nObjs[pObjOld->Type]--; diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c index d3f78902..7b48a73d 100644 --- a/src/aig/aig/aigTsim.c +++ b/src/aig/aig/aigTsim.c @@ -53,13 +53,13 @@ static inline int Aig_XsimAnd( int Value0, int Value1 ) } static inline int Aig_XsimRand2() { - return (rand() & 1) ? AIG_XVS1 : AIG_XVS0; + return (Aig_ManRandom(0) & 1) ? AIG_XVS1 : AIG_XVS0; } static inline int Aig_XsimRand3() { int RetValue; do { - RetValue = rand() & 3; + RetValue = Aig_ManRandom(0) & 3; } while ( RetValue == 0 ); return RetValue; } diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 00e0311d..a01e9582 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -990,6 +990,94 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p ) } } +/**Function************************************************************* + + Synopsis [Creates a sequence or random numbers.] + + Description [] + + SideEffects [] + + SeeAlso [http://en.wikipedia.org/wiki/LFSR] + +***********************************************************************/ +void Aig_ManRandomTest2() +{ + FILE * pFile; + unsigned int lfsr = 1; + unsigned int period = 0; + pFile = fopen( "rand.txt", "w" ); + do { +// lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1 + lfsr = 1; // to prevent the warning + ++period; + fprintf( pFile, "%10d : %10d ", period, lfsr ); +// Extra_PrintBinary( pFile, &lfsr, 32 ); + fprintf( pFile, "\n" ); + if ( period == 20000 ) + break; + } while(lfsr != 1u); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Creates a sequence or random numbers.] + + Description [] + + SideEffects [] + + SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx] + +***********************************************************************/ +void Aig_ManRandomTest1() +{ + FILE * pFile; + unsigned int lfsr; + unsigned int period = 0; + pFile = fopen( "rand.txt", "w" ); + do { + lfsr = Aig_ManRandom( 0 ); + ++period; + fprintf( pFile, "%10d : %10d ", period, lfsr ); +// Extra_PrintBinary( pFile, &lfsr, 32 ); + fprintf( pFile, "\n" ); + if ( period == 20000 ) + break; + } while(lfsr != 1u); + fclose( pFile ); +} + + +#define NUMBER1 3716960521 +#define NUMBER2 2174103536 + +/**Function************************************************************* + + Synopsis [Creates a sequence or random numbers.] + + Description [] + + SideEffects [] + + SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx] + +***********************************************************************/ +unsigned Aig_ManRandom( int fReset ) +{ + static unsigned int m_z = NUMBER1; + static unsigned int m_w = NUMBER2; + if ( fReset ) + { + m_z = NUMBER1; + m_w = NUMBER2; + } + m_z = 36969 * (m_z & 65535) + (m_z >> 16); + m_w = 18000 * (m_w & 65535) + (m_w >> 16); + return (m_z << 16) + m_w; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c index cfe70d15..234ae3f8 100644 --- a/src/aig/bbr/bbrImage.c +++ b/src/aig/bbr/bbrImage.c @@ -89,7 +89,7 @@ struct Bbr_ImageVar_t_ /* Macro declarations */ /*---------------------------------------------------------------------------*/ -#define BDD_BLOW_UP 1000000 +#define BDD_BLOW_UP 2000000 #define b0 Cudd_Not((dd)->one) #define b1 (dd)->one @@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode ) if ( pTree->nNodesMax < nNodes ) pTree->nNodesMax = nNodes; } - if ( dd->keys > BDD_BLOW_UP ) + if ( dd->keys-dd->dead > BDD_BLOW_UP ) return 0; return 1; } @@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd, } *pfStop = 0; - if ( dd->keys > BDD_BLOW_UP ) + if ( dd->keys-dd->dead > BDD_BLOW_UP ) { *pfStop = 1; return 0; diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make index 52a824b9..07a05869 100644 --- a/src/aig/bbr/module.make +++ b/src/aig/bbr/module.make @@ -1,3 +1,3 @@ SRC += src/aig/bbr/bbrImage.c \ src/aig/bbr/bbrNtbdd.c \ - src/aig/bdr/bbrReach.c + src/aig/bbr/bbrReach.c diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index cf763e67..9a49805b 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -138,6 +138,7 @@ extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); +extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 2ee66916..934aab1c 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -326,6 +326,30 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) return pSat; } +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) +{ + sat_solver * pSat = p; + Aig_Obj_t * pObj; + int i, * pLits; + pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) ) + assert( 0 ); + free( pLits ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 23b3e8f0..5556ac2e 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -221,9 +221,18 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) Number = 1; if ( nOutputs ) { - assert( nOutputs == Aig_ManRegNum(p->pManAig) ); - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; + if ( Aig_ManRegNum(p->pManAig) == 0 ) + { + assert( nOutputs == Aig_ManPoNum(p->pManAig) ); + Aig_ManForEachPo( p->pManAig, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + } + else + { + assert( nOutputs == Aig_ManRegNum(p->pManAig) ); + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + pCnf->pVarNums[pObj->Id] = Number++; + } } // assign variables to the internal nodes Vec_PtrForEachEntry( vMapped, pObj, i ) diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 5c9a144f..07685c98 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -220,7 +220,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f /* // we did not find the node to share, randomize choice { - int Choice = rand() % (RightBound - LeftBound + 1); + int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1); pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); if ( pObj3 == pObj2 ) return; diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 44cfe847..7311d414 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -226,7 +226,7 @@ struct Fra_Man_t_ //////////////////////////////////////////////////////////////////////// static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; } -static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } +static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); } static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; } static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; } diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 05f2493a..e91478a4 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -47,14 +47,16 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe int status, RetValue, clk = clock(); Vec_Int_t * vCiIds; - assert( Aig_ManPoNum(pMan) == 1 ); + assert( Aig_ManRegNum(pMan) == 0 ); pMan->pData = NULL; // derive CNF - pCnf = Cnf_Derive( pMan, 0 ); -// pCnf = Cnf_DeriveSimple( pMan, 0 ); + pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); +// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); // convert into the SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // add the OR clause for the outputs + Cnf_DataWriteOrClause( pSat, pCnf ); vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); Cnf_DataFree( pCnf ); // solve SAT diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index c9ea4907..6f0a2012 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -606,7 +606,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs ) // simulate the AIG clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); if ( p->fTarget && pSeq->fNonConstOut ) { @@ -661,7 +662,8 @@ PRT( "Infoseq", clock() - clk ); // perform combinational simulation clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); if ( p->fVerbose ) { @@ -728,7 +730,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs ) // simulate the AIG clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); if ( p->fTarget && pSeq->fNonConstOut ) { @@ -743,7 +746,8 @@ if ( p->fVerbose ) // perform combinational simulation clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); if ( p->fVerbose ) { @@ -1614,7 +1618,8 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) int * pStart, * pVar2Id; int clk = clock(); // simulate the circuit with nCombSimWords * 32 = 64K patterns - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords ); // create mapping from SAT vars to node IDs pVar2Id = ALLOC( int, p->pCnf->nVars ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 222f5bcc..b2156193 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -333,7 +333,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) // generate random sim-info at register outputs vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords ); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); for ( i = 0; i < nRegs; i++ ) { pSim1 = Vec_PtrEntry( vSimInfo, i ); diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index da7c37a3..b8cf13c5 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -120,7 +120,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); // set random number generator - srand( 0xABCABC ); +// srand( 0xABCABC ); + Aig_ManRandom(1); // set the pointer to the manager Aig_ManForEachObj( p->pManAig, pObj, i ) pObj->pData = p; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 64222a47..9a500680 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -44,21 +44,20 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; - Aig_Man_t * pNew = NULL, * pTemp; + 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 ) + pNew = Aig_ManDup( p ); + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) goto finish; // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; pPars->fVerbose = fVeryVerbose; - - pNew = Aig_ManDup( p ); if ( fVerbose ) { printf( "Original miter: Latches = %5d. Nodes = %6d.\n", @@ -78,6 +77,9 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) + goto finish; // perform phase abstraction clk = clock(); @@ -150,6 +152,13 @@ PRT( "Time", clock() - clk ); } } + if ( pNew->nRegs == 0 ) + RetValue = Fra_FraigCec( &pNew, 0 ); + + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) + goto finish; + // perform min-area retiming if ( fRetimeRegs && pNew->nRegs ) { @@ -262,9 +271,7 @@ PRT( "Time", clock() - clkTotal ); assert( Aig_ManRegNum(pNew) > 0 ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); -clk = clock(); RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); -PRT( "Time", clock() - clk ); } finish: @@ -289,8 +296,7 @@ PRT( "Time", clock() - clkTotal ); Ioa_WriteAiger( pNew, pFileName, 0, 0 ); printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); } - if ( pNew ) - Aig_ManStop( pNew ); + Aig_ManStop( pNew ); return RetValue; } diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 7de3ccdc..c9172024 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -2,4 +2,5 @@ SRC += src/aig/saig/saig_.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ src/aig/saig/saigRetMin.c \ + src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f9677cb0..7f6bb292 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -82,6 +82,8 @@ extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, in /*=== saigRetMin.c ==========================================================*/ extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ); extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); +/*=== saigRetStep.c ==========================================================*/ +extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ); /*=== saigScl.c ==========================================================*/ extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ); diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index f98bb49b..f19a27b6 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -58,13 +58,13 @@ static inline int Saig_XsimAnd( int Value0, int Value1 ) } static inline int Saig_XsimRand2() { - return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0; + return (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0; } static inline int Saig_XsimRand3() { int RetValue; do { - RetValue = rand() & 3; + RetValue = Aig_ManRandom(0) & 3; } while ( RetValue == 0 ); return RetValue; } @@ -601,11 +601,11 @@ void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg ) ***********************************************************************/ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose ) { - int Values[256]; + int Values[257]; unsigned * pState; int r, i, k, Reg, Value; int nTests = pTsi->nPrefix + 2 * pTsi->nCycle; - assert( nFrames < 256 ); + assert( nFrames <= 256 ); r = 0; Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i ) { @@ -800,6 +800,8 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame printf( "Print-out finished. Phase assignment is not performed.\n" ); else if ( nFrames < 2 ) printf( "The number of frames is less than 2. Phase assignment is not performed.\n" ); + else if ( nFrames > 256 ) + printf( "The number of frames is more than 256. Phase assignment is not performed.\n" ); else if ( pTsi->nCycle == 1 ) printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" ); else if ( pTsi->nCycle % nFrames != 0 ) @@ -858,6 +860,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) else if ( nFrames < 2 ) { // printf( "The number of frames is less than 2. Phase assignment is not performed.\n" ); + } + else if ( nFrames > 256 ) + { +// printf( "The number of frames is more than 256. Phase assignment is not performed.\n" ); } else if ( pTsi->nCycle == 1 ) { diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index 324d8867..3935db6c 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -628,6 +628,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl if ( !fBackwardOnly ) for ( i = 0; i < nMaxIters; i++ ) { + if ( Saig_ManRegNum(pNew) == 0 ) + break; vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose ); if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) { @@ -648,6 +650,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl if ( !fForwardOnly && !fInitial ) for ( i = 0; i < nMaxIters; i++ ) { + if ( Saig_ManRegNum(pNew) == 0 ) + break; vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose ); if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) { @@ -666,6 +670,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl else if ( !fForwardOnly && fInitial ) for ( i = 0; i < nMaxIters; i++ ) { + if ( Saig_ManRegNum(pNew) == 0 ) + break; pCopy = Aig_ManDup( pNew ); pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose ); Aig_ManStop( pCopy ); diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c new file mode 100644 index 00000000..e7ec3c08 --- /dev/null +++ b/src/aig/saig/saigRetStep.c @@ -0,0 +1,202 @@ +/**CFile**************************************************************** + + FileName [saigRetStep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Implementation of retiming steps.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigRetStep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs one retiming step forward.] + + Description [Returns the pointer to the register output after retiming.] + + SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pFanin0, * pFanin1; + Aig_Obj_t * pInput0, * pInput1; + Aig_Obj_t * pObjNew, * pObjLi, * pObjLo; + + assert( Saig_ManRegNum(p) > 0 ); + assert( Aig_ObjIsNode(pObj) ); + + // get the fanins + pFanin0 = Aig_ObjFanin0(pObj); + pFanin1 = Aig_ObjFanin1(pObj); + // skip of they are not primary inputs + if ( !Aig_ObjIsPi(pFanin0) || !Aig_ObjIsPi(pFanin1) ) + return NULL; + + // skip of they are not register outputs + if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) ) + return NULL; + assert( Aig_ObjPioNum(pFanin0) > 0 ); + assert( Aig_ObjPioNum(pFanin1) > 0 ); + + // get the inputs of these registers + pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); + pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); + pInput0 = Aig_ObjChild0( pInput0 ); + pInput1 = Aig_ObjChild0( pInput1 ); + pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) ); + pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) ); + + // create new node + pObjNew = Aig_And( p, pInput0, pInput1 ); + + // create new register input + pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) ); + pObjLi->PioNum = Aig_ManPoNum(p) - 1; + assert( pObjLi->fPhase == 0 ); + + // create new register output + pObjLo = Aig_ObjCreatePi( p ); + pObjLo->PioNum = Aig_ManPiNum(p) - 1; + p->nRegs++; + + // return register output + return Aig_NotCond( pObjLo, pObjNew->fPhase ); +} + +/**Function************************************************************* + + Synopsis [Performs one retiming step backward.] + + Description [Returns the pointer to node after retiming.] + + SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) +{ + Aig_Obj_t * pFanin0, * pFanin1; + Aig_Obj_t * pLo0New, * pLo1New; + Aig_Obj_t * pLi0New, * pLi1New; + Aig_Obj_t * pObj, * pObjNew, * pObjLi; + int fCompl0, fCompl1; + + assert( Saig_ManRegNum(p) > 0 ); + assert( Aig_ObjPioNum(pObjLo) > 0 ); + assert( Saig_ObjIsLo(p, pObjLo) ); + + // get the corresponding latch input + pObjLi = Saig_ManLi( p, Aig_ObjPioNum(pObjLo) - Saig_ManPiNum(p) ); + + // get the node + pObj = Aig_ObjFanin0(pObjLi); + if ( !Aig_ObjIsNode(pObj) ) + return NULL; + + // get the fanins + pFanin0 = Aig_ObjFanin0(pObj); + pFanin1 = Aig_ObjFanin1(pObj); + + // get the complemented attributes of the fanins + fCompl0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFaninC0(pObjLi); + fCompl1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFaninC0(pObjLi); + + // create latch inputs + pLi0New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin0, fCompl0) ); + pLi0New->PioNum = Aig_ManPoNum(p) - 1; + pLi1New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin1, fCompl1) ); + pLi1New->PioNum = Aig_ManPoNum(p) - 1; + + // create latch outputs + pLo0New = Aig_ObjCreatePi(p); + pLo0New->PioNum = Aig_ManPiNum(p) - 1; + pLo1New = Aig_ObjCreatePi(p); + pLo1New->PioNum = Aig_ManPiNum(p) - 1; + pLo0New = Aig_NotCond( pLo0New, fCompl0 ); + pLo1New = Aig_NotCond( pLo1New, fCompl1 ); + p->nRegs += 2; + + // create node + pObjNew = Aig_And( p, pLo0New, pLo1New ); +// assert( pObjNew->fPhase == 0 ); + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Performs the given number of retiming steps.] + + Description [Returns the pointer to node after retiming.] + + SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward ) +{ + Aig_Obj_t * pObj, * pObjNew; + int RetValue, s, i; + Aig_ManSetPioNumbers( p ); + Aig_ManFanoutStart( p ); + if ( fForward ) + { + for ( s = 0; s < nSteps; s++ ) + { + Aig_ManForEachNode( p, pObj, i ) + { + pObjNew = Saig_ManRetimeNodeFwd( p, pObj ); + if ( pObjNew == NULL ) + continue; + Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); + break; + } + } + } + else + { + for ( s = 0; s < nSteps; s++ ) + { + Saig_ManForEachLo( p, pObj, i ) + { + pObjNew = Saig_ManRetimeNodeBwd( p, pObj ); + if ( pObjNew == NULL ) + continue; + Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); + break; + } + } + } + RetValue = Aig_ManCleanup( p ); + assert( RetValue == 0 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 40d1dcad..3bac7316 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -24,7 +24,7 @@ #include "abc.h" #include "main.h" -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9b3ec291..d3ac7669 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -500,6 +500,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars ); // Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 ); } + + { +// extern void Aig_ManRandomTest1(); +// Aig_ManRandomTest1(); + } } /**Function************************************************************* @@ -7253,7 +7258,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Abc_NtkDarTestBlif( char * pFileName ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ); +// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ); + extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ); @@ -7440,7 +7446,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_NtkDarPartition( pNtk ); - pNtkRes = Abc_NtkNtkTest( pNtk, Abc_FrameReadLibLut() ); + pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -17020,6 +17026,9 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; int c; extern int Ntl_ManSweep( void * p, int fVerbose ); + extern void * Ntl_ManInsertNtk( void * p, void * pNtk ); + extern Aig_Man_t * Ntl_ManExtract( void * p ); + extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); // set defaults fMapped = 0; @@ -17332,12 +17341,13 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); // set defaults - nFrames = 16; - fRetimeFirst = 0; - fRetimeRegs = 0; - fFraiging = 1; - fVerbose = 0; - fVeryVerbose = 0; + nFrames = 8; + fPhaseAbstract = 0; + fRetimeFirst = 0; + fRetimeRegs = 0; + fFraiging = 1; + fVerbose = 0; + fVeryVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) { diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 88435e3f..329bccf8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -20,6 +20,7 @@ #include "abc.h" #include "aig.h" +#include "saig.h" #include "dar.h" #include "cnf.h" #include "fra.h" @@ -1527,6 +1528,41 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + if ( pMan->vFlopNums ) + Vec_IntFree( pMan->vFlopNums ); + pMan->vFlopNums = NULL; + + pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); + pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + + Aig_ManPrintStats(pMan); + Saig_ManRetimeSteps( pMan, 1, 0 ); + Aig_ManPrintStats(pMan); + + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c index f8182532..f262a5d0 100644 --- a/src/base/abci/abcDress.c +++ b/src/base/abci/abcDress.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 316dd8ad..313ae0ed 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1085,7 +1085,7 @@ usage: #ifdef WIN32 -#include +#include // these structures are defined in but are for some reason invisible typedef unsigned long _fsize_t; // Could be 64 bits for Win32 diff --git a/src/base/io/io.c b/src/base/io/io.c index 6b802bf1..6efa8b67 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "mainInt.h" //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.h b/src/base/io/io.h deleted file mode 100644 index eea76efe..00000000 --- a/src/base/io/io.h +++ /dev/null @@ -1,146 +0,0 @@ -/**CFile**************************************************************** - - FileName [io.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Command processing package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: io.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __IO_H__ -#define __IO_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// network functionality -typedef enum { - IO_FILE_NONE = 0, - IO_FILE_AIGER, - IO_FILE_BAF, - IO_FILE_BLIF, - IO_FILE_BLIFMV, - IO_FILE_BENCH, - IO_FILE_CNF, - IO_FILE_DOT, - IO_FILE_EDIF, - IO_FILE_EQN, - IO_FILE_GML, - IO_FILE_LIST, - IO_FILE_PLA, - IO_FILE_VERILOG, - IO_FILE_UNKNOWN -} Io_FileType_t; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#define IO_WRITE_LINE_LENGTH 78 // the output line length - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== abcReadAiger.c ==========================================================*/ -extern Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ); -/*=== abcReadBaf.c ============================================================*/ -extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ); -/*=== abcReadBlif.c ===========================================================*/ -extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ); -/*=== abcReadBlifMv.c =========================================================*/ -extern Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ); -/*=== abcReadBench.c ==========================================================*/ -extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ); -/*=== abcReadEdif.c ===========================================================*/ -extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ); -/*=== abcReadEqn.c ============================================================*/ -extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ); -/*=== abcReadPla.c ============================================================*/ -extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ); -/*=== abcReadVerilog.c ========================================================*/ -extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); -/*=== abcWriteAiger.c =========================================================*/ -extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ); -/*=== abcWriteBaf.c ===========================================================*/ -extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); -/*=== abcWriteBlif.c ==========================================================*/ -extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); -extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); -extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ); -/*=== abcWriteBlifMv.c ==========================================================*/ -extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ); -/*=== abcWriteBench.c =========================================================*/ -extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); -extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName ); -/*=== abcWriteCnf.c ===========================================================*/ -extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes ); -/*=== abcWriteDot.c ===========================================================*/ -extern void Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName ); -extern void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse ); -extern void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse ); -/*=== abcWriteEqn.c ===========================================================*/ -extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName ); -/*=== abcWriteGml.c ===========================================================*/ -extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName ); -/*=== abcWriteList.c ==========================================================*/ -extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost ); -/*=== abcWritePla.c ===========================================================*/ -extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName ); -/*=== abcWriteVerilog.c =======================================================*/ -extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName ); -/*=== abcUtil.c ===============================================================*/ -extern Io_FileType_t Io_ReadFileType( char * pFileName ); -extern Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck ); -extern Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck ); -extern void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ); -extern void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ); -extern Abc_Obj_t * Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ); -extern Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv ); -extern Abc_Obj_t * Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv ); -extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs ); -extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ); -extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); -extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); -extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose ); - - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h new file mode 100644 index 00000000..e62cc168 --- /dev/null +++ b/src/base/io/ioAbc.h @@ -0,0 +1,146 @@ +/**CFile**************************************************************** + + FileName [ioAbc.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioAbc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __IO_H__ +#define __IO_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// network functionality +typedef enum { + IO_FILE_NONE = 0, + IO_FILE_AIGER, + IO_FILE_BAF, + IO_FILE_BLIF, + IO_FILE_BLIFMV, + IO_FILE_BENCH, + IO_FILE_CNF, + IO_FILE_DOT, + IO_FILE_EDIF, + IO_FILE_EQN, + IO_FILE_GML, + IO_FILE_LIST, + IO_FILE_PLA, + IO_FILE_VERILOG, + IO_FILE_UNKNOWN +} Io_FileType_t; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define IO_WRITE_LINE_LENGTH 78 // the output line length + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== abcReadAiger.c ==========================================================*/ +extern Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ); +/*=== abcReadBaf.c ============================================================*/ +extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ); +/*=== abcReadBlif.c ===========================================================*/ +extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck ); +/*=== abcReadBlifMv.c =========================================================*/ +extern Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ); +/*=== abcReadBench.c ==========================================================*/ +extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ); +/*=== abcReadEdif.c ===========================================================*/ +extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ); +/*=== abcReadEqn.c ============================================================*/ +extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck ); +/*=== abcReadPla.c ============================================================*/ +extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ); +/*=== abcReadVerilog.c ========================================================*/ +extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); +/*=== abcWriteAiger.c =========================================================*/ +extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ); +/*=== abcWriteBaf.c ===========================================================*/ +extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); +/*=== abcWriteBlif.c ==========================================================*/ +extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); +extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches ); +extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ); +/*=== abcWriteBlifMv.c ==========================================================*/ +extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteBench.c =========================================================*/ +extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); +extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteCnf.c ===========================================================*/ +extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes ); +/*=== abcWriteDot.c ===========================================================*/ +extern void Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName ); +extern void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse ); +extern void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse ); +/*=== abcWriteEqn.c ===========================================================*/ +extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName ); +/*=== abcWriteGml.c ===========================================================*/ +extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName ); +/*=== abcWriteList.c ==========================================================*/ +extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost ); +/*=== abcWritePla.c ===========================================================*/ +extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteVerilog.c =======================================================*/ +extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcUtil.c ===============================================================*/ +extern Io_FileType_t Io_ReadFileType( char * pFileName ); +extern Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck ); +extern Abc_Ntk_t * Io_Read( char * pFileName, Io_FileType_t FileType, int fCheck ); +extern void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ); +extern void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ); +extern Abc_Obj_t * Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ); +extern Abc_Obj_t * Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv ); +extern Abc_Obj_t * Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv ); +extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs ); +extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ); +extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); +extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); +extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index 4820bced..3739205d 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -19,7 +19,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -327,7 +327,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) } // read the name of the model if given - if ( *pCur == 'c' ) + if ( *pCur == 'c' && pCur < pContents + nFileSize ) { if ( !strncmp( pCur + 2, ".model", 6 ) ) { diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c index 8dce54af..13f644cc 100644 --- a/src/base/io/ioReadBaf.c +++ b/src/base/io/ioReadBaf.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 007147bc..0742ec1f 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index ffa25c7f..68a0bc35 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "main.h" #include "mio.h" diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 84378024..68602e63 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -21,7 +21,7 @@ #include "abc.h" #include "extra.h" #include "vecPtr.h" -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c index 1ab726e5..482b5d06 100644 --- a/src/base/io/ioReadDsd.c +++ b/src/base/io/ioReadDsd.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index 188e5b8c..bea9bf69 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c index e04f2b1a..6a1360d0 100644 --- a/src/base/io/ioReadEqn.c +++ b/src/base/io/ioReadEqn.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index 288c3704..cbee81ef 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c index c64e330c..9847c2da 100644 --- a/src/base/io/ioReadVerilog.c +++ b/src/base/io/ioReadVerilog.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 51a00274..37d57f30 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 758e5335..fb107e77 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -19,7 +19,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c index fc0229a4..33487041 100644 --- a/src/base/io/ioWriteBaf.c +++ b/src/base/io/ioWriteBaf.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c index df4a6259..147976da 100644 --- a/src/base/io/ioWriteBench.c +++ b/src/base/io/ioWriteBench.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index c0c29d65..a0105a6b 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "main.h" #include "mio.h" diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c index 775a2e07..86891fee 100644 --- a/src/base/io/ioWriteBlifMv.c +++ b/src/base/io/ioWriteBlifMv.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "main.h" #include "mio.h" diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index e1b2d956..3df189d1 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "satSolver.h" //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 8ae3cc42..b8ca6f67 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "main.h" #include "mio.h" diff --git a/src/base/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c index 95c54577..94c6e032 100644 --- a/src/base/io/ioWriteEqn.c +++ b/src/base/io/ioWriteEqn.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c index dc897300..d84e5f67 100644 --- a/src/base/io/ioWriteGml.c +++ b/src/base/io/ioWriteGml.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c index 71af7c53..c06b39d7 100644 --- a/src/base/io/ioWriteList.c +++ b/src/base/io/ioWriteList.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" /* -------- Original Message -------- diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c index b119751c..4b316416 100644 --- a/src/base/io/ioWritePla.c +++ b/src/base/io/ioWritePla.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c index 9e71e3e4..c704c6a1 100644 --- a/src/base/io/ioWriteVerilog.c +++ b/src/base/io/ioWriteVerilog.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" #include "main.h" #include "mio.h" diff --git a/src/base/io/io_.c b/src/base/io/io_.c index 62dd60e5..b24d1299 100644 --- a/src/base/io/io_.c +++ b/src/base/io/io_.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/main/main.h b/src/base/main/main.h index 4433a8b4..b5cc0dfe 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -52,7 +52,7 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; // core packages #include "abc.h" #include "cmd.h" -#include "io.h" +#include "ioAbc.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c index 47d338cb..bf249035 100644 --- a/src/opt/fret/fretInit.c +++ b/src/opt/fret/fretInit.c @@ -20,7 +20,7 @@ #include "abc.h" #include "vec.h" -#include "io.h" +#include "ioAbc.h" #include "fretime.h" #include "mio.h" #include "hop.h" -- cgit v1.2.3