From dab716878f6e0f0cabadc480e7cc7cf7cacd8acb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 8 Apr 2020 21:11:09 -0700 Subject: Various changes. --- src/base/abci/abc.c | 28 +++++++++------ src/base/acb/acbFunc.c | 93 +++++++++++++++++++++++++++++++++++--------------- src/base/acb/acbUtil.c | 6 ++-- 3 files changed, 86 insertions(+), 41 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fd239185..f9d7ed4c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7045,11 +7045,11 @@ usage: ***********************************************************************/ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ); + extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose, int fVeryVerbose ); char * pFileNames[4] = {NULL}; - int c, fCheck = 0, fVerbose = 0; + int c, fCheck = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cvwh" ) ) != EOF ) { switch ( c ) { @@ -7059,6 +7059,9 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7074,11 +7077,11 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) } for ( c = 0; c < argc - globalUtilOptind; c++ ) pFileNames[c] = argv[globalUtilOptind+c]; - Acb_NtkRunEco( pFileNames, fCheck, fVerbose ); + Acb_NtkRunEco( pFileNames, fCheck, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: runeco [-cvh] \n" ); + Abc_Print( -2, "usage: runeco [-cvwh] \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" ); @@ -7088,6 +7091,7 @@ usage: 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-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -7154,11 +7158,11 @@ usage: ***********************************************************************/ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose ); + extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose, int fVeryVerbose ); char * pFileNames[4] = {NULL, NULL, "out.v", NULL}; - int c, nWords = 4, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fVerbose = 0; + int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbvwh" ) ) != EOF ) { switch ( c ) { @@ -7218,6 +7222,9 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7232,11 +7239,11 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManRandom(1); for ( c = 0; c < argc - globalUtilOptind; c++ ) pFileNames[c] = argv[globalUtilOptind+c]; - Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ); + Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: runsim [-WBLU] [-ofbvh] [-N ] \n" ); + Abc_Print( -2, "usage: runsim [-WBLU] [-ofbvwh] [-N ] \n" ); Abc_Print( -2, "\t experimental simulation command\n" ); Abc_Print( -2, "\t-W : the number of words of simulation info [default = %d]\n", nWords ); Abc_Print( -2, "\t-B : the beam width parameter [default = %d]\n", nBeam ); @@ -7246,6 +7253,7 @@ usage: Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "yes": "no" ); Abc_Print( -2, "\t-b : toggle using buffers [default = %s]\n", fUseBuf? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index e7fe2f53..e23dedbd 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -26,6 +26,8 @@ #include "map/mio/mio.h" #include "misc/util/utilTruth.h" #include "aig/gia/giaAig.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" ABC_NAMESPACE_IMPL_START @@ -495,6 +497,9 @@ Vec_Int_t * Acb_NtkFindRoots( Acb_Ntk_t * p, Vec_Int_t * vTargets, Vec_Bit_t ** Acb_NtkIncTravId( p ); Acb_NtkForEachCi( p, iObj, i ) Acb_ObjSetTravIdCur( p, iObj ); + // visit internal nodes + Acb_NtkForEachNode( p, iObj ) + Acb_NtkFindRoots_rec(p, iObj, vBlock); // collect outputs reachable from targets Acb_NtkForEachCoDriver( p, iObj, i ) if ( Acb_NtkFindRoots_rec(p, iObj, vBlock) ) @@ -577,7 +582,7 @@ Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp ) 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; + int nDivLimit = 5000; int i, iObj; Vec_Int_t * vDivs = Vec_IntAlloc( 1000 ); // mark inputs @@ -741,7 +746,7 @@ Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes, Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i ) Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) ); // add divisor as primary outputs (if the divisors are not primary inputs) - if ( vDivs && Vec_IntSize(vDivs) > Vec_IntSize(vSupp) ) + if ( vDivs )//&& Vec_IntSize(vDivs) > Vec_IntSize(vSupp) ) Vec_IntForEachEntry( vDivs, iObj, i ) Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) ); Gia_ManHashStop( pNew ); @@ -806,7 +811,7 @@ Gia_Man_t * Acb_CreateMiter( Gia_Man_t * pF, Gia_Man_t * pG ) SeeAlso [] ***********************************************************************/ -#define NWORDS 64 +#define NWORDS 256 void Vec_IntPermute( Vec_Int_t * p ) { @@ -903,12 +908,17 @@ Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) ); fFound = 1; } + if ( fFound == 0 ) + break; +/* if ( fFound == 0 ) { + printf( "For some reason, cannot find a divisor.\n" ); Vec_WrdFree( vPats ); Vec_IntFree( vSupp ); return NULL; } +*/ assert( fFound ); iPat++; } @@ -998,6 +1008,7 @@ Vec_Int_t * Acb_FindSupportNext( sat_solver * pSat, int iFirstDiv, Vec_Int_t * v (*pnPats)++; if ( *pnPats == NWORDS*64 ) { + printf( "Exceeded %d words.\n", NWORDS ); Vec_IntFreeP( &vSupp ); return NULL; } @@ -1100,7 +1111,7 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig abctime clkLimit = TimeOut * CLOCKS_PER_SEC + Abc_Clock(); Vec_Wrd_t * vPats = NULL; int nPats = 0; - Vec_Int_t * vSuppBest, * vSupp;//, * vTemp; + Vec_Int_t * vSuppBest, * vSupp, * vTemp; int CostBest, Cost; int Iter; @@ -1110,25 +1121,21 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig printf( "Starting cost = %d.\n", CostBest ); // iteratively find the one with the most ones in the uncovered rows - for ( Iter = 0; Iter < 200; Iter++ ) + for ( Iter = 0; Iter < 500; Iter++ ) { if ( Abc_Clock() > clkLimit ) { - Vec_IntFree( vSuppBest ); - Vec_WrdFree( vPats ); - return NULL; + printf( "Timeout after %d sec.\n", TimeOut ); + break; } if ( Iter == 0 ) vSupp = Acb_FindSupportStart( pSat, iFirstDiv, vWeights, &vPats, &nPats ); else vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats ); if ( vSupp == NULL ) - { - Vec_IntFree( vSuppBest ); - return NULL; - } - //vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp ); - //Vec_IntFree( vTemp ); + break; + vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp ); + Vec_IntFree( vTemp ); if ( vSupp == NULL ) break; Cost = Acb_ComputeSuppCost( vSupp, vWeights, iFirstDiv ); @@ -1137,15 +1144,15 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig { CostBest = Cost; ABC_SWAP( Vec_Int_t *, vSuppBest, vSupp ); - printf( "Iter %4d: Next cost = %d. ", Iter, Cost ); + printf( "Iter %4d: Next cost = %5d. ", Iter, Cost ); printf( "Updating best solution.\n" ); } Vec_IntFree( vSupp ); } - Acb_FindReplace( pSat, iFirstDiv, vWeights, vPats, nPats, vSuppBest ); - + if ( vPats ) + Acb_FindReplace( pSat, iFirstDiv, vWeights, vPats, nPats, vSuppBest ); //printf( "Number of patterns = %d.\n", nPats ); - Vec_WrdFree( vPats ); + Vec_WrdFreeP( &vPats ); return vSuppBest; } @@ -1898,8 +1905,26 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops); int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1; Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates ); - Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + + int nInvs = 0, nBufs = 0, nNodes = 0, nConst = 0; + Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires ) + { + if ( Vec_IntSize(vGate) > 2 ) + { + char * pName = Acb_Oper2Name(Vec_IntEntry(vGate, 0)); + if ( !strcmp(pName, "buf") ) + nBufs++; + else if ( !strcmp(pName, "not") ) + nInvs++; + else + nNodes++; + } + else + nConst++; + } + Vec_StrPrintF( vStr, "// Patch statistics: in = %d out = %d gate = %d (const = %d buf = %d inv = %d other = %d)\n\n", + Vec_IntSize(vUsed), nOuts, nWires, nConst, nBufs, nInvs, nNodes ); Vec_StrAppend( vStr, "module patch (" ); assert( Vec_IntSize(vTars) == nOuts ); @@ -1955,7 +1980,8 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs Vec_PtrFreeFree( vNames ); Vec_WecFree( vGates ); - printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", Vec_IntSize(vUsed), nOuts, nWires ); + printf( "Synthesized patch with %d inputs, %d outputs and %d gates (const = %d buf = %d inv = %d other = %d).\n", + Vec_IntSize(vUsed), nOuts, nWires, nConst, nBufs, nInvs, nNodes ); return vStr; } @@ -2479,7 +2505,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 * pFileName[4], int fCisOnly, int fCheck, int fVerbose ) +int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose, int fVeryVerbose ) { extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); @@ -2515,7 +2541,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4] Vec_Str_t * vInst = NULL, * vPatch = NULL; char * pSop = NULL; - int i, Res; + int i; if ( fVerbose ) { @@ -2609,6 +2635,8 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4] // add to functions Vec_PtrPush( vSops, pSop ); + if ( fVeryVerbose ) + printf( "Function %d\n%s", i, pSop ); } // add to supports Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp ); @@ -2619,6 +2647,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4] printf( "\n" ); if ( !fCisOnly ) { + int Res; abctime clk = Abc_Clock(); pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGiaM, 8, 0, 0, 0, 0 ); Res = Acb_CheckMiter( pCnf ); @@ -2708,7 +2737,6 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose ) Acb_IntallLibrary(); } - /**Function************************************************************* Synopsis [Top level procedure.] @@ -2720,8 +2748,9 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose ) SeeAlso [] ***********************************************************************/ -void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ) +void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose, int fVeryVerbose ) { + char Command[1000]; int Result = 1; Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] ); Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL ); if ( !pNtkF || !pNtkG ) @@ -2737,15 +2766,23 @@ void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ) Acb_IntallLibrary(); - if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose ) ) + if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose, fVeryVerbose ) ) { - 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" ); +// printf( "General computation timed out. Trying inputs only.\n\n" ); +// if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose, fVeryVerbose ) ) +// printf( "Input-only computation also timed out.\n\n" ); + printf( "Computation did not succeed.\n" ); + Result = 0; } Acb_ManFree( pNtkF->pDesign ); Acb_ManFree( pNtkG->pDesign ); + + // verify the result + sprintf( Command, "read %s; strash; write temp1.aig; read %s; strash; write temp2.aig; &cec temp1.aig temp2.aig", + pFileNames[1], pFileNames[3] ? pFileNames[3] : "out.v" ); + if ( Result && Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index 11af9c01..131aeb7a 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -918,13 +918,13 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, SeeAlso [] ***********************************************************************/ -void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose ) +void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose, int fVeryVerbose ) { extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose ); - extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ); + extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose, int fVeryVerbose ); char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] }; if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ) ) - Acb_NtkRunEco( pFileNames, 1, fVerbose ); + Acb_NtkRunEco( pFileNames, 1, fVerbose, fVeryVerbose ); } -- cgit v1.2.3