diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 178 | ||||
| -rw-r--r-- | src/base/abci/abcIf.c | 44 | ||||
| -rw-r--r-- | src/base/abci/abcMiter.c | 17 | ||||
| -rw-r--r-- | src/base/abci/abcRefactor.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcRenode.c | 44 | ||||
| -rw-r--r-- | src/base/abci/abcSat.c | 250 | ||||
| -rw-r--r-- | src/base/abci/abcStrash.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abcVerify.c | 6 |
8 files changed, 495 insertions, 52 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ff63bbd9..f6c180da 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -72,6 +72,7 @@ static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -207,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "demiter", Abc_CommandDemiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 ); + Cmd_CommandAdd( pAbc, "Various", "andpos", Abc_CommandAndPos, 1 ); Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 ); @@ -2038,25 +2040,30 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int nLutSize, nCutsMax, c; + int nFlowIters, nAreaIters; int fArea; int fUseBdds; int fUseSops; + int fUseCnfs; int fVerbose; - extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int fArea, int fUseBdds, int fUseSops, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nLutSize = 8; - nCutsMax = 5; - fArea = 0; - fUseBdds = 0; - fUseSops = 0; - fVerbose = 0; + nLutSize = 8; + nCutsMax = 5; + nFlowIters = 1; + nAreaIters = 1; + fArea = 0; + fUseBdds = 0; + fUseSops = 0; + fUseCnfs = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCabsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscvh" ) ) != EOF ) { switch ( c ) { @@ -2082,6 +2089,28 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCutsMax < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" ); + goto usage; + } + nFlowIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFlowIters < 0 ) + goto usage; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" ); + goto usage; + } + nAreaIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nAreaIters < 0 ) + goto usage; + break; case 'a': fArea ^= 1; break; @@ -2091,6 +2120,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fUseSops ^= 1; break; + case 'c': + fUseCnfs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -2101,9 +2133,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( fUseBdds && fUseSops ) + if ( fUseBdds && fUseSops || fUseBdds && fUseCnfs || fUseSops && fUseCnfs ) { - fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" ); + fprintf( pErr, "Cannot optimize two parameters at the same time.\n" ); return 1; } @@ -2131,7 +2163,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, fArea, fUseBdds, fUseSops, fVerbose ); + pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Renoding has failed.\n" ); @@ -2142,13 +2174,16 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: renode [-K num] [-C num] [-sbav]\n" ); + fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbcav]\n" ); fprintf( pErr, "\t transforms the AIG into a logic network with larger nodes\n" ); fprintf( pErr, "\t while minimizing the number of FF literals of the node SOPs\n" ); fprintf( pErr, "\t-K num : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize ); fprintf( pErr, "\t-C num : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax ); + fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters ); + fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters ); fprintf( pErr, "\t-s : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" ); fprintf( pErr, "\t-b : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-c : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" ); fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -3450,7 +3485,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk;//, * pNtkRes; int fComb; int c; - extern int Abc_NtkOrPos( Abc_Ntk_t * pNtk ); + extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3489,7 +3524,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( !Abc_NtkOrPos( pNtk ) ) + if ( !Abc_NtkCombinePos( pNtk, 0 ) ) { fprintf( pErr, "ORing the POs has failed.\n" ); return 1; @@ -3517,6 +3552,79 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk;//, * pNtkRes; + int fComb; + int c; + extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fComb ^= 1; + break; + default: + goto usage; + } + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "The network is not strashed.\n" ); + return 1; + } + + if ( Abc_NtkPoNum(pNtk) == 1 ) + { + fprintf( pErr, "The network already has one PO.\n" ); + return 1; + } + + if ( Abc_NtkLatchNum(pNtk) ) + { + fprintf( pErr, "The miter has latches. ORing is not performed.\n" ); + return 1; + } + + // get the new network + if ( !Abc_NtkCombinePos( pNtk, 1 ) ) + { + fprintf( pErr, "ANDing the POs has failed.\n" ); + return 1; + } + // replace the current network +// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: andpos [-h]\n" ); + fprintf( pErr, "\t creates single-output miter by ANDing the POs of the current network\n" ); +// fprintf( pErr, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -5286,6 +5394,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); + extern int Pr_ManProofTest( char * pFileName ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5379,7 +5488,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ - Abc_NtkMaxFlowTest( pNtk ); +// Abc_NtkMaxFlowTest( pNtk ); + Pr_ManProofTest( "trace.cnf" ); return 0; usage: @@ -7524,6 +7634,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) // user-controlable paramters pPars->nLutSize = 4; pPars->nCutsMax = 8; + pPars->nFlowIters = 1; + pPars->nAreaIters = 2; pPars->DelayTarget = -1; pPars->fPreprocess = 1; pPars->fArea = 0; @@ -7542,7 +7654,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncCost = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrstvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflrstvh" ) ) != EOF ) { switch ( c ) { @@ -7570,6 +7682,28 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nCutsMax < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" ); + goto usage; + } + pPars->nFlowIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFlowIters < 0 ) + goto usage; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" ); + goto usage; + } + pPars->nAreaIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nAreaIters < 0 ) + goto usage; + break; case 'D': if ( globalUtilOptind >= argc ) { @@ -7705,10 +7839,12 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" ); + fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" ); fprintf( pErr, "\t performs FPGA technology mapping of the network\n" ); fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); + fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters ); + fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters ); fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer ); fprintf( pErr, "\t-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" ); @@ -9143,11 +9279,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - Abc_Ntk_t * pTemp; - pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterSat( pTemp, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); - pNtk->pModel = pTemp->pModel; pTemp->pModel = NULL; - Abc_NtkDelete( pTemp ); + assert( Abc_NtkIsLogic(pNtk) ); + Abc_NtkLogicToBdd( pNtk ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); } // verify that the pattern is correct diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 871bf148..887f6cc9 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -31,6 +31,8 @@ static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj ); static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ); + +extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -122,6 +124,11 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) // start the mapping manager and set its parameters pIfMan = If_ManStart( pPars ); + // print warning about excessive memory usage + if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30) > 0.5 ) + printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", + 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30), pPars->nCutsMax ); + // create PIs and remember them in the old nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan ); Abc_NtkForEachCi( pNtk, pNode, i ) @@ -177,7 +184,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) Vec_Int_t * vCover; int i, nDupGates; // create the new network - if ( pIfMan->pPars->fUseBdds ) + if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); else if ( pIfMan->pPars->fUseSops ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); @@ -206,6 +213,11 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) ); if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) Abc_NtkDeleteObj( pNodeNew ); + // minimize the node + if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseBdds ) + Abc_NtkSweep( pNtkNew, 0 ); + if ( pIfMan->pPars->fUseBdds ) + Abc_NtkBddReorder( pNtkNew, 0 ); // decouple the PO driver nodes to reduce the number of levels nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); // if ( nDupGates && If_ManReadVerbose(pIfMan) ) @@ -239,28 +251,28 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); - If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i ) - Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + if ( pIfMan->pPars->fUseCnfs ) + { + If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + } + else + { + If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + } // derive the function of this node if ( pIfMan->pPars->fTruth ) { if ( pIfMan->pPars->fUseBdds ) { - extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode ); // transform truth table into the BDD pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 ); Cudd_Ref(pNodeNew->pData); - if ( pNodeNew->pData == Cudd_ReadLogicZero(pNtkNew->pManFunc) || pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ) - { - // replace the node by a constant node - pNodeNew = pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew); - } - else - { - // make sure the node is minimum base - Abc_NodeMinimumBase( pNodeNew ); - // reorder the fanins to minimize the BDD size - Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew ); - } + } + else if ( pIfMan->pPars->fUseCnfs ) + { + // transform truth table into the BDD + pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 ); Cudd_Ref(pNodeNew->pData); } else if ( pIfMan->pPars->fUseSops ) { diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index ddbbf671..15a81723 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -1039,7 +1039,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [ORs the outputs.] + Synopsis [Computes OR or AND of the POs.] Description [] @@ -1048,16 +1048,23 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkOrPos( Abc_Ntk_t * pNtk ) +int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) { Abc_Obj_t * pNode, * pMiter; int i; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); - // OR the POs - pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) ); + // start the result + if ( fAnd ) + pMiter = Abc_AigConst1(pNtk); + else + pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) ); + // perform operations on the POs Abc_NtkForEachPo( pNtk, pNode, i ) - pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); + if ( fAnd ) + pMiter = Abc_AigAnd( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); + else + pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); // remove the POs and their names for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- ) Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) ); diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 0328d8d3..834e33aa 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -233,7 +233,7 @@ p->timeDcs += clock() - clk; // get the SOP of the cut clk = clock(); - pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, p->vCube, -1 ); + pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, 0, p->vCube, -1 ); p->timeSop += clock() - clk; // get the factored form diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 462d9da3..af3f55cf 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -29,6 +29,7 @@ static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ); +static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ); static reo_man * s_pReo = NULL; @@ -50,7 +51,7 @@ static Vec_Int_t * s_vMemory = NULL; SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fArea, int fUseBdds, int fUseSops, int fVerbose ) +Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ) { extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); If_Par_t Pars, * pPars = &Pars; @@ -64,6 +65,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA // user-controlable paramters pPars->nLutSize = nFaninMax; pPars->nCutsMax = nCubeMax; + pPars->nFlowIters = nFlowIters; + pPars->nAreaIters = nAreaIters; pPars->DelayTarget = -1; pPars->fPreprocess = 1; pPars->fArea = fArea; @@ -81,10 +84,16 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA pPars->pTimesArr = NULL; pPars->fUseBdds = fUseBdds; pPars->fUseSops = fUseSops; + pPars->fUseCnfs = fUseCnfs; if ( fUseBdds ) pPars->pFuncCost = Abc_NtkRenodeEvalBdd; else if ( fUseSops ) pPars->pFuncCost = Abc_NtkRenodeEvalSop; + else if ( fUseCnfs ) + { + pPars->fArea = 1; + pPars->pFuncCost = Abc_NtkRenodeEvalCnf; + } else pPars->pFuncCost = Abc_NtkRenodeEvalAig; @@ -176,6 +185,39 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ) /**Function************************************************************* + Synopsis [Computes the cost based on two ISOPs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) +{ + int i, RetValue, nClauses; + for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) + pCut->pPerm[i] = 1; + // compute ISOP for the positive phase + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); + if ( RetValue == -1 ) + return ABC_INFINITY; + assert( RetValue == 0 || RetValue == 1 ); + nClauses = Vec_IntSize( s_vMemory ); + // compute ISOP for the negative phase + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + if ( RetValue == -1 ) + return ABC_INFINITY; + assert( RetValue == 0 || RetValue == 1 ); + nClauses += Vec_IntSize( s_vMemory ); + return nClauses; +} + +/**Function************************************************************* + Synopsis [Computes the cost based on the factored form.] Description [] diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 55498288..cf67db6d 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,6 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ); extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); static nMuxes; @@ -53,7 +54,6 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int if ( pNumInspects ) *pNumInspects = 0; - assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // if ( Abc_NtkPoNum(pNtk) > 1 ) @@ -61,7 +61,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int // load clauses into the solver clk = clock(); - pSat = Abc_NtkMiterSatCreate( pNtk, fJFront ); + pSat = Abc_NtkMiterSatCreate( pNtk, fJFront, 0 ); if ( pSat == NULL ) return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); @@ -121,6 +121,9 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int if ( pNumInspects ) *pNumInspects = (int)pSat->solver_stats.inspects; +Sat_SolverTraceWrite( pSat, NULL, NULL, 0 ); +Sat_SolverTraceStop( pSat ); + solver_delete( pSat ); return RetValue; } @@ -660,14 +663,17 @@ Quits : SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ) +solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ) { solver * pSat; Abc_Obj_t * pNode; int RetValue, i, clk = clock(); - nMuxes = 0; + assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) ); + if ( Abc_NtkIsBddLogic(pNtk) ) + return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes); + nMuxes = 0; pSat = solver_new(); RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront ); Abc_NtkForEachObj( pNtk, pNode, i ) @@ -684,6 +690,242 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ) } + + +/**Function************************************************************* + + Synopsis [Adds clauses for the internal node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ + Abc_Obj_t * pFanin; + int i, c, nFanins; + int RetValue; + char * pCube; + + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum( pSop0 ) ); + +// if ( nFanins == 0 ) + if ( Cudd_Regular(pNode->pData) == Cudd_ReadOne(pNode->pNtk->pManFunc) ) + { + vVars->nSize = 0; +// if ( Abc_SopIsConst1(pSop1) ) + if ( !Cudd_IsComplement(pNode->pData) ) + Vec_IntPush( vVars, toLit(pNode->Id) ); + else + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + return 1; + } + + // add clauses for the negative phase + for ( c = 0; ; c++ ) + { + // get the cube + pCube = pSop0 + c * (nFanins + 3); + if ( *pCube == 0 ) + break; + // add the clause + vVars->nSize = 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pCube[i] == '0' ) + Vec_IntPush( vVars, toLit(pFanin->Id) ); + else if ( pCube[i] == '1' ) + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + } + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + + // add clauses for the positive phase + for ( c = 0; ; c++ ) + { + // get the cube + pCube = pSop1 + c * (nFanins + 3); + if ( *pCube == 0 ) + break; + // add the clause + vVars->nSize = 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pCube[i] == '0' ) + Vec_IntPush( vVars, toLit(pFanin->Id) ); + else if ( pCube[i] == '1' ) + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + } + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds clauses for the PO node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ + Abc_Obj_t * pFanin; + int RetValue; + + pFanin = Abc_ObjFanin0(pNode); + if ( Abc_ObjFaninC0(pNode) ) + { + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pFanin->Id) ); + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + + vVars->nSize = 0; + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + else + { + vVars->nSize = 0; + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pFanin->Id) ); + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) +{ + solver * pSat; + Extra_MmFlex_t * pMmFlex; + Abc_Obj_t * pNode; + Vec_Str_t * vCube; + Vec_Int_t * vVars; + char * pSop0, * pSop1; + int i; + + assert( Abc_NtkIsBddLogic(pNtk) ); + + // transfer the IDs to the copy field + Abc_NtkForEachPi( pNtk, pNode, i ) + pNode->pCopy = (void *)pNode->Id; + + // start the data structures + pSat = solver_new(); + pMmFlex = Extra_MmFlexStart(); + vCube = Vec_StrAlloc( 100 ); + vVars = Vec_IntAlloc( 100 ); + +Sat_SolverTraceStart( pSat, "trace.cnf" ); + + // add clauses for each internal nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + { + // derive SOPs for both phases of the node + Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 ); + // add the clauses to the solver + if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) ) + { + solver_delete( pSat ); + pSat = NULL; + goto finish; + } + } + // add clauses for each PO + Abc_NtkForEachPo( pNtk, pNode, i ) + { + if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) ) + { + solver_delete( pSat ); + pSat = NULL; + goto finish; + } + } + +finish: + // delete + Vec_StrFree( vCube ); + Vec_IntFree( vVars ); + Extra_MmFlexStop( pMmFlex ); + return pSat; +} + + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 9af6dc00..b6aecef9 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) extern int timeRetime; Abc_Ntk_t * pNtkAig; Abc_Obj_t * pObj; - int i, nNodes, RetValue; + int i, nNodes;//, RetValue; assert( Abc_NtkIsStrash(pNtk) ); //timeRetime = clock(); // print warning about choice nodes @@ -79,8 +79,8 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) return NULL; } //timeRetime = clock() - timeRetime; - if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) - printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); +// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) +// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); return pNtkAig; } diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index ec0ba8ca..f3a069f4 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -417,6 +417,12 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) pNtk = Abc_NtkStrash(pNtk, 0, 0); fStrashed = 1; } +/* + printf( "Counter example: " ); + Abc_NtkForEachCi( pNtk, pNode, i ) + printf( " %d", pModel[i] ); + printf( "\n" ); +*/ // increment the trav ID Abc_NtkIncrementTravId( pNtk ); // set the CI values |