From df6fdd1dffd8ce83dfc4a7868ebdd25241f8f24b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 8 Apr 2009 08:01:00 -0700 Subject: Version abc90408 --- src/base/abc/abcAig.c | 2 +- src/base/abc/abcLatch.c | 110 ++++++++++++++++++++++++++++++++ src/base/abc/abcNtk.c | 18 +++--- src/base/abc/abcObj.c | 4 +- src/base/abc/abcUtil.c | 2 +- src/base/abci/abc.c | 152 ++++++++++++++++++++++++++++++++++++++------- src/base/abci/abcBmc.c | 2 +- src/base/abci/abcDar.c | 17 +++-- src/base/abci/abcFxu.c | 4 +- src/base/abci/abcHaig.c | 2 +- src/base/abci/abcMv.c | 2 +- src/base/abci/abcPrint.c | 2 +- src/base/abci/abcReach.c | 2 +- src/base/abci/abcSat.c | 2 +- src/base/abci/abcSweep.c | 2 +- src/base/abci/abcUnreach.c | 2 +- src/base/abci/abcVerify.c | 2 +- src/base/io/io.c | 2 +- src/base/io/ioReadAiger.c | 2 +- src/base/io/ioReadBlifMv.c | 2 +- src/base/io/ioWriteCnf.c | 2 +- src/base/ver/verCore.c | 8 +-- 22 files changed, 283 insertions(+), 60 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 289c422d..a3188901 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -163,7 +163,7 @@ void Abc_AigFree( Abc_Aig_t * pMan ) { assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 ); assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 ); - // ABC_FREE the table + // free the table if ( pMan->vAddedCells ) Vec_PtrFree( pMan->vAddedCells ); if ( pMan->vUpdatedNets ) diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index aef44b11..d870a610 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -371,6 +371,116 @@ printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) ); } +/**Function************************************************************* + + Synopsis [Converts registers with DC values into additional PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin, * pObjNew, * pObjLiNew, * pObjLoNew; + int i, k, nFlops, nStates, iState, pfCompl[32]; + assert( Abc_NtkIsLogic(pNtk) ); + nFlops = Abc_NtkLatchNum(pNtk); + if ( nFlops == 0 ) + return Abc_NtkDup( pNtk ); + if ( nFlops > 16 ) + { + printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops ); + return NULL; + } + // check if there are latches with DC values + iState = 0; + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + if ( Abc_LatchIsInitDc(pObj) ) + { + printf( "Cannot process logic network with don't-care init values. Run \"zero\".\n" ); + return NULL; + } + if ( Abc_LatchIsInit1(pObj) ) + iState |= (1 << i); + } + // transfer logic to SOPs + Abc_NtkToSop( pNtk, 0 ); + // create new network + pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc ); + nStates = (1 << nFlops); + for ( i = 0; i < nStates; i++ ) + { + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pObjLiNew = Abc_NtkCreateBi( pNtkNew ); + pObjLoNew = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pObjLiNew ); + Abc_ObjAddFanin( pObjLoNew, pObjNew ); + if ( i == iState ) + Abc_LatchSetInit1( pObjNew ); + else + Abc_LatchSetInit0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + assert( Abc_NtkLatchNum(pNtkNew) == nStates ); + assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) ); + assert( Abc_NtkPoNum(pNtkNew) == Abc_NtkPoNum(pNtk) ); + assert( Abc_NtkCiNum(pNtkNew) == Abc_NtkPiNum(pNtkNew) + nStates ); + assert( Abc_NtkCoNum(pNtkNew) == Abc_NtkPoNum(pNtkNew) + nStates ); + assert( Abc_NtkCiNum(pNtk) == Abc_NtkPiNum(pNtk) + nFlops ); + assert( Abc_NtkCoNum(pNtk) == Abc_NtkPoNum(pNtk) + nFlops ); + // create hot-to-log transformers + for ( i = 0; i < nFlops; i++ ) + { + pObjNew = Abc_NtkCreateNode( pNtkNew ); + for ( k = 0; k < nStates; k++ ) + if ( (k >> i) & 1 ) + Abc_ObjAddFanin( pObjNew, Abc_NtkCi(pNtkNew, Abc_NtkPiNum(pNtkNew)+k) ); + assert( Abc_ObjFaninNum(pObjNew) == nStates/2 ); + pObjNew->pData = Abc_SopCreateOr( pNtkNew->pManFunc, nStates/2, NULL ); + // save the new flop + pObj = Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ); + pObj->pCopy = pObjNew; + } + // duplicate the nodes + vNodes = Abc_NtkDfs( pNtk, 0 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObj->pCopy = Abc_NtkDupObj( pNtkNew, pObj, 1 ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + } + Vec_PtrFree( vNodes ); + // connect the POs + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj)) ); + // write entries into the nodes + Abc_NtkForEachCo( pNtk, pObj, i ) + pObj->pCopy = Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj)); + // create log-to-hot transformers + for ( k = 0; k < nStates; k++ ) + { + pObjNew = Abc_NtkCreateNode( pNtkNew ); + for ( i = 0; i < nFlops; i++ ) + { + pObj = Abc_NtkCo( pNtk, Abc_NtkPoNum(pNtk) + i ); + Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(pObj->pCopy) ); + pfCompl[i] = Abc_ObjIsComplement(pObj->pCopy) ^ !((k >> i) & 1); + } + pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFlops, pfCompl ); + // connect it to the flop input + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, Abc_NtkPoNum(pNtkNew)+k), pObjNew ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkConvertOnehot(): Network check has failed.\n" ); + return pNtkNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 639319d1..d6ab7ea1 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -935,10 +935,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // int LargePiece = (4 << ABC_NUM_STEPS); if ( pNtk == NULL ) return; - // ABC_FREE the HAIG + // free the HAIG // if ( pNtk->pHaig ) // Abc_NtkHaigStop( pNtk ); - // ABC_FREE EXDC Ntk + // free EXDC Ntk if ( pNtk->pExdc ) Abc_NtkDelete( pNtk->pExdc ); if ( pNtk->pExcare ) @@ -952,7 +952,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // make sure all the marks are clean Abc_NtkForEachObj( pNtk, pObj, i ) { - // ABC_FREE large fanout arrays + // free large fanout arrays // if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece ) // ABC_FREE( pObj->vFanouts.pArray ); // these flags should be always zero @@ -961,7 +961,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) assert( pObj->fMarkB == 0 ); assert( pObj->fMarkC == 0 ); } - // ABC_FREE the nodes + // free the nodes if ( pNtk->pMmStep == NULL ) { Abc_NtkForEachObj( pNtk, pObj, i ) @@ -976,7 +976,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) ABC_FREE( pObj ); } - // ABC_FREE the arrays + // free the arrays Vec_PtrFree( pNtk->vPios ); Vec_PtrFree( pNtk->vPis ); Vec_PtrFree( pNtk->vPos ); @@ -992,14 +992,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0; TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0; // fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) ); - // ABC_FREE the storage + // free the storage if ( pNtk->pMmObj ) Extra_MmFixedStop( pNtk->pMmObj ); if ( pNtk->pMmStep ) Extra_MmStepStop ( pNtk->pMmStep ); // name manager Nm_ManFree( pNtk->pManName ); - // ABC_FREE the timing manager + // free the timing manager if ( pNtk->pManTime ) Abc_ManTimeStop( pNtk->pManTime ); // start the functionality manager @@ -1015,7 +1015,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) pNtk->pManFunc = NULL; else if ( !Abc_NtkHasBlackbox(pNtk) ) assert( 0 ); - // ABC_FREE the hierarchy + // free the hierarchy if ( pNtk->pDesign ) { Abc_LibFree( pNtk->pDesign, pNtk ); @@ -1023,7 +1023,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) } // if ( pNtk->pBlackBoxes ) // Vec_IntFree( pNtk->pBlackBoxes ); - // ABC_FREE node attributes + // free node attributes Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i ) if ( pAttrMan ) { diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 4b18aa36..e4484ec5 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -71,9 +71,9 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj ) { Abc_Ntk_t * pNtk = pObj->pNtk; // int LargePiece = (4 << ABC_NUM_STEPS); - // ABC_FREE large fanout arrays + // free large fanout arrays // if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece ) -// ABC_FREE( pObj->vFanouts.pArray ); +// free( pObj->vFanouts.pArray ); if ( pNtk->pMmStep == NULL ) { ABC_FREE( pObj->vFanouts.pArray ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index cdb9b465..8ebb00a3 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1770,7 +1770,7 @@ void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ) printf( "%4d CO %5d : Supp = %5d. Lev = %3d. Cone = %5d. Rev = %5d. COs = %3d (%3d).\n", Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew ); - // ABC_FREE arrays + // free arrays Vec_PtrFree( vSupp ); Vec_PtrFree( vNodes ); Vec_PtrFree( vReverse ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ef7969be..c48b7e95 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27,7 +27,7 @@ #include "if.h" #include "res.h" #include "lpk.h" -#include "aig.h" +#include "giaAig.h" #include "dar.h" #include "mfs.h" #include "mfx.h" @@ -39,7 +39,6 @@ #include "ssw.h" #include "cgt.h" #include "amap.h" -#include "gia.h" #include "cec.h" //////////////////////////////////////////////////////////////////////// @@ -194,6 +193,7 @@ static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 ); @@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 ); - Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 ); + Cmd_CommandAdd( pAbc, "AIG", "&st", Abc_CommandAbc9Hash, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&topand", Abc_CommandAbc9Topand, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&cof", Abc_CommandAbc9Cof, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 ); @@ -11945,7 +11946,7 @@ usage: fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon ); fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" ); fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" ); - fprintf( pErr, "\t-i : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" ); + fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" ); fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: undc [-h]\n" ); - fprintf( pErr, "\t converts latches with DC init values into ABC_FREE PIs\n" ); + fprintf( pErr, "\t converts latches with DC init values into free PIs\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The current network is combinational.\n" ); + return 0; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "This command works only for logic networks.\n" ); + return 0; + } + // get the new network + pNtkRes = Abc_NtkConvertOnehot( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting to one-hot encoding has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: onehot [-h]\n" ); + fprintf( pErr, "\t converts natural encoding into one-hot encoding\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fNew = 1; + fNew = 0; fComb = 0; nFrames = 32; nWords = 8; @@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConfMax; int fDynamic; int fExtend; + int fSkipProof; + int nFramesBmc; + int nConfMaxBmc; int fVerbose; int c; - extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesMax = 10; - nConfMax = 10000; - fDynamic = 1; - fExtend = 0; - fVerbose = 0; + nFramesMax = 10; + nConfMax = 10000; + fDynamic = 1; + fExtend = 0; + fSkipProof = 0; + nFramesBmc = 2000; + nConfMaxBmc = 5000; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF ) { switch ( c ) { @@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfMax < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + nFramesBmc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFramesBmc < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nConfMaxBmc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfMaxBmc < 0 ) + goto usage; + break; case 'd': fDynamic ^= 1; break; case 'e': fExtend ^= 1; break; + case 's': + fSkipProof ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose ); + pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pNtkRes == NULL ) { if ( pNtk->pSeqModel == NULL ) @@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: abs [-FC num] [-devh]\n" ); - fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" ); - fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); - fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); + fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" ); + fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" ); + fprintf( pErr, "\t followed by counter-example-based abstraction\n" ); + fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax ); + fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax ); + fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc ); + fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc ); fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" ); fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" ); + fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; int c; + int fAddStrash = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { + case 'a': + fAddStrash ^= 1; + break; case 'h': goto usage; default: @@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" ); return 1; } - pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig ); + pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash ); Gia_ManStop( pTemp ); return 0; usage: - fprintf( stdout, "usage: &hash [-h]\n" ); + fprintf( stdout, "usage: &st [-ah]\n" ); fprintf( stdout, "\t performs structural hashing\n" ); + fprintf( stdout, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; } @@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pAig == NULL ) { - printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" ); + printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pAig) > 0 ) diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c index d2c5a12c..1512c76f 100644 --- a/src/base/abci/abcBmc.c +++ b/src/base/abci/abcBmc.c @@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) ); // report the classes // if ( fVerbose ) // Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames ); - // ABC_FREE stuff + // free stuff Vec_PtrFree( vMapping ); Ivy_ManStop( pFraig ); Ivy_ManStop( pFrames ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 91046340..840068d6 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "aig.h" +#include "giaAig.h" #include "saig.h" #include "dar.h" #include "cnf.h" @@ -2299,7 +2299,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pCex; RetValue = 1; - } + } else { RetValue = 0; @@ -2375,7 +2375,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in pGia = Gia_ManFromAig( pMan ); if ( Gia_ManSimSimulate( pGia, pPars ) ) { - if ( (pCex = pMan->pSeqModel) ) + if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) ) { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); @@ -2404,8 +2404,13 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { pCex = Fra_SmlGetCounterExample( pSml ); if ( pCex ) + { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); + status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex ); + if ( status == 0 ) + printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); + } ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pCex; @@ -2557,7 +2562,7 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; @@ -2567,7 +2572,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf return NULL; Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pTemp->pSeqModel ) { ABC_FREE( pNtk->pModel ); @@ -3380,7 +3385,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) return NULL; /* Aig_ManSetRegNum( pMan, pMan->nRegs ); - pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 ); + pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 ); Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index 1596e774..6109870e 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -177,12 +177,12 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) void Abc_NtkFxuFreeInfo( Fxu_Data_t * p ) { int i; - // ABC_FREE the arrays of new fanins + // free the arrays of new fanins if ( p->vFaninsNew ) for ( i = 0; i < p->vFaninsNew->nSize; i++ ) if ( p->vFaninsNew->pArray[i] ) Vec_IntFree( p->vFaninsNew->pArray[i] ); - // ABC_FREE the arrays + // free the arrays if ( p->vSops ) Vec_PtrFree( p->vSops ); if ( p->vSopsNew ) Vec_PtrFree( p->vSopsNew ); if ( p->vFanins ) Vec_PtrFree( p->vFanins ); diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c index 569275f2..3f3fefcd 100644 --- a/src/base/abci/abcHaig.c +++ b/src/base/abci/abcHaig.c @@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk ) pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan ); Hop_ManStop( pMan ); - // ABC_FREE HAIG + // free HAIG return pNtkAig; } diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c index dacd16b2..8ea3697f 100644 --- a/src/base/abci/abcMv.c +++ b/src/base/abci/abcMv.c @@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p ) printf( "%d ", Vec_PtrSize(vCofs) ); Vec_PtrFree( vCofs ); - // ABC_FREE the cofactors + // free the cofactors for ( v1 = 0; v1 < 4; v1++ ) for ( v2 = 0; v2 < 4; v2++ ) Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e65ce11a..d47dfe1f 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -64,7 +64,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) int nPis; // the number of primary inputs int nPos; // the number of primary outputs } ParsNew, ParsBest = { 0 }; - // ABC_FREE storage for the name + // free storage for the name if ( pNtk == NULL ) { ABC_FREE( ParsBest.pName ); diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c index 3834c00d..e25be81a 100644 --- a/src/base/abci/abcReach.c +++ b/src/base/abci/abcReach.c @@ -102,7 +102,7 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i ); pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] ); } - // ABC_FREE the global BDDs + // free the global BDDs Abc_NtkFreeGlobalBdds( pNtk, 0 ); // reorder and disable reordering diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 3cee19ca..5e14116c 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); Vec_IntFree( vCiIds ); } - // ABC_FREE the sat_solver + // free the sat_solver if ( fVerbose ) Sat_SolverPrintStats( stdout, pSat ); diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index d1f4d4f7..dfb8137c 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -111,7 +111,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose ); stmm_free_table( tEquiv ); - // ABC_FREE the manager + // free the manager Fraig_ManFree( pMan ); Abc_NtkDelete( pNtkAig ); diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 196ff643..251d3953 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -143,7 +143,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } - // ABC_FREE the global BDDs + // free the global BDDs // Abc_NtkFreeGlobalBdds( pNtk ); Abc_NtkFreeGlobalBdds( pNtk, 0 ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 60197d29..424c26ec 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -799,7 +799,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo ) for ( k = 0; k <= iFrame; k++ ) if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy ) pObj->pCopy = (void *)1; - // ABC_FREE stuff + // free stuff Vec_PtrFree( vSupp ); Abc_NtkDelete( pFrames ); } diff --git a/src/base/io/io.c b/src/base/io/io.c index 20f412e0..46d61583 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1140,7 +1140,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } printf( "The library contains %d gates.\n", st_count(pLibrary->tModules) ); - // ABC_FREE old library + // free old library if ( Abc_FrameReadLibVer() ) Abc_LibFree( Abc_FrameReadLibVer(), NULL ); // read new library diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index c26e4cd5..85475204 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -327,7 +327,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) i++; } else // modified AIGER - { + { vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); } diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 34ea4294..eea601a8 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -160,7 +160,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) pDesignName = Extra_FileNameGeneric( pFileName ); p->pDesign = Abc_LibCreate( pDesignName ); ABC_FREE( pDesignName ); - // ABC_FREE the HOP manager + // free the HOP manager Hop_ManStop( p->pDesign->pManFunc ); p->pDesign->pManFunc = NULL; // prepare the file for parsing diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 7d03e545..3df189d1 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -78,7 +78,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) s_pNtk = pNtk; Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); s_pNtk = NULL; - // ABC_FREE the solver + // free the solver sat_solver_delete( pSat ); return 1; } diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index c318545b..42d6349a 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -274,7 +274,7 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) else // print the error message with the line number fprintf( p->Output, "%s (line %d): %s\n", p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError ); - // ABC_FREE the data + // free the data Ver_ParseFreeData( p ); } @@ -2104,7 +2104,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) i--; } - // ABC_FREE the bundling + // free the bundling Vec_PtrForEachEntry( vBundles, pBundle, k ) Ver_ParseFreeBundle( pBundle ); Vec_PtrFree( vBundles ); @@ -2227,7 +2227,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) i--; } - // ABC_FREE the bundling + // free the bundling Vec_PtrForEachEntry( vBundles, pBundle, k ) Ver_ParseFreeBundle( pBundle ); Vec_PtrFree( vBundles ); @@ -2626,7 +2626,7 @@ int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs ) Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL ); } - // ABC_FREE the bundles + // free the bundles Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy ); pBox->pCopy = NULL; } -- cgit v1.2.3