diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 70 | ||||
-rw-r--r-- | src/base/acb/acbAbc.c | 6 | ||||
-rw-r--r-- | src/base/acb/acbFunc.c | 138 | ||||
-rw-r--r-- | src/base/acb/acbUtil.c | 298 |
4 files changed, 432 insertions, 80 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8d8f1ba4..11e847ce 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4333,8 +4333,8 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( Abc_NtkNodeNum(pNtk) == 0 || Abc_NtkPiNum(pNtk) == 0 ) { - Abc_Print( -1, "The network does not have internal nodes.\n" ); - return 1; + Abc_Print( 0, "The network does not have internal nodes.\n" ); + return 0; } if ( !Abc_NtkIsLogic(pNtk) ) { @@ -6933,13 +6933,17 @@ usage: ***********************************************************************/ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Acb_NtkRunEco( char * pFileNames[3], int fVerbose ); - int c, fVerbose = 0; + extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ); + char * pFileNames[4] = {NULL}; + int c, fCheck = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) { switch ( c ) { + case 'c': + fCheck ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6951,16 +6955,18 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pArgvNew = argv + globalUtilOptind; // nArgcNew = argc - globalUtilOptind; - if ( argc - globalUtilOptind != 3 ) + if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 3 ) { Abc_Print( 1, "Expecting three file names on the command line.\n" ); goto usage; } - Acb_NtkRunEco( argv + globalUtilOptind, fVerbose ); + for ( c = 0; c < argc - globalUtilOptind; c++ ) + pFileNames[c] = argv[globalUtilOptind+c]; + Acb_NtkRunEco( pFileNames, fCheck, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: runeco <implementation> <specification> <weights> [-vh]\n" ); + Abc_Print( -2, "usage: runeco [-cvh] <implementation> <specification> <weights>\n" ); Abc_Print( -2, "\t performs computation of patch functions during ECO,\n" ); Abc_Print( -2, "\t as described in the following paper: A. Q. Dao et al\n" ); Abc_Print( -2, "\t \"Efficient computation of ECO patch functions\", Proc. DAC\'18\n" ); @@ -6968,6 +6974,7 @@ usage: Abc_Print( -2, "\t (currently only applicable to benchmarks from 2017 ICCAD CAD competition\n" ); Abc_Print( -2, "\t http://cad-contest-2017.el.cycu.edu.tw/Problem_A/default.html as follows:\n" ); Abc_Print( -2, "\t \"runeco unit1/F.v unit1/G.v unit1/weight.txt; cec -n out.v unit1/G.v\")\n" ); + Abc_Print( -2, "\t-c : toggle checking that the problem has a solution [default = %s]\n", fCheck? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -6988,6 +6995,7 @@ usage: int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Acb_NtkRunGen( char * pFileNames[2], int fVerbose ); + char * pFileNames[4] = {NULL}; int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -7008,11 +7016,13 @@ int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Expecting two file names on the command line.\n" ); goto usage; } - Acb_NtkRunGen( argv + globalUtilOptind, fVerbose ); + for ( c = 0; c < 2; c++ ) + pFileNames[c] = argv[globalUtilOptind+c]; + Acb_NtkRunGen( pFileNames, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: rungen <file1> <file2> [-vh]\n" ); + Abc_Print( -2, "usage: rungen [-vh] <file1> <file2>\n" ); Abc_Print( -2, "\t experimental command\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -7032,13 +7042,28 @@ usage: ***********************************************************************/ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_Sim4Try( char * pFileName0, char * pFileName1, int fVerbose ); - int c, fVerbose = 1; + extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose ); + char * pFileNames[4] = {NULL, NULL, "out.v", NULL}; + int c, fOrder = 0, nWords = 1, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF ) { switch ( c ) { + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords < 0 ) + goto usage; + break; + case 'o': + fOrder ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7048,19 +7073,24 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( argc - globalUtilOptind != 2 ) + if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 4 ) { - Abc_Print( 1, "Expecting two file names on the command line.\n" ); + Abc_Print( 1, "Expecting two or three file names on the command line.\n" ); goto usage; } - Gia_Sim4Try( argv[globalUtilOptind+0], argv[globalUtilOptind+1], fVerbose ); + Gia_ManRandom(1); + for ( c = 0; c < argc - globalUtilOptind; c++ ) + pFileNames[c] = argv[globalUtilOptind+c]; + Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: runsim <file1> <file2> [-vh]\n" ); - Abc_Print( -2, "\t experimental command\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: runsim [-W] [-ovh] [-N <num>] <file1> <file2> <file3>\n" ); + Abc_Print( -2, "\t experimental simulation command\n" ); + Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords ); + Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c index 5fe7c7e3..9c2db080 100644 --- a/src/base/acb/acbAbc.c +++ b/src/base/acb/acbAbc.c @@ -177,7 +177,7 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames ObjId = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 ); Vec_IntWriteEntry( vMap, NameId, ObjId ); Acb_ObjSetName( pNtk, ObjId, NameId ); - Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 ); + Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 ); } Ndr_ModForEachTarget( p, Mod, Obj ) { @@ -198,12 +198,14 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames } Ndr_ModForEachNode( p, Mod, Obj ) { + //char * pName; NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT ); + //pName = Abc_NamStr( pMan->pStrs, NameId ); ObjId = Vec_IntEntry( vMap, NameId ); nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray ); for ( k = 0; k < nArray; k++ ) Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) ); - Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 ); + Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 ); } Ndr_ModForEachPo( p, Mod, Obj ) { diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index f6fcf2b0..1708e51d 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -175,6 +175,14 @@ Abc_Nam_t * Acb_VerilogStartNames() } return pNames; } +void Acb_VerilogRemoveComments ( char * pBuffer ) +{ + char * pTemp; + for ( pTemp = pBuffer; *pTemp; pTemp++ ) + if ( pTemp[0] == '/' && pTemp[1] == '/' ) + while ( *pTemp && *pTemp != '\n' ) + *pTemp++ = ' '; +} Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames ) { Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 ); @@ -182,11 +190,12 @@ Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames ) char * pToken; if ( pBuffer == NULL ) return NULL; - pToken = strtok( pBuffer, " \n\r()," ); + Acb_VerilogRemoveComments( pBuffer ); + pToken = strtok( pBuffer, " \n\r\t()," ); while ( pToken ) { Vec_IntPush( vBuffer, Abc_NamStrFindOrAdd(pNames, pToken, NULL) ); - pToken = strtok( NULL, " \n\r(),;" ); + pToken = strtok( NULL, " \n\r\t(),;" ); } ABC_FREE( pBuffer ); return vBuffer; @@ -204,7 +213,7 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) Vec_Int_t * vWires = Vec_IntAlloc(100); Vec_Int_t * vTypes = Vec_IntAlloc(100); Vec_Int_t * vFanins = Vec_IntAlloc(100); - Vec_Int_t * vCur = NULL; + Vec_Int_t * vCur = NULL; int i, ModuleID, Token, Size, Count = 0; assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE ); Vec_IntForEachEntryStart( vBuffer, Token, i, 2 ) @@ -221,9 +230,12 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) vCur = vWires; else if ( Token >= ACB_BUF && Token <= ACB_XNOR ) { + char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1)); Vec_IntPush( vTypes, Token ); Vec_IntPush( vTypes, Vec_IntSize(vFanins) ); vCur = vFanins; + if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' ) + i++; } else Vec_IntPush( vCur, Token ); @@ -412,7 +424,7 @@ void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName ) assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) ); fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); - fprintf( pFile, " );" ); + fprintf( pFile, " );\n" ); } fprintf( pFile, "\nendmodule\n\n" ); @@ -547,7 +559,7 @@ Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp ) printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) ); return vDivs; } -Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock ) +Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock, int fVerbose ) { int fPrintWeights = 0; int nDivLimit = 3000; @@ -589,8 +601,10 @@ Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBloc printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 ); printf( "\n" ); } + if ( fVerbose ) printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) ); Vec_IntShrink( vDivs, nDivLimit ); + if ( fVerbose ) printf( "%d.\n", Vec_IntSize(vDivs) ); return vDivs; } @@ -644,11 +658,15 @@ Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDi ***********************************************************************/ int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp ) { + //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) ); int * pFanin, iFanin, k, Type, Res; assert( !Acb_ObjIsCio(p, iObj) ); Vec_IntClear( vTemp ); Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k ) + { + assert( Acb_ObjCopy(p, iFanin) >= 0 ); Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) ); + } Type = Acb_ObjType( p, iObj ); if ( Type == ABC_OPER_CONST_F ) return 0; @@ -688,6 +706,7 @@ Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes, Vec_Int_t * vFanins; int i, iObj; pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 ); + pNew->pName = Abc_UtilStrsav(Acb_NtkName(p)); Gia_ManHashAlloc( pNew ); Acb_NtkCleanObjCopies( p ); // create primary inputs @@ -1202,7 +1221,14 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() ); status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 ); - if ( status != l_False ) + if ( status == l_True ) + { + printf( "ECO does not exist.\n" ); + sat_solver_delete( pSat ); + Vec_IntFree( vSupp ); + return NULL; + } + if ( status == l_Undef ) { printf( "Support computation timed out after %d sec.\n", TimeOut ); sat_solver_delete( pSat ); @@ -1789,12 +1815,12 @@ Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * { int i, iObj; Vec_Str_t * vStr = Vec_StrAlloc( 100 ); - Vec_StrAppend( vStr, "patch p0 (" ); + Vec_StrAppend( vStr, " patch p0 (" ); Vec_IntForEachEntry( vTars, iObj, i ) Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) ); Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) ); - Vec_StrAppend( vStr, " );\n" ); + Vec_StrAppend( vStr, " );\n\n" ); Vec_StrPush( vStr, '\0' ); return vStr; } @@ -1880,7 +1906,7 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) ); Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) ); Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T ); - Vec_StrPrintF( vStr, " );" ); + Vec_StrPrintF( vStr, " );\n" ); } } Vec_StrAppend( vStr, "\nendmodule\n\n" ); @@ -1913,28 +1939,23 @@ void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch ) } void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch ) { - char * pBuffer = ABC_ALLOC( char, 10000 ); - FILE * pFileIn, * pFileOut; - // input file - pFileIn = fopen( pFileNameF, "rb" ); - if ( !pFileIn ) + FILE * pFileOut; + char * pBuffer = Extra_FileReadContents( pFileNameF ); + if ( pBuffer == NULL ) return; - // output file pFileOut = fopen( pFileNameOut, "wb" ); - if ( !pFileOut ) - return; - // copy line by line - while ( fgets(pBuffer, 10000, pFileIn) ) + if ( pFileOut ) { - if ( strstr(pBuffer, "endmodule") ) - fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) ); - fputs( pBuffer, pFileOut ); + char * pTemp = strstr( pBuffer, "endmodule" ); + int nFirst = pTemp-pBuffer, nSecond = strlen(pBuffer) - nFirst; + int Value = fwrite( pBuffer, nFirst, 1, pFileOut ); + fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) ); + Value = fwrite( pBuffer+nFirst, nSecond, 1, pFileOut ); + if ( vPatch ) + fprintf( pFileOut, "\n%s\n", Vec_StrArray(vPatch) ); } - if ( vPatch ) - fprintf( pFileOut, "\n\n%s\n", Vec_StrArray(vPatch) ); - fclose( pFileIn ); - fclose( pFileOut ); ABC_FREE( pBuffer ); + fclose( pFileOut ); } /**Function************************************************************* @@ -2012,10 +2033,10 @@ Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p ) } return pNew; } -Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars ) +Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerbose ) { Gia_Man_t * pCof = Gia_ManDup( p ); - Cnf_Dat_t * pCnf; int v, fVerbose = 1; + Cnf_Dat_t * pCnf; int v; for ( v = 0; v < iTar; v++ ) { pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v ); @@ -2024,8 +2045,8 @@ Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars ) } if ( fVerbose ) printf( "M_quo: " ); if ( fVerbose ) Gia_ManPrintStats( pCof, NULL ); - pCof = Acb_NtkEcoSynthesize( p = pCof ); - Gia_ManStop( p ); + //pCof = Acb_NtkEcoSynthesize( p = pCof ); + //Gia_ManStop( p ); if ( fVerbose ) printf( "M_syn: " ); if ( fVerbose ) Gia_ManPrintStats( pCof, NULL ); if ( 0 && iTar < nTars ) @@ -2113,7 +2134,7 @@ Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth Gia_ManStop( pInter[m] ); return pFinal; } -Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars ) +Gia_Man_t * Acb_NtkDeriveMiterCnfInter2( Gia_Man_t * p, int iTar, int nTars ) { // extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose ); extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p ); @@ -2154,7 +2175,7 @@ Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars ) //Gia_ManPrintStats( pInter, NULL ); return pInter; } -Gia_Man_t * Acb_NtkEcoComputeInter( Gia_Man_t * p, int iTar, int nTars ) +Gia_Man_t * Acb_NtkDeriveMiterCnfInter( Gia_Man_t * p, int iTar, int nTars ) { Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v; for ( v = 0; v < iTar; v++ ) @@ -2271,7 +2292,7 @@ Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps, SeeAlso [] ***********************************************************************/ -int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, int fCisOnly ) +int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose ) { extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); @@ -2286,7 +2307,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, Vec_Int_t * vSuppF = Acb_NtkFindSupp( pNtkF, vRoots ); Vec_Int_t * vSuppG = Acb_NtkFindSupp( pNtkG, vRoots ); Vec_Int_t * vSupp = Vec_IntTwoMerge( vSuppF, vSuppG ); - Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock ); + Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose ); Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs ); Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL ); @@ -2309,21 +2330,24 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, char * pSop = NULL; int i, Res; - printf( "The number of targets = %d.\n", nTargets ); - - printf( "NtkF: " ); - Gia_ManPrintStats( pGiaF, NULL ); - printf( "NtkG: " ); - Gia_ManPrintStats( pGiaG, NULL ); - printf( "Miter: " ); - Gia_ManPrintStats( pGiaM, NULL ); + if ( fVerbose ) + { + printf( "The number of targets = %d.\n", nTargets ); + + printf( "NtkF: " ); + Gia_ManPrintStats( pGiaF, NULL ); + printf( "NtkG: " ); + Gia_ManPrintStats( pGiaG, NULL ); + printf( "Miter: " ); + Gia_ManPrintStats( pGiaM, NULL ); + } // check that the problem has a solution - if ( 0 )//fCisOnly ) + if ( fCheck )//fCisOnly ) { int Lit, status; sat_solver * pSat; - pCnf = Acb_NtkEcoCompute( pGiaM, nTargets, nTargets ); + pCnf = Acb_NtkDeriveMiterCnf( pGiaM, nTargets, nTargets, fVerbose ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); Cnf_DataFree( pCnf ); // add output clause @@ -2350,7 +2374,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) ); printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) ); - pOne = Acb_NtkEcoComputeInter( pGiaM, i, nTargets ); + pOne = Acb_NtkDeriveMiterCnfInter( pGiaM, i, nTargets ); printf( "Tar%02d: ", i ); Gia_ManPrintStats( pOne, NULL ); @@ -2363,12 +2387,11 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, } else { - pCnf = Acb_NtkEcoCompute( pGiaM, i, nTargets ); + pCnf = Acb_NtkDeriveMiterCnf( pGiaM, i, nTargets, fVerbose ); // vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut ); vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut ); if ( vSupp == NULL ) { - Vec_IntFree( vSuppOld ); Cnf_DataFree( pCnf ); RetValue = 0; goto cleanup; @@ -2383,7 +2406,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, Cnf_DataFree( pCnf ); if ( pSop == NULL ) { - Vec_IntFree( vSuppOld ); RetValue = 0; goto cleanup; } @@ -2405,7 +2427,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp ); Vec_IntFree( vSupp ); } - Vec_IntFree( vSuppOld ); // make sure the function is UNSAT printf( "\n" ); @@ -2443,8 +2464,9 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, Acb_PrintPatch( pNtkF, vDivs, vUsed, clk ); // generate output files - Acb_GenerateFilePatch( vPatch, "patch.v" ); - Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch ); + if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" ); + Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch ); + printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : "out.v" ); //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 ); cleanup: // cleanup @@ -2460,9 +2482,9 @@ cleanup: Vec_PtrFreeFree( vSops ); Vec_WecFree( vSupps ); - - if ( vFuncs ) Vec_PtrFreeFree( vFuncs ); + Vec_IntFree( vSuppOld ); Vec_IntFreeP( &vUsed ); + if ( vFuncs ) Vec_PtrFreeFree( vFuncs ); Gia_ManStop( pGiaF ); Gia_ManStop( pGiaG ); @@ -2511,7 +2533,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose ) SeeAlso [] ***********************************************************************/ -void Acb_NtkRunEco( char * pFileNames[3], int fVerbose ) +void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ) { Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] ); Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL ); @@ -2528,11 +2550,11 @@ void Acb_NtkRunEco( char * pFileNames[3], int fVerbose ) Acb_IntallLibrary(); - if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 0 ) ) + if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose ) ) { - printf( "General ECO computation timed out. Trying inputs only.\n\n" ); - if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 1 ) ) - printf( "Input-only ECO computation also timed out.\n\n" ); + printf( "General computation timed out. Trying inputs only.\n\n" ); + if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose ) ) + printf( "Input-only computation also timed out.\n\n" ); } Acb_ManFree( pNtkF->pDesign ); diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index 2d56a553..ecf84bb6 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -470,6 +470,304 @@ void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp Vec_IntClear( &p->vSuppOld ); } +/**Function************************************************************* + + Synopsis [Derive AIG for one network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkFindNodes2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes ) +{ + int * pFanin, iFanin, i; + if ( Acb_ObjSetTravIdCur(p, iObj) ) + return; + if ( Acb_ObjIsCi(p, iObj) ) + return; + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i ) + Acb_NtkFindNodes2_rec( p, iFanin, vNodes ); + assert( !Acb_ObjIsCo(p, iObj) ); + Vec_IntPush( vNodes, iObj ); +} +Vec_Int_t * Acb_NtkFindNodes2( Acb_Ntk_t * p ) +{ + int i, iObj; + Vec_Int_t * vNodes = Vec_IntAlloc( 1000 ); + Acb_NtkIncTravId( p ); + Acb_NtkForEachCo( p, iObj, i ) + Acb_NtkFindNodes2_rec( p, Acb_ObjFanin(p, iObj, 0), vNodes ); + return vNodes; +} +int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp ) +{ + //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) ); + int * pFanin, iFanin, k, Type, Res; + assert( !Acb_ObjIsCio(p, iObj) ); + Vec_IntClear( vTemp ); + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k ) + { + assert( Acb_ObjCopy(p, iFanin) >= 0 ); + Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) ); + } + Type = Acb_ObjType( p, iObj ); + if ( Type == ABC_OPER_CONST_F ) + return 0; + if ( Type == ABC_OPER_CONST_T ) + return 1; + if ( Type == ABC_OPER_BIT_BUF ) + return Vec_IntEntry(vTemp, 0); + if ( Type == ABC_OPER_BIT_INV ) + return Abc_LitNot( Vec_IntEntry(vTemp, 0) ); + if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND ) + { + Res = 1; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManAppendAnd2( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND ); + } + if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR ) + { + Res = 0; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManAppendOr2( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR ); + } + if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR ) + { + Res = 0; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManAppendXor2( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR ); + } + assert( 0 ); + return -1; +} +Gia_Man_t * Acb_NtkToGia2( Acb_Ntk_t * p ) +{ + Gia_Man_t * pNew, * pOne; + Vec_Int_t * vFanins, * vNodes; + int i, iObj; + pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 ); + pNew->pName = Abc_UtilStrsav(Acb_NtkName(p)); + Acb_NtkCleanObjCopies( p ); + Acb_NtkForEachCi( p, iObj, i ) + Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) ); + vFanins = Vec_IntAlloc( 4 ); + vNodes = Acb_NtkFindNodes2( p ); + Vec_IntForEachEntry( vNodes, iObj, i ) + Acb_ObjSetCopy( p, iObj, Acb_ObjToGia2(pNew, p, iObj, vFanins) ); + Vec_IntFree( vNodes ); + Vec_IntFree( vFanins ); + Acb_NtkForEachCo( p, iObj, i ) + Gia_ManAppendCo( pNew, Acb_ObjCopy(p, Acb_ObjFanin(p, iObj, 0)) ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManUpdateCopy( &p->vObjCopy, pOne ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR ) +{ + int i, iObj, iLit; + Vec_Int_t * vObjs = Acb_NtkFindNodes2( p ); + Vec_Int_t * vNodes = Vec_IntAlloc( Acb_NtkObjNum(p) ); + Vec_Ptr_t * vNodesR = Vec_PtrStart( Gia_ManObjNum(pGia) ); + Vec_IntForEachEntry( vObjs, iObj, i ) + if ( (iLit = Acb_ObjCopy(p, iObj)) >= 0 && Gia_ObjIsAnd(Gia_ManObj(pGia, Abc_Lit2Var(iLit))) ) + { + if ( Vec_PtrEntry(vNodesR, Abc_Lit2Var(iLit)) == NULL ) + { + Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) ); + Vec_IntPush( vNodes, Abc_Lit2Var(iLit) ); + } + } + Vec_IntFree( vObjs ); + Vec_IntSort( vNodes, 0 ); + *pvNodesR = vNodesR; + return vNodes; +} +Vec_Int_t * Acb_NtkCollectUser( Acb_Ntk_t * p, Vec_Ptr_t * vUser ) +{ + char * pTemp; int i; + Vec_Int_t * vRes = Vec_IntAlloc( Vec_PtrSize(vUser) ); + Vec_Int_t * vMap = Vec_IntStart( Abc_NamObjNumMax(Acb_NtkNam(p)) ); + Acb_NtkForEachNode( p, i ) + if ( Acb_ObjName(p, i) > 0 ) + Vec_IntWriteEntry( vMap, Acb_ObjName(p, i), Acb_ObjCopy(p, i) ); + Vec_PtrForEachEntry( char *, vUser, pTemp, i ) + if ( Acb_NtkStrId(p, pTemp) < Vec_IntSize(vMap) ) + { + int iLit = Vec_IntEntry( vMap, Acb_NtkStrId(p, pTemp) ); + assert( iLit > 0 ); + //printf( "Obj = %3d Name = %3d Copy = %3d\n", i, Acb_NtkStrId(p, pTemp), iLit ); + Vec_IntPush( vRes, Abc_Lit2Var(iLit) ); + } + assert( Vec_IntSize(vRes) == Vec_PtrSize(vUser) ); + Vec_IntFree( vMap ); + Vec_IntUniqify( vRes ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fVerbose, + Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR ) +{ + extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW ); + Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileName0, NULL ); + Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileName1, NULL ); + int RetValue = 0; + if ( pNtkF && pNtkG ) + { + Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF ); + Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG ); + assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) ); + assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) ); + *ppGiaF = pGiaF; + *ppGiaG = pGiaG; + *pvNodes = Acb_NtkCollectCopies( pNtkF, pGiaF, pvNodesR ); + RetValue = 1; + } + if ( pNtkF->pDesign ) Acb_ManFree( pNtkF->pDesign ); + if ( pNtkG->pDesign ) Acb_ManFree( pNtkG->pDesign ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames ) +{ + Vec_Int_t * vPlaces; int First = 1, Pos = -1; + char * pTemp, * pBuffer = Extra_FileReadContents( pFileName ); + char * pLimit = pBuffer + strlen(pBuffer); + if ( pBuffer == NULL ) + return NULL; + vPlaces = Vec_IntAlloc( Vec_PtrSize(vNames) ); + for ( pTemp = pBuffer; *pTemp; pTemp++ ) + { + if ( *pTemp == '\n' ) + Pos = pTemp - pBuffer + 1; + else if ( *pTemp == '(' ) + { + if ( First ) + First = 0; + else + { + char * pToken = strtok( pTemp+1, " \n\r\t" ); + char * pName; int i; + Vec_PtrForEachEntry( char *, vNames, pName, i ) + if ( !strcmp(pName, pToken) ) + Vec_IntPushTwo( vPlaces, Pos, i ); + pTemp = pToken + strlen(pToken); + while ( *pTemp == 0 ) + pTemp++; + assert( pTemp < pLimit ); + } + } + } + assert( Vec_IntSize(vPlaces) == 2*Vec_PtrSize(vNames) ); + ABC_FREE( pBuffer ); + return vPlaces; +} +void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames ) +{ + int i, k, Prev = 0, Pos, Pos2, iObj; + Vec_Int_t * vPlaces; + char * pName, * pBuffer; + FILE * pFile = fopen( pFileNameOut, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileNameOut ); + return; + } + pBuffer = Extra_FileReadContents( pFileNameIn ); + if ( pBuffer == NULL ) + { + fclose( pFile ); + printf( "Cannot open input file \"%s\".\n", pFileNameIn ); + return; + } + vPlaces = Acb_NtkPlaces( pFileNameIn, vNames ); + Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i ) + { + for ( k = Prev; k < Pos; k++ ) + fputc( pBuffer[k], pFile ); + fprintf( pFile, "// [t_%d = %s] //", iObj, (char *)Vec_PtrEntry(vNames, iObj) ); + Prev = Pos; + } + Vec_IntFree( vPlaces ); + pName = strstr(pBuffer, "endmodule"); + Pos2 = pName - pBuffer; + for ( k = Prev; k < Pos2; k++ ) + fputc( pBuffer[k], pFile ); + fprintf( pFile, "\n\n" ); + fprintf( pFile, " wire " ); + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " t_%d%s", i, i==Vec_PtrSize(vNames)-1 ? ";" : "," ); + fprintf( pFile, "\n\n" ); + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " buf( %s, t_%d );\n", pName, i ); + fprintf( pFile, "\n" ); + for ( k = Pos2; pBuffer[k]; k++ ) + fputc( pBuffer[k], pFile ); + ABC_FREE( pBuffer ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose ) +{ + extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose ); + extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ); + char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] }; + if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) ) + Acb_NtkRunEco( pFileNames, 0, fVerbose ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |