From 7174787abafe80437892b55a53f994da85a37342 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Feb 2008 08:01:00 -0800 Subject: Version abc80205 --- src/opt/mfs/mfs.h | 6 +- src/opt/mfs/mfsCore.c | 116 +++++++++++++++--- src/opt/mfs/mfsDiv.c | 303 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/mfs/mfsInt.h | 35 +++++- src/opt/mfs/mfsInter.c | 254 ++++++++++++++++++++++++++++++++++++++++ src/opt/mfs/mfsMan.c | 66 ++++++++--- src/opt/mfs/mfsResub.c | 276 +++++++++++++++++++++++++++++++++++++++++++ src/opt/mfs/mfsSat.c | 24 ++-- src/opt/mfs/mfsStrash.c | 41 +++++-- src/opt/mfs/mfsWin.c | 2 +- src/opt/mfs/module.make | 3 + src/opt/res/resCore.c | 3 + 12 files changed, 1075 insertions(+), 54 deletions(-) create mode 100644 src/opt/mfs/mfsDiv.c create mode 100644 src/opt/mfs/mfsInter.c create mode 100644 src/opt/mfs/mfsResub.c (limited to 'src/opt') diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index a7ca3819..9fc6a253 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -43,7 +43,11 @@ struct Mfs_Par_t_ // general parameters int nWinTfoLevs; // the maximum fanout levels int nFanoutsMax; // the maximum number of fanouts - int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis + int nDepthMax; // the maximum number of logic levels + int nDivMax; // the maximum number of divisors + int nWinSizeMax; // the maximum size of the window + int nGrowthLevel; // the maximum allowed growth in level + int fResub; // performs resubstitution int fArea; // performs optimization for area int fDelay; // performs optimization for delay int fVerbose; // enable basic stats diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index fe0d84c3..332a6ad9 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -6,7 +6,7 @@ PackageName [The good old minimization with complete don't-cares.] - Synopsis [] + Synopsis [Core procedures of this package.] Author [Alan Mishchenko] @@ -28,6 +28,60 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + int clk; + p->nNodesTried++; + // prepare data structure for this node + Mfs_ManClean( p ); + // compute window roots, window support, and window nodes +clk = clock(); + p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax ); + p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); + p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); +p->timeWin += clock() - clk; + if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax ) + return 1; + // compute the divisors of the window +clk = clock(); + p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); +p->timeDiv += clock() - clk; + // construct AIG for the window +clk = clock(); + p->pAigWin = Abc_NtkConstructAig( p, pNode ); +p->timeAig += clock() - clk; + // translate it into CNF +clk = clock(); + p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) ); +p->timeCnf += clock() - clk; + // create the SAT problem +clk = clock(); + p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 ); + if ( p->pSat == NULL ) + { + p->nNodesBad++; + return 1; + } + // solve the SAT problem + if ( p->pPars->fArea ) + Abc_NtkMfsResubArea( p, pNode ); + else + Abc_NtkMfsResubEdge( p, pNode ); +p->timeSat += clock() - clk; + return 1; +} + /**Function************************************************************* Synopsis [] @@ -42,6 +96,7 @@ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { int clk; + p->nNodesTried++; // prepare data structure for this node Mfs_ManClean( p ); // compute window roots, window support, and window nodes @@ -80,9 +135,14 @@ p->timeSat += clock() - clk; ***********************************************************************/ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ); + + ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; - int i, Counter; + int i, clk = clock(); + int nTotalNodesBeg = Abc_NtkNodeNum(pNtk); + int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); assert( Abc_NtkIsLogic(pNtk) ); if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX ) @@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) return 0; } assert( Abc_NtkHasAig(pNtk) ); - if ( pNtk->pManExdc != NULL ) - printf( "Performing don't-care computation with don't-cares.\n" ); // start the manager - p = Mfs_ManAlloc(); - p->pPars = pPars; + p = Mfs_ManAlloc( pPars ); p->pNtk = pNtk; - p->pCare = pNtk->pManExdc; + if ( pNtk->pExcare ) + { + Abc_Ntk_t * pTemp; + pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 ); + p->pCare = Abc_NtkToDar( pTemp, 0 ); + Abc_NtkDelete( pTemp ); + } + if ( pPars->fVerbose ) + { + if ( p->pCare != NULL ) + printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); + else + printf( "Performing optimization without constraints.\n" ); + } + if ( !pPars->fResub ) + printf( "Currently don't-cares are not used but the stats are printed.\n" ); // label the register outputs if ( p->pCare ) { - Counter = 1; Abc_NtkForEachCi( pNtk, pObj, i ) - if ( Abc_ObjFaninNum(pObj) == 0 ) - pObj->pData = NULL; - else - pObj->pData = (void *)Counter++; - assert( Counter == Abc_NtkLatchNum(pNtk) + 1 ); + pObj->pData = (void *)i; } + + // compute levels + Abc_NtkLevel( pNtk ); + Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel ); // compute don't-cares for each node + p->nTotalNodesBeg = nTotalNodesBeg; + p->nTotalEdgesBeg = nTotalEdgesBeg; + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachNode( pNtk, pObj, i ) - Abc_NtkMfsNode( p, pObj ); + { + if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) + continue; + if ( !p->pPars->fVeryVerbose ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( pPars->fResub ) + Abc_NtkMfsResub( p, pObj ); + else + Abc_NtkMfsNode( p, pObj ); + } + Extra_ProgressBarStop( pProgress ); + Abc_NtkStopReverseLevels( pNtk ); + p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk); + p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk); // undo labesl if ( p->pCare ) @@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) } // free the manager + p->timeTotal = clock() - clk; Mfs_ManStop( p ); return 1; } diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c new file mode 100644 index 00000000..7b156b97 --- /dev/null +++ b/src/opt/mfs/mfsDiv.c @@ -0,0 +1,303 @@ +/**CFile**************************************************************** + + FileName [mfsDiv.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures to compute candidate divisors.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Marks and collects the TFI cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsWinMarkTfi_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vCone ) +{ + Abc_Obj_t * pFanin; + int i; + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent( pObj ); + if ( Abc_ObjIsCi(pObj) ) + { + Vec_PtrPush( vCone, pObj ); + return; + } + assert( Abc_ObjIsNode(pObj) ); + // visit the fanins of the node + Abc_ObjForEachFanin( pObj, pFanin, i ) + Abc_MfsWinMarkTfi_rec( pFanin, vCone ); + Vec_PtrPush( vCone, pObj ); +} + +/**Function************************************************************* + + Synopsis [Marks and collects the TFI cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_MfsWinMarkTfi( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vCone; + vCone = Vec_PtrAlloc( 100 ); + Abc_MfsWinMarkTfi_rec( pNode, vCone ); + return vCone; +} + +/**Function************************************************************* + + Synopsis [Marks the TFO of the collected nodes up to the given level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ) +{ + Abc_Obj_t * pFanout; + int i; + if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) + return; + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent( pObj ); + Abc_ObjForEachFanout( pObj, pFanout, i ) + Abc_MfsWinSweepLeafTfo_rec( pFanout, nLevelLimit ); +} + +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfsNodeDeref_rec( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i, Counter = 1; + if ( Abc_ObjIsCi(pNode) ) + return 0; + Abc_NodeSetTravIdCurrent( pNode ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + assert( pFanin->vFanouts.nSize > 0 ); + if ( --pFanin->vFanouts.nSize == 0 ) + Counter += Abc_MfsNodeDeref_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfsNodeRef_rec( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i, Counter = 1; + if ( Abc_ObjIsCi(pNode) ) + return 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pFanin->vFanouts.nSize++ == 0 ) + Counter += Abc_MfsNodeRef_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Labels MFFC of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfsWinVisitMffc( Abc_Obj_t * pNode ) +{ + int Count1, Count2; + assert( Abc_ObjIsNode(pNode) ); + // dereference the node (mark with the current trav ID) + Count1 = Abc_MfsNodeDeref_rec( pNode ); + // reference it back + Count2 = Abc_MfsNodeRef_rec( pNode ); + assert( Count1 == Count2 ); + return Count1; +} + +/**Function************************************************************* + + Synopsis [Computes divisors and add them to nodes in the window.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax ) +{ + Vec_Ptr_t * vCone, * vDivs; + Abc_Obj_t * pObj, * pFanout, * pFanin; + int k, f, m; + int nDivsPlus = 0, nTrueSupp; + assert( p->vDivs == NULL ); + + // mark the TFI with the current trav ID + Abc_NtkIncrementTravId( pNode->pNtk ); + vCone = Abc_MfsWinMarkTfi( pNode ); + + // count the number of PIs + nTrueSupp = 0; + Vec_PtrForEachEntry( vCone, pObj, k ) + nTrueSupp += Abc_ObjIsCi(pObj); +// printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m ); + + // mark with the current trav ID those nodes that should not be divisors: + // (1) the node and its TFO + // (2) the MFFC of the node + // (3) the node's fanins (these are treated as a special case) + Abc_NtkIncrementTravId( pNode->pNtk ); + Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax ); + Abc_MfsWinVisitMffc( pNode ); + Abc_ObjForEachFanin( pNode, pObj, k ) + Abc_NodeSetTravIdCurrent( pObj ); + + // at this point the nodes are marked with two trav IDs: + // nodes to be collected as divisors are marked with previous trav ID + // nodes to be avoided as divisors are marked with current trav ID + + // start collecting the divisors + vDivs = Vec_PtrAlloc( p->pPars->nDivMax ); + Vec_PtrForEachEntry( vCone, pObj, k ) + { + if ( !Abc_NodeIsTravIdPrevious(pObj) ) + continue; + if ( (int)pObj->Level > nLevDivMax ) + continue; + Vec_PtrPush( vDivs, pObj ); + if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + break; + } + Vec_PtrFree( vCone ); + + // explore the fanouts of already collected divisors + if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax ) + Vec_PtrForEachEntry( vDivs, pObj, k ) + { + // consider fanouts of this node + Abc_ObjForEachFanout( pObj, pFanout, f ) + { + // stop if there are too many fanouts + if ( f > 20 ) + break; + // skip nodes that are already added + if ( Abc_NodeIsTravIdPrevious(pFanout) ) + continue; + // skip nodes in the TFO or in the MFFC of node + if ( Abc_NodeIsTravIdCurrent(pFanout) ) + continue; + // skip COs + if ( !Abc_ObjIsNode(pFanout) ) + continue; + // skip nodes with large level + if ( (int)pFanout->Level >= nLevDivMax ) + continue; + // skip nodes whose fanins are not divisors + Abc_ObjForEachFanin( pFanout, pFanin, m ) + if ( !Abc_NodeIsTravIdPrevious(pFanin) ) + break; + if ( m < Abc_ObjFaninNum(pFanout) ) + continue; + // make sure this divisor in not among the nodes +// Vec_PtrForEachEntry( p->vNodes, pFanin, m ) +// assert( pFanout != pFanin ); + // add the node to the divisors + Vec_PtrPush( vDivs, pFanout ); +// Vec_PtrPush( p->vNodes, pFanout ); + Vec_PtrPushUnique( p->vNodes, pFanout ); + Abc_NodeSetTravIdPrevious( pFanout ); + nDivsPlus++; + if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + break; + } + if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + break; + } + + // sort the divisors by level in the increasing order + Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease ); + + // add the fanins of the node + Abc_ObjForEachFanin( pNode, pFanin, k ) + Vec_PtrPush( vDivs, pFanin ); + +/* + printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) ); + Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus ) + printf( "%d ", Abc_ObjLevel(pObj) ); + printf( "\n" ); +*/ +//printf( "%d ", p->nDivsPlus ); +// printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), +// nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus ); + return vDivs; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 6ba5903e..54826bc1 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -34,6 +34,7 @@ extern "C" { #include "aig.h" #include "cnf.h" #include "satSolver.h" +#include "satStore.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -52,11 +53,23 @@ struct Mfs_Man_t_ Vec_Ptr_t * vRoots; // the roots of the window Vec_Ptr_t * vSupp; // the support of the window Vec_Ptr_t * vNodes; // the internal nodes of the window + Vec_Ptr_t * vDivs; // the divisors of the node + Vec_Int_t * vDivLits; // the SAT literals of divisor nodes Vec_Int_t * vProjVars; // the projection variables + // intermediate simulation data + Vec_Ptr_t * vDivCexes; // the counter-example for dividors + int nDivWords; // the number of words + int nCexes; // the numbe rof current counter-examples + int nSatCalls; + int nSatCexes; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window sat_solver * pSat; // the SAT solver used + Int_Man_t * pMan; // interpolation manager; + Vec_Int_t * vMem; // memory for intermediate SOPs + Vec_Vec_t * vLevels; // levelized structure for updating + Vec_Ptr_t * vFanins; // the new set of fanins // the result of solving int nFanins; // the number of fanins int nWords; // the number of words @@ -64,14 +77,24 @@ struct Mfs_Man_t_ unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set // performance statistics int nNodesTried; - int nNodesBad; + int nNodesResub; + int nNodesGained; int nMintsCare; int nMintsTotal; + int nNodesBad; + // node/edge stats + int nTotalNodesBeg; + int nTotalNodesEnd; + int nTotalEdgesBeg; + int nTotalEdgesEnd; // statistics int timeWin; + int timeDiv; int timeAig; int timeCnf; int timeSat; + int timeInt; + int timeTotal; }; //////////////////////////////////////////////////////////////////////// @@ -86,10 +109,18 @@ struct Mfs_Man_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== mfsDiv.c ==========================================================*/ +extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax ); +/*=== mfsInter.c ==========================================================*/ +extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ); +extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ); /*=== mfsMan.c ==========================================================*/ -extern Mfs_Man_t * Mfs_ManAlloc(); +extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ); extern void Mfs_ManStop( Mfs_Man_t * p ); extern void Mfs_ManClean( Mfs_Man_t * p ); +/*=== mfsResub.c ==========================================================*/ +extern int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsSat.c ==========================================================*/ extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c new file mode 100644 index 00000000..16db5061 --- /dev/null +++ b/src/opt/mfs/mfsInter.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [mfsInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures for computing resub function by interpolation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" +#include "kit.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds constraints for the two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC ) +{ + lit Lits[3]; + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Creates miter for checking resubsitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands ) +{ + sat_solver * pSat; + Aig_Obj_t * pObjPo; + int Lits[2], status, iVar, i, c; + + // get the literal for the output of F + pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 ); + Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 ); + + // collect the outputs of the divisors + Vec_IntClear( p->vProjVars ); + Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) + { + assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); + Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + } + assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); + + // start the solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) ); + if ( pCands ) + sat_solver_store_alloc( pSat ); + + // load the first copy of the clauses + for ( i = 0; i < p->pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + // add the clause for the first output of F + if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + + // bookmark the clauses of A + if ( pCands ) + sat_solver_store_mark_clauses_a( pSat ); + + // transform the literals + for ( i = 0; i < p->pCnf->nLiterals; i++ ) + p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars; + // load the second copy of the clauses + for ( i = 0; i < p->pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + // transform the literals + for ( i = 0; i < p->pCnf->nLiterals; i++ ) + p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars; + // add the clause for the second output of F + Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] ); + if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + + if ( pCands ) + { + // add relevant clauses for EXOR gates + for ( c = 0; c < nCands; c++ ) + { + // get the variable number of this divisor + i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; + // get the corresponding SAT variable + iVar = Vec_IntEntry( p->vProjVars, i ); + // add the corresponding EXOR gate + if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + // add the corresponding clause + if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + } + // bookmark the roots + sat_solver_store_mark_roots( pSat ); + } + else + { + // add the clauses for the EXOR gates - and remember their outputs + Vec_IntForEachEntry( p->vProjVars, iVar, i ) + { + if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) + { + sat_solver_delete( pSat ); + return NULL; + } + Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); + } + // simplify the solver + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { +// printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" ); + sat_solver_delete( pSat ); + return NULL; + } + } + return pSat; +} + +/**Function************************************************************* + + Synopsis [Performs interpolation.] + + Description [Derives the new function of the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) +{ + extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); + + sat_solver * pSat; + Sto_Man_t * pCnf = NULL; + unsigned * puTruth; + Kit_Graph_t * pGraph; + Hop_Obj_t * pFunc; + int nFanins, status; + + // derive the SAT solver for interpolation + pSat = Abc_MfsCreateSolverResub( p, pCands, nCands ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + if ( status != l_False ) + { + printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" ); + return NULL; + } + // get the learned clauses + pCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + + // derive the interpolant + nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth ); + Sto_ManFree( pCnf ); + assert( nFanins == nCands ); + + // transform interpolant into AIG + pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem ); + pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph ); + Kit_GraphFree( pGraph ); + return pFunc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 1341e373..67981d5a 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -6,7 +6,7 @@ PackageName [The good old minimization with complete don't-cares.] - Synopsis [Procedure to manipulation the manager.] + Synopsis [Procedures working with the manager.] Author [Alan Mishchenko] @@ -28,7 +28,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - /**Function************************************************************* Synopsis [] @@ -40,13 +39,21 @@ SeeAlso [] ***********************************************************************/ -Mfs_Man_t * Mfs_ManAlloc() +Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) { Mfs_Man_t * p; // start the manager p = ALLOC( Mfs_Man_t, 1 ); memset( p, 0, sizeof(Mfs_Man_t) ); + p->pPars = pPars; p->vProjVars = Vec_IntAlloc( 100 ); + p->vDivLits = Vec_IntAlloc( 100 ); + p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); + p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); + p->pMan = Int_ManAlloc(); + p->vMem = Vec_IntAlloc( 0 ); + p->vLevels = Vec_VecStart( 32 ); + p->vFanins = Vec_PtrAlloc( 32 ); return p; } @@ -75,12 +82,15 @@ void Mfs_ManClean( Mfs_Man_t * p ) Vec_PtrFree( p->vSupp ); if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + if ( p->vDivs ) + Vec_PtrFree( p->vDivs ); p->pAigWin = NULL; - p->pCnf = NULL; - p->pSat = NULL; + p->pCnf = NULL; + p->pSat = NULL; p->vRoots = NULL; - p->vSupp = NULL; + p->vSupp = NULL; p->vNodes = NULL; + p->vDivs = NULL; } /**Function************************************************************* @@ -96,14 +106,31 @@ void Mfs_ManClean( Mfs_Man_t * p ) ***********************************************************************/ void Mfs_ManPrint( Mfs_Man_t * p ) { - printf( "Nodes tried = %d. Bad nodes = %d.\n", - p->nNodesTried, p->nNodesBad ); - printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n", - p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal ); - PRT( "Win", p->timeWin ); - PRT( "Aig", p->timeAig ); - PRT( "Cnf", p->timeCnf ); - PRT( "Sat", p->timeSat ); + if ( p->pPars->fResub ) + { + printf( "Reduction in nodes = %5d. (%.2f %%) ", + p->nTotalNodesBeg-p->nTotalNodesEnd, + 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg ); + printf( "Reduction in edges = %5d. (%.2f %%) ", + p->nTotalEdgesBeg-p->nTotalEdgesEnd, + 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg ); + printf( "\n" ); + printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", + Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls ); + } + else + { + printf( "Nodes = %d. Care mints = %d. Total mints = %d. Ratio = %5.2f.\n", + p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal ); + } + PRTP( "Win", p->timeWin , p->timeTotal ); + PRTP( "Div", p->timeDiv , p->timeTotal ); + PRTP( "Aig", p->timeAig , p->timeTotal ); + PRTP( "Cnf", p->timeCnf , p->timeTotal ); + PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); + PRTP( "Int", p->timeInt , p->timeTotal ); + PRTP( "ALL", p->timeTotal , p->timeTotal ); + } /**Function************************************************************* @@ -119,9 +146,18 @@ void Mfs_ManPrint( Mfs_Man_t * p ) ***********************************************************************/ void Mfs_ManStop( Mfs_Man_t * p ) { - Mfs_ManPrint( p ); + if ( p->pPars->fVerbose ) + Mfs_ManPrint( p ); + if ( p->pCare ) + Aig_ManStop( p->pCare ); Mfs_ManClean( p ); + Int_ManFree( p->pMan ); + Vec_IntFree( p->vMem ); + Vec_VecFree( p->vLevels ); + Vec_PtrFree( p->vFanins ); Vec_IntFree( p->vProjVars ); + Vec_IntFree( p->vDivLits ); + Vec_PtrFree( p->vDivCexes ); free( p ); } diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c new file mode 100644 index 00000000..ae1132f2 --- /dev/null +++ b/src/opt/mfs/mfsResub.c @@ -0,0 +1,276 @@ +/**CFile**************************************************************** + + FileName [mfsResub.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures to perform resubstitution.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Updates the network after resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) +{ + Abc_Obj_t * pObjNew, * pFanin; + int k; + // create the new node + pObjNew = Abc_NtkCreateNode( pObj->pNtk ); + pObjNew->pData = pFunc; + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Abc_ObjAddFanin( pObjNew, pFanin ); + // replace the old node by the new node +//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); +//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew ); + // update the level of the node + Abc_NtkUpdate( pObj, pObjNew, p->vLevels ); +} + +/**Function************************************************************* + + Synopsis [Tries resubstitution.] + + Description [Returns 1 if it is feasible, or 0 if c-ex is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) +{ + unsigned * pData, * pDataTot; + int RetValue, iVar, i; + p->nSatCalls++; + RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue == l_False ) + return 1; + p->nSatCexes++; + // store the counter-example + pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ ); + assert( pData[0] == 0 ); + Vec_IntForEachEntry( p->vProjVars, iVar, i ) + { + if ( sat_solver_var_value( p->pSat, iVar ) ) + Aig_InfoSetBit( pData, i ); + } + // AND the result with the previous ones + pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); + for ( i = 0; i < p->nDivWords; i++ ) + pDataTot[i] &= pData[i]; + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove ) +{ + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData; + int pCands[MFS_FANIN_MAX]; + int iVar, i, nCands, clk; + Abc_Obj_t * pFanin; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + + // clean simulation info + Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); + pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); + memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords ); + p->nCexes = 0; + + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + iFanin, Abc_ObjFaninNum(pNode), + Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == iFanin ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); + p->nNodesResub++; +// p->nNodesGained += Abc_NodeMffcLabel(pNode); +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fOnlyRemove ) + return 0; + + // shift variables by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; + + if ( fVeryVerbose ) + { + for ( i = 0; i < 8; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + if ( i == iFanin ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = -1; + while ( 1 ) + { + if ( fVeryVerbose ) + { + printf( "%3d: %2d ", p->nCexes, iVar ); + pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 ); +// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + printf( "%d", Aig_InfoHasBit(pData, i) ); + printf( "\n" ); + } + + // find the next divisor to try + pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); + for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) + if ( Aig_InfoHasBit( pData, iVar ) ) + break; + if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) + return 0; + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); + p->nNodesResub++; +// p->nNodesGained += Abc_NodeMffcLabel(pNode); +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); + // update the network +// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) ); + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) + return 1; + } + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) ) + return 1; + } + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index d995000f..efb09b39 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -6,7 +6,7 @@ PackageName [The good old minimization with complete don't-cares.] - Synopsis [] + Synopsis [Procedures to compute don't-cares using SAT.] Author [Alan Mishchenko] @@ -43,9 +43,11 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) { int Lits[MFS_FANIN_MAX]; int RetValue, iVar, b, Mint; - RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); - if ( RetValue != l_True ) + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue == l_False ) return 0; + p->nCares++; // add SAT assignment to the solver Mint = 0; Vec_IntForEachEntry( p->vProjVars, iVar, b ) @@ -95,15 +97,19 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); // iterate through the SAT assignments - while ( Abc_NtkMfsSolveSat_iter( p ) ); - - // write statistics p->nCares = 0; - for ( i = 0; i < p->nWords; i++ ) - p->nCares += Aig_WordCountOnes( p->uCare[i] ); + while ( Abc_NtkMfsSolveSat_iter(p) ); + // write statistics p->nMintsCare += p->nCares; - p->nMintsTotal += 32 * p->nWords; + p->nMintsTotal += (1<nFanins); + + if ( p->pPars->fVeryVerbose ) + { + printf( "Node %4d : Care = %2d. Total = %2d. ", pNode->Id, p->nCares, (1<nFanins) ); + Extra_PrintBinary( stdout, p->uCare, (1<nFanins) ); + printf( "\n" ); + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index 7b467936..8e945045 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -144,18 +144,18 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan ) +Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan ) { Aig_Obj_t * pObj0, * pObj1; - if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) ) + if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) ) return pObj->pData; - Aig_ObjSetTravIdCurrent( pMan, pObj ); + Aig_ObjSetTravIdCurrent( pCare, pObj ); if ( Aig_ObjIsPi(pObj) ) return pObj->pData = NULL; - pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan ); + pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan ); if ( pObj0 == NULL ) return pObj->pData = NULL; - pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan ); + pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan ); if ( pObj1 == NULL ) return pObj->pData = NULL; pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) ); @@ -184,6 +184,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) pMan = Aig_ManStart( 1000 ); // construct the root node's AIG cone pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan ); +// assert( Aig_ManConst1(pMan) == pObjAig ); Aig_ObjCreatePo( pMan, pObjAig ); if ( p->pCare ) { @@ -191,27 +192,43 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_ManIncrementTravId( p->pCare ); Vec_PtrForEachEntry( p->vSupp, pFanin, i ) { - if ( pFanin->pData == NULL ) - continue; - pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 ); + pPi = Aig_ManPi( p->pCare, (int)pFanin->pData ); Aig_ObjSetTravIdCurrent( p->pCare, pPi ); pPi->pData = pFanin->pCopy; } // construct the constraints Aig_ManForEachPo( p->pCare, pPo, i ) { - pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan ); +// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); if ( pObjAig == NULL ) continue; pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); Aig_ObjCreatePo( pMan, pObjAig ); } } - // construct the fanins - Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( p->pPars->fResub ) { - pObjAig = (Aig_Obj_t *)pFanin->pCopy; + // construct the node + pObjAig = (Aig_Obj_t *)pNode->pCopy; Aig_ObjCreatePo( pMan, pObjAig ); + // construct the divisors + Vec_PtrForEachEntry( p->vDivs, pFanin, i ) + { + pObjAig = (Aig_Obj_t *)pFanin->pCopy; + Aig_ObjCreatePo( pMan, pObjAig ); + } + } + else + { + // construct the fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pObjAig = (Aig_Obj_t *)pFanin->pCopy; + Aig_ObjCreatePo( pMan, pObjAig ); + } } Aig_ManCleanup( pMan ); return pMan; diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c index b812d44d..e3e5e24e 100644 --- a/src/opt/mfs/mfsWin.c +++ b/src/opt/mfs/mfsWin.c @@ -6,7 +6,7 @@ PackageName [The good old minimization with complete don't-cares.] - Synopsis [] + Synopsis [Procedures to compute windows stretching to the PIs.] Author [Alan Mishchenko] diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make index 7b9f1260..544accec 100644 --- a/src/opt/mfs/module.make +++ b/src/opt/mfs/module.make @@ -1,5 +1,8 @@ SRC += src/opt/mfs/mfsCore.c \ + src/opt/mfs/mfsDiv.c \ + src/opt/mfs/mfsInter.c \ src/opt/mfs/mfsMan.c \ + src/opt/mfs/mfsResub.c \ src/opt/mfs/mfsSat.c \ src/opt/mfs/mfsStrash.c \ src/opt/mfs/mfsWin.c diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index cb448fc0..a19a1573 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -183,12 +183,15 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc { Abc_Obj_t * pObjNew, * pFanin; int k; + // create the new node pObjNew = Abc_NtkCreateNode( pObj->pNtk ); pObjNew->pData = pFunc; Vec_PtrForEachEntry( vFanins, pFanin, k ) Abc_ObjAddFanin( pObjNew, pFanin ); // replace the old node by the new node +//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj ); +//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew ); // update the level of the node Abc_NtkUpdate( pObj, pObjNew, vLevels ); } -- cgit v1.2.3