From 9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 May 2008 08:01:00 -0700 Subject: Version abc80527 --- src/aig/fra/fra.h | 3 +- src/aig/fra/fraSim.c | 147 +++++++++++++++++++++++++++++++++------------ src/aig/ntl/ntlCheck.c | 3 + src/aig/ntl/ntlReadBlif.c | 38 ++++++++++-- src/aig/saig/saig.h | 1 + src/aig/saig/saigBmc.c | 6 +- src/aig/saig/saigHaig.c | 115 ++++++++++++++++++----------------- src/aig/saig/saigRetStep.c | 8 +++ src/base/abc/abcNtk.c | 2 +- src/base/abci/abc.c | 44 ++++++++++++-- src/base/main/mainMC.c | 147 +++++++++++++++++++++++++++++++++++++++++++++ 11 files changed, 408 insertions(+), 106 deletions(-) create mode 100644 src/base/main/mainMC.c diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7cb846fa..7549dfca 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -370,8 +370,9 @@ extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p ); -extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ); extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); +extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ); +extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ); #ifdef __cplusplus } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index a8de5e37..00a35fcd 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -844,44 +844,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW return p; } -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ) -{ - Fra_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Aig_ManForEachLoSeq( pAig, pObj, i ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - // assign simulation info for the primary inputs - for ( i = 0; i <= p->iFrame; i++ ) - Aig_ManForEachPiSeq( pAig, pObj, k ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Fra_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - Fra_SmlStop( pSml ); - return RetValue; -} - - /**Function************************************************************* Synopsis [Allocates a counter-example.] @@ -1082,6 +1044,115 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) return pCex; } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ) +{ + Fra_Sml_t * pSml; + Aig_Obj_t * pObj; + int RetValue, i, k, iBit; + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); + // start a new sequential simulator + pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); + // assign simulation info for the registers + iBit = 0; + Aig_ManForEachLoSeq( pAig, pObj, i ) + Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + // assign simulation info for the primary inputs + for ( i = 0; i <= p->iFrame; i++ ) + Aig_ManForEachPiSeq( pAig, pObj, k ) + Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + assert( iBit == p->nBits ); + // run random simulation + Fra_SmlSimulateOne( pSml ); + // check if the given output has failed + RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); + Fra_SmlStop( pSml ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p ) +{ + Fra_Sml_t * pSml; + Aig_Obj_t * pObj; + int RetValue, i, k, iBit; + unsigned * pSims; + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); + // start a new sequential simulator + pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); + // assign simulation info for the registers + iBit = 0; + Aig_ManForEachLoSeq( pAig, pObj, i ) +// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + Fra_SmlAssignConst( pSml, pObj, 0, 0 ); + // assign simulation info for the primary inputs + iBit = p->nRegs; + for ( i = 0; i <= p->iFrame; i++ ) + Aig_ManForEachPiSeq( pAig, pObj, k ) + Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + assert( iBit == p->nBits ); + // run random simulation + Fra_SmlSimulateOne( pSml ); + // check if the given output has failed + 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 ) + { + pSims = Fra_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } + fprintf( pFile, " " ); + Aig_ManForEachLiSeq( pAig, pObj, k ) + { + pSims = Fra_ObjSim(pSml, pObj->Id); + fprintf( pFile, "%d", (int)(pSims[i] != 0) ); + } + fprintf( pFile, "\n" ); + } + + Fra_SmlStop( pSml ); + return RetValue; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index c5c62433..d5100312 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -123,8 +123,11 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) } // check models Ntl_ManForEachModel( pMan, pMod1, i ) + { if ( !Ntl_ModelCheck( pMod1 ) ) fStatus = 0; + break; + } return fStatus; } diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 3574b61e..a291f8a0 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -534,6 +534,18 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) ); break; } + 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--; @@ -682,7 +694,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) char * pToken; Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry( vTokens, 0 ); - assert( !strcmp(pToken, "attrib") ); + 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) ); @@ -695,6 +708,7 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) 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; } +*/ return 1; } @@ -864,12 +878,28 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine ) sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName ); return 0; } - +/* + // temporary fix for splitting the .subckt line + if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ) + { + Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 ); + // get one additional token + pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 ); + for ( ; *pToken; pToken++ ); + for ( ; *pToken == 0; pToken++ ); + Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' ); +// assert( Vec_PtrSize( vTokens2 ) == 2 ); + Vec_PtrForEachEntry( vTokens2, pToken, i ) + Vec_PtrPush( vTokens, pToken ); + nEquals += Vec_PtrSize(vTokens2)/2; + Vec_PtrFree( vTokens2 ); + } +*/ // check if the number of tokens is correct if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ) { - sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).", - Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ); + sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).", + Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ); return 0; } diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 49d3f5ef..67f38758 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -89,6 +89,7 @@ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int /*=== 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 ==========================================================*/ +extern void Saig_ManMarkAutonomous( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ); /*=== saigRetMin.c ==========================================================*/ extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ); diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 2d5af2d3..32b2d186 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -191,7 +191,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else pFrames = Saig_ManFramesBmc( pAig, nFrames ); - *piFrame = nFrames; + if ( piFrame ) + *piFrame = nFrames; if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", @@ -281,7 +282,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else { - *piFrame = i / Saig_ManPoNum(pAig); + if ( piFrame ) + *piFrame = i / Saig_ManPoNum(pAig); RetValue = -1; break; } diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index 4250ca79..8a75ae1f 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig ) SeeAlso [] ***********************************************************************/ -int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) +int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth ) { int nBTLimit = 0; Aig_Man_t * pFrames, * pTemp; @@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n sat_solver * pSat; Aig_Obj_t * pObj1, * pObj2; int i, RetValue1, RetValue2, Counter, Lits[2], nOvers; - int clk = clock(); + int clk = clock(), clkVerif; nOvers = Aig_ManMapHaigNodes( pHaig ); @@ -226,57 +226,6 @@ clk = clock(); // pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); -/* - // print the statistic into a file - { - FILE * pTable; - Aig_Man_t * pTemp, * pHaig2; - - pHaig2 = pAig->pManHaig; - pAig->pManHaig = NULL; - pTemp = Aig_ManDupDfs( pAig ); - pAig->pManHaig = pHaig2; - - Aig_ManSeqCleanup( pTemp ); - - pTable = fopen( "stats.txt", "a+" ); - fprintf( pTable, "%s ", p->pName ); - fprintf( pTable, "%d ", Saig_ManPiNum(p) ); - fprintf( pTable, "%d ", Saig_ManPoNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(p) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(p) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - - pTable = fopen( "stats2.txt", "a+" ); - fprintf( pTable, "%s ", p->pSpec ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) ); - - fprintf( pTable, "%d ", pCnf->nVars ); - fprintf( pTable, "%d ", pCnf->nClauses ); - fprintf( pTable, "%d ", pCnf->nLiterals ); - - fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - Aig_ManStop( pTemp ); - } -*/ // pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); @@ -375,11 +324,66 @@ clk = clock(); } printf( " \r" ); PRT( "Solving ", clock() - clk ); +clkVerif = clock() - clk; if ( Counter ) printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 ); else printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 ); + // print the statistic into a file + { + FILE * pTable; + Aig_Man_t * pTemp, * pHaig2; + + pHaig2 = pAig->pManHaig; + pAig->pManHaig = NULL; + pTemp = Aig_ManDupDfs( pAig ); + pAig->pManHaig = pHaig2; + + Aig_ManSeqCleanup( pTemp ); + + pTable = fopen( "stats.txt", "a+" ); + fprintf( pTable, "%s ", p->pName ); + fprintf( pTable, "%d ", Saig_ManPiNum(p) ); + fprintf( pTable, "%d ", Saig_ManPoNum(p) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(p) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(p) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(p) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) ); + + fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) ); + fprintf( pTable, "\n" ); + fclose( pTable ); + + + pTable = fopen( "stats2.txt", "a+" ); + fprintf( pTable, "%s ", p->pName ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) ); + + fprintf( pTable, "%d ", pCnf->nVars ); + fprintf( pTable, "%d ", pCnf->nClauses ); + fprintf( pTable, "%d ", pCnf->nLiterals ); + + fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 ); + fprintf( pTable, "%d ", pFrames->nAsserts/2 ); + fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); + + fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) ); + fprintf( pTable, "\n" ); + fclose( pTable ); + + Aig_ManStop( pTemp ); + } + // clean up Aig_ManStop( pFrames ); Cnf_DataFree( pCnf ); @@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Aig_Man_t * pNew, * pTemp; Aig_Obj_t * pObj; - int i, k, nStepsReal, clk = clock(); + int i, k, nStepsReal, clk = clock(), clkSynth; Dar_ManDefaultRwrParams( pParsRwr ); clk = clock(); @@ -679,6 +683,7 @@ clk = clock(); } } PRT( "Synthesis time ", clock() - clk ); +clkSynth = clock() - clk; // use the haig for verification // Aig_ManAntiCleanup( pNew->pManHaig ); @@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk ); } else { - if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) ) + if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) ) printf( "Constructing SAT solver has failed.\n" ); } diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c index fe726702..e2502761 100644 --- a/src/aig/saig/saigRetStep.c +++ b/src/aig/saig/saigRetStep.c @@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug assert( Aig_ObjPioNum(pFanin0) > 0 ); assert( Aig_ObjPioNum(pFanin1) > 0 ); + // skip latch guns + if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) ) + return NULL; + // get the inputs of these registers pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); @@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug pObjLo->PioNum = Aig_ManPiNum(p) - 1; p->nRegs++; + // make sure the register is retimable. + Aig_ObjSetTravIdCurrent(p, pObjLo); + //printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", // pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl ); @@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs ) p->fCreatePios = 1; if ( fForward ) { + Saig_ManMarkAutonomous( p ); for ( s = 0; s < nSteps; s++ ) { Aig_ManForEachNode( p, pObj, i ) diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index b66c3f32..4d543547 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -522,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode int i, k; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); - assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode)) ); + assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && (Abc_AigNodeIsConst(pNode) || Abc_ObjIsCi(pNode))) ); // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 39fdb9fb..d9defa1b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -14291,9 +14291,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Fra_SecSetDefaultParams( pSecPar ); - pSecPar->TimeLimit = 600; + pSecPar->TimeLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfwvh" ) ) != EOF ) { switch ( c ) { @@ -14308,6 +14308,17 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pSecPar->nFramesMax < 0 ) goto usage; break; + case 'T': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->TimeLimit < 0 ) + goto usage; + break; case 'a': pSecPar->fPhaseAbstract ^= 1; break; @@ -14350,9 +14361,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dsec [-F num] [-armfwvh] \n" ); + fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] \n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); + fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); @@ -14459,6 +14471,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) // perform verification Abc_NtkDarProve( pNtk, pSecPar ); + + // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p ) + return 0; usage: @@ -15617,20 +15632,25 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) char * pFileName; int c; int fMapped; + int fTest; extern void * Ioa_ReadBlif( char * pFileName, int fCheck ); extern Aig_Man_t * Ntl_ManExtract( void * p ); extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); // set defaults fMapped = 0; + fTest = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF ) { switch ( c ) { case 'm': fMapped ^= 1; break; + case 't': + fTest ^= 1; + break; case 'h': goto usage; default: @@ -15650,6 +15670,19 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) } fclose( pFile ); + if ( fTest ) + { + extern void Ntl_ManFree( void * p ); + extern void Ntl_ManPrintStats( void * p ); + void * pTemp = Ioa_ReadBlif( pFileName, 1 ); + if ( pTemp ) + { + Ntl_ManPrintStats( pTemp ); + Ntl_ManFree( pTemp ); + } + return 0; + } + Abc_FrameClearDesign(); pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 ); if ( pAbc->pAbc8Ntl == NULL ) @@ -15672,9 +15705,10 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: *r [-mh]\n" ); + fprintf( stdout, "usage: *r [-mth]\n" ); fprintf( stdout, "\t reads the design with whiteboxes\n" ); fprintf( stdout, "\t-m : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" ); + fprintf( stdout, "\t-t : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c new file mode 100644 index 00000000..3f6b81a4 --- /dev/null +++ b/src/base/main/mainMC.c @@ -0,0 +1,147 @@ +/**CFile**************************************************************** + + FileName [mainMC.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The main package.] + + Synopsis [The main file for the model checker.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mainInt.h" +#include "aig.h" +#include "saig.h" +#include "fra.h" +#include "ioa.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [The main() procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int main( int argc, char * argv[] ) +{ + Fra_Sec_t SecPar, * pSecPar = &SecPar; + FILE * pFile; + Aig_Man_t * pAig; + int RetValue; + // BMC parameters + int nFrames = 30; + int nSizeMax = 200000; + int nBTLimit = 10000; + int fRewrite = 0; + int fNewAlgo = 1; + int fVerbose = 0; + + if ( argc != 2 ) + { + printf( " Expecting one command-line argument (an input file in AIGER format).\n" ); + printf( " usage: %s ", 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 ", argv[0] ); + return 0; + } + fclose( pFile ); + pAig = Ioa_ReadAiger( argv[1], 1 ); + if ( pAig == NULL ) + { + printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] ); + printf( " usage: %s ", 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 ) + { + 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 again + if ( RetValue == -1 ) + { + } + + // decide how to report the output + pFile = stdout; + + // report the result + if ( RetValue == 0 ) + { +// fprintf(stdout, "s SATIFIABLE\n"); + Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel ); + if ( pFile != stdout ) + fclose(pFile); + Aig_ManStop( pAig ); + exit(10); + } + else if ( RetValue == 1 ) + { +// fprintf(stdout, "s UNSATISFIABLE\n"); + fprintf( pFile, "0\n" ); + if ( pFile != stdout ) + fclose(pFile); + Aig_ManStop( pAig ); + exit(20); + } + else // if ( RetValue == -1 ) + { +// fprintf(stdout, "s UNKNOWN\n"); + if ( pFile != stdout ) + fclose(pFile); + Aig_ManStop( pAig ); + exit(0); + } + return 0; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3