diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abc/abc.h | 4 | ||||
| -rw-r--r-- | src/base/abc/abcNtk.c | 33 | ||||
| -rw-r--r-- | src/base/abc/abcUtil.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 812 | ||||
| -rw-r--r-- | src/base/abci/abcNtbdd.c | 21 | ||||
| -rw-r--r-- | src/base/abci/abcQbf.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abcResub.c | 492 | ||||
| -rw-r--r-- | src/base/acb/acb.h | 2 | ||||
| -rw-r--r-- | src/base/acb/acbAbc.c | 17 | ||||
| -rw-r--r-- | src/base/acb/acbFunc.c | 277 | ||||
| -rw-r--r-- | src/base/acb/acbTest.c | 55 | ||||
| -rw-r--r-- | src/base/acb/acbUtil.c | 307 | ||||
| -rw-r--r-- | src/base/acb/module.make | 1 | ||||
| -rw-r--r-- | src/base/cmd/cmdApi.c | 2 | ||||
| -rw-r--r-- | src/base/io/io.c | 2 | ||||
| -rw-r--r-- | src/base/main/mainInit.c | 4 | ||||
| -rw-r--r-- | src/base/main/mainReal.c | 4 | ||||
| -rw-r--r-- | src/base/ver/verStream.c | 2 | ||||
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 2 | ||||
| -rw-r--r-- | src/base/wlc/wlcCom.c | 16 | ||||
| -rw-r--r-- | src/base/wlc/wlcNdr.c | 3 | ||||
| -rw-r--r-- | src/base/wlc/wlcNtk.c | 7 | ||||
| -rw-r--r-- | src/base/wlc/wlcShow.c | 2 | ||||
| -rw-r--r-- | src/base/wln/wln.h | 4 | ||||
| -rw-r--r-- | src/base/wln/wlnNdr.c | 15 | ||||
| -rw-r--r-- | src/base/wln/wlnNtk.c | 132 | ||||
| -rw-r--r-- | src/base/wln/wlnRetime.c | 11 |
27 files changed, 1831 insertions, 410 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index c35ba879..312354da 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -761,7 +761,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk ); extern ABC_DLL Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk ); /*=== abcNtbdd.c ==========================================================*/ extern ABC_DLL Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi ); -extern ABC_DLL Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal ); +extern ABC_DLL Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit ); extern ABC_DLL void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose ); extern ABC_DLL void * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ); extern ABC_DLL int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk ); @@ -789,7 +789,7 @@ extern ABC_DLL void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemove extern ABC_DLL void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pFlopPermFile ); extern ABC_DLL void Abc_NtkUnpermute( Abc_Ntk_t * pNtk ); extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops ); -extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias ); +extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias, Gia_Man_t * pMulti ); /*=== abcObj.c ==========================================================*/ extern ABC_DLL Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); extern ABC_DLL void Abc_ObjRecycle( Abc_Obj_t * pObj ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 8e10ab3b..7c54f3c4 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -2250,15 +2250,43 @@ Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias ) +Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias, Gia_Man_t * pMulti ) { - Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry(vGias, 0); + Gia_Man_t * pGia = pMulti ? pMulti : (Gia_Man_t *)Vec_PtrEntry(vGias, 0); Abc_Ntk_t * pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); Abc_Obj_t * pAbcObj, * pAbcObjPo; Gia_Obj_t * pObj; int i, k; pNtk->pName = Extra_UtilStrsav( pName ); for ( k = 0; k < Gia_ManCiNum(pGia); k++ ) Abc_NtkCreatePi( pNtk ); + if ( pMulti ) + { + Gia_ManCleanValue(pGia); + Gia_ManForEachCi( pGia, pObj, k ) + pObj->Value = Abc_ObjId( Abc_NtkCi(pNtk, k) ); + Gia_ManForEachAnd( pGia, pObj, k ) + { + Abc_Obj_t * pAbcObj0 = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value ); + Abc_Obj_t * pAbcObj1 = Abc_NtkObj( pNtk, Gia_ObjFanin1(pObj)->Value ); + pAbcObj0 = Abc_ObjNotCond( pAbcObj0, Gia_ObjFaninC0(pObj) ); + pAbcObj1 = Abc_ObjNotCond( pAbcObj1, Gia_ObjFaninC1(pObj) ); + pAbcObj = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pAbcObj0, pAbcObj1 ); + pObj->Value = Abc_ObjId( pAbcObj ); + } + Gia_ManForEachCo( pGia, pObj, k ) + { + //pObj = Gia_ManCo(pGia, 0); + if ( Gia_ObjFaninId0p(pGia, pObj) == 0 ) + pAbcObj = Abc_ObjNot( Abc_AigConst1(pNtk) ); + else + pAbcObj = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value ); + pAbcObj = Abc_ObjNotCond( pAbcObj, Gia_ObjFaninC0(pObj) ); + pAbcObjPo = Abc_NtkCreatePo( pNtk ); + Abc_ObjAddFanin( pAbcObjPo, pAbcObj ); + } + } + else + { Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) { assert( Gia_ManCoNum(pGia) == 1 ); @@ -2283,6 +2311,7 @@ Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias ) pAbcObjPo = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pAbcObjPo, pAbcObj ); } + } Abc_NtkAddDummyPiNames( pNtk ); Abc_NtkAddDummyPoNames( pNtk ); return pNtk; diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 038079e8..1f0c9725 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -3141,10 +3141,10 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops ) assert( Vec_WecSize(vRes) == iNode ); return vRes; } -Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias ) +Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti ) { Vec_Wec_t * vRes = NULL; - Abc_Ntk_t * pNtk = Abc_NtkCreateFromGias( "top", vGias ); + Abc_Ntk_t * pNtk = Abc_NtkCreateFromGias( "top", vGias, pMulti ); Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pFanin; int i, k, iNode = 0; @@ -3173,7 +3173,7 @@ Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p ) Abc_Ntk_t * pNtkNew, * pNtk; Vec_Ptr_t * vGias = Vec_PtrAlloc( 1 ); Vec_PtrPush( vGias, p ); - pNtk = Abc_NtkCreateFromGias( "top", vGias ); + pNtk = Abc_NtkCreateFromGias( "top", vGias, NULL ); Vec_PtrFree( vGias ); Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "balance; collapse; muxes; strash; dc2" ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6a852bf7..85053e18 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -139,6 +139,7 @@ static int Abc_CommandTestTruth ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -397,6 +398,7 @@ static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MuxProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MuxPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9MuxStr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PrintTruth ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Unate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Rex2Gia ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -411,9 +413,12 @@ static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sim3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9MLGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9MLTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReadSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9WriteSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9SimPat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9PrintSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SimRsb ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -516,6 +521,7 @@ static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9QVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9HomoQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -853,6 +859,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "runsim", Abc_CommandRunSim, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "runtest", Abc_CommandRunTest, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); @@ -1110,6 +1117,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&status", Abc_CommandAbc9Status, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&profile", Abc_CommandAbc9MuxProfile, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&muxpos", Abc_CommandAbc9MuxPos, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&muxstr", Abc_CommandAbc9MuxStr, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&print_truth", Abc_CommandAbc9PrintTruth, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&unate", Abc_CommandAbc9Unate, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rex2gia", Abc_CommandAbc9Rex2Gia, 0 ); @@ -1124,9 +1132,12 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sim3", Abc_CommandAbc9Sim3, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&read_sim", Abc_CommandAbc9ReadSim, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&write_sim", Abc_CommandAbc9WriteSim, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&simpat", Abc_CommandAbc9SimPat, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mlgen", Abc_CommandAbc9MLGen, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mltest", Abc_CommandAbc9MLTest, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sim_read", Abc_CommandAbc9ReadSim, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sim_write", Abc_CommandAbc9WriteSim, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sim_print", Abc_CommandAbc9PrintSim, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sim_gen", Abc_CommandAbc9GenSim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&simrsb", Abc_CommandAbc9SimRsb, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 ); @@ -1229,6 +1240,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&qvar", Abc_CommandAbc9QVar, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&homoqbf", Abc_CommandAbc9HomoQbf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 ); @@ -7039,20 +7051,26 @@ 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 fRandom, int fVerbose, int fVeryVerbose ); char * pFileNames[4] = {NULL}; - int c, fCheck = 0, fVerbose = 0; + int c, fCheck = 0, fRandom = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "crvwh" ) ) != EOF ) { switch ( c ) { case 'c': fCheck ^= 1; break; + case 'r': + fRandom ^= 1; + break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7067,12 +7085,22 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } for ( c = 0; c < argc - globalUtilOptind; c++ ) + { + FILE * pFile = fopen( argv[globalUtilOptind+c], "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file \"%s\".\n", argv[globalUtilOptind+c] ); + return 0; + } + else + fclose( pFile ); pFileNames[c] = argv[globalUtilOptind+c]; - Acb_NtkRunEco( pFileNames, fCheck, fVerbose ); + } + Acb_NtkRunEco( pFileNames, fCheck, fRandom, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: runeco [-cvh] <implementation> <specification> <weights>\n" ); + Abc_Print( -2, "usage: runeco [-crvwh] <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" ); @@ -7081,7 +7109,9 @@ usage: 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-r : toggle using random permutation of support variables [default = %s]\n", fRandom? "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; } @@ -7148,11 +7178,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 fVerbose ); + extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fVerbose, int fVeryVerbose ); char * pFileNames[4] = {NULL, NULL, "out.v", NULL}; - int c, nWords = 4, nBeam = 4, LevL = 0, LevU = 0, fOrder = 0, fFancy = 0, fVerbose = 0; + int c, nWords = 8, nBeam = 4, LevL = -1, LevU = -1, fOrder = 0, fFancy = 0, fUseBuf = 0, fRandom = 0, fUseWeights = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofbruvwh" ) ) != EOF ) { switch ( c ) { @@ -7206,9 +7236,21 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': fFancy ^= 1; break; + case 'b': + fUseBuf ^= 1; + break; + case 'r': + fRandom ^= 1; + break; + case 'u': + fUseWeights ^= 1; + break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7223,11 +7265,22 @@ 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, fVerbose ); + for ( c = 0; c < argc - globalUtilOptind - 1; c++ ) + { + FILE * pFile = fopen( pFileNames[c], "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file \"%s\".\n", pFileNames[c] ); + return 0; + } + else + fclose( pFile ); + } + Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fRandom, fUseWeights, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: runsim [-WBLU] [-ofvh] [-N <num>] <file1> <file2> <file3>\n" ); + Abc_Print( -2, "usage: runsim [-WBLU] [-ofbruvwh] [-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-B <num> : the beam width parameter [default = %d]\n", nBeam ); @@ -7235,12 +7288,68 @@ usage: Abc_Print( -2, "\t-U <num> : the upper bound on level [default = %d]\n", LevU ); Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" ); Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle using buffers [default = %s]\n", fUseBuf? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle using random permutation of support variables [default = %s]\n", fRandom? "yes": "no" ); + Abc_Print( -2, "\t-u : toggle using topological info to select support variables [default = %s]\n", fUseWeights? "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; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose ); + char * pFileNames[4] = {NULL}; + int c, fFancy = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF ) + { + switch ( c ) + { + case 'f': + fFancy ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 5 ) + { + Abc_Print( 1, "Expecting two or three file names on the command line.\n" ); + goto usage; + } + for ( c = 0; c < argc - globalUtilOptind; c++ ) + pFileNames[c] = argv[globalUtilOptind+c]; + Acb_NtkRunTest( pFileNames, fFancy, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: runtest [-fvh] <file1> <file2>\n" ); + Abc_Print( -2, "\t experimental simulation command\n" ); + Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "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; +} + /**Function************************************************************* @@ -10927,15 +11036,25 @@ usage: int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk, * pNtkRes; - int c, fGlobal = 0; - + int c, fGlobal = 0, Limit = 1000000; pNtk = Abc_FrameReadNtk(pAbc); // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Bgh" ) ) != EOF ) { switch ( c ) { + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + Limit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Limit < 0 ) + goto usage; + break; case 'g': fGlobal ^= 1; break; @@ -10970,22 +11089,23 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkBddToMuxes( pNtk, fGlobal ); + pNtkRes = Abc_NtkBddToMuxes( pNtk, fGlobal, Limit ); if ( pNtkRes == NULL ) { - Abc_Print( -1, "Converting to MUXes has failed.\n" ); - return 1; + Abc_Print( 0, "Converting to MUXes has failed.\n" ); + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - Abc_Print( -2, "usage: muxes [-gh]\n" ); - Abc_Print( -2, "\t converts the current network into a network derived by\n" ); - Abc_Print( -2, "\t replacing all nodes by DAGs isomorphic to the local BDDs\n" ); - Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: muxes [-B num] [-gh]\n" ); + Abc_Print( -2, "\t converts the current network into a network derived by\n" ); + Abc_Print( -2, "\t replacing all nodes by DAGs isomorphic to the local BDDs\n" ); + Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", Limit ); + Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -13559,6 +13679,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Gia_Gen2CodeTest(); extern void Dau_NetworkEnumTest(); //Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int nCutMax = 1; @@ -13772,7 +13893,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) //Dau_NetworkEnumTest(); //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder ); //Mnist_ExperimentWithScaling( nDecMax ); - //Extra_ReadForestTest(); + Gia_Gen2CodeTest(); return 0; usage: Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" ); @@ -23375,7 +23496,7 @@ int Abc_CommandSymFun( Abc_Frame_t * pAbc, int argc, char ** argv ) else printf( "Generated truth table of the %d-variable function (%s) and set it as the current network\n", nVars, pTruth ); } - else + else if ( nVars <= 8 ) printf( "%s\n", pTruth ); // read the truth table to be the current network in ABC pCommand = ABC_CALLOC( char, strlen(pTruth) + 100 ); @@ -30532,12 +30653,15 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c; + int c, fArea = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { + case 'a': + fArea ^= 1; + break; case 'h': goto usage; default: @@ -30549,6 +30673,8 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } + if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) ) + return 0; // save the design as best Gia_ManStopP( &pAbc->pGiaSaved ); pAbc->pGiaSaved = Gia_ManDupWithAttributes( pAbc->pGia ); @@ -30557,6 +30683,7 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &saveaig [-ah]\n" ); Abc_Print( -2, "\t saves the current AIG into the internal storage\n" ); + Abc_Print( -2, "\t-a : toggle saving AIG with the smaller area [default = %s]\n", fArea? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -31314,6 +31441,53 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9MuxStr( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManCofStructure( Gia_Man_t * p ); + Gia_Man_t * pGia; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9MuxStr(): There is no AIG.\n" ); + return 1; + } + pGia = Gia_ManCofStructure( pAbc->pGia ); + Abc_FrameUpdateGia( pAbc, pGia ); + return 0; + +usage: + Abc_Print( -2, "usage: &muxstr [-vh]\n" ); + Abc_Print( -2, "\t performs restructuring\n" ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -31822,7 +31996,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) } else if ( pAbc->pGia->pMuxes ) { - pTemp = Gia_ManDupNoMuxes( pAbc->pGia ); + pTemp = Gia_ManDupNoMuxes( pAbc->pGia, 0 ); if ( !Abc_FrameReadFlag("silentmode") ) printf( "Generated AIG from AND/XOR/MUX graph.\n" ); } @@ -32493,15 +32667,16 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9MLGen( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords ); - extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ); - int c, nWords = 4, fVerbose = 0; + extern void Gia_ManDumpFiles( Gia_Man_t * p, int nCexesT, int nCexesV, int Seed, char * pFileName ); + extern void Gia_ManDumpPlaFiles( Gia_Man_t * p, int nCexesT, int nCexesV, int Seed, char * pFileName ); + int c, Seed = 0, nWords = 10, fBinData = 0, fVerbose = 0; + char * pFileName = NULL; char ** pArgvNew; int nArgcNew; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WSbvh" ) ) != EOF ) { switch ( c ) { @@ -32516,6 +32691,20 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nWords < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'b': + fBinData ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -32527,44 +32716,213 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9ReadSim(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9MLGen(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) > 0 ) { - Abc_Print( -1, "Abc_CommandAbc9ReadSim(): This command works only for combinational AIGs.\n" ); + Abc_Print( -1, "Abc_CommandAbc9MLGen(): This command works only for combinational AIGs.\n" ); return 0; } Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( nArgcNew == 0 ) + printf( "Default file names will be used.\n" ); + else + pFileName = pArgvNew[0]; + if ( nArgcNew != 0 && nArgcNew != 1 ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + if ( fBinData ) + Gia_ManDumpFiles( pAbc->pGia, nWords, nWords, Seed, pFileName ); + else + Gia_ManDumpPlaFiles( pAbc->pGia, nWords, nWords, Seed, pFileName ); + return 0; + +usage: + Abc_Print( -2, "usage: &mlgen [-WS num] [-bvh] <file>\n" ); + Abc_Print( -2, "\t generates data files for machine learning\n" ); + Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); + Abc_Print( -2, "\t-S num : the random seed for simulation data (num < 10000) [default = %d]\n", Seed ); + Abc_Print( -2, "\t-b : toggle using binary data files [default = %s]\n", fBinData? "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"); + Abc_Print( -2, "\t<file> : file to store the simulation info\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9MLTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManTestOneFile( Gia_Man_t * p, char * pFileName, char * pDumpFile ); + int c, fVerbose = 0; + char * pDumpFile = NULL; + char ** pArgvNew; + int nArgcNew; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Dvh" ) ) != EOF ) + { + switch ( c ) + { + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" ); + goto usage; + } + pDumpFile = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9MLTest(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9MLTest(): This command works only for combinational AIGs.\n" ); + return 0; + } + Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9MLTest(): Expecting data file name on the command line.\n" ); + return 0; + } + Gia_ManTestOneFile( pAbc->pGia, pArgvNew[0], pDumpFile ); + return 0; + +usage: + Abc_Print( -2, "usage: &mltest [-vh] [-D file] <file>\n" ); + Abc_Print( -2, "\t testing command for machine learning data\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, "\t-D file : file name to dump statistics [default = none]\n" ); + Abc_Print( -2, "\tfile : file with input simulation info\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ); + int c, fOutputs = 0, nWords = 4, fVerbose = 0; + char ** pArgvNew; + int nArgcNew; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF ) { - Gia_ManRandom( 1 ); - pAbc->pGia->vSimsPi = Gia_ManSimPatGenRandom( Gia_ManCiNum(pAbc->pGia) * nWords ); - printf( "Generated %d random patterns (%d 64-bit words) for each input of the AIG.\n", 64*nWords, nWords ); + 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': + fOutputs ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9ReadSim(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9ReadSim(): This command works only for combinational AIGs.\n" ); return 0; } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; if ( nArgcNew != 1 ) { Abc_Print( -1, "File name is not given on the command line.\n" ); return 1; } - pAbc->pGia->vSimsPi = Gia_ManSimPatRead( pArgvNew[0] ); - if ( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) != 0 ) + if ( fOutputs ) + { + Vec_WrdFreeP( &pAbc->pGia->vSimsPo ); + pAbc->pGia->vSimsPo = Gia_ManSimPatRead( pArgvNew[0] ); + if ( Vec_WrdSize(pAbc->pGia->vSimsPo) % Gia_ManCoNum(pAbc->pGia) != 0 ) + { + Vec_WrdFreeP( &pAbc->pGia->vSimsPo ); + Abc_Print( -1, "File size (%d words) does not match the number of AIG inputs (%d %% %d != %d).\n", + Vec_WrdSize(pAbc->pGia->vSimsPo), Vec_WrdSize(pAbc->pGia->vSimsPo), Gia_ManCiNum(pAbc->pGia), + Vec_WrdSize(pAbc->pGia->vSimsPo) % Gia_ManCiNum(pAbc->pGia) ); + return 1; + } + pAbc->pGia->nSimWords = Vec_WrdSize(pAbc->pGia->vSimsPo) / Gia_ManCoNum(pAbc->pGia); + } + else { Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); - Abc_Print( -1, "File size (%d words) does not match the number of AIG inputs (%d %% %d = %d).\n", - Vec_WrdSize(pAbc->pGia->vSimsPi), Vec_WrdSize(pAbc->pGia->vSimsPi), Gia_ManCiNum(pAbc->pGia), - Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) ); - return 1; + pAbc->pGia->vSimsPi = Gia_ManSimPatRead( pArgvNew[0] ); + if ( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) != 0 ) + { + Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); + Abc_Print( -1, "File size (%d words) does not match the number of AIG inputs (%d %% %d != %d).\n", + Vec_WrdSize(pAbc->pGia->vSimsPi), Vec_WrdSize(pAbc->pGia->vSimsPi), Gia_ManCiNum(pAbc->pGia), + Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) ); + return 1; + } + pAbc->pGia->nSimWords = Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia); } return 0; usage: - Abc_Print( -2, "usage: &read_sim [-W num] [-vh] <file>\n" ); + Abc_Print( -2, "usage: &sim_read [-W num] [-ovh] <file>\n" ); Abc_Print( -2, "\t reads simulation patterns from file\n" ); - Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords ); + Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); + Abc_Print( -2, "\t-o : toggle reading output information [default = %s]\n", fOutputs? "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"); Abc_Print( -2, "\t<file> : file to store the simulation info\n"); @@ -32585,14 +32943,17 @@ usage: int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ); - int c, fVerbose = 0; + int c, fOutputs = 0, fVerbose = 0; char ** pArgvNew; int nArgcNew; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ovh" ) ) != EOF ) { switch ( c ) { + case 'o': + fOutputs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -32612,7 +32973,7 @@ int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9WriteSim(): This command works only for combinational AIGs.\n" ); return 0; } - if ( pAbc->pGia->vSimsPi == NULL ) + if ( (fOutputs ? pAbc->pGia->vSimsPo : pAbc->pGia->vSimsPi) == NULL ) { Abc_Print( -1, "Abc_CommandAbc9WriteSim(): Does not have simulation information available.\n" ); return 0; @@ -32624,13 +32985,22 @@ int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "File name is not given on the command line.\n" ); return 1; } - assert( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) == 0 ); - Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPi, Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia) ); + if ( fOutputs ) + { + assert( Vec_WrdSize(pAbc->pGia->vSimsPo) % Gia_ManCoNum(pAbc->pGia) == 0 ); + Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPo, Vec_WrdSize(pAbc->pGia->vSimsPo) / Gia_ManCoNum(pAbc->pGia) ); + } + else + { + assert( Vec_WrdSize(pAbc->pGia->vSimsPi) % Gia_ManCiNum(pAbc->pGia) == 0 ); + Gia_ManSimPatWrite( pArgvNew[0], pAbc->pGia->vSimsPi, Vec_WrdSize(pAbc->pGia->vSimsPi) / Gia_ManCiNum(pAbc->pGia) ); + } return 0; usage: - Abc_Print( -2, "usage: &write_sim [-vh] <file>\n" ); + Abc_Print( -2, "usage: &sim_write [-vh] <file>\n" ); Abc_Print( -2, "\t writes simulation patterns into a file\n" ); + Abc_Print( -2, "\t-o : toggle writing output information [default = %s]\n", fOutputs? "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"); Abc_Print( -2, "\t<file> : file to store the simulation info\n"); @@ -32648,12 +33018,70 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9PrintSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManSimPat( Gia_Man_t * pGia, int nWords, int fVerbose ); - int c, nWords = 4, fVerbose = 0; + extern void Gia_ManSimProfile( Gia_Man_t * pGia ); + int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9PrintSim(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9PrintSim(): This command works only for combinational AIGs.\n" ); + return 0; + } + if ( pAbc->pGia->vSimsPi == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9PrintSim(): Simulation patterns are not defined.\n" ); + return 0; + } + Gia_ManSimProfile( pAbc->pGia ); + return 0; + +usage: + Abc_Print( -2, "usage: &sim_print [-vh]\n" ); + Abc_Print( -2, "\t writes simulation patterns into a file\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"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GenSim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManSimProfile( Gia_Man_t * pGia ); + extern void Gia_ManPatSatImprove( Gia_Man_t * pGia, int nWords, int fVerbose ); + extern void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose ); + extern void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose ); + int c, nWords = 4, nRare = -1, fDist = 0, fSatBased = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "WRsdvh" ) ) != EOF ) { switch ( c ) { @@ -32668,6 +33096,23 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nWords < 0 ) goto usage; break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRare = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRare < 0 ) + goto usage; + break; + case 's': + fSatBased ^= 1; + break; + case 'd': + fDist ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -32679,27 +33124,59 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9SimPat(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GenSim(): There is no AIG.\n" ); return 1; } if ( Gia_ManRegNum(pAbc->pGia) > 0 ) { - Abc_Print( -1, "Abc_CommandAbc9SimPat(): This command works only for combinational AIGs.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GenSim(): This command works only for combinational AIGs.\n" ); return 0; } - if ( pAbc->pGia->vSimsPi == NULL ) + if ( fSatBased ) { - Abc_Print( -1, "Abc_CommandAbc9SimPat(): Does not have simulation information available.\n" ); - return 0; + if ( pAbc->pGia->vSimsPi == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" ); + return 0; + } + Gia_ManPatSatImprove( pAbc->pGia, nWords, fVerbose ); + } + else if ( fDist ) + { + if ( pAbc->pGia->vSimsPi == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" ); + return 0; + } + Gia_ManPatDistImprove( pAbc->pGia, fVerbose ); } - Gia_ManSimPat( pAbc->pGia, nWords, fVerbose ); + else if ( nRare >= 0 ) + { + if ( pAbc->pGia->vSimsPi == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" ); + return 0; + } + Gia_ManPatRareImprove( pAbc->pGia, nRare, fVerbose ); + } + else + { + Abc_Random(1); + Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); + pAbc->pGia->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pAbc->pGia) * nWords ); + printf( "Generated %d random patterns (%d 64-bit data words) for each input of the AIG.\n", 64*nWords, nWords ); + } + Gia_ManSimProfile( pAbc->pGia ); return 0; usage: - Abc_Print( -2, "usage: &simpat [-W num] [-vh]\n" ); - Abc_Print( -2, "\t performs simulation of the AIG\n" ); - Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "usage: &sim_gen [-WR num] [-sdvh]\n" ); + Abc_Print( -2, "\t generates random simulation patterns\n" ); + Abc_Print( -2, "\t-W num : the number of 64-bit words of simulation info [default = %d]\n", nWords ); + Abc_Print( -2, "\t-R num : the rarity parameter used to define scope [default = %d]\n", nRare ); + Abc_Print( -2, "\t-s : toggle using SAT-based improvement of available patterns [default = %s]\n", fSatBased? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle using one improvement of available patterns [default = %s]\n", fDist? "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; } @@ -40191,13 +40668,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ); Gia_Man_t * pTemp; Dch_Pars_t Pars, * pPars = &Pars; - int c, fEquiv = 0; + int c, fMinLevel = 0, fEquiv = 0; // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfrevh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremvh" ) ) != EOF ) { switch ( c ) { @@ -40252,6 +40730,9 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'e': fEquiv ^= 1; break; + case 'm': + fMinLevel ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -40281,12 +40762,17 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Gia_ManEquivReduce( pAbc->pGia, 1, 0, 0, 0 ); } else + { pTemp = Gia_ManPerformDch( pAbc->pGia, pPars ); + Abc_FrameUpdateGia( pAbc, pTemp ); + if ( fMinLevel ) + pTemp = Gia_ManEquivReduce2( pAbc->pGia ); + } Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &dch [-WCS num] [-sptfrevh]\n" ); + Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremvh]\n" ); Abc_Print( -2, "\t computes structural choices using a new approach\n" ); Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -40297,6 +40783,7 @@ usage: Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" ); Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -43382,16 +43869,17 @@ usage: int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); - extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose ); + extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose ); int c, nPars = -1; int nIterLimit = 0; int nConfLimit = 0; int nTimeOut = 0; + int nEncVars = 0; int fDumpCnf = 0; int fGlucose = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdgvh" ) ) != EOF ) { switch ( c ) { @@ -43439,6 +43927,17 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut < 0 ) goto usage; break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nEncVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nEncVars < 0 ) + goto usage; + break; case 'd': fDumpCnf ^= 1; break; @@ -43477,16 +43976,17 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fDumpCnf ) Gia_QbfDumpFile( pAbc->pGia, nPars ); else - Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fGlucose, fVerbose ); + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICT num] [-dgvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICTK num] [-dgvh]\n" ); Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" ); Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars ); Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit ); Abc_Print( -2, "\t-C num : conflict limit per problem [default = %d]\n", nConfLimit ); Abc_Print( -2, "\t-T num : global timeout [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-K num : the number of input bits (for encoding miters only) [default = %d]\n", nEncVars ); Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -43705,6 +44205,75 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9HomoQbf( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_Gen2CreateMiter( int nLutSize, int nLutNum ); + int nLutSize = 2; + int nLutNum = 3; + int fVerbose = 0; + int c; + Gia_Man_t * pTemp; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KNvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLutNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutNum < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pTemp = Gia_Gen2CreateMiter( nLutSize, nLutNum ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &homoqbf [-KN num] [-vh]\n" ); + Abc_Print( -2, "\t generates QBF miter for the encoding problem\n" ); + Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-N num : the number of LUTs [default = %d]\n", nLutNum ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9SatFx( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern int Bmc_FxCompute( Gia_Man_t * p ); @@ -47210,39 +47779,11 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; int nFrames = 5; int fSwitch = 0; int nWords = 1000; int nProcs = 2; -// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); -// extern int Gia_ManSuppSizeTest( Gia_Man_t * p ); -// extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); -// extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); -// extern void Ga2_ManComputeTest( Gia_Man_t * p ); -// extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); -// extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); -// extern void Unr_ManTest( Gia_Man_t * pGia, int nFrames ); -// extern int Gia_ManVerify( Gia_Man_t * pGia ); -// extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p ); -// extern void Gia_ManCollectSeqTest( Gia_Man_t * p ); -// extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); -// extern Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose ); -// extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames ); -// extern void Gia_ManMuxProfiling( Gia_Man_t * p ); -// extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia ); -// extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p ); -// extern Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p ); -// extern Gia_Man_t * Unm_ManTest( Gia_Man_t * pGia ); -// extern void Agi_ManTest( Gia_Man_t * pGia ); -// extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax ); -// extern void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs ); -// extern void Gia_ManTisTest( Gia_Man_t * pInit ); -// extern void Gia_StoComputeCuts( Gia_Man_t * p ); -// extern void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose ); - extern Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName ); - Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "WPFsvh" ) ) != EOF ) { @@ -47298,69 +47839,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); // return 1; // } -/* - if ( pAbc->pCex == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9Test(): There is no CEX.\n" ); - return 1; - } -*/ -// Gia_ManFrontTest( pAbc->pGia ); -// Gia_ManReduceConst( pAbc->pGia, 1 ); -// Sat_ManTest( pAbc->pGia, Gia_ManCo(pAbc->pGia, 0), 0 ); -// Gia_ManTestDistance( pAbc->pGia ); -// Gia_SatSolveTest( pAbc->pGia ); -// For_ManExperiment( pAbc->pGia, 20, 1, 1 ); -// Gia_ManUnrollSpecial( pAbc->pGia, 5, 100, 1 ); -// pAbc->pGia = Gia_ManDupSelf( pTemp = pAbc->pGia ); -// pAbc->pGia = Gia_ManRemoveEnables( pTemp = pAbc->pGia ); -// Cbs_ManSolveTest( pAbc->pGia ); -// pAbc->pGia = Gia_VtaTest( pTemp = pAbc->pGia ); -// Gia_ManStopP( &pTemp ); -// Gia_ManSuppSizeTest( pAbc->pGia ); -// Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); -// Gia_IsoTest( pAbc->pGia, fVerbose ); -// Ga2_ManComputeTest( pAbc->pGia ); -// Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose ); -// Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); -// Unr_ManTest( pAbc->pGia, nFrames ); -// Gia_ManVerifyWithBoxes( pAbc->pGia ); -// Gia_ManCollectSeqTest( pAbc->pGia ); -// pTemp = Gia_ManOptimizeRing( pAbc->pGia ); -// pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// pTemp = Bmc_CexDepthTest( pAbc->pGia, pAbc->pCex, nFrames, fVerbose ); -// pTemp = Bmc_CexTarget( pAbc->pGia, nFrames ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// Gia_ManMuxProfiling( pAbc->pGia ); -// pTemp = Mig_ManTest( pAbc->pGia ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// pTemp = Gia_ManInterTest( pAbc->pGia ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// pTemp = Llb_ReachableStatesGia( pAbc->pGia ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// Unm_ManTest( pAbc->pGia ); -// Agi_ManTest( pAbc->pGia ); -// Gia_ManResubTest( pAbc->pGia ); -// Jf_ManTestCnf( pAbc->pGia ); -// Gia_ManCheckFalseTest( pAbc->pGia, nFrames ); -// Gia_ParTest( pAbc->pGia, nWords, nProcs ); -// Gia_StoComputeCuts( pAbc->pGia ); -// printf( "\nThis command is currently disabled.\n\n" ); -/* - { - char Buffer[10]; - extern void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName ); - sprintf( Buffer, "stats%d.txt", nFrames ); - if ( pAbc->pGia ) - Gia_DumpLutSizeDistrib( pAbc->pGia, Buffer ); - } -*/ -// pTemp = Slv_ManToAig( pAbc->pGia ); -// Abc_FrameUpdateGia( pAbc, pTemp ); -// Extra_TestGia2( pAbc->pGia ); - pTemp = Dau_ConstructAigFromFile( "lib4var2.txt" ); - Abc_FrameUpdateGia( pAbc, pTemp ); +// Abc_FrameUpdateGia( pAbc, Abc_Procedure(pAbc->pGia) ); +// Gia_SimQualityTest( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" ); diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 5dc662d7..d3a19d83 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START #ifdef ABC_USE_CUDD -static void Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +static int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit ); static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st__table * tBdd2Node ); @@ -129,12 +129,18 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd0, void * bFunc, char * pNamePo, Vec_ SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal ) +Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit ) { Abc_Ntk_t * pNtkNew; pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); if ( fGlobal ) - Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew ); + { + if ( !Abc_NtkBddToMuxesPerformGlo( pNtk, pNtkNew, Limit ) ) + { + Abc_NtkDelete( pNtkNew ); + return NULL; + } + } else { Abc_NtkBddToMuxesPerform( pNtk, pNtkNew ); @@ -259,17 +265,17 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * SeeAlso [] ***********************************************************************/ -void Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +int Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int Limit ) { DdManager * dd; Abc_Obj_t * pObj, * pObjNew; int i; st__table * tBdd2Node; assert( Abc_NtkIsStrash(pNtk) ); - dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, 0 ); + dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, Limit, 1, 1, 0, 0 ); if ( dd == NULL ) { printf( "Construction of global BDDs has failed.\n" ); - return; + return 0; } //printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); @@ -292,6 +298,7 @@ void Abc_NtkBddToMuxesPerformGlo( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) Abc_NtkFreeGlobalBdds( pNtk, 0 ); Extra_StopManager( dd ); Abc_NtkCleanCopy( pNtk ); + return 1; } /**Function************************************************************* @@ -655,7 +662,7 @@ ABC_PRT( "Time", Abc_Clock() - clk ); #else double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) { return 0.0; } -Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal ) { return NULL; } +Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk, int fGlobal, int Limit ) { return NULL; } #endif diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index aa67ad74..5ddd25f1 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -195,8 +195,6 @@ clkV = Abc_Clock() - clkV; ABC_PRT( "Syn", clkS ); // ABC_PRT( "Ver", clkV ); } - if ( nIters+1 == nItersMax ) - break; } Abc_NtkDelete( pNtkSyn ); // report the results @@ -206,12 +204,10 @@ clkV = Abc_Clock() - clkV; printf( "Parameters: " ); Abc_NtkVectorPrintPars( vPiValues, nPars ); printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(vPiValues) - nZeros ); - printf( "Solved after %d interations. ", nIters ); + printf( "Solved after %d iterations. ", nIters ); } else if ( nIters == nItersMax ) - printf( "Unsolved after %d interations. ", nIters ); - else if ( nIters == nItersMax ) - printf( "Quit after %d interatios. ", nItersMax ); + printf( "Quit after %d iterations. ", nItersMax ); else printf( "Implementation does not exist. " ); ABC_PRT( "Total runtime", Abc_Clock() - clkTotal ); diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 9323f9e7..b8934e23 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -650,14 +650,12 @@ Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, eNode0, eNode1; - assert( pObj0 != pObj1 ); - assert( !Abc_ObjIsComplement(pObj0) ); - assert( !Abc_ObjIsComplement(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); pGraph = Dec_GraphCreate( 2 ); - Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; - Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; - eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); if ( fOrGate ) eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); else @@ -683,17 +681,16 @@ Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_ { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, eNode0, eNode1, eNode2; - assert( pObj0 != pObj1 ); - assert( !Abc_ObjIsComplement(pObj0) ); - assert( !Abc_ObjIsComplement(pObj1) ); - assert( !Abc_ObjIsComplement(pObj2) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) ); + assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) ); pGraph = Dec_GraphCreate( 3 ); - Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; - Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; - Dec_GraphNode( pGraph, 2 )->pFunc = pObj2; - eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); - eNode2 = Dec_EdgeCreate( 2, pObj2->fPhase ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) ); if ( fOrGate ) { eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); @@ -725,15 +722,14 @@ Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2; - assert( pObj0 != pObj1 ); - assert( pObj0 != pObj2 ); - assert( pObj1 != pObj2 ); - assert( !Abc_ObjIsComplement(pObj0) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) ); + assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) ); pGraph = Dec_GraphCreate( 3 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); - eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) { eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ); @@ -771,8 +767,8 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3; - assert( pObj0 != pObj1 ); - assert( pObj2 != pObj3 ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj2) != Abc_ObjRegular(pObj3) ); pGraph = Dec_GraphCreate( 4 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); @@ -840,6 +836,7 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t ***********************************************************************/ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) { + int fMoreDivs = 1; // bug fix by Siang-Yun Lee Abc_Obj_t * pObj; unsigned * puData, * puDataR; int i, w; @@ -863,6 +860,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs1UP, pObj ); continue; } + if ( fMoreDivs ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( ~puData[w] & ~puDataR[w] ) + if ( ~puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs1UP, Abc_ObjNot(pObj) ); + continue; + } + } // check negative containment for ( w = 0; w < p->nWords; w++ ) // if ( ~puData[w] & puDataR[w] ) @@ -873,6 +882,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs1UN, pObj ); continue; } + if ( fMoreDivs ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( puData[w] & puDataR[w] ) + if ( puData[w] & puDataR[w] & p->pCareSet[w] ) // care set + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs1UN, Abc_ObjNot(pObj) ); + continue; + } + } // add the node to binates Vec_PtrPush( p->vDivs1B, pObj ); } @@ -1081,14 +1102,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | puData1[w]) != puDataR[w] ) - if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } if ( w == p->nWords ) { p->nUsedNode1Or++; @@ -1099,14 +1144,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & puData1[w]) != puDataR[w] ) - if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + if ( Abc_ObjIsComplement(pObj0) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } if ( w == p->nWords ) { p->nUsedNode1And++; @@ -1137,31 +1206,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj2, j, k + 1 ) { - puData2 = (unsigned *)pObj2->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) - if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else assert( 0 ); if ( w == p->nWords ) { - LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) ); + LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) ); assert( LevelMax <= Required - 1 ); pObjMax = NULL; - if ( (int)pObj0->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax ) pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; - if ( (int)pObj1->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; } - if ( (int)pObj2->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; @@ -1178,31 +1300,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj2, j, k + 1 ) { - puData2 = (unsigned *)pObj2->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) - if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else assert( 0 ); if ( w == p->nWords ) { - LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) ); + LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) ); assert( LevelMax <= Required - 1 ); pObjMax = NULL; - if ( (int)pObj0->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax ) pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; - if ( (int)pObj1->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; } - if ( (int)pObj2->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; @@ -1239,40 +1414,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj1, k ) { pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k ); puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; - if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj1) ) + if ( Abc_ObjIsComplement(pObj0) ) { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } - else + else { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } if ( w == p->nWords ) { @@ -1284,40 +1493,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj1, k ) { pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UN1, k ); puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; - if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj1) ) + if ( Abc_ObjIsComplement(pObj0) ) { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } - else + else { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } if ( w == p->nWords ) { @@ -1472,6 +1715,7 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) } } } + /* // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj0, i ) @@ -1493,85 +1737,85 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) { case 0: // 0000 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 1: // 0001 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 2: // 0010 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 3: // 0011 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 4: // 0100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 5: // 0101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 6: // 0110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 7: // 0111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 8: // 1000 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 9: // 1001 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 10: // 1010 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 11: // 1011 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 12: // 1100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 13: // 1101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 14: // 1110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 15: // 1111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h index 36300efd..9aed414c 100644 --- a/src/base/acb/acb.h +++ b/src/base/acb/acb.h @@ -1028,6 +1028,8 @@ extern void Acb_NtkPrintNode( Acb_Ntk_t * p, int iObj ); extern int Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp ); extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ); +extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW ); + ABC_NAMESPACE_HEADER_END diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c index 9c2db080..cea89809 100644 --- a/src/base/acb/acbAbc.c +++ b/src/base/acb/acbAbc.c @@ -167,6 +167,7 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames Acb_Man_t * pMan = Acb_ManAlloc( pFileName, 1, Abc_NamRef(pNames), NULL, NULL, NULL ); int k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, pMan->pName, NULL ); int Mod = 2, Obj, Type, nArray, * pArray, ObjId; + int Token0 = Abc_NamStrFind( pMan->pStrs, "1\'b0" ); Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Ndr_DataCiNum(p, Mod), Ndr_DataCoNum(p, Mod), Ndr_DataObjNum(p, Mod) ); Vec_Int_t * vMap = Vec_IntStart( nNameIdMax ); Acb_NtkCleanObjWeights( pNtk ); @@ -198,20 +199,30 @@ 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 ); + int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT ); + char * 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++ ) + { + if ( Vec_IntEntry(vMap, pArray[k]) == 0 ) + printf( "Cannot find fanin %d of node \"%s\".\n", k, pName ); Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) ); + } Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 ); } Ndr_ModForEachPo( p, Mod, Obj ) { + int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT ); + char * pName = Abc_NamStr( pMan->pStrs, NameId ); nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray ); assert( nArray == 1 ); ObjId = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 ); + if ( Vec_IntEntry(vMap, pArray[0]) == 0 ) + { + printf( "Adding constant 0 driver to non-driven PO \"%s\".\n", pName ); + Vec_IntWriteEntry( vMap, pArray[0], Token0 ); + } Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[0]) ); Acb_ObjSetName( pNtk, ObjId, pArray[0] ); } diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index 6ffeb0e8..8f72a00f 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 @@ -187,15 +189,30 @@ Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames ) { Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 ); char * pBuffer = Extra_FileReadContents( pFileName ); - char * pToken; + char * pToken, * pStart, * pLimit = pBuffer + strlen(pBuffer); if ( pBuffer == NULL ) return NULL; Acb_VerilogRemoveComments( pBuffer ); - pToken = strtok( pBuffer, " \n\r\t()," ); + pToken = strtok( pBuffer, " \n\r\t(),;=" ); while ( pToken ) { - Vec_IntPush( vBuffer, Abc_NamStrFindOrAdd(pNames, pToken, NULL) ); - pToken = strtok( NULL, " \n\r\t(),;" ); + int iToken = Abc_NamStrFindOrAdd( pNames, pToken, NULL ); + if ( !strcmp(pToken, "assign") ) + Vec_IntPush( vBuffer, ACB_BUF ); + else + Vec_IntPush( vBuffer, iToken ); + if ( iToken >= ACB_BUF && iToken < ACB_UNUSED ) + { + for ( pStart = pToken; pStart < pLimit && *pStart != '\n'; pStart++ ) + if ( *pStart == '(' ) + break; + if ( *pStart == '(' ) + { + pToken = strtok( pStart, " \n\r\t(),;=" ); + continue; + } + } + pToken = strtok( NULL, " \n\r\t(),;=" ); } ABC_FREE( pBuffer ); return vBuffer; @@ -230,12 +247,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)); + //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++; + //if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' ) + // i++; } else Vec_IntPush( vCur, Token ); @@ -243,7 +260,7 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) Vec_IntPush( vTypes, -1 ); Vec_IntPush( vTypes, Vec_IntSize(vFanins) ); // create design - pDesign = Ndr_Create( Vec_IntEntry(vBuffer, 1) ); + pDesign = (Ndr_Data_t *)Ndr_Create( Vec_IntEntry(vBuffer, 1) ); ModuleID = Ndr_AddModule( pDesign, Vec_IntEntry(vBuffer, 1) ); // create inputs Ndr_DataResize( pDesign, Vec_IntSize(vInputs) ); @@ -480,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) ) @@ -562,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 @@ -726,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 ); @@ -791,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 ) { @@ -889,11 +909,16 @@ Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * 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++; } @@ -983,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; } @@ -1085,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; @@ -1094,26 +1120,22 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig vSuppBest = Vec_IntDup( vSuppStart ); printf( "Starting cost = %d.\n", CostBest ); - // interatively find the one with the most ones in the uncovered rows - for ( Iter = 0; Iter < 200; Iter++ ) + // iteratively find the one with the most ones in the uncovered rows + 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 ); @@ -1122,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; } @@ -1878,13 +1900,31 @@ Vec_Ptr_t * Acb_GenerateSignalNames( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars ) { extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops ); - extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias ); - Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate; + extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti ); + Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate; 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 ); @@ -1940,9 +1980,146 @@ 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; +} + +/**Function************************************************************* + + Synopsis [Patch generation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Acb_GenerateInstance2( Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts ) +{ + char * pName; int i; + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Vec_StrAppend( vStr, " patch p0 (" ); + Vec_PtrForEachEntry( char *, vOuts, pName, i ) + Vec_StrPrintF( vStr, "%s .%s(t%d_%s)", i ? ",":"", pName, i, pName ); + Vec_PtrForEachEntry( char *, vIns, pName, i ) + Vec_StrPrintF( vStr, ", .%s(%s)", pName, pName ); + Vec_StrAppend( vStr, " );\n\n" ); + Vec_StrPush( vStr, '\0' ); + return vStr; +} +Vec_Ptr_t * Acb_GenerateSignalNames2( Vec_Wec_t * vGates, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts ) +{ + int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts); + int nNodes = Vec_WecSize(vGates) - nIns - nOuts; + Vec_Ptr_t * vRes = Vec_PtrStart( Vec_WecSize(vGates) ); char * pName; + Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, nWires = 1; + // create input names + Vec_PtrForEachEntry( char *, vIns, pName, i ) + Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(pName) ); + // create names for nodes driving outputs + Vec_PtrForEachEntry( char *, vOuts, pName, i ) + { + Vec_Int_t * vGate = Vec_WecEntry( vGates, nIns + nNodes + i ); + assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF ); + Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(pName) ); + } + for ( i = nIns; i < nIns + nNodes; i++ ) + if ( Vec_PtrEntry(vRes, i) == NULL ) + { + Vec_StrPrintF( vStr, "ww%d", nWires++ ); + Vec_StrPush( vStr, '\0' ); + Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) ); + } + Vec_StrFree( vStr ); + return vRes; +} +Vec_Str_t * Acb_GeneratePatch2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts ) +{ + extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias, Gia_Man_t * pMulti ); + Vec_Wec_t * vGates = Abc_GiaSynthesize( NULL, pGia ); Vec_Int_t * vGate; + int nIns = Vec_PtrSize(vIns), nOuts = Vec_PtrSize(vOuts); char * pName; + int i, k, iObj, nWires = Vec_WecSize(vGates) - nIns - nOuts, fFirst = 1; + Vec_Ptr_t * vNames = Acb_GenerateSignalNames2( vGates, vIns, vOuts ); + + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Vec_StrAppend( vStr, "module patch (" ); + + Vec_PtrForEachEntry( char *, vOuts, pName, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName ); + Vec_PtrForEachEntry( char *, vIns, pName, i ) + Vec_StrPrintF( vStr, ", %s", pName ); + Vec_StrAppend( vStr, " );\n\n" ); + + Vec_StrAppend( vStr, " output" ); + Vec_PtrForEachEntry( char *, vOuts, pName, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName ); + Vec_StrAppend( vStr, ";\n" ); + + Vec_StrAppend( vStr, " input" ); + Vec_PtrForEachEntry( char *, vIns, pName, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", pName ); + Vec_StrAppend( vStr, ";\n" ); + + if ( nWires > nOuts ) + { + Vec_StrAppend( vStr, " wire" ); + for ( i = 0; i < nWires; i++ ) + { + char * pName = (char *)Vec_PtrEntry( vNames, nIns+i ); + if ( !strncmp(pName, "ww", 2) ) + Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0; + } + Vec_StrAppend( vStr, ";\n\n" ); + } + + // create internal nodes + Vec_WecForEachLevelStartStop( vGates, vGate, i, nIns, nIns+nWires ) + { + if ( Vec_IntSize(vGate) > 2 ) + { + Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) ); + Vec_IntForEachEntryStart( vGate, iObj, k, 1 ) + Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) ); + Vec_StrAppend( vStr, " );\n" ); + } + else + { + assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T ); + 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, " );\n" ); + } + } + Vec_StrAppend( vStr, "\nendmodule\n\n" ); + Vec_StrPush( vStr, '\0' ); + Vec_PtrFreeFree( vNames ); + Vec_WecFree( vGates ); + + printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", nIns, nOuts, nWires ); return vStr; } +void Acb_GenerateFile2( Gia_Man_t * pGia, Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts, char * pFileName, char * pFileNameOut ) +{ + extern void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch ); + extern void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch ); + extern void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber ); + Vec_Str_t * vInst = Acb_GenerateInstance2( vIns, vOuts ); + Vec_Str_t * vPatch = Acb_GeneratePatch2( pGia, vIns, vOuts ); + //printf( "%s", Vec_StrArray(vPatch) ); + //Gia_AigerWrite( pGia, "test.aig", 0, 0, 0 ); + // generate output files + Acb_GenerateFilePatch( vPatch, "patch.v" ); + printf( "Finished dumping patch file \"%s\".\n", "patch.v" ); + Acb_NtkInsert( pFileName, "temp.v", vOuts, 0 ); + printf( "Finished dumping intermediate file \"%s\".\n", "temp.v" ); + Acb_GenerateFileOut( vInst, "temp.v", pFileNameOut, vPatch ); + printf( "Finished dumping the resulting file \"%s\".\n", pFileNameOut ); + Vec_StrFree( vInst ); + Vec_StrFree( vPatch ); +} /**Function************************************************************* @@ -2328,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 ); @@ -2364,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 ) { @@ -2458,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 ); @@ -2468,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 ); @@ -2501,7 +2681,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4] // generate output files if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" ); - Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch ); + Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : (char *)"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: @@ -2557,7 +2737,6 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose ) Acb_IntallLibrary(); } - /**Function************************************************************* Synopsis [Top level procedure.] @@ -2569,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 fRandom, 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 ) @@ -2578,23 +2758,36 @@ void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ) //int * pArray = Vec_IntArray( &pNtkF->vTargets ); //ABC_SWAP( int, pArray[7], pArray[4] ); //Vec_IntReverseOrder( &pNtkF->vTargets ); - //Vec_IntPermute( &pNtkF->vTargets ); - //Vec_IntPrint( &pNtkF->vTargets ); + if ( fRandom ) + { + printf( "Permuting targets as follows: " ); + Vec_IntPermute( &pNtkF->vTargets ); + Vec_IntPrint( &pNtkF->vTargets ); + } assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) ); assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) ); 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 ); + printf( "\n" ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/acb/acbTest.c b/src/base/acb/acbTest.c new file mode 100644 index 00000000..fa632ca0 --- /dev/null +++ b/src/base/acb/acbTest.c @@ -0,0 +1,55 @@ +/**CFile**************************************************************** + + FileName [acbTest.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Hierarchical word-level netlist.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 21, 2015.] + + Revision [$Id: acbTest.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acb.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose ) +{ +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index 001a137b..2243541b 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -20,6 +20,7 @@ #include "acb.h" #include "base/abc/abc.h" +#include "base/io/ioAbc.h" ABC_NAMESPACE_IMPL_START @@ -27,6 +28,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -502,7 +504,7 @@ Vec_Int_t * Acb_NtkFindNodes2( Acb_Ntk_t * p ) 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 ) +int Acb_ObjToGia2( Gia_Man_t * pNew, int fUseBuf, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp, int fUseXors ) { //char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) ); int * pFanin, iFanin, k, Type, Res; @@ -518,10 +520,11 @@ int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp 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_BUF || Type == ABC_OPER_BIT_INV ) + { + Res = fUseBuf ? Gia_ManAppendBuf(pNew, Vec_IntEntry(vTemp, 0)) : Vec_IntEntry(vTemp, 0); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_INV ); + } if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND ) { Res = 1; @@ -540,13 +543,13 @@ int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp { Res = 0; Vec_IntForEachEntry( vTemp, iFanin, k ) - Res = Gia_ManAppendXor2( pNew, Res, iFanin ); + Res = fUseXors ? Gia_ManAppendXorReal2(pNew, Res, iFanin) : 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 * Acb_NtkToGia2( Acb_Ntk_t * p, int fUseBuf, int fUseXors, Vec_Int_t * vTargets, int nTargets ) { Gia_Man_t * pNew, * pOne; Vec_Int_t * vFanins, * vNodes; @@ -556,10 +559,17 @@ Gia_Man_t * Acb_NtkToGia2( Acb_Ntk_t * p ) Acb_NtkCleanObjCopies( p ); Acb_NtkForEachCi( p, iObj, i ) Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) ); + if ( vTargets ) + Vec_IntForEachEntry( vTargets, iObj, i ) + Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) ); + else + for ( i = 0; i < nTargets; i++ ) + 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) ); + if ( Acb_ObjCopy(p, iObj) == -1 ) // skip targets assigned above + Acb_ObjSetCopy( p, iObj, Acb_ObjToGia2(pNew, fUseBuf, p, iObj, vFanins, fUseXors) ); Vec_IntFree( vNodes ); Vec_IntFree( vFanins ); Acb_NtkForEachCo( p, iObj, i ) @@ -581,13 +591,19 @@ Gia_Man_t * Acb_NtkToGia2( Acb_Ntk_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR ) +Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR, Vec_Bit_t ** pvPolar ) { - int i, iObj, iLit; + int i, iObj, iLit, nTargets = Vec_IntSize(&p->vTargets); 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_Bit_t * vDriver = Vec_BitStart( Gia_ManObjNum(pGia) ); + Vec_Bit_t * vPolar = Vec_BitStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCiId( pGia, iObj, i ) + if ( i < Gia_ManCiNum(pGia) - nTargets ) + Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Acb_ObjNameStr(p, Acb_NtkCi(p, i))) ); + else + Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Acb_ObjNameStr(p, Vec_IntEntry(&p->vTargets, i-(Gia_ManCiNum(pGia) - nTargets)))) ); Gia_ManForEachCoId( pGia, iObj, i ) { Vec_BitWriteEntry( vDriver, Gia_ObjFaninId0(Gia_ManObj(pGia, iObj), iObj), 1 ); @@ -601,12 +617,14 @@ Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** { Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) ); Vec_IntPush( vNodes, Abc_Lit2Var(iLit) ); + Vec_BitWriteEntry( vPolar, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); } } Vec_BitFree( vDriver ); Vec_IntFree( vObjs ); Vec_IntSort( vNodes, 0 ); *pvNodesR = vNodesR; + *pvPolar = vPolar; return vNodes; } Vec_Int_t * Acb_NtkCollectUser( Acb_Ntk_t * p, Vec_Ptr_t * vUser ) @@ -642,23 +660,23 @@ Vec_Int_t * Acb_NtkCollectUser( Acb_Ntk_t * p, Vec_Ptr_t * vUser ) 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 ) +int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVerbose, + Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, int fUseBuf, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR, Vec_Bit_t ** pvPolar ) { - 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; + int RetValue = -1; if ( pNtkF && pNtkG ) { - Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF ); - Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG ); + int nTargets = Vec_IntSize(&pNtkF->vTargets); + Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF, fUseBuf, fUseXors, &pNtkF->vTargets, 0 ); + Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG, 0, 0, NULL, nTargets ); 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; + *pvNodes = Acb_NtkCollectCopies( pNtkF, pGiaF, pvNodesR, pvPolar ); + RetValue = nTargets; } if ( pNtkF ) Acb_ManFree( pNtkF->pDesign ); if ( pNtkG ) Acb_ManFree( pNtkG->pDesign ); @@ -676,9 +694,120 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fVerbose, SeeAlso [] ***********************************************************************/ +Vec_Int_t * Abc_NtkCollectCopies( Abc_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR, Vec_Bit_t ** pvPolar ) +{ + int i, iObj, iLit; + Abc_Obj_t * pObj; + Vec_Ptr_t * vObjs = Abc_NtkDfs( p, 0 ); + Vec_Int_t * vNodes = Vec_IntAlloc( Abc_NtkObjNumMax(p) ); + Vec_Ptr_t * vNodesR = Vec_PtrStart( Gia_ManObjNum(pGia) ); + Vec_Bit_t * vDriver = Vec_BitStart( Gia_ManObjNum(pGia) ); + Vec_Bit_t * vPolar = Vec_BitStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCiId( pGia, iObj, i ) + Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Abc_ObjName(Abc_NtkCi(p, i))) ); + Gia_ManForEachCoId( pGia, iObj, i ) + { + Vec_BitWriteEntry( vDriver, Gia_ObjFaninId0(Gia_ManObj(pGia, iObj), iObj), 1 ); + Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Abc_ObjName(Abc_NtkCo(p, i))) ); + Vec_IntPush( vNodes, iObj ); + } + Vec_PtrForEachEntry( Abc_Obj_t *, vObjs, pObj, i ) + if ( (iLit = pObj->iTemp) >= 0 && Gia_ObjIsAnd(Gia_ManObj(pGia, Abc_Lit2Var(iLit))) ) + { + if ( !Vec_BitEntry(vDriver, Abc_Lit2Var(iLit)) && Vec_PtrEntry(vNodesR, Abc_Lit2Var(iLit)) == NULL ) + { + Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Abc_ObjName(pObj)) ); + Vec_IntPush( vNodes, Abc_Lit2Var(iLit) ); + Vec_BitWriteEntry( vPolar, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); + } + } + Vec_BitFree( vDriver ); + Vec_PtrFree( vObjs ); + Vec_IntSort( vNodes, 0 ); + *pvNodesR = vNodesR; + *pvPolar = vPolar; + return vNodes; +} +int Abc_ObjToGia2( Gia_Man_t * pNew, Abc_Ntk_t * p, Abc_Obj_t * pObj, Vec_Int_t * vTemp, int fUseXors ) +{ + Abc_Obj_t * pFanin; int k; + assert( Abc_ObjIsNode(pObj) ); + Vec_IntClear( vTemp ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( pFanin->iTemp >= 0 ); + Vec_IntPush( vTemp, pFanin->iTemp ); + } + if ( Abc_ObjFaninNum(pObj) == 0 ) + return Abc_SopIsConst0( (char*)pObj->pData ) ? 0 : 1; + if ( Abc_ObjFaninNum(pObj) == 1 ) + return Abc_SopIsBuf( (char*)pObj->pData ) ? Vec_IntEntry(vTemp, 0) : Abc_LitNot(Vec_IntEntry(vTemp, 0)); + if ( Abc_ObjFaninNum(pObj) == 2 ) // nand2 + return Abc_LitNot( Gia_ManAppendAnd2( pNew, Vec_IntEntry(vTemp, 0), Vec_IntEntry(vTemp, 1) ) ); + assert( 0 ); + return -1; +} +Gia_Man_t * Abc_NtkToGia2( Abc_Ntk_t * p, int fUseXors ) +{ + Gia_Man_t * pNew, * pOne; + Vec_Int_t * vFanins; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; int i; + pNew = Gia_ManStart( 2 * Abc_NtkObjNumMax(p) + 1000 ); + pNew->pName = Abc_UtilStrsav(Abc_NtkName(p)); + Abc_NtkForEachObj( p, pObj, i ) + pObj->iTemp = -1; + Abc_NtkForEachCi( p, pObj, i ) + pObj->iTemp = Gia_ManAppendCi(pNew); + vFanins = Vec_IntAlloc( 4 ); + vNodes = Abc_NtkDfs( p, 0 ); + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + pObj->iTemp = Abc_ObjToGia2(pNew, p, pObj, vFanins, fUseXors); + Vec_PtrFree( vNodes ); + Vec_IntFree( vFanins ); + Abc_NtkForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Abc_ObjFanin0(pObj)->iTemp ); + pNew = Gia_ManCleanup( pOne = pNew ); + //Gia_ManUpdateCopy( &p->vObjCopy, pOne ); + Gia_ManStop( pOne ); + return pNew; +} +int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVerbose, + Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR, Vec_Bit_t ** pvPolar ) +{ + Abc_Ntk_t * pNtkF = Io_Read( pFileName0, Io_ReadFileType(pFileName0), 1, 0 ); + Abc_Ntk_t * pNtkG = Io_Read( pFileName1, Io_ReadFileType(pFileName1), 1, 0 ); + int RetValue = -1; + if ( pNtkF && pNtkG ) + { + Gia_Man_t * pGiaF = Abc_NtkToGia2( pNtkF, fUseXors ); + Gia_Man_t * pGiaG = Abc_NtkToGia2( pNtkG, 0 ); + assert( Abc_NtkCiNum(pNtkF) == Abc_NtkCiNum(pNtkG) ); + assert( Abc_NtkCoNum(pNtkF) == Abc_NtkCoNum(pNtkG) ); + *ppGiaF = pGiaF; + *ppGiaG = pGiaG; + *pvNodes = Abc_NtkCollectCopies( pNtkF, pGiaF, pvNodesR, pvPolar ); + RetValue = 0; + } + if ( pNtkF ) Abc_NtkDelete( pNtkF ); + if ( pNtkG ) Abc_NtkDelete( pNtkG ); + 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; + Vec_Int_t * vPlaces; int First = 1, Pos = -1, fComment = 0; char * pTemp, * pBuffer = Extra_FileReadContents( pFileName ); char * pLimit = pBuffer + strlen(pBuffer); if ( pBuffer == NULL ) @@ -687,6 +816,13 @@ Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames ) for ( pTemp = pBuffer; *pTemp; pTemp++ ) { if ( *pTemp == '\n' ) + fComment = 0; + if ( *pTemp == '/' && *(pTemp + 1) == '/' ) + fComment = 1; + if ( fComment ) + continue; + + if ( *pTemp == '\n' ) Pos = pTemp - pBuffer + 1; else if ( *pTemp == '(' ) { @@ -710,7 +846,7 @@ Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames ) ABC_FREE( pBuffer ); return vPlaces; } -void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames ) +void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames, int fNumber ) { int i, k, Prev = 0, Pos, Pos2, iObj; Vec_Int_t * vPlaces; @@ -743,11 +879,27 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames 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 ? ";" : "," ); + if ( fNumber ) + { + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " t_%d%s", i, i==Vec_PtrSize(vNames)-1 ? ";" : "," ); + } + else + { + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " t%d_%s%s", i, pName, i==Vec_PtrSize(vNames)-1 ? ";" : "," ); + } fprintf( pFile, "\n\n" ); - Vec_PtrForEachEntry( char *, vNames, pName, i ) - fprintf( pFile, " buf( %s, t_%d );\n", pName, i ); + if ( fNumber ) + { + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " buf( %s, t_%d );\n", pName, i ); + } + else + { + Vec_PtrForEachEntry( char *, vNames, pName, i ) + fprintf( pFile, " buf( %s, t%d_%s );\n", pName, i, pName ); + } fprintf( pFile, "\n" ); for ( k = Pos2; pBuffer[k]; k++ ) fputc( pBuffer[k], pFile ); @@ -760,21 +912,114 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose ) +void Acb_Ntk4CollectAdd( Acb_Ntk_t * pNtk, int iObj, Vec_Int_t * vRes, Vec_Int_t * vDists, int Dist ) +{ + if ( Acb_ObjSetTravIdCur(pNtk, iObj) ) + return; + Vec_IntWriteEntry( vDists, iObj, Dist ); + Vec_IntPush( vRes, iObj ); +} +void Acb_Ntk4CollectRing( Acb_Ntk_t * pNtk, Vec_Int_t * vStart, Vec_Int_t * vRes, Vec_Int_t * vDists ) +{ + int i, iObj; + Vec_IntForEachEntry( vStart, iObj, i ) + { + int k, iFanin, * pFanins, Weight = Vec_IntEntry(vDists, iObj); + Acb_ObjForEachFaninFast( pNtk, iObj, pFanins, iFanin, k ) + Acb_Ntk4CollectAdd( pNtk, iFanin, vRes, vDists, Weight + 1*(Acb_ObjFaninNum(pNtk, iObj) > 1) ); + Acb_ObjForEachFanout( pNtk, iObj, iFanin, k ) + Acb_Ntk4CollectAdd( pNtk, iFanin, vRes, vDists, Weight + 2*(Acb_ObjFaninNum(pNtk, iObj) > 1) ); + } +} +void Acb_Ntk4DumpWeightsInt( Acb_Ntk_t * pNtk, Vec_Int_t * vObjs, char * pFileName ) +{ + int i, iObj;//, Weight; + Vec_Int_t * vDists, * vStart, * vNexts; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Canont open input file \"%s\".\n", pFileName ); + return; + } + vStart = Vec_IntAlloc( 100 ); + vNexts = Vec_IntAlloc( 100 ); + vDists = Vec_IntStart( Acb_NtkObjNumMax(pNtk) ); + Acb_NtkIncTravId( pNtk ); + Vec_IntForEachEntry( vObjs, iObj, i ) + { + Acb_ObjSetTravIdCur(pNtk, iObj); + Vec_IntWriteEntry( vDists, iObj, 1 ); + Vec_IntPush( vStart, iObj ); + } + while ( 1 ) + { + Acb_Ntk4CollectRing( pNtk, vStart, vNexts, vDists ); + if ( Vec_IntSize(vNexts) == 0 ) + break; + Vec_IntClear( vStart ); + ABC_SWAP( Vec_Int_t, *vStart, *vNexts ); + } + Vec_IntFree( vStart ); + Vec_IntFree( vNexts ); + // create weights +// Vec_IntForEachEntry( vDists, Weight, i ) +// if ( Weight && Acb_ObjNameStr(pNtk, i)[0] != '1' ) +// fprintf( pFile, "%s %d\n", Acb_ObjNameStr(pNtk, i), 10000+Weight ); + Acb_NtkForEachObj( pNtk, iObj ) + { + char * pName = Acb_ObjNameStr(pNtk, iObj); + int Weight = Vec_IntEntry(vDists, iObj); + if ( Weight == 0 ) + Weight = 10000; + fprintf( pFile, "%s %d\n", pName, 100000+Weight ); + } + + Vec_IntFree( vDists ); + fclose( pFile ); +} +void Acb_Ntk4DumpWeights( char * pFileNameIn, Vec_Ptr_t * vObjNames, char * pFileName ) { - extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, 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, nBeam, LevL, LevU, fOrder, fFancy, fVerbose ) ) - Acb_NtkRunEco( pFileNames, 1, fVerbose ); + char * pName; int i, iObj; + Vec_Int_t * vObjs = Vec_IntAlloc( Vec_PtrSize(vObjNames) ); + Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNameIn, NULL ); + Acb_NtkCreateFanout( pNtkF ); + Vec_PtrForEachEntry( char *, vObjNames, pName, i ) + { + Acb_NtkForEachObj( pNtkF, iObj ) + if ( !strcmp(Acb_ObjNameStr(pNtkF, iObj), pName) ) + Vec_IntPush( vObjs, iObj ); + } + Acb_Ntk4DumpWeightsInt( pNtkF, vObjs, pFileName ); + Acb_ManFree( pNtkF->pDesign ); + Vec_IntFree( vObjs ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, 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 fRandom, int fVerbose, int fVeryVerbose ); + char * pFileNames[4] = { pFileName[2], pFileName[1], fUseWeights ? (char *)"weights.txt" : NULL, pFileName[2] }; + if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ) ) + Acb_NtkRunEco( pFileNames, 1, fRandom, fVerbose, fVeryVerbose ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/acb/module.make b/src/base/acb/module.make index 46294f9f..ec78b3b0 100644 --- a/src/base/acb/module.make +++ b/src/base/acb/module.make @@ -5,4 +5,5 @@ SRC += src/base/acb/acbAbc.c \ src/base/acb/acbMfs.c \ src/base/acb/acbPush.c \ src/base/acb/acbSets.c \ + src/base/acb/acbTest.c \ src/base/acb/acbUtil.c diff --git a/src/base/cmd/cmdApi.c b/src/base/cmd/cmdApi.c index 2ee10229..73ebcf89 100644 --- a/src/base/cmd/cmdApi.c +++ b/src/base/cmd/cmdApi.c @@ -125,7 +125,7 @@ int Cmd_CommandHandleSpecial( Abc_Frame_t * pAbc, const char * sCommand ) if ( strstr(sCommand, "#ASSERT") ) { int Status = 0; - char * pNumb = strrchr( sCommand, '=' ); + char * pNumb = strrchr( (char *)sCommand, '=' ); if ( strstr(sCommand, "_PI_") ) { piCount = pNumb ? atoi(pNumb+1) : 0; diff --git a/src/base/io/io.c b/src/base/io/io.c index 49e1def1..a5cffbf4 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -231,6 +231,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) sprintf( Command, "read_constr %s", pFileName ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "c" ) ) sprintf( Command, "so %s", pFileName ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "script" ) ) + sprintf( Command, "so %s", pFileName ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) ) sprintf( Command, "dsd_load %s", pFileName ); if ( Command[0] ) diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c index 7f5f13a8..d85d7b67 100644 --- a/src/base/main/mainInit.c +++ b/src/base/main/mainInit.c @@ -55,6 +55,8 @@ extern void Cba_Init( Abc_Frame_t * pAbc ); extern void Cba_End( Abc_Frame_t * pAbc ); extern void Pla_Init( Abc_Frame_t * pAbc ); extern void Pla_End( Abc_Frame_t * pAbc ); +extern void Sim_Init( Abc_Frame_t * pAbc ); +extern void Sim_End( Abc_Frame_t * pAbc ); extern void Test_Init( Abc_Frame_t * pAbc ); extern void Test_End( Abc_Frame_t * pAbc ); extern void Abc2_Init( Abc_Frame_t * pAbc ); @@ -115,6 +117,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc ) Bac_Init( pAbc ); Cba_Init( pAbc ); Pla_Init( pAbc ); + Sim_Init( pAbc ); Test_Init( pAbc ); Glucose_Init( pAbc ); for( p = s_InitializerStart ; p ; p = p->next ) @@ -154,6 +157,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc ) Bac_End( pAbc ); Cba_End( pAbc ); Pla_End( pAbc ); + Sim_End( pAbc ); Test_End( pAbc ); Glucose_End( pAbc ); } diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 180ec447..be099be4 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -145,8 +145,8 @@ int Abc_RealMain( int argc, char * argv[] ) } case 'l': { #ifndef WIN32 - int maxTime = atoi(globalUtilOptarg); - printf("Limiting time to %d seconds\n", maxTime); + rlim_t maxTime = atoi(globalUtilOptarg); + printf("Limiting time to %d seconds\n", (int)maxTime); struct rlimit limit = { maxTime, /* soft limit */ maxTime /* hard limit */ diff --git a/src/base/ver/verStream.c b/src/base/ver/verStream.c index 134bb2f9..4dca9ef6 100644 --- a/src/base/ver/verStream.c +++ b/src/base/ver/verStream.c @@ -454,7 +454,7 @@ char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop ) ***********************************************************************/ void Ver_StreamMove( Ver_Stream_t * p ) { - if ( !strncmp(p->pBufferCur+1, "z_g_", 4) ) + if ( !strncmp(p->pBufferCur+1, "z_g_", 4) || !strncmp(p->pBufferCur+1, "co_g", 3) ) while ( p->pBufferCur[0] != '(' ) p->pBufferCur++; } diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 2eb665bb..402ce21b 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -816,7 +816,7 @@ static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Vec_Ptr_t * vMults = Vec_PtrAlloc( 1000 ); Vec_Ptr_t * vFlops = Vec_PtrAlloc( 1000 ); Wlc_Obj_t * pObj; int i; - Int_Pair_t * pPair; + Int_Pair_t * pPair = NULL; if ( pPars->nLimit == ABC_INFINITY ) return NULL; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 58c5d2ac..51f15597 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -1327,19 +1327,22 @@ usage: ******************************************************************************/ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Wln_NtkRetimeTest( char * pFileName, int fSkipSimple, int fVerbose ); + extern void Wln_NtkRetimeTest( char * pFileName, int fSkipSimple, int fDump, int fVerbose ); FILE * pFile; char * pFileName = NULL; int fSkipSimple = 0; - int c, fVerbose = 0; + int c, fDump = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sdvh" ) ) != EOF ) { switch ( c ) { case 's': fSkipSimple ^= 1; break; + case 'd': + fDump ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -1352,7 +1355,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pNdr ) { Vec_Int_t * vMoves; - Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pAbc->pNdr ); + Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pAbc->pNdr, fDump ); Wln_NtkRetimeCreateDelayInfo( pNtk ); if ( pNtk == NULL ) { @@ -1382,12 +1385,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); - Wln_NtkRetimeTest( pFileName, fSkipSimple, fVerbose ); + Wln_NtkRetimeTest( pFileName, fSkipSimple, fDump, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: %%retime [-svh]\n" ); + Abc_Print( -2, "usage: %%retime [-sdvh]\n" ); Abc_Print( -2, "\t performs retiming for the NDR design\n" ); Abc_Print( -2, "\t-s : toggle printing simple nodes [default = %s]\n", !fSkipSimple? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping the network in Verilog [default = %s]\n", fDump? "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/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c index e0be9002..3212500f 100644 --- a/src/base/wlc/wlcNdr.c +++ b/src/base/wlc/wlcNdr.c @@ -504,9 +504,10 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData ) { int iObj = Wlc_ObjId(pNtk, pObj); int NameId = Wlc_ObjNameId(pNtk, iObj); - word Truth = Vec_WrdEntry(vTruths, NameId); + word Truth; if ( pObj->Type != WLC_OBJ_LUT || NameId == 0 ) continue; + Truth = Vec_WrdEntry(vTruths, NameId); assert( sizeof(void *) == 8 || Wlc_ObjFaninNum(pObj) < 6 ); Vec_WrdWriteEntry( pNtk->vLutTruths, iObj, Truth ); } diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 7d246c0f..ca5e615b 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -90,10 +90,11 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = { "addsub", // 56: adder/subtractor "sel", // 57: selector "dec", // 58: decoder + "LUT", // 59: lookup table NULL // 58: unused }; -char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; } +char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return p ? (p->Type < WLC_OBJ_NUMBER ? Wlc_Names[p->Type] : (char *)"out_of_bound") : (char *)"no_obj"; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -512,7 +513,7 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose ) Wlc_Obj_t * pObj, * pObjRange = NULL; int nCountRange = 0; Vec_Ptr_t * vTypes, * vOccurs; Vec_Int_t * vAnds = Vec_IntStart( WLC_OBJ_NUMBER ); - word Sign; + word Sign = 0; int i, k, s, s0, s1; if ( Wlc_NtkPoNum(p) != 2 ) fTwoSides = 0; @@ -945,8 +946,8 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v return; if ( Wlc_ObjCopy(p, iObj) ) return; - //printf( "Visiting node %d with type %d (%s)\n", iObj, Wlc_NtkObj(p, iObj)->Type, Wlc_NtkObj(p, iObj)->Type < WLC_OBJ_NUMBER ? Wlc_Names[Wlc_NtkObj(p, iObj)->Type] : NULL ); pObj = Wlc_NtkObj( p, iObj ); + //printf( "Visiting node %16s (ID %6d) of type %5s (type ID %2d)\n", Wlc_ObjName(p, iObj), iObj, Wlc_ObjTypeName(pObj), Wlc_NtkObj(p, iObj)->Type ); assert( pObj->Type != WLC_OBJ_FF ); Wlc_ObjForEachFanin( pObj, iFanin, i ) Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins ); diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c index f43f8baa..59f42db5 100644 --- a/src/base/wlc/wlcShow.c +++ b/src/base/wlc/wlcShow.c @@ -362,7 +362,7 @@ void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold ) FILE * pFile; char FileNameDot[200]; char * pName = Extra_FileDesignName(p->pName); - char * pSpec = p->pSpec ? Extra_FileDesignName(p->pSpec) : "unknown"; + char * pSpec = p->pSpec ? Extra_FileDesignName(p->pSpec) : (char *)"unknown"; sprintf( FileNameDot, "%s_%s.dot", pName, pSpec ); ABC_FREE( pName ); if ( strcmp(pSpec, "unknown") ) diff --git a/src/base/wln/wln.h b/src/base/wln/wln.h index 54150c56..510d74c1 100644 --- a/src/base/wln/wln.h +++ b/src/base/wln/wln.h @@ -163,6 +163,7 @@ static inline void Wln_ObjSetFanout( Wln_Ntk_t * p, int i, int f, int v static inline void Wln_NtkIncrementTravId( Wln_Ntk_t * p ) { if (!p->nTravIds++) Vec_IntFill(&p->vTravIds, Vec_IntCap(&p->vTypes), 0); } static inline void Wln_ObjSetTravIdCurrent( Wln_Ntk_t * p, int i ) { Vec_IntWriteEntry( &p->vTravIds, i, p->nTravIds ); } +static inline void Wln_ObjSetTravIdPrevious( Wln_Ntk_t * p, int i ) { Vec_IntWriteEntry( &p->vTravIds, i, p->nTravIds-1 ); } static inline int Wln_ObjIsTravIdCurrent( Wln_Ntk_t * p, int i ) { return (Vec_IntEntry(&p->vTravIds, i) == p->nTravIds); } static inline int Wln_ObjIsTravIdPrevious( Wln_Ntk_t * p, int i ) { return (Vec_IntEntry(&p->vTravIds, i) == p->nTravIds-1); } static inline int Wln_ObjCheckTravId( Wln_Ntk_t * p, int i ) { if ( Wln_ObjIsTravIdCurrent(p, i) ) return 1; Wln_ObjSetTravIdCurrent(p, i); return 0; } @@ -217,7 +218,7 @@ static inline int Wln_ObjRiToRo( Wln_Ntk_t * p, int i ) /*=== wlcNdr.c ========================================================*/ extern Wln_Ntk_t * Wln_ReadNdr( char * pFileName ); extern void Wln_WriteNdr( Wln_Ntk_t * pNtk, char * pFileName ); -extern Wln_Ntk_t * Wln_NtkFromNdr( void * pData ); +extern Wln_Ntk_t * Wln_NtkFromNdr( void * pData, int fDump ); extern void * Wln_NtkToNdr( Wln_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ extern Wln_Ntk_t * Wln_NtkAlloc( char * pName, int nObjsMax ); @@ -225,6 +226,7 @@ extern void Wln_NtkFree( Wln_Ntk_t * p ); extern int Wln_NtkMemUsage( Wln_Ntk_t * p ); extern void Wln_NtkPrint( Wln_Ntk_t * p ); extern Wln_Ntk_t * Wln_NtkDupDfs( Wln_Ntk_t * p ); +extern int Wln_NtkIsAcyclic( Wln_Ntk_t * p ); extern void Wln_NtkCreateRefs( Wln_Ntk_t * p ); extern void Wln_NtkStartFaninMap( Wln_Ntk_t * p, Vec_Int_t * vFaninMap, int nMulti ); extern void Wln_NtkStartFanoutMap( Wln_Ntk_t * p, Vec_Int_t * vFanoutMap, Vec_Int_t * vFanoutNums, int nMulti ); diff --git a/src/base/wln/wlnNdr.c b/src/base/wln/wlnNdr.c index 60179ed4..eb685463 100644 --- a/src/base/wln/wlnNdr.c +++ b/src/base/wln/wlnNdr.c @@ -179,7 +179,7 @@ void Wln_NtkCheckIntegrity( void * pData ) } Vec_IntFree( vMap ); } -Wln_Ntk_t * Wln_NtkFromNdr( void * pData ) +Wln_Ntk_t * Wln_NtkFromNdr( void * pData, int fDump ) { Ndr_Data_t * p = (Ndr_Data_t *)pData; Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 ); @@ -270,6 +270,11 @@ Wln_Ntk_t * Wln_NtkFromNdr( void * pData ) //Ndr_NtkPrintObjects( pNtk ); Wln_WriteVer( pNtk, "temp_ndr.v" ); printf( "Dumped design \"%s\" into file \"temp_ndr.v\".\n", pNtk->pName ); + if ( !Wln_NtkIsAcyclic(pNtk) ) + { + Wln_NtkFree(pNtk); + return NULL; + } // derive topological order pNtk = Wln_NtkDupDfs( pTemp = pNtk ); Wln_NtkFree( pTemp ); @@ -293,7 +298,7 @@ Wln_Ntk_t * Wln_NtkFromNdr( void * pData ) Wln_Ntk_t * Wln_ReadNdr( char * pFileName ) { void * pData = Ndr_Read( pFileName ); - Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData ) : NULL; + Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData, 0 ) : NULL; if ( pNtk ) return NULL; //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" }; //Ndr_WriteVerilog( NULL, pData, ppNames ); @@ -309,17 +314,17 @@ void Wln_ReadNdrTest() Wln_NtkStaticFanoutTest( pNtk ); Wln_NtkFree( pNtk ); } -void Wln_NtkRetimeTest( char * pFileName, int fSkipSimple, int fVerbose ) +void Wln_NtkRetimeTest( char * pFileName, int fSkipSimple, int fDump, int fVerbose ) { Vec_Int_t * vMoves; void * pData = Ndr_Read( pFileName ); - Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData ) : NULL; + Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData, fDump ) : NULL; + Ndr_Delete( pData ); if ( pNtk == NULL ) { printf( "Retiming network is not available.\n" ); return; } - Ndr_Delete( pData ); Wln_NtkRetimeCreateDelayInfo( pNtk ); vMoves = Wln_NtkRetime( pNtk, fSkipSimple, fVerbose ); //Vec_IntPrint( vMoves ); diff --git a/src/base/wln/wlnNtk.c b/src/base/wln/wlnNtk.c index a845b55e..5b3acb6f 100644 --- a/src/base/wln/wlnNtk.c +++ b/src/base/wln/wlnNtk.c @@ -129,6 +129,136 @@ void Wln_NtkPrint( Wln_Ntk_t * p ) printf( "\n" ); } + + +/**Function************************************************************* + + Synopsis [Detects combinational loops.] + + Description [This procedure is based on the idea suggested by Donald Chai. + As we traverse the network and visit the nodes, we need to distinquish + three types of nodes: (1) those that are visited for the first time, + (2) those that have been visited in this traversal but are currently not + on the traversal path, (3) those that have been visited and are currently + on the travesal path. When the node of type (3) is encountered, it means + that there is a combinational loop. To mark the three types of nodes, + two new values of the traversal IDs are used.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wln_NtkIsAcyclic_rec( Wln_Ntk_t * p, int iObj ) +{ + int i, iFanin; + //printf( "Visiting node %d\n", iObj ); + // skip the node if it is already visited + if ( Wln_ObjIsTravIdPrevious(p, iObj) ) + return 1; + // check if the node is part of the combinational loop + if ( Wln_ObjIsTravIdCurrent(p, iObj) ) + { + fprintf( stdout, "Network contains combinational loop!\n" ); + fprintf( stdout, "Node %16s is encountered twice on the following path:\n", Wln_ObjName(p, iObj) ); + fprintf( stdout, "Node %16s (ID %6d) of type %5s (type ID %2d) ->\n", + Wln_ObjName(p, iObj), iObj, Abc_OperName(Wln_ObjType(p, iObj)), Wln_ObjType(p, iObj) ); + return 0; + } + // mark this node as a node on the current path + Wln_ObjSetTravIdCurrent( p, iObj ); + // quit if it is a CI or constant node + if ( Wln_ObjIsCi(p, iObj) || Wln_ObjIsFf(p, iObj) || Wln_ObjFaninNum(p, iObj) == 0 ) + { + // mark this node as a visited node + Wln_ObjSetTravIdPrevious( p, iObj ); + return 1; + } + // traverse the fanin's cone searching for the loop + Wln_ObjForEachFanin( p, iObj, iFanin, i ) + { + if ( !Wln_NtkIsAcyclic_rec(p, iFanin) ) + { + // return as soon as the loop is detected + fprintf( stdout, "Node %16s (ID %6d) of type %5s (type ID %2d) ->\n", + Wln_ObjName(p, iObj), iObj, Abc_OperName(Wln_ObjType(p, iObj)), Wln_ObjType(p, iObj) ); + return 0; + } + } + // mark this node as a visited node + Wln_ObjSetTravIdPrevious( p, iObj ); + return 1; +} +int Wln_NtkIsAcyclic( Wln_Ntk_t * p ) +{ + int fAcyclic, i, iObj, nUnvisited = 0 ; + // set the traversal ID for this DFS ordering + Wln_NtkIncrementTravId( p ); + Wln_NtkIncrementTravId( p ); + // iObj->TravId == pNet->nTravIds means "iObj is on the path" + // iObj->TravId == pNet->nTravIds - 1 means "iObj is visited but is not on the path" + // iObj->TravId < pNet->nTravIds - 1 means "iObj is not visited" + // traverse the network to detect cycles + fAcyclic = 1; + Wln_NtkForEachCo( p, iObj, i ) + { + // traverse the output logic cone + if ( (fAcyclic = Wln_NtkIsAcyclic_rec(p, iObj)) ) + continue; + // stop as soon as the first loop is detected + fprintf( stdout, "Primary output %16s (ID %6d)\n", Wln_ObjName(p, iObj), iObj ); + goto finish; + } + Wln_NtkForEachFf( p, iObj, i ) + { + // traverse the output logic cone + if ( (fAcyclic = Wln_NtkIsAcyclic_rec(p, iObj)) ) + continue; + // stop as soon as the first loop is detected + fprintf( stdout, "Flip-flop %16s (ID %6d)\n", Wln_ObjName(p, iObj), iObj ); + goto finish; + } + Wln_NtkForEachObj( p, iObj ) + nUnvisited += !Wln_ObjIsTravIdPrevious(p, iObj) && !Wln_ObjIsCi(p, iObj); + if ( nUnvisited ) + { + int nSinks = 0; + Wln_NtkCreateRefs(p); + printf( "The network has %d objects and %d (%6.2f %%) of them are not connected to the outputs.\n", + Wln_NtkObjNum(p), nUnvisited, 100.0*nUnvisited/Wln_NtkObjNum(p) ); + Wln_NtkForEachObj( p, iObj ) + if ( !Wln_ObjRefs(p, iObj) && !Wln_ObjIsCi(p, iObj) && !Wln_ObjIsCo(p, iObj) && !Wln_ObjIsFf(p, iObj) ) + nSinks++; + if ( nSinks ) + { + int nPrinted = 0; + printf( "These unconnected objects feed into %d sink objects without fanout:\n", nSinks ); + Wln_NtkForEachObj( p, iObj ) + if ( !Wln_ObjRefs(p, iObj) && !Wln_ObjIsCi(p, iObj) && !Wln_ObjIsCo(p, iObj) && !Wln_ObjIsFf(p, iObj) ) + { + fprintf( stdout, "Node %16s (ID %6d) of type %5s (type ID %2d)\n", + Wln_ObjName(p, iObj), iObj, Abc_OperName(Wln_ObjType(p, iObj)), Wln_ObjType(p, iObj) ); + if ( ++nPrinted == 5 ) + break; + } + if ( nPrinted < nSinks ) + printf( "...\n" ); + } + Wln_NtkForEachObj( p, iObj ) + if ( /*!Wln_ObjRefs(p, iObj) &&*/ !Wln_ObjIsTravIdPrevious(p, iObj) && !Wln_ObjIsCi(p, iObj) ) + { + // traverse the output logic cone + if ( (fAcyclic = Wln_NtkIsAcyclic_rec(p, iObj)) ) + continue; + // stop as soon as the first loop is detected + fprintf( stdout, "Unconnected object %s\n", Wln_ObjName(p, iObj) ); + goto finish; + } + } +finish: + return fAcyclic; +} + /**Function************************************************************* Synopsis [Duplicating network.] @@ -186,7 +316,7 @@ int Wln_NtkDupDfs_rec( Wln_Ntk_t * pNew, Wln_Ntk_t * p, int iObj ) return 0; if ( Wln_ObjCopy(p, iObj) ) return Wln_ObjCopy(p, iObj); - //printf( "Visiting node %d\n", iObj ); + //printf( "Visiting node %16s (ID %6d) of type %5s (type ID %2d)\n", Wln_ObjName(p, iObj), iObj, Abc_OperName(Wln_ObjType(p, iObj)), Wln_ObjType(p, iObj) ); assert( !Wln_ObjIsFf(p, iObj) ); Wln_ObjForEachFanin( p, iObj, iFanin, i ) Wln_NtkDupDfs_rec( pNew, p, iFanin ); diff --git a/src/base/wln/wlnRetime.c b/src/base/wln/wlnRetime.c index 3c4b4822..734ac194 100644 --- a/src/base/wln/wlnRetime.c +++ b/src/base/wln/wlnRetime.c @@ -487,6 +487,8 @@ void Wln_RetRetimeForward( Wln_Ret_t * p, Vec_Int_t * vSet ) Vec_IntForEachEntry( vSet, iObj, i ) { iFlop = Wln_RetRemoveOneFanin( p, iObj ); + if ( iFlop == -1 ) + continue; Wln_RetInsertOneFanout( p, iObj, iFlop ); } } @@ -496,6 +498,8 @@ void Wln_RetRetimeBackward( Wln_Ret_t * p, Vec_Int_t * vSet ) Vec_IntForEachEntry( vSet, iObj, i ) { iFlop = Wln_RetRemoveOneFanout( p, iObj ); + if ( iFlop == -1 ) + continue; Wln_RetInsertOneFanin( p, iObj, iFlop ); } } @@ -538,13 +542,18 @@ void Wln_RetAddToMoves( Wln_Ret_t * p, Vec_Int_t * vSet, int Delay, int fForward ***********************************************************************/ void Wln_NtkRetimeCreateDelayInfo( Wln_Ntk_t * pNtk ) { + int i, iObj; // if ( Wln_NtkHasInstId(pNtk) ) // Vec_IntErase( &pNtk->vInstIds ); if ( Wln_NtkHasInstId(pNtk) ) + { printf( "Using delays given by the user in the input file.\n" ); + Wln_NtkForEachObj( pNtk, iObj ) + if ( !Wln_ObjIsCio(pNtk, iObj) && !Wln_ObjIsConst(pNtk, iObj) && Wln_ObjInstId(pNtk, iObj) == 0 ) + printf( "Warning: Object %d of type %s has zero delay. Retiming will not work correctly.\n", iObj, Abc_OperName(Wln_ObjType(pNtk, iObj)) ); + } else { - int i, iObj; printf( "The design has no delay information.\n" ); Wln_NtkCleanInstId(pNtk); Wln_NtkForEachObj( pNtk, iObj ) |