diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.h | 1 | ||||
-rw-r--r-- | src/base/abci/abc.c | 352 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 471 | ||||
-rw-r--r-- | src/base/abci/abcPart.c | 143 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c | 7 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcTiming.c | 8 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c | 2 |
9 files changed, 824 insertions, 167 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index faa2fe2e..bda8781c 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -234,6 +234,7 @@ struct Abc_Lib_t_ // maximum/minimum operators #define ABC_MIN(a,b) (((a) < (b))? (a) : (b)) #define ABC_MAX(a,b) (((a) > (b))? (a) : (b)) +#define ABC_ABS(a) (((a) >= 0)? (a) :-(a)) #define ABC_INFINITY (100000000) // transforming floats into ints and back diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6b32cd43..1dd9b65e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -92,6 +92,7 @@ static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -113,6 +114,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -169,6 +171,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -252,6 +255,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); + Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -273,6 +277,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 ); @@ -329,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); @@ -5032,6 +5038,95 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTopmost( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nLevels; + extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nLevels = 10; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevels < 0 ) + goto usage; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only works for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently expects a single-output miter.\n" ); + return 0; + } + + pNtkRes = Abc_NtkTopmost( pNtk, nLevels ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "The command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: topmost [-N num] [-h]\n" ); + fprintf( pErr, "\t replaces the current network by several of its topmost levels\n" ); + fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tname : the node name\n"); + return 1; +} + /**Function************************************************************* @@ -6098,9 +6193,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } - pNtkRes = Abc_NtkDar( pNtk ); -// pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); - pNtkRes = NULL; +// pNtkRes = Abc_NtkDar( pNtk ); + pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); +// pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6635,7 +6730,7 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dar_ManDefaultRwrParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzvwh" ) ) != EOF ) { switch ( c ) { @@ -6661,6 +6756,9 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nSubgMax < 0 ) goto usage; break; + case 'f': + pPars->fFanout ^= 1; + break; case 'l': pPars->fUpdateLevel ^= 1; break; @@ -6695,10 +6793,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" ); + fprintf( pErr, "usage: drw [-C num] [-N num] [-flzvwh]\n" ); fprintf( pErr, "\t performs combinational AIG rewriting\n" ); fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax ); fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax ); + fprintf( pErr, "\t-f : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" ); fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -6842,21 +6941,29 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int fVerbose, c; + int fBalance, fVerbose, fUpdateLevel, c; - extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fBalance = 0; fVerbose = 0; + fUpdateLevel = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF ) { switch ( c ) { + case 'b': + fBalance ^= 1; + break; + case 'l': + fUpdateLevel ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6871,7 +6978,7 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - pNtkRes = Abc_NtkDCompress2( pNtk, fVerbose ); + pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6882,8 +6989,77 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dcompress2 [-vh]\n" ); + fprintf( pErr, "usage: dcompress2 [-blvh]\n" ); fprintf( pErr, "\t performs combinational AIG optimization\n" ); + fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); + fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int fBalance, fVerbose, c; + + extern Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fBalance = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fBalance ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: drwsat [-bvh]\n" ); + fprintf( pErr, "\t performs combinational AIG optimization for SAT\n" ); + fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -7212,10 +7388,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c, fProve, fVerbose, fDoSparse, fSpeculate; - int nConfLimit; + int c, nConfLimit, fDoSparse, fProve, fSpeculate, fChoicing, fVerbose; - extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7223,12 +7398,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nConfLimit = 100; - fSpeculate = 0; fDoSparse = 1; fProve = 0; + fSpeculate = 0; + fChoicing = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Csprcvh" ) ) != EOF ) { switch ( c ) { @@ -7252,6 +7428,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fSpeculate ^= 1; break; + case 'c': + fChoicing ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7267,7 +7446,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose ); + pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -7278,12 +7457,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dfraig [-C num] [-sprvh]\n" ); + fprintf( pErr, "usage: dfraig [-C num] [-sprcvh]\n" ); fprintf( pErr, "\t performs fraiging using a new method\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" ); fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" ); fprintf( pErr, "\t-r : toggle speculative reduction [default = %s]\n", fSpeculate? "yes": "no" ); + fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", fChoicing? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -7836,7 +8016,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fFuncRed = 1; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns - pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fDoSparse = 1; // performs equiv tests for sparse functions pParams->fChoicing = 0; // enables recording structural choices pParams->fTryProve = 0; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag @@ -11327,6 +11507,142 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int RetValue; + int fVerbose; + int nConfLimit; + int nInsLimit; + int clk; + + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); + + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + nConfLimit = 100000; + nInsLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nInsLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nInsLimit < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently expects a single-output miter.\n" ); + return 0; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + clk = clock(); + RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose ); + // verify that the pattern is correct + if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) + { + //int i; + //Abc_Obj_t * pObj; + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); + free( pSimInfo ); + /* + // print model + Abc_NtkForEachPi( pNtk, pObj, i ) + { + printf( "%d", (int)(pNtk->pModel[i] > 0) ); + if ( i == 70 ) + break; + } + printf( "\n" ); + */ + } + + if ( RetValue == -1 ) + printf( "UNDECIDED " ); + else if ( RetValue == 0 ) + printf( "SATISFIABLE " ); + else + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); + return 0; + +usage: + fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" ); + fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); + fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index bc47e2dc..f04f3d97 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -123,6 +123,69 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Aig_Obj_t * pObj, * pTemp; + int i; + assert( pMan->pReprs != NULL ); + assert( Aig_ManBufNum(pMan) == 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // rebuild the AIG + vNodes = Aig_ManDfsChoices( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + if ( pTemp = pMan->pReprs[pObj->Id] ) + { + Abc_Obj_t * pAbcRepr, * pAbcObj; + assert( pTemp->pData != NULL ); + pAbcRepr = pObj->pData; + pAbcObj = pTemp->pData; + pAbcObj->pData = pAbcRepr->pData; + pAbcRepr->pData = pAbcObj; + } + } +printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); +/* + { + Abc_Obj_t * pNode; + int k, Counter = 0; + Abc_NtkForEachNode( pNtkNew, pNode, k ) + if ( pNode->pData != 0 ) + { + int x = 0; + Counter++; + } + printf( "Choices = %d.\n", Counter ); + } +*/ + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { Vec_Ptr_t * vNodes; @@ -291,7 +354,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) */ // Aig_ManDumpBlif( pMan, "aig_temp.blif" ); -// pMan->pPars = Dar_ManDefaultRwrParams(); +// pMan->pPars = Dar_ManDefaultRwrPars(); Dar_ManRewrite( pMan, NULL ); Aig_ManPrintStats( pMan ); // Dar_ManComputeCuts( pMan ); @@ -336,120 +399,31 @@ Aig_CnfFree( pCnf ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose ) { - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pNode, * pNodeNew; - Aig_Obj_t * pObj, * pLeaf; - Cnf_Cut_t * pCut; - Vec_Int_t * vCover; - unsigned uTruth; - int i, k, nDupGates; - // create the new network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // make the mapper point to the new network - Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pNode, i ) - Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy; - // process the nodes in topological order - vCover = Vec_IntAlloc( 1 << 16 ); - Vec_PtrForEachEntry( vMapped, pObj, i ) - { - // create new node - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - // add fanins according to the cut - pCut = pObj->pData; - Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) - Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); - // add logic function - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); - pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); - } - else - pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); - // save the node - pObj->pData = pNodeNew; - } - Vec_IntFree( vCover ); - // add the CO drivers - Abc_NtkForEachCo( pNtk, pNode, i ) - { - pObj = Aig_ManPo(p->pManAig, i); - pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); - Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - } - - // remove the constant node if not used - pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData; - if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) - Abc_NtkDeleteObj( pNodeNew ); - // minimize the node -// Abc_NtkSweep( pNtkNew, 0 ); - // decouple the PO driver nodes to reduce the number of levels - nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); -// if ( nDupGates && If_ManReadVerbose(pIfMan) ) -// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) -{ - Abc_Ntk_t * pNtkNew = NULL; - Cnf_Man_t * pCnf; - Aig_Man_t * pMan; - Cnf_Dat_t * pData; - assert( Abc_NtkIsStrash(pNtk) ); - // convert to the AIG manager + Fra_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - if ( !Aig_ManCheck( pMan ) ) - { - printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); - Aig_ManStop( pMan ); - return NULL; - } - // perform balance - Aig_ManPrintStats( pMan ); - - // derive CNF - pCnf = Cnf_ManStart(); - pData = Cnf_Derive( pCnf, pMan ); - - { - Vec_Ptr_t * vMapped; - vMapped = Cnf_ManScanMapping( pCnf, 1 ); - pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped ); - Vec_PtrFree( vMapped ); - } - + Fra_ParamsDefault( pPars ); + pPars->nBTLimitNode = nConfLimit; + pPars->fVerbose = fVerbose; + pPars->fProve = fProve; + pPars->fDoSparse = fDoSparse; + pPars->fSpeculate = fSpeculate; + pPars->fChoicing = fChoicing; + pMan = Fra_Perform( pTemp = pMan, pPars ); + if ( fChoicing ) + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pTemp ); Aig_ManStop( pMan ); - Cnf_ManStop( pCnf ); - - // write CNF into a file -// Cnf_DataWriteIntoFile( pData, pFileName ); - Cnf_DataFree( pData ); - - return pNtkNew; + return pNtkAig; } - /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -461,21 +435,15 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose ) +Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose ) { - Fra_Par_t Params, * pParams = &Params; + extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - Fra_ParamsDefault( pParams ); - pParams->nBTLimitNode = nConfLimit; - pParams->fVerbose = fVerbose; - pParams->fProve = fProve; - pParams->fDoSparse = fDoSparse; - pParams->fSpeculate = fSpeculate; - pMan = Fra_Perform( pTemp = pMan, pParams ); + pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pTemp ); Aig_ManStop( pMan ); @@ -493,17 +461,35 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose ) +Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) { - extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); - Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + int clk; + assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; - pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); +// Aig_ManPrintStats( pMan ); + +// Aig_ManSupports( pMan ); + { + Vec_Vec_t * vParts; + vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL ); + Vec_VecFree( vParts ); + } + + Dar_ManRewrite( pMan, pPars ); +// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); +// Aig_ManStop( pTemp ); + +clk = clock(); + pMan = Aig_ManDup( pTemp = pMan, 0 ); Aig_ManStop( pTemp ); +//PRT( "time", clock() - clk ); + +// Aig_ManPrintStats( pMan ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; } @@ -519,7 +505,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) +Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) { Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; @@ -530,7 +516,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) return NULL; // Aig_ManPrintStats( pMan ); - Dar_ManRewrite( pMan, pPars ); + Dar_ManRefactor( pMan, pPars ); // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); // Aig_ManStop( pTemp ); @@ -556,9 +542,9 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) +Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) { - Aig_Man_t * pMan, * pTemp; + Aig_Man_t * pMan;//, * pTemp; Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -567,13 +553,9 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) return NULL; // Aig_ManPrintStats( pMan ); - Dar_ManRefactor( pMan, pPars ); -// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); -// Aig_ManStop( pTemp ); - clk = clock(); - pMan = Aig_ManDup( pTemp = pMan, 0 ); - Aig_ManStop( pTemp ); + pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose ); +// Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); // Aig_ManPrintStats( pMan ); @@ -593,7 +575,7 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ) +Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) { Aig_Man_t * pMan;//, * pTemp; Abc_Ntk_t * pNtkAig; @@ -605,7 +587,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose ) // Aig_ManPrintStats( pMan ); clk = clock(); - pMan = Dar_ManCompress2( pMan, fVerbose ); + pMan = Dar_ManRwsat( pMan, fBalance, fVerbose ); // Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); @@ -615,6 +597,227 @@ clk = clock(); return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + Aig_Obj_t * pObj, * pLeaf; + Cnf_Cut_t * pCut; + Vec_Int_t * vCover; + unsigned uTruth; + int i, k, nDupGates; + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // make the mapper point to the new network + Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pNode, i ) + Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy; + // process the nodes in topological order + vCover = Vec_IntAlloc( 1 << 16 ); + Vec_PtrForEachEntry( vMapped, pObj, i ) + { + // create new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add fanins according to the cut + pCut = pObj->pData; + Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) + Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); + // add logic function + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); + } + else + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); + // save the node + pObj->pData = pNodeNew; + } + Vec_IntFree( vCover ); + // add the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pObj = Aig_ManPo(p->pManAig, i); + pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + + // remove the constant node if not used + pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData; + if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) + Abc_NtkDeleteObj( pNodeNew ); + // minimize the node +// Abc_NtkSweep( pNtkNew, 0 ); + // decouple the PO driver nodes to reduce the number of levels + nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); +// if ( nDupGates && If_ManReadVerbose(pIfMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Vec_Ptr_t * vMapped; + Aig_Man_t * pMan; + Cnf_Man_t * pManCnf; + Cnf_Dat_t * pCnf; + Abc_Ntk_t * pNtkNew = NULL; + assert( Abc_NtkIsStrash(pNtk) ); + + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Aig_ManCheck( pMan ) ) + { + printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); + Aig_ManStop( pMan ); + return NULL; + } + // perform balance + Aig_ManPrintStats( pMan ); + + // derive CNF + pCnf = Cnf_Derive( pMan ); + pManCnf = Cnf_ManRead(); + + // write the network for verification + vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 ); + pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped ); + Vec_PtrFree( vMapped ); + + // write CNF into a file + Cnf_DataWriteIntoFile( pCnf, pFileName ); + Cnf_DataFree( pCnf ); + Cnf_ClearMemory(); + + Aig_ManStop( pMan ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Solves combinational miter using a SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +{ + sat_solver * pSat; + Aig_Man_t * pMan; + Cnf_Dat_t * pCnf; + int status, RetValue, clk = clock(); + Vec_Int_t * vCiIds; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + + // conver to the manager + pMan = Abc_NtkToDar( pNtk ); + // derive CNF + pCnf = Cnf_Derive( pMan ); + // convert into the SAT solver + pSat = Cnf_DataWriteIntoSolver( pCnf ); + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); + Aig_ManStop( pMan ); + Cnf_DataFree( pCnf ); + // solve SAT + if ( pSat == NULL ) + { + Vec_IntFree( vCiIds ); +// printf( "Trivially unsat\n" ); + return 1; + } + + +// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); + PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = sat_solver_simplify(pSat); +// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + if ( status == 0 ) + { + Vec_IntFree( vCiIds ); + sat_solver_delete( pSat ); +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return 1; + } + + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); +// PRT( "SAT sat_solver time", clock() - clk ); +// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + } + // free the sat_solver + if ( fVerbose ) + Sat_SolverPrintStats( stdout, pSat ); +//sat_solver_store_write( pSat, "trace.cnf" ); +//sat_solver_store_free( pSat ); + sat_solver_delete( pSat ); + Vec_IntFree( vCiIds ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 787e3f88..f0989b23 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -45,13 +45,17 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) Vec_Int_t * vSuppI; Abc_Obj_t * pObj, * pTemp; int i, k; + // set the PI numbers + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (void *)i; + // save hte CI numbers vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pObj, i ) { vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); vSuppI = (Vec_Int_t *)vSupp; Vec_PtrForEachEntry( vSupp, pTemp, k ) - Vec_IntWriteEntry( vSuppI, k, pTemp->Id ); + Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pCopy ); Vec_IntSort( vSuppI, 0 ); // append the number of this output Vec_IntPush( vSuppI, i ); @@ -65,6 +69,71 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Start char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis ) +{ + char * pBuffer; + int i, Entry; + pBuffer = ALLOC( char, nPis ); + memset( pBuffer, 0, sizeof(char) * nPis ); + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [Add to char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis ) +{ + int i, Entry; + Vec_IntForEachEntry( vOne, Entry, i ) + { + assert( Entry < nPis ); + pBuffer[Entry] = 1; + } +} + +/**Function************************************************************* + + Synopsis [Find the common variables using char-bases support representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSuppCharCommon( char * pBuffer, Vec_Int_t * vOne ) +{ + int i, Entry, nCommon = 0; + Vec_IntForEachEntry( vOne, Entry, i ) + nCommon += pBuffer[Entry]; + return nCommon; +} + +/**Function************************************************************* + Synopsis [Find the best partition.] Description [] @@ -74,8 +143,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne ) +int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne ) { +/* Vec_Int_t * vPartSupp, * vPart; double Attract, Repulse, Cost, CostBest; int i, nCommon, iBest; @@ -83,12 +153,12 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts CostBest = 0.0; Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i ) { + vPart = Vec_PtrEntry( vPartsAll, i ); + if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit ) + continue; nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne ); if ( nCommon == 0 ) continue; - vPart = Vec_PtrEntry( vPartsAll, i ); - if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit ) - continue; if ( nCommon == Vec_IntSize(vOne) ) return i; Attract = 1.0 * nCommon / Vec_IntSize(vOne); @@ -106,6 +176,41 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts if ( CostBest < 0.6 ) return -1; return iBest; +*/ + + Vec_Int_t * vPartSupp, * vPart; + int Attract, Repulse, Value, ValueBest; + int i, nCommon, iBest; +// int nCommon2; + iBest = -1; + ValueBest = 0; + Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i ) + { + vPart = Vec_PtrEntry( vPartsAll, i ); + if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit ) + continue; +// nCommon2 = Vec_IntTwoCountCommon( vPartSupp, vOne ); + nCommon = Abc_NtkSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne ); +// assert( nCommon2 == nCommon ); + if ( nCommon == 0 ) + continue; + if ( nCommon == Vec_IntSize(vOne) ) + return i; + Attract = 1000 * nCommon / Vec_IntSize(vOne); + if ( Vec_IntSize(vPartSupp) < 100 ) + Repulse = 1; + else + Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100); + Value = Attract/Repulse; + if ( ValueBest < Value ) + { + ValueBest = Value; + iBest = i; + } + } + if ( ValueBest < 75 ) + return -1; + return iBest; } /**Function************************************************************* @@ -222,9 +327,10 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, ***********************************************************************/ Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose ) { + Vec_Ptr_t * vPartSuppsChar; Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr; Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; - int i, iPart, iOut, clk; + int i, iPart, iOut, clk, clk2, timeFind = 0; // compute the supports for all outputs clk = clock(); @@ -233,6 +339,8 @@ if ( fVerbose ) { PRT( "Supps", clock() - clk ); } + // start char-based support representation + vPartSuppsChar = Vec_PtrAlloc( 1000 ); // create partitions clk = clock(); @@ -243,7 +351,10 @@ clk = clock(); // get the output number iOut = Vec_IntPop(vOne); // find closely matching part - iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne ); +clk2 = clock(); + iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne ); +timeFind += clock() - clk2; +//printf( "%4d->%4d ", i, iPart ); if ( iPart == -1 ) { // create new partition @@ -254,6 +365,8 @@ clk = clock(); // add this partition and its support Vec_PtrPush( vPartsAll, vPart ); Vec_PtrPush( vPartSuppsAll, vPartSupp ); + + Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) ); } else { @@ -266,11 +379,21 @@ clk = clock(); Vec_IntFree( vTemp ); // reinsert new support Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + + Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) ); } } + + // stop char-based support representation + Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i ) + free( vTemp ); + Vec_PtrFree( vPartSuppsChar ); + +//printf( "\n" ); if ( fVerbose ) { PRT( "Parts", clock() - clk ); +//PRT( "Find ", timeFind ); } clk = clock(); @@ -290,7 +413,9 @@ clk = clock(); // Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit ); if ( fVerbose ) - Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); +// Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll ); + printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) ); + if ( fVerbose ) { PRT( "Comps", clock() - clk ); @@ -676,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams ) // perform partitioning assert( Abc_NtkIsStrash(pNtk) ); // vParts = Abc_NtkPartitionNaive( pNtk, 20 ); - vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 ); + vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index cbbea1be..2376b72c 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -70,6 +70,13 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb // cleanup the AIG Abc_AigCleanup(pNtk->pManFunc); + { + Vec_Vec_t * vParts; + vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 ); + Vec_VecFree( vParts ); + } + + // start placement package if ( fPlaceEnable ) { diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index d9cae254..aafa6530 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -49,7 +49,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int sat_solver * pSat; lbool status; int RetValue, clk; - + if ( pNumConfs ) *pNumConfs = 0; if ( pNumInspects ) @@ -70,7 +70,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int //return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); + PRT( "Time", clock() - clk ); // simplify the problem clk = clock(); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index b1a0dc5b..978b7cdb 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -351,7 +351,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco ***********************************************************************/ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int LevelCut ) { - assert( Abc_ObjIsComplement(pNode) ); + assert( !Abc_ObjIsComplement(pNode) ); if ( pNode->pCopy ) return pNode->pCopy; if ( pNode->Level <= (unsigned)LevelCut ) @@ -388,6 +388,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) // create PIs below the cut and nodes above the cut Abc_NtkCleanCopy( pNtk ); pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut ); + pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) ); // add the PO node and name pPoNew = Abc_NtkCreatePo(pNtkNew); Abc_ObjAddFanin( pPoNew, pObjNew ); diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 5d5e6e93..967e4617 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -819,6 +819,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA ) { + assert( Abc_ObjLevel(pFanout) >= Lev ); Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout ); pFanout->fMarkA = 1; } @@ -840,7 +841,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { Abc_Obj_t * pFanin, * pTemp; - int LevelOld, Lev, k, m; + int LevelOld, LevFanin, Lev, k, m; // check if level has changed LevelOld = Abc_ObjReverseLevel(pObjNew); if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) ) @@ -866,7 +867,9 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA ) { - Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin ); + LevFanin = Abc_ObjReverseLevel( pFanin ); + assert( LevFanin >= Lev ); + Vec_VecPush( vLevels, LevFanin, pFanin ); pFanin->fMarkA = 1; } } @@ -891,6 +894,7 @@ void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) Abc_ObjReplace( pObj, pObjNew ); // update the level of the node Abc_NtkUpdateLevel( pObjNew, vLevels ); + Abc_ObjSetReverseLevel( pObjNew, 0 ); Abc_NtkUpdateReverseLevel( pObjNew, vLevels ); } diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 6ab2c552..63ba4843 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -368,7 +368,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); // partition the outputs - vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 ); + vParts = Abc_NtkPartitionSmart( pMiter, 50, 1 ); // fraig each partition Status = 1; |