diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-10 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-06-10 08:01:00 -0700 |
commit | 9d09f583b6ea1181ebd5af1654acd3432c427445 (patch) | |
tree | 2ea6fb1cc6f70871f861dd0ccbe7f8522c34c765 /src | |
parent | 9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff (diff) | |
download | abc-9d09f583b6ea1181ebd5af1654acd3432c427445.tar.gz abc-9d09f583b6ea1181ebd5af1654acd3432c427445.tar.bz2 abc-9d09f583b6ea1181ebd5af1654acd3432c427445.zip |
Version abc80610
Diffstat (limited to 'src')
38 files changed, 1430 insertions, 691 deletions
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 2adcabfb..2c779c40 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -591,10 +591,11 @@ void Aig_ManComputeSccs( Aig_Man_t * p ) Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose ) { extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ); + extern int Saig_ManReportComplements( Aig_Man_t * p ); Aig_Man_t * pAigInit, * pAigNew; Aig_Obj_t * pFlop1, * pFlop2; - int i, Entry1, Entry2, nTruePis; + int i, Entry1, Entry2, nTruePis;//, nRegs; // store the original AIG assert( pAig->vFlopNums == NULL ); pAigInit = pAig; @@ -627,6 +628,11 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int Aig_ManSeqCleanup( pAigNew ); Saig_ManReportUselessRegisters( pAigNew ); + if ( Aig_ManRegNum(pAigNew) == 0 ) + return pAigNew; +// nRegs = Saig_ManReportComplements( pAigNew ); +// if ( nRegs ) +// printf( "The number of complemented registers = %d.\n", nRegs ); return pAigNew; } diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h index 504fc463..69d5fae7 100644 --- a/src/aig/bbr/bbr.h +++ b/src/aig/bbr/bbr.h @@ -74,7 +74,7 @@ extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ); extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ); extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose ); /*=== bbrReach.c ==========================================================*/ -extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); +extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); #ifdef __cplusplus } diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index 95bfe1ba..a78a3fb2 100644 --- a/src/aig/bbr/bbrReach.c +++ b/src/aig/bbr/bbrReach.c @@ -203,7 +203,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, SeeAlso [] ***********************************************************************/ -int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) { int fInternalReorder = 0; Bbr_ImageTree_t * pTree; @@ -231,7 +231,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D free( pbVarsY ); if ( pTree == NULL ) { - printf( "BDDs blew up during qualitification scheduling. " ); + if ( !fSilent ) + printf( "BDDs blew up during qualitification scheduling. " ); return -1; } @@ -247,7 +248,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D bNext = Bbr_bddImageCompute2( pTree2, bCurrent ); if ( bNext == NULL ) { - printf( "BDDs blew up during image computation. " ); + if ( !fSilent ) + printf( "BDDs blew up during image computation. " ); if ( fPartition ) Bbr_bddImageTreeDelete( pTree ); else @@ -271,7 +273,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D { if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) ) { - printf( "Output %d was asserted in frame %d. ", i, nIters ); + if ( !fSilent ) + printf( "Output %d was asserted in frame %d. ", i, nIters ); Cudd_RecursiveDeref( dd, bReached ); bReached = NULL; break; @@ -326,10 +329,12 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D Cudd_RecursiveDeref( dd, bReached ); if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax ) { - printf( "Verified only for states reachable in %d frames. ", nIters ); - return -1; // undecided + if ( !fSilent ) + printf( "Verified only for states reachable in %d frames. ", nIters ); + return -1; // undecided } - printf( "The miter is proved unreachable after %d iterations. ", nIters ); + if ( !fSilent ) + printf( "The miter is proved unreachable after %d iterations. ", nIters ); return 1; // unreachable } @@ -344,7 +349,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D SeeAlso [] ***********************************************************************/ -int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) { DdManager * dd; DdNode ** pbParts, ** pbOutputs; @@ -357,7 +362,8 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose ); if ( dd == NULL ) { - printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax ); + if ( !fSilent ) + printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax ); return -1; } if ( fVerbose ) @@ -378,14 +384,15 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti { if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) ) { - printf( "The miter output %d is proved REACHABLE in the initial state. ", i ); + if ( !fSilent ) + printf( "The miter output %d is proved REACHABLE in the initial state. ", i ); RetValue = 0; break; } } // explore reachable states if ( RetValue == -1 ) - RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); // cleanup Cudd_RecursiveDeref( dd, bInitial ); @@ -401,8 +408,11 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti Bbr_StopManager( dd ); // report the runtime + if ( !fSilent ) + { PRT( "Time", clock() - clk ); fflush( stdout ); + } return RetValue; } diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index e664b1bc..bf109b17 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -139,7 +139,7 @@ extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); -extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); +extern int 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 b6ed3da0..fc71f936 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -362,7 +362,7 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) +int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) { sat_solver * pSat = p; Aig_Obj_t * pObj; @@ -371,8 +371,12 @@ void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) 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 ); + return 0; + } free( pLits ); + return 1; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7549dfca..025ce046 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -104,6 +104,7 @@ struct Fra_Ssw_t_ int fWriteImps; // write implications into a file int fUse1Hot; // use one-hotness constraints int fVerbose; // enable verbose output + int fSilent; // disable any output int nIters; // the number of iterations performed float TimeLimit; // the runtime budget for this call }; @@ -121,6 +122,7 @@ struct Fra_Sec_t_ int fInterpolation; // enables interpolation int fReachability; // enables BDD based reachability int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting int TimeLimit; // enables the timeout diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index e91478a4..d67839a4 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -53,19 +53,22 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe // derive CNF pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); - // convert into the SAT solver + // convert into 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 if ( pSat == NULL ) { - Vec_IntFree( vCiIds ); -// printf( "Trivially unsat\n" ); + Cnf_DataFree( pCnf ); return 1; } + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); + Cnf_DataFree( pCnf ); // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index df92792a..9c52d0e2 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -422,7 +422,8 @@ PRT( "Time", clock() - clk ); if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) { - printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + if ( !pParams->fSilent ) + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); goto finish; } @@ -452,7 +453,8 @@ PRT( "Time", clock() - clk ); if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) { - printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + if ( !pParams->fSilent ) + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); goto finish; } diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 4528b9c4..96c0de77 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -53,11 +53,12 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fInterpolation = 1; // enables interpolation p->fReachability = 1; // enables BDD based reachability p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove + p->fSilent = 0; // disables all output p->fVerbose = 0; // enables verbose reporting of statistics p->fVeryVerbose = 0; // enables very verbose reporting p->TimeLimit = 0; // enables the timeout // internal parameters - p->fReportSolution = 1; // enables specialized format for reporting solution + p->fReportSolution = 0; // enables specialized format for reporting solution } /**Function************************************************************* @@ -158,7 +159,8 @@ clk = clock(); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { - printf( "Runtime limit exceeded.\n" ); + if ( !pParSec->fSilent ) + printf( "Runtime limit exceeded.\n" ); RetValue = -1; TimeOut = 1; goto finish; @@ -166,14 +168,16 @@ clk = clock(); } pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; - Aig_ManStop( pTemp ); if ( pNew == NULL ) { if ( p->pSeqModel ) { RetValue = 0; - printf( "Networks are NOT EQUIVALENT after simulation. " ); + if ( !pParSec->fSilent ) + { + printf( "Networks are NOT EQUIVALENT after simulation. " ); PRT( "Time", clock() - clkTotal ); + } if ( pParSec->fReportSolution && !pParSec->fRecursive ) { printf( "SOLUTION: FAIL " ); @@ -186,6 +190,7 @@ PRT( "Time", clock() - clkTotal ); TimeOut = 1; goto finish; } + Aig_ManStop( pTemp ); if ( pParSec->fVerbose ) { @@ -201,7 +206,8 @@ PRT( "Time", clock() - clk ); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { - printf( "Runtime limit exceeded.\n" ); + if ( !pParSec->fSilent ) + printf( "Runtime limit exceeded.\n" ); RetValue = -1; TimeOut = 1; goto finish; @@ -235,7 +241,8 @@ PRT( "Time", clock() - clk ); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { - printf( "Runtime limit exceeded.\n" ); + if ( !pParSec->fSilent ) + printf( "Runtime limit exceeded.\n" ); RetValue = -1; TimeOut = 1; goto finish; @@ -273,7 +280,8 @@ PRT( "Time", clock() - clk ); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { - printf( "Runtime limit exceeded.\n" ); + if ( !pParSec->fSilent ) + printf( "Runtime limit exceeded.\n" ); RetValue = -1; TimeOut = 1; goto finish; @@ -283,6 +291,7 @@ PRT( "Time", clock() - clk ); clk = clock(); pPars->nFramesK = nFrames; pPars->TimeLimit = TimeLeft; + pPars->fSilent = pParSec->fSilent; pNew = Fra_FraigInduction( pTemp = pNew, pPars ); if ( pNew == NULL ) { @@ -357,8 +366,11 @@ PRT( "Time", clock() - clk ); Fra_SmlStop( pSml ); Aig_ManStop( pNew ); RetValue = 0; - printf( "Networks are NOT EQUIVALENT after simulation. " ); + if ( !pParSec->fSilent ) + { + printf( "Networks are NOT EQUIVALENT after simulation. " ); PRT( "Time", clock() - clkTotal ); + } if ( pParSec->fReportSolution && !pParSec->fRecursive ) { printf( "SOLUTION: FAIL " ); @@ -399,10 +411,10 @@ PRT( "Time", clock() - clk ); // try reachability analysis if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 ) { - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); + RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent ); } // try one-output at a time @@ -414,8 +426,9 @@ PRT( "Time", clock() - clk ); for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) ) Counter++; - printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", - Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) ); + if ( !pParSec->fSilent ) + printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", + Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) ); iCount = 0; for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) { @@ -427,7 +440,8 @@ PRT( "Time", clock() - clk ); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { - printf( "Runtime limit exceeded.\n" ); + if ( !pParSec->fSilent ) + printf( "Runtime limit exceeded.\n" ); TimeOut = 1; goto finish; } @@ -438,7 +452,8 @@ PRT( "Time", clock() - clk ); if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) ) continue; iCount++; - printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter ); + if ( !pParSec->fSilent ) + printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter ); pNew2 = Aig_ManDupOneOutput( pNew, i ); TimeLimitCopy = pParSec->TimeLimit; @@ -462,15 +477,19 @@ PRT( "Time", clock() - clk ); RetValue = -1; else RetValue = 1; - printf( "*** Finished running separate outputs of the miter.\n" ); + if ( !pParSec->fSilent ) + printf( "*** Finished running separate outputs of the miter.\n" ); } finish: // report the miter if ( RetValue == 1 ) { - printf( "Networks are equivalent. " ); + if ( !pParSec->fSilent ) + { + printf( "Networks are equivalent. " ); PRT( "Time", clock() - clkTotal ); + } if ( pParSec->fReportSolution && !pParSec->fRecursive ) { printf( "SOLUTION: PASS " ); @@ -479,8 +498,11 @@ PRT( "Time", clock() - clkTotal ); } else if ( RetValue == 0 ) { - printf( "Networks are NOT EQUIVALENT. " ); + if ( !pParSec->fSilent ) + { + printf( "Networks are NOT EQUIVALENT. " ); PRT( "Time", clock() - clkTotal ); + } if ( pParSec->fReportSolution && !pParSec->fRecursive ) { printf( "SOLUTION: FAIL " ); @@ -489,14 +511,17 @@ PRT( "Time", clock() - clkTotal ); } else { - printf( "Networks are UNDECIDED. " ); + if ( !pParSec->fSilent ) + { + printf( "Networks are UNDECIDED. " ); PRT( "Time", clock() - clkTotal ); + } if ( pParSec->fReportSolution && !pParSec->fRecursive ) { printf( "SOLUTION: UNDECIDED " ); PRT( "Time", clock() - clkTotal ); } - if ( !TimeOut ) + if ( !TimeOut && !pParSec->fSilent ) { static int Counter = 1; char pFileName[1000]; diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip Binary files differdeleted file mode 100644 index 0adf10df..00000000 --- a/src/aig/fra/fraSec80516.zip +++ /dev/null diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 00a35fcd..53493201 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -1119,20 +1119,22 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ) RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); // write the output file - fprintf( pFile, "1\n" ); for ( i = 0; i <= p->iFrame; i++ ) { +/* Aig_ManForEachLoSeq( pAig, pObj, k ) { pSims = Fra_ObjSim(pSml, pObj->Id); fprintf( pFile, "%d", (int)(pSims[i] != 0) ); } fprintf( pFile, " " ); +*/ Aig_ManForEachPiSeq( pAig, pObj, k ) { pSims = Fra_ObjSim(pSml, pObj->Id); fprintf( pFile, "%d", (int)(pSims[i] != 0) ); } +/* fprintf( pFile, " " ); Aig_ManForEachPoSeq( pAig, pObj, k ) { @@ -1145,6 +1147,7 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ) pSims = Fra_ObjSim(pSml, pObj->Id); fprintf( pFile, "%d", (int)(pSims[i] != 0) ); } +*/ fprintf( pFile, "\n" ); } diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index d049d660..0d9d42a3 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2260,8 +2260,8 @@ p->timeSat += clock() - clk; { p->timeSatUnsat += clock() - clk; pLits[0] = lit_neg( pLits[0] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); - assert( RetValue ); +// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); +// assert( RetValue ); // continue solving the other implication p->nSatCallsUnsat++; } diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 4179754c..b496cb13 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -43,6 +43,7 @@ extern "C" { typedef struct Ntl_Man_t_ Ntl_Man_t; typedef struct Ntl_Mod_t_ Ntl_Mod_t; +typedef struct Ntl_Reg_t_ Ntl_Reg_t; typedef struct Ntl_Obj_t_ Ntl_Obj_t; typedef struct Ntl_Net_t_ Ntl_Net_t; typedef struct Ntl_Lut_t_ Ntl_Lut_t; @@ -65,6 +66,7 @@ struct Ntl_Man_t_ char * pName; // the name of this design char * pSpec; // the name of input file Vec_Ptr_t * vModels; // the array of all models used to represent boxes + int BoxTypes[15]; // the array of box types among the models // memory managers Aig_MmFlex_t * pMemObjs; // memory for objects Aig_MmFlex_t * pMemSops; // memory for SOPs @@ -75,6 +77,12 @@ struct Ntl_Man_t_ Vec_Int_t * vBox1Cos; // the first COs of the boxes Aig_Man_t * pAig; // the extracted AIG Tim_Man_t * pManTime; // the timing manager + int iLastCi; // the last true CI + Vec_Ptr_t * vLatchIns; // the AIG nodes driving latch inputs for internal latches + // hashing names into models + Ntl_Mod_t ** pModTable; // the hash table of names into models + int nModTableSize; // the allocated table size + int nModEntries; // the number of entries in the hash table }; struct Ntl_Mod_t_ @@ -86,21 +94,33 @@ struct Ntl_Mod_t_ Vec_Ptr_t * vPis; // the array of PI objects Vec_Ptr_t * vPos; // the array of PO objects int nObjs[NTL_OBJ_VOID]; // counter of objects of each type - int fKeep; // indicates persistant model + // box attributes + unsigned int attrWhite : 1; // box has known logic + unsigned int attrBox : 1; // box is to remain unmapped + unsigned int attrComb : 1; // box is combinational + unsigned int attrKeep : 1; // box cannot be removed by structural sweep // hashing names into nets Ntl_Net_t ** pTable; // the hash table of names into nets int nTableSize; // the allocated table size int nEntries; // the number of entries in the hash table // delay information Vec_Int_t * vDelays; - Vec_Int_t * vArrivals; - Vec_Int_t * vRequireds; + Vec_Int_t * vTimeInputs; + Vec_Int_t * vTimeOutputs; float * pDelayTable; // other data members + Ntl_Mod_t * pNext; void * pCopy; int nUsed, nRems; }; +struct Ntl_Reg_t_ +{ + unsigned int regInit : 2; // register initial value + unsigned int regType : 3; // register type + unsigned int regClass : 28; // register class +}; + struct Ntl_Obj_t_ { Ntl_Mod_t * pModel; // the model @@ -113,7 +133,11 @@ struct Ntl_Obj_t_ union { // functionality Ntl_Mod_t * pImplem; // model (for boxes) char * pSop; // SOP (for logic nodes) - unsigned LatchId; // init state + register class (for latches) + Ntl_Reg_t LatchId; // init state + register class (for latches) + }; + union { // clock / other data + Ntl_Net_t * pClock; // clock (for registers) + void * pTemp; // other data }; Ntl_Net_t * pFanio[0]; // fanins/fanouts }; @@ -164,8 +188,6 @@ static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nO 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]; } -static inline int Ntl_ModelCoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i); } static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i); } @@ -173,8 +195,6 @@ static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return (Ntl_ static inline char * Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } static inline char * Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } -static inline int Ntl_ModelIsBlackBox( Ntl_Mod_t * p ) { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } - static inline int Ntl_ObjFaninNum( Ntl_Obj_t * p ) { return p->nFanins; } static inline int Ntl_ObjFanoutNum( Ntl_Obj_t * p ) { return p->nFanouts; } @@ -193,6 +213,23 @@ static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i ) { return p->pF static inline void Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[i] = pNet; } static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } +static inline int Ntl_ObjIsInit1( Ntl_Obj_t * p ) { assert( Ntl_ObjIsLatch(p) ); return p->LatchId.regInit == 1; } +static inline void Ntl_ObjSetInit0( Ntl_Obj_t * p ) { assert( Ntl_ObjIsLatch(p) ); p->LatchId.regInit = 0; } + +static inline int Ntl_BoxIsWhite( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrWhite; } +static inline int Ntl_BoxIsBlack( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite; } +static inline int Ntl_BoxIsComb( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb; } +static inline int Ntl_BoxIsSeq( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb; } + +static inline int Ntl_ObjIsMapLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } +static inline int Ntl_ObjIsMapRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } + +static inline int Ntl_ObjIsCombLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p))); } +static inline int Ntl_ObjIsCombRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p))); } + +static inline int Ntl_ObjIsSeqLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p)); } +static inline int Ntl_ObjIsSeqRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p)); } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -203,10 +240,10 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int Vec_PtrForEachEntry( p->vCis, pNet, i ) #define Ntl_ManForEachCoNet( p, pNet, i ) \ Vec_PtrForEachEntry( p->vCos, pNet, i ) -#define Ntl_ManForEachNode( p, pObj, i ) \ +#define Ntl_ManForEachNode( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else -#define Ntl_ManForEachBox( p, pObj, i ) \ +#define Ntl_ManForEachBox( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else @@ -214,6 +251,9 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ ) #define Ntl_ModelForEachPo( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ ) +#define Ntl_ModelForEachNet( pNwk, pNet, i ) \ + for ( i = 0; i < pNwk->nTableSize; i++ ) \ + for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) #define Ntl_ModelForEachObj( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ if ( pObj == NULL ) {} else @@ -226,15 +266,31 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int #define Ntl_ModelForEachBox( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else -#define Ntl_ModelForEachNet( pNwk, pNet, i ) \ - for ( i = 0; i < pNwk->nTableSize; i++ ) \ - for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) #define Ntl_ObjForEachFanin( pObj, pFanin, i ) \ for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ ) #define Ntl_ObjForEachFanout( pObj, pFanout, i ) \ for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ ) +#define Ntl_ModelForEachMapLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsMapLeaf(pObj) ) {} else +#define Ntl_ModelForEachMapRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsMapRoot(pObj) ) {} else +#define Ntl_ModelForEachCombLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsCombLeaf(pObj) ) {} else +#define Ntl_ModelForEachCombRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsCombRoot(pObj) ) {} else +#define Ntl_ModelForEachSeqLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsSeqLeaf(pObj) ) {} else +#define Ntl_ModelForEachSeqRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsSeqRoot(pObj) ) {} else + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -247,17 +303,17 @@ extern ABC_DLL void Ntl_ManPrepareCec( char * pFileName1, char * pFil extern ABC_DLL Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); /*=== ntlExtract.c ==========================================================*/ extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ); +extern ABC_DLL Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ); +extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p ); /*=== ntlInsert.c ==========================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); extern ABC_DLL Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ); extern ABC_DLL Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ); /*=== ntlCheck.c ==========================================================*/ extern ABC_DLL int Ntl_ManCheck( Ntl_Man_t * pMan ); -extern ABC_DLL int Ntl_ModelCheck( Ntl_Mod_t * pModel ); +extern ABC_DLL int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain ); extern ABC_DLL void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ); +extern ABC_DLL void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel ); /*=== ntlMan.c ============================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManAlloc(); extern ABC_DLL void Ntl_ManCleanup( Ntl_Man_t * p ); @@ -269,10 +325,12 @@ extern ABC_DLL int Ntl_ManLatchNum( Ntl_Man_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p ); extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); +extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL void Ntl_ModelFree( Ntl_Mod_t * p ); +extern ABC_DLL Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ); /*=== ntlMap.c ============================================================*/ extern ABC_DLL Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars ); extern ABC_DLL Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p ); @@ -294,11 +352,13 @@ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); -extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ); +extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ); extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelCountNets( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ); +extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); /*=== ntlTime.c ==========================================================*/ extern ABC_DLL Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); /*=== ntlReadBlif.c ==========================================================*/ @@ -315,9 +375,14 @@ extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p ); extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManMarkCiCoNets( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ); -extern ABC_DLL int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); extern ABC_DLL void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManTransformInitValues( Ntl_Man_t * p ); +extern ABC_DLL int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCombRootNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); +extern ABC_DLL void Ntl_ModelClearNets( Ntl_Mod_t * pModel ); #ifdef __cplusplus } diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index d5100312..d3aecc8d 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -40,11 +40,100 @@ SeeAlso [] ***********************************************************************/ -int Ntl_ModelCheck( Ntl_Mod_t * pModel ) +int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i, k, fStatus = 1; + + // check root level model + if ( fMain ) + { + if ( Ntl_ModelLatchNum(pModel) > 0 ) + { + printf( "Root level model has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + fStatus = 0; + } + goto checkobjs; + } + + // check delay information + if ( pModel->attrBox && pModel->attrComb ) + { + if ( pModel->vDelays == NULL ) + { + printf( "Warning: Comb model %s does not have delay info. Default 1.0 delays are assumed.\n", pModel->pName ); + pModel->vDelays = Vec_IntAlloc( 3 ); + Vec_IntPush( pModel->vDelays, -1 ); + Vec_IntPush( pModel->vDelays, -1 ); + Vec_IntPush( pModel->vDelays, Aig_Float2Int(1.0) ); + } + if ( pModel->vTimeInputs != NULL ) + { + printf( "Combinational model %s has input arrival/required time information.\n", pModel->pName ); + fStatus = 0; + } + if ( pModel->vTimeOutputs != NULL ) + { + printf( "Combinational model %s has output arrival/required time information.\n", pModel->pName ); + fStatus = 0; + } + } + if ( pModel->attrBox && !pModel->attrComb ) + { + if ( pModel->vDelays != NULL ) + { + printf( "Sequential model %s has delay info.\n", pModel->pName ); + fStatus = 0; + } + if ( pModel->vTimeInputs == NULL ) + { + printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName ); + pModel->vTimeInputs = Vec_IntAlloc( 2 ); + Vec_IntPush( pModel->vTimeInputs, -1 ); + Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) ); + } + if ( pModel->vTimeOutputs == NULL ) + { + printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName ); + pModel->vTimeOutputs = Vec_IntAlloc( 2 ); + Vec_IntPush( pModel->vTimeOutputs, -1 ); + Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) ); + } + } + + // check box attributes + if ( pModel->attrBox ) + { + if ( !pModel->attrWhite ) + { + if ( Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) > 0 ) + { + printf( "Model %s is a blackbox, yet it has %d nodes.\n", pModel->pName, Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) ); + fStatus = 0; + } + if ( Ntl_ModelLatchNum(pModel) > 0 ) + { + printf( "Model %s is a blackbox, yet it has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + fStatus = 0; + } + return fStatus; + } + // this is a white box + if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 ) + { + printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName ); + fStatus = 0; + } + if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 ) + { + printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName ); + fStatus = 0; + } + } + +checkobjs: + // check nets Ntl_ModelForEachNet( pModel, pNet, i ) { if ( pNet->pName == NULL ) @@ -58,6 +147,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) fStatus = 0; } } + + // check objects Ntl_ModelForEachObj( pModel, pObj, i ) { Ntl_ObjForEachFanin( pObj, pNet, k ) @@ -89,8 +180,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) ***********************************************************************/ int Ntl_ManCheck( Ntl_Man_t * pMan ) { - Ntl_Mod_t * pMod1, * pMod2; - int i, k, fStatus = 1; + Ntl_Mod_t * pMod1; + int i, fStatus = 1; // check that the models have unique names Ntl_ManForEachModel( pMan, pMod1, i ) { @@ -99,16 +190,6 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) printf( "Model %d does not have a name\n", i ); fStatus = 0; } - Ntl_ManForEachModel( pMan, pMod2, k ) - { - if ( i >= k ) - continue; - if ( strcmp(pMod1->pName, pMod2->pName) == 0 ) - { - printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName ); - fStatus = 0; - } - } } // check that the models (except the first one) do not have boxes Ntl_ManForEachModel( pMan, pMod1, i ) @@ -124,9 +205,8 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) // check models Ntl_ManForEachModel( pMan, pMod1, i ) { - if ( !Ntl_ModelCheck( pMod1 ) ) + if ( !Ntl_ModelCheck( pMod1, i==0 ) ) fStatus = 0; - break; } return fStatus; } @@ -150,7 +230,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) Ntl_Obj_t * pNode; int i; - if ( Ntl_ModelIsBlackBox(pModel) ) + if ( !pModel->attrWhite ) return; // check for non-driven nets @@ -186,6 +266,37 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) Vec_PtrFree( vNets ); } +/**Function************************************************************* + + Synopsis [Fixed problems with non-driven nets in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel ) +{ + Ntl_Mod_t * pMod[3] = { NULL }; + Ntl_Obj_t * pLatch; + int i, Init; + if ( Ntl_ModelLatchNum(pModel) == 0 ) + return; + Ntl_ModelForEachLatch( pModel, pLatch, i ) + { + Init = pLatch->LatchId.regInit; + if ( pMod[Init] == NULL ) + pMod[Init] = Ntl_ManCreateLatchModel( pModel->pMan, Init ); + pLatch->pImplem = pMod[Init]; + pLatch->Type = NTL_OBJ_BOX; + } + printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel); + pModel->nObjs[NTL_OBJ_LATCH] = 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c index 8c7f7156..3ed6556d 100644 --- a/src/aig/ntl/ntlEc.c +++ b/src/aig/ntl/ntlEc.c @@ -42,33 +42,48 @@ 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 ) + Ntl_Net_t * pNet, * pNext; + int i, k; + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ModelForEachSeqLeaf( p1, pObj, i ) + { + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p2, pNext->pName ); + } + } + Ntl_ModelForEachSeqLeaf( p2, pObj, i ) + { + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p1, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, pNext->pName ); + } + } } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p1, pObj, i ) + Ntl_ModelForEachCombLeaf( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p2, pNext->pName ); + } } - Ntl_ModelForEachLatch( p2, pObj, i ) + Ntl_ModelForEachCombLeaf( p2, pObj, i ) { - pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p1, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, pNext->pName ); + } } } } @@ -89,38 +104,45 @@ 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) ); + Ntl_Net_t * pNet, * pNext; + int i, k; // order the CIs Vec_PtrClear( pMan1->vCis ); Vec_PtrClear( pMan2->vCis ); - Ntl_ModelForEachPi( p1, pObj, i ) + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) + assert( Ntl_ModelSeqLeafNum(p1) == Ntl_ModelSeqLeafNum(p2) ); + Ntl_ModelForEachSeqLeaf( p1, pObj, i ) { - printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); - return; + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pNext ); + Vec_PtrPush( pMan2->vCis, pNet ); + } } - Vec_PtrPush( pMan1->vCis, pObj ); - Vec_PtrPush( pMan2->vCis, pNet->pDriver ); } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p1, pObj, i ) + assert( Ntl_ModelCombLeafNum(p1) == Ntl_ModelCombLeafNum(p2) ); + Ntl_ModelForEachCombLeaf( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) + Ntl_ObjForEachFanout( pObj, pNext, k ) { - printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); - return; + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pNext ); + Vec_PtrPush( pMan2->vCis, pNet ); } - Vec_PtrPush( pMan1->vCis, pObj ); - Vec_PtrPush( pMan2->vCis, pNet->pDriver ); } } } @@ -141,45 +163,47 @@ 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; + Ntl_Net_t * pNet, * pNext; + int i, k; // order the COs Vec_PtrClear( pMan1->vCos ); Vec_PtrClear( pMan2->vCos ); - Ntl_ModelForEachPo( p1, pObj, i ) + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); - if ( pNet == NULL ) + assert( Ntl_ModelSeqRootNum(p1) == Ntl_ModelSeqRootNum(p2) ); + Ntl_ModelForEachSeqRoot( p1, pObj, i ) { - printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", - Ntl_ObjFanin0(pObj)->pName ); - continue; + Ntl_ObjForEachFanin( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + pNext->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pNext ); + Vec_PtrPush( pMan2->vCos, pNet ); + } } - Vec_PtrPush( pMan1->vCos, pObj ); - Vec_PtrPush( pMan2->vCos, pNet->pCopy ); } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p2, pObj, i ) - Ntl_ObjFanin0(pObj)->pCopy = pObj; - Ntl_ModelForEachLatch( p1, pObj, i ) + assert( Ntl_ModelCombRootNum(p1) == Ntl_ModelCombRootNum(p2) ); + Ntl_ModelForEachCombRoot( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); - if ( pNet == NULL ) + Ntl_ObjForEachFanin( pObj, pNext, k ) { - printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", - Ntl_ObjFanin0(pObj)->pName ); - continue; + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + pNext->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pNext ); + Vec_PtrPush( pMan2->vCos, pNet ); } - Vec_PtrPush( pMan1->vCos, pObj ); - Vec_PtrPush( pMan2->vCos, pNet->pCopy ); } } } @@ -214,19 +238,19 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan // make sure they are compatible pModel1 = Ntl_ManRootModel( pMan1 ); pModel2 = Ntl_ManRootModel( pMan2 ); - if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) ) { printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", - Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) ); + Ntl_ModelCombLeafNum(pModel1), Ntl_ModelCombLeafNum(pModel2) ); } - if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) ) + if ( Ntl_ModelCombRootNum(pModel1) != Ntl_ModelCombRootNum(pModel2) ) { printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", - Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) ); + Ntl_ModelCombRootNum(pModel1), Ntl_ModelCombRootNum(pModel2) ); } // normalize inputs/outputs Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 ); - if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) ) { if ( pMan1 ) Ntl_ManFree( pMan1 ); if ( pMan2 ) Ntl_ManFree( pMan2 ); @@ -243,8 +267,8 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan return; } // derive AIGs - *ppMan1 = Ntl_ManCollapseForCec( pMan1 ); - *ppMan2 = Ntl_ManCollapseForCec( pMan2 ); + *ppMan1 = Ntl_ManCollapseComb( pMan1 ); + *ppMan2 = Ntl_ManCollapseComb( pMan2 ); // cleanup Ntl_ManFree( pMan1 ); Ntl_ManFree( pMan2 ); @@ -263,7 +287,9 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan ***********************************************************************/ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) { - Aig_Man_t * pAig; + extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); + + Aig_Man_t * pAig1, * pAig2, * pAig; Ntl_Man_t * pMan1, * pMan2; Ntl_Mod_t * pModel1, * pModel2; // read the netlists @@ -286,12 +312,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" ); return NULL; } - if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) ) + if ( Ntl_ModelSeqLeafNum(pModel1) != Ntl_ModelSeqLeafNum(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) ) + if ( Ntl_ModelSeqRootNum(pModel1) != Ntl_ModelSeqRootNum(pModel2) ) { printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) ); @@ -308,9 +334,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) return NULL; } // derive AIGs - pAig = Ntl_ManCollapseForSec( pMan1, pMan2 ); + pAig1 = Ntl_ManCollapseSeq( pMan1 ); + pAig2 = Ntl_ManCollapseSeq( pMan2 ); + pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + Aig_ManStop( pAig1 ); + Aig_ManStop( pAig2 ); // cleanup - pMan1->pAig = pMan2->pAig = NULL; Ntl_ManFree( pMan1 ); Ntl_ManFree( pMan2 ); return pAig; diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index be6626df..a552f949 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -178,6 +178,9 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) if ( Ntl_ObjIsBox(pObj) ) { int LevelCur, LevelMax = -TIM_ETERNITY; + assert( Ntl_BoxIsComb(pObj) ); + assert( Ntl_ModelLatchNum(pObj->pImplem) == 0 ); + assert( pObj->pImplem->vDelays != NULL ); Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) ); Ntl_ObjForEachFanin( pObj, pNetFanin, i ) { @@ -218,7 +221,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; - int i, nUselessObjects; + int i, k, nUselessObjects; Ntl_ManCleanup( p ); assert( Vec_PtrSize(p->vCis) == 0 ); assert( Vec_PtrSize(p->vCos) == 0 ); @@ -231,63 +234,39 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); // get the root model pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelLatchNum(pRoot) == 0 ); // clear net visited flags - Ntl_ModelForEachNet( pRoot, pNet, i ) + Ntl_ModelClearNets( pRoot ); + // collect mapping leafs + Ntl_ModelForEachMapLeaf( pRoot, pObj, i ) { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // collect primary inputs - Ntl_ModelForEachPi( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - Vec_PtrPush( p->vCis, pNet ); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // collect latch outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - Vec_PtrPush( p->vCis, pNet ); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) + assert( !Ntl_ObjIsBox(pObj) || Ntl_BoxIsBlack(pObj) || Ntl_ModelLatchNum(pObj->pImplem) > 0 ); + Ntl_ObjForEachFanout( pObj, pNet, k ) { - printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" ); - return 0; + Vec_PtrPush( p->vCis, pNet ); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( pNet->nVisits ) + { + printf( "Ntl_ManExtract(): Seq leaf is duplicated or defined as a primary input.\n" ); + return 0; + } + pNet->nVisits = 2; } - pNet->nVisits = 2; } - // visit the nodes starting from primary outputs - Ntl_ModelForEachPo( pRoot, pObj, i ) + p->iLastCi = Aig_ManPiNum(p->pAig); + // collect mapping roots + Ntl_ModelForEachMapRoot( pRoot, pObj, i ) { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManExtract_rec( p, pNet ) ) - { - printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); - return 0; - } - Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); - } - // visit the nodes starting from latch inputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManExtract_rec( p, pNet ) ) + Ntl_ObjForEachFanin( pObj, pNet, k ) { - printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); - return 0; + if ( !Ntl_ManExtract_rec( p, pNet ) ) + { + printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); + return 0; + } + Vec_PtrPush( p->vCos, pNet ); + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } - Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // visit dangling boxes Ntl_ModelForEachBox( pRoot, pObj, i ) @@ -314,6 +293,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) return pAig; } + + + /**Function************************************************************* Synopsis [Collects the nodes in a topological order.] @@ -325,9 +307,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) +int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq ) { - extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ); + extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq ); Ntl_Mod_t * pModel = pBox->pImplem; Ntl_Obj_t * pObj; Ntl_Net_t * pNet, * pNetBox; @@ -335,8 +317,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) ); assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) ); // clear net visited flags - Ntl_ModelForEachNet( pModel, pNet, i ) - pNet->nVisits = 0; + Ntl_ModelClearNets( pModel ); // transfer from the box to the PIs of the model Ntl_ModelForEachPi( pModel, pObj, i ) { @@ -345,17 +326,41 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) pNet->pCopy = pNetBox->pCopy; pNet->nVisits = 2; } + // check if there are registers + if ( Ntl_ModelLatchNum(pModel) ) + { + Ntl_ModelForEachLatch( pModel, pObj, i ) + { + pNet = Ntl_ObjFanout0(pObj); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( fSeq && Ntl_ObjIsInit1( pObj ) ) + pNet->pCopy = Aig_Not(pNet->pCopy); + pNet->nVisits = 2; + } + } // compute AIG for the internal nodes Ntl_ModelForEachPo( pModel, pObj, i ) - if ( !Ntl_ManCollapse_rec( p, Ntl_ObjFanin0(pObj) ) ) - return 0; - // transfer from the POs of the model to the box - Ntl_ModelForEachPo( pModel, pObj, i ) { pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) + return 0; pNetBox = Ntl_ObjFanout( pBox, i ); pNetBox->pCopy = pNet->pCopy; } + // compute AIGs for the registers + if ( Ntl_ModelLatchNum(pModel) ) + { + Ntl_ModelForEachLatch( pModel, pObj, i ) + { + pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) + return 0; + if ( fSeq && Ntl_ObjIsInit1( pObj ) ) + Vec_PtrPush( p->vLatchIns, Aig_Not(pNet->pCopy) ); + else + Vec_PtrPush( p->vLatchIns, pNet->pCopy ); + } + } return 1; } @@ -370,7 +375,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) SeeAlso [] ***********************************************************************/ -int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) +int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNetFanin; @@ -388,12 +393,13 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) ); // visit the input nets of the box Ntl_ObjForEachFanin( pObj, pNetFanin, i ) - if ( !Ntl_ManCollapse_rec( p, pNetFanin ) ) + if ( !Ntl_ManCollapse_rec( p, pNetFanin, fSeq ) ) return 0; // add box inputs/outputs to COs/CIs if ( Ntl_ObjIsBox(pObj) ) { - if ( !Ntl_ManBuildModelAig( p, pObj ) ) + assert( Ntl_BoxIsWhite(pObj) ); + if ( !Ntl_ManCollapseBox_rec( p, pObj, fSeq ) ) return 0; } if ( Ntl_ObjIsNode(pObj) ) @@ -417,310 +423,125 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ) { Aig_Man_t * pAig; + Aig_Obj_t * pTemp; Ntl_Mod_t * pRoot; - Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i; - // start the AIG manager - assert( p->pAig == NULL ); + assert( Vec_PtrSize(p->vCis) != 0 ); + assert( Vec_PtrSize(p->vCos) != 0 ); + assert( Vec_PtrSize(p->vLatchIns) == 0 ); + // clear net visited flags + pRoot = Ntl_ManRootModel(p); + Ntl_ModelClearNets( pRoot ); + assert( Ntl_ModelLatchNum(pRoot) == 0 ); + // create the manager p->pAig = Aig_ManStart( 10000 ); p->pAig->pName = Aig_UtilStrsav( p->pName ); p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); - // get the root model - pRoot = Ntl_ManRootModel( p ); - // clear net visited flags - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // collect primary inputs - Ntl_ModelForEachPi( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // collect latch outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) + // set the inputs + Ntl_ManForEachCiNet( p, pNet, i ) { - 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" ); + printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" ); return 0; } pNet->nVisits = 2; } - // visit the nodes starting from primary outputs - Ntl_ModelForEachPo( pRoot, pObj, i ) + // derive the outputs + Ntl_ManForEachCoNet( p, pNet, i ) { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p, pNet ) ) + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) { - printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); + printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" ); return 0; } Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } - // visit the nodes starting from latch inputs outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p, pNet ) ) - { - 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 ); - } + // add the latch inputs + Vec_PtrForEachEntry( p->vLatchIns, pTemp, i ) + Aig_ObjCreatePo( p->pAig, pTemp ); // cleanup the AIG + Aig_ManSetRegNum( p->pAig, Vec_PtrSize(p->vLatchIns) ); Aig_ManCleanup( p->pAig ); pAig = p->pAig; p->pAig = NULL; return pAig; } + /**Function************************************************************* - Synopsis [Derives AIG for CEC.] + Synopsis [Collapses the netlist combinationally.] - Description [Uses CIs/COs collected in the internal arrays.] + Description [Checks for combinational loops. Collects PI/PO nets. + Collects nodes in the topological order.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ) +Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ) { - Aig_Man_t * pAig; Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; - int i; - // clear net visited flags + int i, k; + Vec_PtrClear( p->vCis ); + Vec_PtrClear( p->vCos ); + Vec_PtrClear( p->vLatchIns ); + // prepare the model pRoot = Ntl_ManRootModel(p); - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // 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 - Aig_ManCleanup( p->pAig ); - pAig = p->pAig; p->pAig = NULL; - return pAig; + // collect the leaves for this traversal + Ntl_ModelForEachCombLeaf( pRoot, pObj, i ) + Ntl_ObjForEachFanout( pObj, pNet, k ) + Vec_PtrPush( p->vCis, pNet ); + // collect the roots for this traversal + Ntl_ModelForEachCombRoot( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNet, k ) + Vec_PtrPush( p->vCos, pNet ); + // perform the traversal + return Ntl_ManCollapse( p, 0 ); } /**Function************************************************************* - Synopsis [Derives AIG for SEC.] + Synopsis [Collapses the netlist combinationally.] - Description [Uses CIs/COs collected in the internal arrays.] + 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 * Ntl_ManCollapseSeq( Ntl_Man_t * p ) { - Aig_Man_t * pAig; - Aig_Obj_t * pMiter; - Ntl_Mod_t * pRoot1, * pRoot2; + Ntl_Mod_t * pRoot; 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) ); - - ///////////////////////////////////////////////////// - // clear net visited flags - pRoot1 = Ntl_ManRootModel(p1); - Ntl_ModelForEachNet( pRoot1, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // 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 - 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 ); - } - - ///////////////////////////////////////////////////// - // clear net visited flags - pRoot2 = Ntl_ManRootModel(p2); - Ntl_ModelForEachNet( pRoot2, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // 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 - 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 ); - Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) ); - Aig_ManCleanup( pAig ); - return pAig; + int i, k; + Vec_PtrClear( p->vCis ); + Vec_PtrClear( p->vCos ); + Vec_PtrClear( p->vLatchIns ); + // prepare the model + pRoot = Ntl_ManRootModel(p); + // collect the leaves for this traversal + Ntl_ModelForEachSeqLeaf( pRoot, pObj, i ) + Ntl_ObjForEachFanout( pObj, pNet, k ) + Vec_PtrPush( p->vCis, pNet ); + // collect the roots for this traversal + Ntl_ModelForEachSeqRoot( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNet, k ) + Vec_PtrPush( p->vCos, pNet ); + // perform the traversal + return Ntl_ManCollapse( p, 1 ); } + /**Function************************************************************* Synopsis [Increments reference counter of the net.] @@ -806,11 +627,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan vCover = Vec_IntAlloc( 100 ); vMemory = Vec_IntAlloc( 1 << 16 ); // count the number of fanouts of each net - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->pCopy = NULL; - pNet->fMark = 0; - } + Ntl_ModelClearNets( pRoot ); Ntl_ModelForEachObj( pRoot, pObj, i ) Ntl_ObjForEachFanin( pObj, pNet, k ) Ntl_NetIncrementRefs( pNet ); @@ -867,11 +684,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan } } // Aig_ManCleanPioNumbers( pAig ); - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->pCopy = NULL; - pNet->fMark = 0; - } + Ntl_ModelClearNets( pRoot ); Vec_IntFree( vCover ); Vec_IntFree( vMemory ); // create timing manager from the current design diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 6de41679..cdc1323b 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -203,7 +203,7 @@ void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol ) pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { pObjCol = Ntl_ObjFanout0(pObj)->pCopy; assert( pObjCol->fPhase == 0 ); @@ -275,7 +275,7 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 0 ); + pAigCol = Ntl_ManCollapseComb( pNew ); // perform fraiging for the given design nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol); @@ -309,7 +309,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -343,7 +343,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -377,7 +377,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -502,7 +502,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol ) iLatch = 0; Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch ); assert( pObjCol->fMarkA == 0 ); @@ -524,7 +524,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol ) iLatch = 0; Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { // flip the latch input pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch ); @@ -554,7 +554,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars ) Ntl_Man_t * pNew; Aig_Man_t * pAigRed, * pAigCol; // collapse the AIG - pAigCol = Ntl_ManCollapse( p, 1 ); + pAigCol = Ntl_ManCollapseSeq( p ); Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); // transform the collapsed AIG pAigRed = Fra_FraigInduction( pAigCol, pPars ); diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 3cd9470b..9675eb28 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -257,7 +257,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) ***********************************************************************/ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { - char Buffer[100]; + char Buffer[100]; Vec_Ptr_t * vObjs; Vec_Int_t * vTruth; Vec_Int_t * vCover; diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index e80e02c6..0083e04c 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -50,9 +50,14 @@ Ntl_Man_t * Ntl_ManAlloc() p->vCos = Vec_PtrAlloc( 1000 ); p->vNodes = Vec_PtrAlloc( 1000 ); p->vBox1Cos = Vec_IntAlloc( 1000 ); + p->vLatchIns = Vec_PtrAlloc( 1000 ); // start the manager p->pMemObjs = Aig_MmFlexStart(); p->pMemSops = Aig_MmFlexStart(); + // allocate model table + p->nModTableSize = Aig_PrimeCudd( 100 ); + p->pModTable = ALLOC( Ntl_Mod_t *, p->nModTableSize ); + memset( p->pModTable, 0, sizeof(Ntl_Mod_t *) * p->nModTableSize ); return p; } @@ -185,14 +190,16 @@ void Ntl_ManFree( Ntl_Man_t * p ) Ntl_ModelFree( pModel ); Vec_PtrFree( p->vModels ); } - if ( p->vCis ) Vec_PtrFree( p->vCis ); - if ( p->vCos ) Vec_PtrFree( p->vCos ); - if ( p->vNodes ) Vec_PtrFree( p->vNodes ); - if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos ); - if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); - if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 ); - if ( p->pAig ) Aig_ManStop( p->pAig ); - if ( p->pManTime ) Tim_ManStop( p->pManTime ); + if ( p->vCis ) Vec_PtrFree( p->vCis ); + if ( p->vCos ) Vec_PtrFree( p->vCos ); + if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos ); + if ( p->vLatchIns ) Vec_PtrFree( p->vLatchIns ); + if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); + if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 ); + if ( p->pAig ) Aig_ManStop( p->pAig ); + if ( p->pManTime ) Tim_ManStop( p->pManTime ); + FREE( p->pModTable ); free( p ); } @@ -239,7 +246,7 @@ int Ntl_ManLatchNum( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) +Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName ) { Ntl_Mod_t * pModel; int i; @@ -276,6 +283,8 @@ void Ntl_ManPrintStats( Ntl_Man_t * p ) printf( "\n" ); fflush( stdout ); assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) ); + Ntl_ManPrintTypes( p ); + fflush( stdout ); } /**Function************************************************************* @@ -296,6 +305,67 @@ Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ) /**Function************************************************************* + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj ) +{ + Ntl_Mod_t * pModel = pObj->pImplem; + int Number = 0; + assert( Ntl_ObjIsBox(pObj) ); + Number |= (pModel->attrWhite << 0); + Number |= (pModel->attrBox << 1); + Number |= (pModel->attrComb << 2); + Number |= (pModel->attrKeep << 3); + pModel->pMan->BoxTypes[Number]++; +} + +/**Function************************************************************* + + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManPrintTypes( Ntl_Man_t * p ) +{ + Ntl_Mod_t * pModel; + Ntl_Obj_t * pObj; + int i; + pModel = Ntl_ManRootModel( p ); + if ( Ntl_ModelBoxNum(pModel) == 0 ) + return; + printf( "BOX STATISTICS:\n" ); + Ntl_ModelForEachBox( pModel, pObj, i ) + Ntl_ManSaveBoxType( pObj ); + for ( i = 0; i < 15; i++ ) + { + if ( !p->BoxTypes[i] ) + continue; + printf( "%5d :", p->BoxTypes[i] ); + printf( " %s", ((i & 1) > 0)? "white": "black" ); + printf( " %s", ((i & 2) > 0)? "box ": "logic" ); + printf( " %s", ((i & 4) > 0)? "comb ": "seq " ); + printf( " %s", ((i & 8) > 0)? "keep ": "sweep" ); + printf( "\n" ); + } + printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) ); + for ( i = 0; i < 15; i++ ) + p->BoxTypes[i] = 0; +} + +/**Function************************************************************* + Synopsis [Allocates the model.] Description [] @@ -311,16 +381,25 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ) // start the manager p = ALLOC( Ntl_Mod_t, 1 ); memset( p, 0, sizeof(Ntl_Mod_t) ); + p->attrBox = 1; + p->attrComb = 1; + p->attrWhite = 1; + p->attrKeep = 0; p->pMan = pMan; p->pName = Ntl_ManStoreName( p->pMan, pName ); - Vec_PtrPush( pMan->vModels, p ); - p->vObjs = Vec_PtrAlloc( 1000 ); - p->vPis = Vec_PtrAlloc( 100 ); - p->vPos = Vec_PtrAlloc( 100 ); + p->vObjs = Vec_PtrAlloc( 100 ); + p->vPis = Vec_PtrAlloc( 10 ); + p->vPos = Vec_PtrAlloc( 10 ); // start the table - p->nTableSize = Aig_PrimeCudd( 1000 ); + p->nTableSize = Aig_PrimeCudd( 100 ); p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize ); memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize ); + // add model to the table + if ( !Ntl_ManAddModel( pMan, p ) ) + { + Ntl_ModelFree( p ); + return NULL; + } return p; } @@ -371,11 +450,14 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) if ( pNet->pCopy != NULL ) Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); if ( Ntl_ObjIsLatch(pObj) ) + { ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy; + } } 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; + pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL; + pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL; return pModelNew; } @@ -397,11 +479,20 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_Obj_t * pObj; int i, k; pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); + pModelNew->attrWhite = pModelOld->attrWhite; + pModelNew->attrBox = pModelOld->attrBox; + pModelNew->attrComb = pModelOld->attrComb; + pModelNew->attrKeep = pModelOld->attrKeep; Ntl_ModelForEachObj( pModelOld, pObj, i ) pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj ); Ntl_ModelForEachNet( pModelOld, pNet, i ) { pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); + if ( pNet->pDriver == NULL ) + { + assert( !pModelOld->attrWhite ); + continue; + } ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy; assert( pNet->pDriver->pCopy != NULL ); } @@ -412,13 +503,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_ObjForEachFanout( pObj, pNet, k ) Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); if ( Ntl_ObjIsLatch(pObj) ) + { ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy; + } if ( Ntl_ObjIsNode(pObj) ) ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop ); } 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; + pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL; + pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL; return pModelNew; } @@ -435,10 +529,10 @@ 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 ); + assert( Ntl_ModelCheckNetsAreNotMarked(p) ); + if ( p->vTimeOutputs ) Vec_IntFree( p->vTimeOutputs ); + if ( p->vTimeInputs ) Vec_IntFree( p->vTimeInputs ); + if ( p->vDelays ) Vec_IntFree( p->vDelays ); Vec_PtrFree( p->vObjs ); Vec_PtrFree( p->vPis ); Vec_PtrFree( p->vPos ); @@ -446,6 +540,45 @@ void Ntl_ModelFree( Ntl_Mod_t * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Create model equal to the latch with the given init value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ) +{ + char Name[100]; + Ntl_Mod_t * pModel; + Ntl_Obj_t * pObj; + Ntl_Net_t * pNetLi, * pNetLo; + // create model + sprintf( Name, "%s%d", "latch", Init ); + pModel = Ntl_ModelAlloc( pMan, Name ); + pModel->attrWhite = 1; + pModel->attrBox = 1; + pModel->attrComb = 0; + pModel->attrKeep = 0; + // create primary input + pObj = Ntl_ModelCreatePi( pModel ); + pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" ); + Ntl_ModelSetNetDriver( pObj, pNetLi ); + // create latch + pObj = Ntl_ModelCreateLatch( pModel ); + pObj->LatchId.regInit = Init; + pObj->pFanio[0] = pNetLi; + // create primary output + pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" ); + Ntl_ModelSetNetDriver( pObj, pNetLo ); + pObj = Ntl_ModelCreatePo( pModel, pNetLo ); + return pModel; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index a291f8a0..ebfb2a80 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -38,8 +38,8 @@ struct Ioa_ReadMod_t_ Vec_Ptr_t * vNames; // .names lines Vec_Ptr_t * vSubckts; // .subckt lines Vec_Ptr_t * vDelays; // .delay lines - Vec_Ptr_t * vArrivals; // .input_arrival lines - Vec_Ptr_t * vRequireds; // .output_required lines + Vec_Ptr_t * vTimeInputs; // .input_arrival/required lines + Vec_Ptr_t * vTimeOutputs; // .output_required/arrival lines int fBlackBox; // indicates blackbox model // the resulting network Ntl_Mod_t * pNtk; @@ -249,14 +249,14 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc() Ioa_ReadMod_t * p; p = ALLOC( Ioa_ReadMod_t, 1 ); memset( p, 0, sizeof(Ioa_ReadMod_t) ); - p->vInputs = Vec_PtrAlloc( 512 ); - p->vOutputs = Vec_PtrAlloc( 512 ); - p->vLatches = Vec_PtrAlloc( 512 ); - p->vNames = Vec_PtrAlloc( 512 ); - p->vSubckts = Vec_PtrAlloc( 512 ); - p->vDelays = Vec_PtrAlloc( 512 ); - p->vArrivals = Vec_PtrAlloc( 512 ); - p->vRequireds = Vec_PtrAlloc( 512 ); + p->vInputs = Vec_PtrAlloc( 8 ); + p->vOutputs = Vec_PtrAlloc( 8 ); + p->vLatches = Vec_PtrAlloc( 8 ); + p->vNames = Vec_PtrAlloc( 8 ); + p->vSubckts = Vec_PtrAlloc( 8 ); + p->vDelays = Vec_PtrAlloc( 8 ); + p->vTimeInputs = Vec_PtrAlloc( 8 ); + p->vTimeOutputs = Vec_PtrAlloc( 8 ); return p; } @@ -279,8 +279,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p ) Vec_PtrFree( p->vNames ); Vec_PtrFree( p->vSubckts ); Vec_PtrFree( p->vDelays ); - Vec_PtrFree( p->vArrivals ); - Vec_PtrFree( p->vRequireds ); + Vec_PtrFree( p->vTimeInputs ); + Vec_PtrFree( p->vTimeOutputs ); free( p ); } @@ -509,10 +509,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) Vec_PtrPush( p->pLatest->vSubckts, pCur ); else if ( !strncmp(pCur, "delay", 5) ) Vec_PtrPush( p->pLatest->vDelays, pCur ); - else if ( !strncmp(pCur, "input_arrival", 13) ) - Vec_PtrPush( p->pLatest->vArrivals, pCur ); - else if ( !strncmp(pCur, "output_required", 15) ) - Vec_PtrPush( p->pLatest->vRequireds, pCur ); + else if ( !strncmp(pCur, "input_arrival", 13) || + !strncmp(pCur, "input_required", 14) ) + Vec_PtrPush( p->pLatest->vTimeInputs, pCur ); + else if ( !strncmp(pCur, "output_required", 14) || + !strncmp(pCur, "output_arrival", 13) ) + Vec_PtrPush( p->pLatest->vTimeOutputs, pCur ); else if ( !strncmp(pCur, "blackbox", 8) ) p->pLatest->fBlackBox = 1; else if ( !strncmp(pCur, "model", 5) ) @@ -522,7 +524,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) p->pLatest->pMan = p; } else if ( !strncmp(pCur, "attrib", 6) ) - p->pLatest->pAttrib = pCur; + { + if ( p->pLatest->pAttrib != NULL ) + fprintf( stdout, "Line %d: Skipping second .attrib line for this model.\n", Ioa_ReadGetLine(p, pCur) ); + else + p->pLatest->pAttrib = pCur; + } else if ( !strncmp(pCur, "end", 3) ) { if ( p->pLatest ) @@ -537,15 +544,6 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) else if ( !strncmp(pCur, "no_merge", 8) ) { } - else if ( !strncmp(pCur, "attribute", 9) ) - { - } - else if ( !strncmp(pCur, "input_required", 14) ) - { - } - else if ( !strncmp(pCur, "output_arrival", 14) ) - { - } else { pCur--; @@ -593,10 +591,10 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ) Vec_PtrForEachEntry( pMod->vDelays, pLine, k ) if ( !Ioa_ReadParseLineDelay( pMod, pLine ) ) return 0; - Vec_PtrForEachEntry( pMod->vArrivals, pLine, k ) + Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k ) if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) ) return 0; - Vec_PtrForEachEntry( pMod->vRequireds, pLine, k ) + Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k ) if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) ) return 0; } @@ -643,6 +641,8 @@ static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p ) return NULL; // update the design name pMod = Vec_PtrEntry( p->vModels, 0 ); + if ( Ntl_ModelLatchNum(pMod->pNtk) > 0 ) + Ntl_ModelTransformLatches( pMod->pNtk ); p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName ); // return the network pDesign = p->pDesign; @@ -674,6 +674,11 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ) return 0; } p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) ); + if ( p->pNtk == NULL ) + { + sprintf( p->pMan->sError, "Line %d: Model %s already exists.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } return 1; } @@ -692,23 +697,33 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; char * pToken; + int i; Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry( vTokens, 0 ); assert( !strncmp(pToken, "attrib", 6) ); -/* - if ( Vec_PtrSize(vTokens) != 2 ) - { - sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); - return 0; - } - if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 ) - p->pNtk->fKeep = 1; - else + Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 ) { - sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName ); - return 0; + pToken = Vec_PtrEntry( vTokens, i ); + if ( strcmp( pToken, "white" ) == 0 ) + p->pNtk->attrWhite = 1; + else if ( strcmp( pToken, "black" ) == 0 ) + p->pNtk->attrWhite = 0; + else if ( strcmp( pToken, "box" ) == 0 ) + p->pNtk->attrBox = 1; + else if ( strcmp( pToken, "white" ) == 0 ) + p->pNtk->attrWhite = 1; + else if ( strcmp( pToken, "comb" ) == 0 ) + p->pNtk->attrComb = 1; + else if ( strcmp( pToken, "seq" ) == 0 ) + p->pNtk->attrComb = 0; + else if ( strcmp( pToken, "keep" ) == 0 ) + p->pNtk->attrKeep = 1; + else + { + sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName ); + return 0; + } } -*/ return 1; } @@ -792,7 +807,6 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) Ntl_Net_t * pNetLi, * pNetLo; Ntl_Obj_t * pObj; char * pToken, * pNameLi, * pNameLo; - int Init, Class; Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry(vTokens,0); assert( !strcmp(pToken, "latch") ); @@ -815,31 +829,47 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) } // get initial value if ( Vec_PtrSize(vTokens) > 3 ) - Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) ); + pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) ); else - Init = 2; - if ( Init < 0 || Init > 2 ) + pObj->LatchId.regInit = 2; + if ( pObj->LatchId.regInit < 0 || pObj->LatchId.regInit > 2 ) { sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); return 0; } // get the register class if ( Vec_PtrSize(vTokens) == 6 ) - Class = atoi( Vec_PtrEntry(vTokens,3) ); - else - Class = 0; - if ( Class < 0 || Class > (1<<24) ) { - sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) ); + pToken = Vec_PtrEntry(vTokens,3); + if ( strcmp( pToken, "fe" ) == 0 ) + pObj->LatchId.regType = 1; + else if ( strcmp( pToken, "re" ) == 0 ) + pObj->LatchId.regType = 2; + else if ( strcmp( pToken, "ah" ) == 0 ) + pObj->LatchId.regType = 3; + else if ( strcmp( pToken, "al" ) == 0 ) + pObj->LatchId.regType = 4; + else if ( strcmp( pToken, "as" ) == 0 ) + pObj->LatchId.regType = 5; + else if ( pToken[0] >= '0' && pToken[0] <= '9' ) + pObj->LatchId.regClass = atoi(pToken); + else + { + sprintf( p->pMan->sError, "Line %d: Type/class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), pToken ); + return 0; + } + } + if ( pObj->LatchId.regClass < 0 || pObj->LatchId.regClass > (1<<24) ) + { + sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); return 0; } - pObj->LatchId = (Class << 2) | Init; // get the clock if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 ) { pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2); pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); -// pObj->pFanio[1] = pNetLi; + pObj->pClock = pNetLi; } return 1; } @@ -984,7 +1014,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) RetValue1 = 0; Number1 = -1; if ( Vec_PtrSize(vTokens) > 2 ) { - RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 ); + RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 1), &Number1 ); if ( RetValue1 == 0 ) { sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); @@ -994,7 +1024,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) RetValue2 = 0; Number2 = -1; if ( Vec_PtrSize(vTokens) > 3 ) { - RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 ); + RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 2), &Number2 ); if ( RetValue2 == 0 ) { sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) ); @@ -1037,19 +1067,19 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; - int RetValue, Number; + int RetValue, Number = -1; char * pToken, * pTokenNum; float Delay; assert( sizeof(float) == sizeof(int) ); Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry(vTokens,0); if ( fOutput ) - assert( !strcmp(pToken, "output_required") ); + assert( !strncmp(pToken, "output_", 7) ); else - assert( !strcmp(pToken, "input_arrival") ); - if ( Vec_PtrSize(vTokens) != 3 ) + assert( !strncmp(pToken, "input_", 6) ); + if ( Vec_PtrSize(vTokens) != 2 && Vec_PtrSize(vTokens) != 3 ) { - sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) ); + sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) ); return 0; } // find the delay number @@ -1068,31 +1098,37 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput // find the PI/PO numbers if ( fOutput ) { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) + if ( Vec_PtrSize(vTokens) == 3 ) { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; + RetValue = Ntl_ModelFindPioNumber( p->pNtk, 0, 1, Vec_PtrEntry(vTokens, 1), &Number ); + if ( RetValue == 0 ) + { + sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } } // store the values - if ( p->pNtk->vRequireds == NULL ) - p->pNtk->vRequireds = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vRequireds, Number ); - Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) ); + if ( p->pNtk->vTimeOutputs == NULL ) + p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 ); + Vec_IntPush( p->pNtk->vTimeOutputs, Number ); + Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) ); } else { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) + if ( Vec_PtrSize(vTokens) == 3 ) { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; + RetValue = Ntl_ModelFindPioNumber( p->pNtk, 1, 0, Vec_PtrEntry(vTokens, 1), &Number ); + if ( RetValue == 0 ) + { + sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } } // store the values - if ( p->pNtk->vArrivals == NULL ) - p->pNtk->vArrivals = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vArrivals, Number ); - Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) ); + if ( p->pNtk->vTimeInputs == NULL ) + p->pNtk->vTimeInputs = Vec_IntAlloc( 100 ); + Vec_IntPush( p->pNtk->vTimeInputs, Number ); + Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) ); } return 1; } diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c index 8309e1b3..991d701a 100644 --- a/src/aig/ntl/ntlSweep.c +++ b/src/aig/ntl/ntlSweep.c @@ -79,7 +79,7 @@ void Ntl_ManSweepMark( Ntl_Man_t * p ) Ntl_ManSweepMark_rec( p, pObj ); // start from the persistant boxes Ntl_ModelForEachBox( pRoot, pObj, i ) - if ( pObj->pImplem->fKeep ) + if ( pObj->pImplem->attrKeep ) Ntl_ManSweepMark_rec( p, pObj ); } diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index c3acc0b1..fe58e2f8 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -189,7 +189,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) SeeAlso [] ***********************************************************************/ -int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ) +int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) { Ntl_Net_t * pNet; Ntl_Obj_t * pObj; @@ -198,6 +198,30 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ) pNet = Ntl_ModelFindNet( p, pName ); if ( pNet == NULL ) return 0; + if ( fPiOnly ) + { + Ntl_ModelForEachPi( p, pObj, i ) + { + if ( Ntl_ObjFanout0(pObj) == pNet ) + { + *pNumber = i; + return -1; + } + } + return 0; + } + if ( fPoOnly ) + { + Ntl_ModelForEachPo( p, pObj, i ) + { + if ( Ntl_ObjFanin0(pObj) == pNet ) + { + *pNumber = i; + return 1; + } + } + return 0; + } Ntl_ModelForEachPo( p, pObj, i ) { if ( Ntl_ObjFanin0(pObj) == pNet ) @@ -281,6 +305,97 @@ int Ntl_ModelCountNets( Ntl_Mod_t * p ) return Counter; } + + + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManModelTableResize( Ntl_Man_t * p ) +{ + Ntl_Mod_t ** pModTableNew, ** ppSpot, * pEntry, * pEntry2; + int nModTableSizeNew, Counter, e, clk; +clk = clock(); + // get the new table size + nModTableSizeNew = Aig_PrimeCudd( 3 * p->nModTableSize ); + // allocate a new array + pModTableNew = ALLOC( Ntl_Mod_t *, nModTableSizeNew ); + memset( pModTableNew, 0, sizeof(Ntl_Mod_t *) * nModTableSizeNew ); + // rehash entries + Counter = 0; + for ( e = 0; e < p->nModTableSize; e++ ) + for ( pEntry = p->pModTable[e], pEntry2 = pEntry? pEntry->pNext : NULL; + pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL ) + { + ppSpot = pModTableNew + Ntl_HashString( pEntry->pName, nModTableSizeNew ); + pEntry->pNext = *ppSpot; + *ppSpot = pEntry; + Counter++; + } + assert( Counter == p->nModEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pModTable ); + p->pModTable = pModTableNew; + p->nModTableSize = nModTableSizeNew; +} + +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ) +{ + Ntl_Mod_t * pEnt; + unsigned Key = Ntl_HashString( pModel->pName, p->nModTableSize ); + for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext ) + if ( !strcmp( pEnt->pName, pModel->pName ) ) + return 0; + pModel->pNext = p->pModTable[Key]; + p->pModTable[Key] = pModel; + if ( ++p->nModEntries > 2 * p->nModTableSize ) + Ntl_ManModelTableResize( p ); + Vec_PtrPush( p->vModels, pModel ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) +{ + Ntl_Mod_t * pEnt; + unsigned Key = Ntl_HashString( pName, p->nModTableSize ); + for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext ) + if ( !strcmp( pEnt->pName, pName ) ) + return pEnt; + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c index 94691ab8..c23a4e24 100644 --- a/src/aig/ntl/ntlTime.c +++ b/src/aig/ntl/ntlTime.c @@ -88,13 +88,27 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ) // start the timing manager pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) ); // unpack the data in the arrival times - if ( pRoot->vArrivals ) - Vec_IntForEachEntry( pRoot->vArrivals, Entry, i ) - Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) ); + if ( pRoot->vTimeInputs ) + { + Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i ) + { + if ( Entry == -1 ) + Tim_ManSetCiArrivalAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) ); + else + Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) ); + } + } // unpack the data in the required times - if ( pRoot->vRequireds ) - Vec_IntForEachEntry( pRoot->vRequireds, Entry, i ) - Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) ); + if ( pRoot->vTimeOutputs ) + { + Vec_IntForEachEntry( pRoot->vTimeOutputs, Entry, i ) + { + if ( Entry == -1 ) + Tim_ManSetCoRequiredAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) ); + else + Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) ); + } + } // derive timing tables vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) ); Ntl_ManForEachModel( p, pModel, i ) @@ -106,7 +120,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ) Tim_ManSetDelayTables( pMan, vDelayTables ); // set up the boxes iBox = 0; - curPi = Ntl_ModelCiNum(pRoot); + curPi = p->iLastCi; Ntl_ManForEachBox( p, pObj, i ) { Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable ); diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 6849889d..c9ef2dc4 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -238,26 +238,6 @@ void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ) /**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; -} - -/**Function************************************************************* - Synopsis [Convert initial values of registers to be zero.] Description [] @@ -274,7 +254,7 @@ void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ) int i; pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) - pObj->LatchId &= ~3; + pObj->LatchId.regInit = 0; } /**Function************************************************************* @@ -296,7 +276,7 @@ void Ntl_ManAddInverters( Ntl_Obj_t * pObj ) Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv; Ntl_Obj_t * pNode; int nLength, RetValue; - assert( (pObj->LatchId & 3) == 1 ); + assert( Ntl_ObjIsInit1( pObj ) ); // get the nets pNetLi = Ntl_ObjFanin0(pObj); pNetLo = Ntl_ObjFanout0(pObj); @@ -362,11 +342,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p ) pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) Ntl_ManAddInverters( pObj ); - pObj->LatchId &= ~3; + pObj->LatchId.regInit = 0; } +} + +/**Function************************************************************* + + Synopsis [Counts the number of CIs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachCombLeaf( p, pObj, i ) + Counter += Ntl_ObjFanoutNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of COs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCombRootNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachCombRoot( p, pObj, i ) + Counter += Ntl_ObjFaninNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of CIs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachSeqLeaf( p, pObj, i ) + Counter += Ntl_ObjFanoutNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of COs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachSeqRoot( p, pObj, i ) + Counter += Ntl_ObjFaninNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Unmarks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ModelForEachNet( pModel, pNet, i ) + assert( pNet->fMark == 0 ); + return 1; +} + +/**Function************************************************************* + Synopsis [Unmarks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ModelClearNets( Ntl_Mod_t * pModel ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ModelForEachNet( pModel, pNet, i ) + { + pNet->nVisits = 0; + pNet->pCopy = NULL; + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 51d41c26..f93e3fa1 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -40,15 +40,22 @@ SeeAlso [] ***********************************************************************/ -void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) +void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNet; float Delay; - int i, k, fClockAdded = 0; + int i, k; fprintf( pFile, ".model %s\n", pModel->pName ); - if ( pModel->fKeep ) - fprintf( pFile, ".attrib keep\n" ); + if ( pModel->attrWhite || pModel->attrBox || pModel->attrComb || pModel->attrKeep ) + { + fprintf( pFile, ".attrib" ); + fprintf( pFile, " %s", pModel->attrWhite? "white": "black" ); + fprintf( pFile, " %s", pModel->attrBox? "box" : "logic" ); + fprintf( pFile, " %s", pModel->attrComb? "comb" : "seq" ); +// fprintf( pFile, " %s", pModel->attrKeep? "keep" : "sweep" ); + fprintf( pFile, "\n" ); + } fprintf( pFile, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); @@ -63,19 +70,25 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 ) { fprintf( pFile, ".delay" ); - fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName ); - fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName ); + if ( Vec_IntEntry(pModel->vDelays,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName ); + if ( Vec_IntEntry(pModel->vDelays,i+1) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName ); fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) ); fprintf( pFile, "\n" ); } } - if ( pModel->vArrivals ) + if ( pModel->vTimeInputs ) { - for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 ) + for ( i = 0; i < Vec_IntSize(pModel->vTimeInputs); i += 2 ) { - fprintf( pFile, ".input_arrival" ); - fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName ); - Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1)); + if ( fMain ) + fprintf( pFile, ".input_arrival" ); + else + fprintf( pFile, ".input_required" ); + if ( Vec_IntEntry(pModel->vTimeInputs,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vTimeInputs,i)))->pName ); + Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeInputs,i+1)); if ( Delay == -TIM_ETERNITY ) fprintf( pFile, " -inf" ); else if ( Delay == TIM_ETERNITY ) @@ -85,13 +98,17 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, "\n" ); } } - if ( pModel->vRequireds ) + if ( pModel->vTimeOutputs ) { - for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 ) + for ( i = 0; i < Vec_IntSize(pModel->vTimeOutputs); i += 2 ) { - fprintf( pFile, ".output_required" ); - fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName ); - Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1)); + if ( fMain ) + fprintf( pFile, ".output_required" ); + else + fprintf( pFile, ".output_arrival" ); + if ( Vec_IntEntry(pModel->vTimeOutputs,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vTimeOutputs,i)))->pName ); + Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeOutputs,i+1)); if ( Delay == -TIM_ETERNITY ) fprintf( pFile, " -inf" ); else if ( Delay == TIM_ETERNITY ) @@ -117,13 +134,27 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, ".latch" ); fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName ); fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); - if ( pObj->LatchId >> 2 ) - fprintf( pFile, " %d", pObj->LatchId >> 2 ); - if ( Ntl_ObjFanin(pObj, 1) != NULL ) - fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName ); - else if ( pObj->LatchId >> 2 ) - fprintf( pFile, " clock99" ), fClockAdded = 1; - fprintf( pFile, " %d", pObj->LatchId & 3 ); + assert( pObj->LatchId.regType == 0 || pObj->LatchId.regClass == 0 ); + if ( pObj->LatchId.regType ) + { + if ( pObj->LatchId.regType == 1 ) + fprintf( pFile, " fe" ); + else if ( pObj->LatchId.regType == 2 ) + fprintf( pFile, " re" ); + else if ( pObj->LatchId.regType == 3 ) + fprintf( pFile, " ah" ); + else if ( pObj->LatchId.regType == 4 ) + fprintf( pFile, " al" ); + else if ( pObj->LatchId.regType == 5 ) + fprintf( pFile, " as" ); + else + assert( 0 ); + } + else if ( pObj->LatchId.regClass ) + fprintf( pFile, " %d", pObj->LatchId.regClass ); + if ( pObj->pClock ) + fprintf( pFile, " %s", pObj->pClock->pName ); + fprintf( pFile, " %d", pObj->LatchId.regInit ); fprintf( pFile, "\n" ); } else if ( Ntl_ObjIsBox(pObj) ) @@ -136,8 +167,6 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, "\n" ); } } - if ( fClockAdded ) - fprintf( pFile, ".names clock99\n 0\n" ); fprintf( pFile, ".end\n\n" ); } @@ -167,7 +196,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ) fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() ); // write the models Ntl_ManForEachModel( p, pModel, i ) - Ioa_WriteBlifModel( pFile, pModel ); + Ioa_WriteBlifModel( pFile, pModel, i==0 ); // close the file fclose( pFile ); } diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 50d6db49..6639db21 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -3,6 +3,7 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInter.c \ src/aig/saig/saigIoa.c \ + src/aig/saig/saigMiter.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ src/aig/saig/saigRetMin.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 67f38758..f3bd028a 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -86,6 +86,8 @@ extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigInter.c ==========================================================*/ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); +/*=== saigMiter.c ==========================================================*/ +extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 32b2d186..f03364a4 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -277,6 +277,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim free( pModel ); Vec_IntFree( vCiIds ); +// if ( piFrame ) +// *piFrame = i / Saig_ManPoNum(pAig); RetValue = 0; break; } diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c new file mode 100644 index 00000000..fc721154 --- /dev/null +++ b/src/aig/saig/saigMiter.c @@ -0,0 +1,95 @@ +/**CFile**************************************************************** + + FileName [saigMiter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Computes sequential miter of two sequential AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Saig_ManRegNum(p1) > 0 || Saig_ManRegNum(p2) > 0 ); + assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) ); + assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) ); + // map constant nodes + Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew); + // map primary inputs + Saig_ManForEachPi( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Saig_ManForEachPi( p2, pObj, i ) + pObj->pData = Aig_ManPi( pNew, i ); + // map register outputs + Saig_ManForEachLo( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Saig_ManForEachLo( p2, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // map internal nodes + Aig_ManForEachNode( p1, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_ManForEachNode( p2, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create primary outputs + Saig_ManForEachPo( p1, pObj, i ) + { + if ( Oper == 0 ) // XOR + pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) ); + else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2) ... complement is PO(p1) & !PO(p2) + pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) ); + else + assert( 0 ); + } + // create register inputs + Saig_ManForEachLi( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachLi( p2, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // cleanup + Aig_ManSetRegNum( pNew, Saig_ManRegNum(p1) + Saig_ManRegNum(p2) ); + Aig_ManCleanup( pNew ); + return pNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c index b747eff9..67e3e95b 100644 --- a/src/aig/saig/saigScl.c +++ b/src/aig/saig/saigScl.c @@ -67,6 +67,42 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ) printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) ); } + +/**Function************************************************************* + + Synopsis [Report the number of pairs of complemented registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManReportComplements( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFanin; + int i, Counter = 0, Diffs = 0; + assert( Aig_ManRegNum(p) > 0 ); + Aig_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( pFanin->fMarkA ) + Counter++; + else + pFanin->fMarkA = 1; + } + // count fanins that have both attributes + Aig_ManForEachLiSeq( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + pFanin->fMarkA = 0; + } + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index 51970425..9d5c8f7f 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -554,6 +554,8 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) ); memset( pBox, 0, sizeof(Tim_Box_t) ); pBox->iBox = Vec_PtrSize( p->vBoxes ); +//printf( "Creating box %d: First in = %d. (%d) First out = %d. (%d)\n", pBox->iBox, +// firstIn, nIns, firstOut, nOuts ); Vec_PtrPush( p->vBoxes, pBox ); pBox->pDelayTable = pDelayTable; pBox->nInputs = nIns; @@ -704,6 +706,25 @@ void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay ) SeeAlso [] ***********************************************************************/ +void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay ) +{ + Tim_Obj_t * pObj; + int i; + Tim_ManForEachCi( p, pObj, i ) + Tim_ManInitCiArrival( p, i, Delay ); +} + +/**Function************************************************************* + + Synopsis [Sets the correct required times for all POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay ) { Tim_Obj_t * pObj; diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h index 3b9707e0..7c6e33f1 100644 --- a/src/aig/tim/tim.h +++ b/src/aig/tim/tim.h @@ -81,6 +81,7 @@ extern void Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Dela extern void Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay ); extern void Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay ); extern void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay ); +extern void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay ); extern void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay ); extern float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi ); extern float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d9defa1b..450a245f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9298,7 +9298,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Prove_Params_t Params, * pParams = &Params; FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkTemp; - int c, clk, RetValue; + int c, clk, RetValue, iOut = -1; extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ); @@ -9351,8 +9351,16 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) // verify that the pattern is correct if ( RetValue == 0 ) { + Abc_Obj_t * pObj; + int i; int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel ); - if ( pSimInfo[0] != 1 ) + Abc_NtkForEachCo( pNtk, pObj, i ) + if ( pSimInfo[i] == 1 ) + { + iOut = i; + break; + } + if ( i == Abc_NtkCoNum(pNtk) ) printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); free( pSimInfo ); } @@ -9360,7 +9368,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( RetValue == -1 ) printf( "UNDECIDED " ); else if ( RetValue == 0 ) - printf( "SATISFIABLE " ); + printf( "SATISFIABLE (output = %d) ", iOut ); else printf( "UNSATISFIABLE " ); //printf( "\n" ); @@ -15634,6 +15642,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) int fMapped; int fTest; extern void * Ioa_ReadBlif( char * pFileName, int fCheck ); + extern void Ioa_WriteBlif( void * p, char * pFileName ); extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); @@ -15678,6 +15687,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pTemp ) { Ntl_ManPrintStats( pTemp ); +// Ioa_WriteBlif( pTemp, "test_boxes.blif" ); Ntl_ManFree( pTemp ); } return 0; @@ -17888,6 +17898,8 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + printf( "Currently *cec works only for two designs given on command line.\n" ); +/* // derive AIGs pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 ); pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk ); @@ -17903,6 +17915,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose ); Aig_ManStop( pAig1 ); Aig_ManStop( pAig2 ); +*/ return 0; usage: diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c index 3f6b81a4..84c75b7b 100644 --- a/src/base/main/mainMC.c +++ b/src/base/main/mainMC.c @@ -45,29 +45,36 @@ ***********************************************************************/ int main( int argc, char * argv[] ) { + int fEnableBmcOnly = 0; // enable to make it BMC-only + + int fEnableCounter = 1; // should be 1 in the final version + int fEnableComment = 0; // should be 0 in the final version + Fra_Sec_t SecPar, * pSecPar = &SecPar; FILE * pFile; Aig_Man_t * pAig; - int RetValue; + int RetValue = -1; + int Depth = -1; // BMC parameters - int nFrames = 30; - int nSizeMax = 200000; + int nFrames = 50; + int nSizeMax = 500000; int nBTLimit = 10000; int fRewrite = 0; int fNewAlgo = 1; int fVerbose = 0; + int clkTotal = clock(); if ( argc != 2 ) { printf( " Expecting one command-line argument (an input file in AIGER format).\n" ); - printf( " usage: %s <file.aig>", argv[0] ); + printf( " usage: %s <file.aig>\n", argv[0] ); return 0; } pFile = fopen( argv[1], "r" ); if ( pFile == NULL ) { printf( " Cannot open input AIGER file \"%s\".\n", argv[1] ); - printf( " usage: %s <file.aig>", argv[0] ); + printf( " usage: %s <file.aig>\n", argv[0] ); return 0; } fclose( pFile ); @@ -75,33 +82,47 @@ int main( int argc, char * argv[] ) if ( pAig == NULL ) { printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] ); - printf( " usage: %s <file.aig>", argv[0] ); + printf( " usage: %s <file.aig>\n", argv[0] ); return 0; } - // perform BMC Aig_ManSetRegNum( pAig, pAig->nRegs ); - RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL ); - - // perform full-blown SEC - if ( RetValue != 0 ) + if ( !fEnableBmcOnly ) { - extern void Dar_LibStart(); - extern void Dar_LibStop(); - extern void Cnf_ClearMemory(); - - Fra_SecSetDefaultParams( pSecPar ); - pSecPar->nFramesMax = 2; // the max number of frames used for induction - - Dar_LibStart(); - RetValue = Fra_FraigSec( pAig, pSecPar ); - Dar_LibStop(); - Cnf_ClearMemory(); + // perform BMC + if ( pAig->nRegs != 0 ) + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL ); + + // perform full-blown SEC + if ( RetValue != 0 ) + { + extern void Dar_LibStart(); + extern void Dar_LibStop(); + extern void Cnf_ClearMemory(); + + Fra_SecSetDefaultParams( pSecPar ); + pSecPar->TimeLimit = 600; + pSecPar->nFramesMax = 4; // the max number of frames used for induction + pSecPar->fPhaseAbstract = 0; // disable phase-abstraction + pSecPar->fSilent = 1; // disable phase-abstraction + + Dar_LibStart(); + RetValue = Fra_FraigSec( pAig, pSecPar ); + Dar_LibStop(); + Cnf_ClearMemory(); + } } // perform BMC again - if ( RetValue == -1 ) + if ( RetValue == -1 && pAig->nRegs != 0 ) { + int nFrames = 200; + int nSizeMax = 500000; + int nBTLimit = 10000000; + int fRewrite = 0; + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth ); + if ( RetValue != 0 ) + RetValue = -1; } // decide how to report the output @@ -111,7 +132,20 @@ int main( int argc, char * argv[] ) if ( RetValue == 0 ) { // fprintf(stdout, "s SATIFIABLE\n"); + fprintf( pFile, "1" ); + if ( fEnableCounter ) + { + printf( "\n" ); + if ( pAig->pSeqModel ) Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel ); + } + + if ( fEnableComment ) + { + printf( " # File %10s. ", argv[1] ); + PRT( "Time", clock() - clkTotal ); + } + if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); @@ -120,7 +154,15 @@ int main( int argc, char * argv[] ) else if ( RetValue == 1 ) { // fprintf(stdout, "s UNSATISFIABLE\n"); - fprintf( pFile, "0\n" ); + fprintf( pFile, "0" ); + + if ( fEnableComment ) + { + printf( " # File %10s. ", argv[1] ); + PRT( "Time", clock() - clkTotal ); + } + printf( "\n" ); + if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); @@ -129,6 +171,15 @@ int main( int argc, char * argv[] ) else // if ( RetValue == -1 ) { // fprintf(stdout, "s UNKNOWN\n"); + fprintf( pFile, "2" ); + + if ( fEnableComment ) + { + printf( " # File %10s. ", argv[1] ); + PRT( "Time", clock() - clkTotal ); + } + printf( "\n" ); + if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c index 21a37070..eb89b3e3 100644 --- a/src/bdd/parse/parseCore.c +++ b/src/bdd/parse/parseCore.c @@ -58,7 +58,9 @@ #define PARSE_SYM_XOR1 '<' // logic EXOR (the 1st symbol) #define PARSE_SYM_XOR2 '+' // logic EXOR (the 2nd symbol) #define PARSE_SYM_XOR3 '>' // logic EXOR (the 3rd symbol) -#define PARSE_SYM_OR '+' // logic OR +#define PARSE_SYM_XOR '^' // logic XOR +#define PARSE_SYM_OR1 '+' // logic OR +#define PARSE_SYM_OR2 '|' // logic OR #define PARSE_SYM_EQU1 '<' // equvalence (the 1st symbol) #define PARSE_SYM_EQU2 '=' // equvalence (the 2nd symbol) #define PARSE_SYM_EQU3 '>' // equvalence (the 3rd symbol) @@ -220,7 +222,9 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in case PARSE_SYM_AND1: case PARSE_SYM_AND2: - case PARSE_SYM_OR: + case PARSE_SYM_OR1: + case PARSE_SYM_OR2: + case PARSE_SYM_XOR: if ( Flag != PARSE_FLAG_VAR ) { fprintf( pOutput, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR.\n" ); @@ -229,8 +233,10 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in } if ( *pTemp == PARSE_SYM_AND1 || *pTemp == PARSE_SYM_AND2 ) Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); - else //if ( Str[Pos] == PARSE_SYM_OR ) + else if ( *pTemp == PARSE_SYM_OR1 || *pTemp == PARSE_SYM_OR2 ) Parse_StackOpPush( pStackOp, PARSE_OPER_OR ); + else //if ( Str[Pos] == PARSE_SYM_XOR ) + Parse_StackOpPush( pStackOp, PARSE_OPER_XOR ); Flag = PARSE_FLAG_OPER; break; diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 7e529ef6..75370dff 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -296,6 +296,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr } else if ( If_ObjIsCi(pObj) ) { +//printf( "processing CI %d\n", pObj->Id ); arrTime = Tim_ManGetCiArrival( p->pManTim, pObj->IdPio ); If_ObjSetArrTime( pObj, arrTime ); } diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c index 21a078f9..1fca5764 100644 --- a/src/map/mio/mioFunc.c +++ b/src/map/mio/mioFunc.c @@ -25,7 +25,9 @@ // these symbols (and no other) can appear in the formulas #define MIO_SYMB_AND '*' -#define MIO_SYMB_OR '+' +#define MIO_SYMB_OR1 '+' +#define MIO_SYMB_OR2 '|' +#define MIO_SYMB_XOR '^' #define MIO_SYMB_NOT '!' #define MIO_SYMB_AFTNOT '\'' #define MIO_SYMB_OPEN '(' @@ -239,8 +241,9 @@ int Mio_GateCollectNames( char * pFormula, char * pPinNames[] ) // remove the non-name symbols for ( pTemp = Buffer; *pTemp; pTemp++ ) - if ( *pTemp == MIO_SYMB_AND || *pTemp == MIO_SYMB_OR || *pTemp == MIO_SYMB_NOT - || *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT ) + if ( *pTemp == MIO_SYMB_AND || *pTemp == MIO_SYMB_OR1 || *pTemp == MIO_SYMB_OR2 + || *pTemp == MIO_SYMB_XOR || *pTemp == MIO_SYMB_NOT || *pTemp == MIO_SYMB_OPEN + || *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT ) *pTemp = ' '; // save the names diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c index 13c2cdcd..dc665050 100644 --- a/src/map/mio/mioRead.c +++ b/src/map/mio/mioRead.c @@ -265,7 +265,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, bool fExtendedFormat ) // then rest of the expression pToken = strtok( NULL, ";" ); - pGate->pForm = Extra_UtilStrsav( pToken ); + pGate->pForm = chomp( pToken ); // read the pin info // start the linked list of pins @@ -392,21 +392,27 @@ Mio_Pin_t * Mio_LibraryReadPin( char ** ppToken, bool fExtendedFormat ) SeeAlso [] ***********************************************************************/ -char *chomp( char *s ) +char * chomp( char *s ) { - char *b = ALLOC(char, strlen(s)+1), *c = b; - while (*s && isspace(*s)) - ++s; - while (*s && !isspace(*s)) - *c++ = *s++; - *c = 0; - return b; + char *a, *b, *c; + // remove leading spaces + for ( b = s; *b; b++ ) + if ( !isspace(*b) ) + break; + // strsav the string + a = strcpy( ALLOC(char, strlen(b)+1), b ); + // remove trailing spaces + for ( c = a+strlen(a); c > a; c-- ) + if ( *c == 0 || isspace(*c) ) + *c = 0; + else + break; + return a; } /**Function************************************************************* - Synopsis [Duplicates string and returns it with leading and - trailing spaces removed.] + Synopsis [] Description [] |