diff --git a/.gitignore b/.gitignore index cbb424152..f0c5201c6 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,12 @@ ReleaseExt/ _/ _TEST/ +_sandwich/ +_scripts/ +*.aig +*.vcproj +*.sh +*.v lib/abc* lib/m114* lib/bip* diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4efbe90dc..24c1d3b0e 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5669,7 +5669,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) +Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) { Vec_Int_t * vLits; Gia_Man_t * pNew, * pTemp; @@ -5717,6 +5717,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 ); Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 ); int n = Gia_ManBufNum(p1) / 2; + if(biNum > 0){ + n = biNum; + } Gia_ManStaticFanoutStart( p1 ); Vec_Ptr_t * vQ = Vec_PtrAlloc(16); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 906b456ad..dab809c25 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -38074,6 +38074,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'w': pPars->fVeryVerbose ^= 1; break; + case 'q': + pPars->fBMiterInfo ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -38138,6 +38141,7 @@ usage: Abc_Print( -2, "\t-o : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" ); Abc_Print( -2, "\t-p : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-q : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -51689,16 +51693,25 @@ usage: ***********************************************************************/ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); Gia_Man_t * pTemp, * pSecond; char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0; + int bi = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + bi = atoi(argv[globalUtilOptind++]); + break; case 'v': fVerbose ^= 1; break; @@ -51737,14 +51750,15 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" ); return 0; } - pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose ); + pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose, bi); Gia_ManStop( pSecond ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &bmiter [-vh] \n" ); + Abc_Print( -2, "usage: &bmiter -I [-vh] \n" ); Abc_Print( -2, "\t creates the boundary miter\n" ); + Abc_Print( -2, "\t-I : number of boundary inputs\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the implementation file\n"); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 6086fc616..6077a20c2 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer pNtkFrames->pName = Extra_UtilStrsav(Buffer); // map the constant nodes Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); + // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index d11bca3c3..ca4ac9aba 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -120,6 +120,7 @@ struct Cec_ParFra_t_ int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the failed output + int fBMiterInfo; // printing BMiter information }; // combinational equivalence checking parameters diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 1a6309ebe..424369b8c 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -222,6 +222,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars ) pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 100; // pattern generation iterations + pPars->fBMiterInfo = 0; // printing BMiter information } /**Function************************************************************* @@ -1891,39 +1892,41 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { - if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) - { - switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) + if (pPars->fBMiterInfo){ + if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) { - case 1: - case 4: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); - break; - default: - break; - } - } - else - { - if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); break; default: break; - } + } + else + { + if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + break; + default: + break; + + } + } } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); } @@ -1979,22 +1982,24 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); // TODO - int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; - Vec_IntForEachEntry( vLitBmiter, e, i ) - { - if ( i%2 ) continue; - switch (e) + if (pPars -> fBMiterInfo){ + int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; + Vec_IntForEachEntry( vLitBmiter, e, i ) { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; + if ( i%2 ) continue; + switch (e) + { + case 1: c1++; break; + case 2: c2++; break; + case 3: c3++; break; + case 4: c4++; break; + case 5: c5++; break; + default: + break; + } } + printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); } - printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )