diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index bdd979eb2..9d2a2c875 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -238,6 +238,22 @@ Gia_Man_t * Gia_ManRandSyn( Gia_Man_t * p, unsigned random_seed ) return pRes; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ) +{ + return Gia_ManDeepSyn( pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 78d3a2f77..fca1b8e6b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42510,6 +42510,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } } + pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL; + pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL; + pPars->vNamesIn = pGias[0] ? pGias[0]->vNamesIn : NULL; // compute the miter if ( Gia_ManCiNum(pGias[0]) < 6 ) { @@ -54533,9 +54536,10 @@ usage: int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ); - Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fChoices = 0, fVerbose = 0; + extern Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ); + Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fChoices = 0, fOpt = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStcovh" ) ) != EOF ) { switch ( c ) { @@ -54600,6 +54604,9 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fChoices ^= 1; break; + case 'o': + fOpt ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -54614,12 +54621,15 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9DeepSyn(): There is no AIG.\n" ); return 0; } - pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); + if ( fOpt ) + pTemp = Gia_ManDeepSyn2( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); + else + pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &deepsyn [-IJTAS ] [-tcvh]\n" ); + Abc_Print( -2, "usage: &deepsyn [-IJTAS ] [-tcovh]\n" ); Abc_Print( -2, "\t performs synthesis\n" ); Abc_Print( -2, "\t-I : the number of iterations [default = %d]\n", nIters ); Abc_Print( -2, "\t-J : the number of steps without improvements [default = %d]\n", nNoImpr ); @@ -54628,6 +54638,7 @@ usage: Abc_Print( -2, "\t-S : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed ); Abc_Print( -2, "\t-t : toggle using two-input LUTs [default = %s]\n", fUseTwo? "yes": "no" ); Abc_Print( -2, "\t-c : toggle computing structural choices [default = %s]\n", fChoices? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle using optimization [default = %s]\n", fOpt? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 3ae3e1846..c4744ebe0 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -731,6 +731,147 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) return pValues; } +typedef struct Abc_NtkCexWord_t_ +{ + char * pBase; + Vec_Int_t * vBits; +} Abc_NtkCexWord_t; + +static Abc_NtkCexWord_t * Abc_NtkVerifyFindWord( Vec_Ptr_t * vWords, const char * pBase ) +{ + Abc_NtkCexWord_t * pWord; + int i; + Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i ) + if ( !strcmp( pWord->pBase, pBase ) ) + return pWord; + pWord = ABC_ALLOC( Abc_NtkCexWord_t, 1 ); + pWord->pBase = ABC_ALLOC( char, strlen(pBase) + 1 ); + strcpy( pWord->pBase, pBase ); + pWord->vBits = Vec_IntAlloc( 0 ); + Vec_PtrPush( vWords, pWord ); + return pWord; +} + +static void Abc_NtkVerifyFreeWords( Vec_Ptr_t * vWords ) +{ + Abc_NtkCexWord_t * pWord; + int i; + Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i ) + { + ABC_FREE( pWord->pBase ); + Vec_IntFree( pWord->vBits ); + ABC_FREE( pWord ); + } + Vec_PtrFree( vWords ); +} + +static int Abc_NtkVerifyParseBitName( const char * pName, char ** ppBase, int * pIndex ) +{ + const char * pOpen; + const char * pClose; + char * pEnd; + long Index; + *ppBase = NULL; + pClose = strrchr( pName, ']' ); + pOpen = pClose ? strrchr( pName, '[' ) : NULL; + if ( pOpen == NULL || pClose == NULL || pClose < pOpen || pClose[1] != 0 ) + return 0; + Index = strtol( pOpen + 1, &pEnd, 10 ); + if ( pEnd != pClose || Index < 0 ) + return 0; + *pIndex = (int)Index; + *ppBase = ABC_ALLOC( char, pOpen - pName + 1 ); + strncpy( *ppBase, pName, pOpen - pName ); + (*ppBase)[pOpen - pName] = 0; + return 1; +} + +static int Abc_NtkVerifyCollectWords( Vec_Ptr_t * vWords, const char * const * ppNames, const int * pValues, int nEntries ) +{ + int i, fHasVector = 0; + for ( i = 0; i < nEntries; i++ ) + { + char * pBase = NULL; + int Index = 0; + int fVector = Abc_NtkVerifyParseBitName( ppNames[i], &pBase, &Index ); + Abc_NtkCexWord_t * pWord = Abc_NtkVerifyFindWord( vWords, fVector ? pBase : ppNames[i] ); + Vec_IntSetEntry( pWord->vBits, fVector ? Index : 0, pValues[i] ); + fHasVector |= fVector; + if ( pBase ) + ABC_FREE( pBase ); + } + return fHasVector; +} + +static void Abc_NtkVerifyPrintWords( Vec_Ptr_t * vWords ) +{ + Abc_NtkCexWord_t * pWord; + int i, d, b, nBits, nHex, Digit; + Vec_PtrForEachEntry( Abc_NtkCexWord_t *, vWords, pWord, i ) + { + nBits = Vec_IntSize( pWord->vBits ); + nHex = (nBits + 3) / 4; + nHex = nHex ? nHex : 1; + { + char * pHex = ABC_ALLOC( char, nHex + 1 ); + for ( d = 0; d < nHex; d++ ) + { + Digit = 0; + for ( b = 0; b < 4; b++ ) + { + int iBit = d * 4 + b; + if ( iBit < nBits && Vec_IntEntry( pWord->vBits, iBit ) ) + Digit |= 1 << b; + } + pHex[nHex - d - 1] = "0123456789ABCDEF"[Digit]; + } + pHex[nHex] = 0; + printf( "%s = %d'h%s", pWord->pBase, nBits, pHex ); + ABC_FREE( pHex ); + } + if ( i + 1 < Vec_PtrSize(vWords) ) + printf( ", " ); + } +} + +void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, + const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, + const char * pNtkName1, const char * pNtkName2 ) +{ + Vec_Ptr_t * vInputs = Vec_PtrAlloc( 0 ); + Vec_Ptr_t * vOutputs1 = Vec_PtrAlloc( 0 ); + Vec_Ptr_t * vOutputs2 = Vec_PtrAlloc( 0 ); + Abc_NtkVerifyCollectWords( vInputs, ppInputNames, pModel, nInputs ); + Abc_NtkVerifyCollectWords( vOutputs1, ppOutputNames, pValues1, nOutputs ); + if ( pValues2 ) + Abc_NtkVerifyCollectWords( vOutputs2, ppOutputNames, pValues2, nOutputs ); + if ( Vec_PtrSize(vInputs) || Vec_PtrSize(vOutputs1) || Vec_PtrSize(vOutputs2) ) + { + printf( "INPUT: " ); + Abc_NtkVerifyPrintWords( vInputs ); + printf( ". OUTPUT: " ); + Abc_NtkVerifyPrintWords( vOutputs1 ); + printf( " (%s)", pNtkName1 ? pNtkName1 : "network1" ); + if ( pValues2 && Vec_PtrSize(vOutputs2) ) + { + printf( ", " ); + Abc_NtkVerifyPrintWords( vOutputs2 ); + printf( " (%s)", pNtkName2 ? pNtkName2 : "network2" ); + } + printf( ".\n" ); + } + Abc_NtkVerifyFreeWords( vInputs ); + Abc_NtkVerifyFreeWords( vOutputs1 ); + Abc_NtkVerifyFreeWords( vOutputs2 ); +} + +static const char * Abc_NtkVerifyNetworkName( Abc_Ntk_t * pNtk ) +{ + if ( pNtk == NULL ) + return NULL; + return Abc_NtkSpec(pNtk) ? Abc_NtkSpec(pNtk) : Abc_NtkName(pNtk); +} + /**Function************************************************************* @@ -747,6 +888,8 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode { Vec_Ptr_t * vNodes; Abc_Obj_t * pNode; + const char ** ppCiNames = NULL; + const char ** ppCoNames = NULL; int * pValues1, * pValues2; int nErrors, nPrinted, i, iNode = -1; @@ -755,6 +898,17 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode // get the CO values under this model pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel ); pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel ); + // print word-level counter-example, if available + ppCiNames = ABC_ALLOC( const char *, Abc_NtkCiNum(pNtk1) ); + Abc_NtkForEachCi( pNtk1, pNode, i ) + ppCiNames[i] = Abc_ObjName( pNode ); + ppCoNames = ABC_ALLOC( const char *, Abc_NtkCoNum(pNtk1) ); + Abc_NtkForEachCo( pNtk1, pNode, i ) + ppCoNames[i] = Abc_ObjName( pNode ); + Abc_NtkVerifyPrintCex( pModel, pValues1, pValues2, ppCiNames, Abc_NtkCiNum(pNtk1), + ppCoNames, Abc_NtkCoNum(pNtk1), Abc_NtkVerifyNetworkName(pNtk1), Abc_NtkVerifyNetworkName(pNtk2) ); + ABC_FREE( ppCiNames ); + ABC_FREE( ppCoNames ); // count the mismatches nErrors = 0; for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) @@ -1115,4 +1269,3 @@ int Abc_NtkIsValidCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index a3fb06376..e360bb99d 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -140,6 +140,9 @@ struct Cec_ParCec_t_ int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the number of failed output + const char * pNameSpec; // name of the first (spec) network + const char * pNameImpl; // name of the second (impl) network + Vec_Ptr_t * vNamesIn; // input names of the first network }; // sequential register correspodence parameters @@ -273,4 +276,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index e52258b9d..5951b58fa 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -24,6 +24,10 @@ #include "misc/extra/extra.h" #include "sat/cnf/cnf.h" +void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, + const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, + const char * pNtkName1, const char * pNtkName2 ); + ABC_NAMESPACE_IMPL_START @@ -35,6 +39,105 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static int * Cec_ManSimulateCombOutputs( Gia_Man_t * p, const int * pInputs ) +{ + Gia_Obj_t * pObj; + int * pValues, * pOutputs, i; + pValues = ABC_ALLOC( int, Gia_ManObjNum(p) ); + if ( pValues == NULL ) + return NULL; + pValues[0] = 0; + Gia_ManForEachPi( p, pObj, i ) + pValues[Gia_ObjId(p, pObj)] = pInputs[i]; + Gia_ManForEachAnd( p, pObj, i ) + { + int v0 = pValues[Gia_ObjFaninId0p(p, pObj)] ^ Gia_ObjFaninC0(pObj); + int v1 = pValues[Gia_ObjFaninId1p(p, pObj)] ^ Gia_ObjFaninC1(pObj); + pValues[Gia_ObjId(p, pObj)] = v0 & v1; + } + pOutputs = ABC_ALLOC( int, Gia_ManPoNum(p) ); + Gia_ManForEachPo( p, pObj, i ) + pOutputs[i] = pValues[Gia_ObjFaninId0p(p, pObj)] ^ Gia_ObjFaninC0(pObj); + ABC_FREE( pValues ); + return pOutputs; +} + +static const char * Cec_ManGetName( const char * pName, const char * pPrefix, int Idx, Vec_Ptr_t * vStore ) +{ + if ( pName ) + return pName; + { + char Buffer[64]; + sprintf( Buffer, "%s[%d]", pPrefix, Idx ); + pName = Abc_UtilStrsav( Buffer ); + Vec_PtrPush( vStore, (void *)pName ); + return pName; + } +} + +static void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars ) +{ + Vec_Ptr_t * vToFree = NULL; + const char ** ppInNames = NULL; + const char ** ppOutNames = NULL; + int * pInputs = NULL; + int * pOutputs = NULL; + int * pOut1 = NULL; + int * pOut2 = NULL; + int nPis, nPairs, i; + if ( (pPars && pPars->fSilent) || pCex == NULL ) + return; + if ( pCex->nRegs || pCex->iFrame || Gia_ManRegNum(p) ) + return; + if ( (Gia_ManPoNum(p) & 1) || Gia_ManPiNum(p) != pCex->nPis ) + return; + nPis = Gia_ManPiNum(p); + nPairs = Gia_ManPoNum(p) / 2; + pInputs = ABC_ALLOC( int, nPis ); + for ( i = 0; i < nPis; i++ ) + pInputs[i] = Abc_InfoHasBit( pCex->pData, pCex->nRegs + i ); + pOutputs = Cec_ManSimulateCombOutputs( p, pInputs ); + if ( pOutputs == NULL ) + goto finish; + pOut1 = ABC_ALLOC( int, nPairs ); + pOut2 = ABC_ALLOC( int, nPairs ); + for ( i = 0; i < nPairs; i++ ) + { + pOut1[i] = pOutputs[2 * i]; + pOut2[i] = pOutputs[2 * i + 1]; + } + vToFree = Vec_PtrAlloc( 16 ); + ppInNames = ABC_ALLOC( const char *, nPis ); + for ( i = 0; i < nPis; i++ ) + { + const char * pName = Gia_ObjCiName(p, i); + if ( pName == NULL && pPars && pPars->vNamesIn && i < Vec_PtrSize(pPars->vNamesIn) ) + pName = (const char *)Vec_PtrEntry( pPars->vNamesIn, i ); + ppInNames[i] = Cec_ManGetName( pName, "a", i, vToFree ); + } + ppOutNames = ABC_ALLOC( const char *, nPairs ); + for ( i = 0; i < nPairs; i++ ) + ppOutNames[i] = Cec_ManGetName( Gia_ObjCoName(p, 2 * i), "z", i, vToFree ); + Abc_NtkVerifyPrintCex( pInputs, pOut1, pOut2, ppInNames, nPis, ppOutNames, nPairs, + pPars && pPars->pNameSpec ? pPars->pNameSpec : Gia_ManName(p), + pPars && pPars->pNameImpl ? pPars->pNameImpl : (p->pSpec ? p->pSpec : Gia_ManName(p)) ); + +finish: + if ( vToFree ) + { + char * pName; + Vec_PtrForEachEntry( char *, vToFree, pName, i ) + ABC_FREE( pName ); + Vec_PtrFree( vToFree ); + } + ABC_FREE( ppInNames ); + ABC_FREE( ppOutNames ); + ABC_FREE( pOut1 ); + ABC_FREE( pOut2 ); + ABC_FREE( pOutputs ); + ABC_FREE( pInputs ); +} + /**Function************************************************************* Synopsis [Saves the input pattern with the given number.] @@ -160,6 +263,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) } pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); + Cec_ManPrintCexSummary( p, p->pCexComb, pPars ); return 0; } // get the drivers @@ -178,6 +282,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) // if their compl attributes are the same - one should be complemented assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) ); Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) ); + Cec_ManPrintCexSummary( p, p->pCexComb, pPars ); return 0; } // one of the drivers is a PI; another is a constant 0 @@ -197,6 +302,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) ); else Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri2) ); + Cec_ManPrintCexSummary( p, p->pCexComb, pPars ); return 0; } } @@ -383,6 +489,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } + Cec_ManPrintCexSummary( p, p->pCexComb, pPars ); return 0; } Vec_IntFreeP( &pInit->vIdsEquiv ); @@ -417,6 +524,8 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); + if ( RetValue == 0 ) + Cec_ManPrintCexSummary( p, p->pCexComb, pPars ); Gia_ManStop( pNew ); return RetValue; } @@ -601,4 +710,3 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index f94bd27f9..fdba94f00 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -167,6 +167,9 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats p->iOutFail = -1; // the number of failed output + p->pNameSpec = NULL; // name of the first (spec) network + p->pNameImpl = NULL; // name of the second (impl) network + p->vNamesIn = NULL; // input names of the first network } /**Function************************************************************* @@ -569,4 +572,3 @@ finalize: ABC_NAMESPACE_IMPL_END -