From 2c7f6e39b84d29db096388459db7583c01b79b01 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Mar 2008 08:01:00 -0700 Subject: Version abc80330 --- src/aig/mfx/mfx.h | 80 ++++++++ src/aig/mfx/mfxCore.c | 330 ++++++++++++++++++++++++++++++ src/aig/mfx/mfxDiv.c | 303 +++++++++++++++++++++++++++ src/aig/mfx/mfxInt.h | 160 +++++++++++++++ src/aig/mfx/mfxInter.c | 361 +++++++++++++++++++++++++++++++++ src/aig/mfx/mfxMan.c | 186 +++++++++++++++++ src/aig/mfx/mfxResub.c | 529 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/mfx/mfxSat.c | 140 +++++++++++++ src/aig/mfx/mfxStrash.c | 339 +++++++++++++++++++++++++++++++ src/aig/mfx/mfxWin.c | 112 ++++++++++ src/aig/mfx/mfx_.c | 47 +++++ src/aig/mfx/module.make | 8 + 12 files changed, 2595 insertions(+) create mode 100644 src/aig/mfx/mfx.h create mode 100644 src/aig/mfx/mfxCore.c create mode 100644 src/aig/mfx/mfxDiv.c create mode 100644 src/aig/mfx/mfxInt.h create mode 100644 src/aig/mfx/mfxInter.c create mode 100644 src/aig/mfx/mfxMan.c create mode 100644 src/aig/mfx/mfxResub.c create mode 100644 src/aig/mfx/mfxSat.c create mode 100644 src/aig/mfx/mfxStrash.c create mode 100644 src/aig/mfx/mfxWin.c create mode 100644 src/aig/mfx/mfx_.c create mode 100644 src/aig/mfx/module.make (limited to 'src/aig/mfx') diff --git a/src/aig/mfx/mfx.h b/src/aig/mfx/mfx.h new file mode 100644 index 00000000..783de56c --- /dev/null +++ b/src/aig/mfx/mfx.h @@ -0,0 +1,80 @@ +/**CFile**************************************************************** + + FileName [mfx.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfx.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFX_H__ +#define __MFX_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Mfx_Par_t_ Mfx_Par_t; +struct Mfx_Par_t_ +{ + // general parameters + int nWinTfoLevs; // the maximum fanout levels + int nFanoutsMax; // the maximum number of fanouts + 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 nBTLimit; // the maximum number of conflicts in one SAT run + int fResub; // performs resubstitution + int fArea; // performs optimization for area + int fMoreEffort; // performs high-affort minimization + int fSwapEdge; // performs edge swapping + int fDelay; // performs optimization for delay + int fVerbose; // enable basic stats + int fVeryVerbose; // enable detailed stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfxCore.c ==========================================================*/ +extern void Mfx_ParsDefault( Mfx_Par_t * pPars ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c new file mode 100644 index 00000000..4c8988cc --- /dev/null +++ b/src/aig/mfx/mfxCore.c @@ -0,0 +1,330 @@ +/**CFile**************************************************************** + + FileName [mfxCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Core procedures of this package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ParsDefault( Mfx_Par_t * pPars ) +{ + pPars->nWinTfoLevs = 2; + pPars->nFanoutsMax = 10; + pPars->nDepthMax = 20; + pPars->nDivMax = 250; + pPars->nWinSizeMax = 300; + pPars->nGrowthLevel = 0; + pPars->nBTLimit = 5000; + pPars->fResub = 1; + pPars->fArea = 0; + pPars->fMoreEffort = 0; + pPars->fSwapEdge = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_Resub( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + int clk; + p->nNodesTried++; + // prepare data structure for this node + Mfx_ManClean( p ); + // compute window roots, window support, and window nodes +clk = clock(); + p->vRoots = Mfx_ComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax ); + p->vSupp = Nwk_ManSupportNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); + p->vNodes = Nwk_ManDfsNodes( p->pNtk, (Nwk_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 = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) ); + p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY ); + p->nTotalDivs += Vec_PtrSize(p->vDivs); +p->timeDiv += clock() - clk; + // construct AIG for the window +clk = clock(); + p->pAigWin = Mfx_ConstructAig( 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 = Mfx_CreateSolverResub( p, NULL, 0, 0 ); + if ( p->pSat == NULL ) + { + p->nNodesBad++; + return 1; + } + // solve the SAT problem + if ( p->pPars->fSwapEdge ) + Mfx_EdgeSwapEval( p, pNode ); + else + { + Mfx_ResubNode( p, pNode ); + if ( p->pPars->fMoreEffort ) + Mfx_ResubNode2( p, pNode ); + } +p->timeSat += clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_Node( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Hop_Obj_t * pObj; + int RetValue; + + int nGain, clk; + p->nNodesTried++; + // prepare data structure for this node + Mfx_ManClean( p ); + // compute window roots, window support, and window nodes +clk = clock(); + p->vRoots = Mfx_ComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax ); + p->vSupp = Nwk_ManSupportNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); + p->vNodes = Nwk_ManDfsNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); +p->timeWin += clock() - clk; + // count the number of patterns +// p->dTotalRatios += Mfx_ConstraintRatio( p, pNode ); + // construct AIG for the window +clk = clock(); + p->pAigWin = Mfx_ConstructAig( p, pNode ); +p->timeAig += clock() - clk; + // translate it into CNF +clk = clock(); + p->pCnf = Cnf_DeriveSimple( p->pAigWin, Nwk_ObjFaninNum(pNode) ); +p->timeCnf += clock() - clk; + // create the SAT problem +clk = clock(); + p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + if ( p->pSat == NULL ) + return 0; + // solve the SAT problem + RetValue = Mfx_SolveSat( p, pNode ); + p->nTotConfLevel += p->pSat->stats.conflicts; +p->timeSat += clock() - clk; + if ( RetValue == 0 ) + { + p->nTimeOutsLevel++; + p->nTimeOuts++; + return 0; + } + // minimize the local function of the node using bi-decomposition + assert( p->nFanins == Nwk_ObjFaninNum(pNode) ); + pObj = Nwk_NodeIfNodeResyn( p->pManDec, pNode->pMan->pManHop, pNode->pFunc, p->nFanins, p->vTruth, p->uCare ); + nGain = Hop_DagSize(pNode->pFunc) - Hop_DagSize(pObj); + if ( nGain >= 0 ) + { + p->nNodesDec++; + p->nNodesGained += nGain; + p->nNodesGainedLevel += nGain; + pNode->pFunc = pObj; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ) +{ + Bdc_Par_t Pars = {0}, * pDecPars = &Pars; +// ProgressBar * pProgress; + Mfx_Man_t * p; + Tim_Man_t * pManTimeOld = NULL; + Nwk_Obj_t * pObj; + Vec_Vec_t * vLevels; + Vec_Ptr_t * vNodes; + int i, k, nNodes, nFaninMax, clk = clock(), clk2; + int nTotalNodesBeg = Nwk_ManNodeNum(pNtk); + int nTotalEdgesBeg = Nwk_ManGetTotalFanins(pNtk); + + // check limits on the number of fanins + nFaninMax = Nwk_ManGetFaninMax(pNtk); + if ( pPars->fResub ) + { + if ( nFaninMax > 8 ) + { + printf( "Nodes with more than %d fanins will node be processed.\n", 8 ); + nFaninMax = 8; + } + } + else + { + if ( nFaninMax > MFX_FANIN_MAX ) + { + printf( "Nodes with more than %d fanins will node be processed.\n", MFX_FANIN_MAX ); + nFaninMax = MFX_FANIN_MAX; + } + } + +/* + // prepare timing information + if ( pNtk->pManTime ) + { + // compute levels + Nwk_ManLevel( pNtk ); + // compute delay trace with white-boxes + Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib ); + // save the general timing manager + pManTimeOld = pNtk->pManTime; + // derive an approximate timing manager without white-boxes + pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime ); + } + // compute delay trace with the given timing manager + Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib ); +*/ + + // start the manager + p = Mfx_ManAlloc( pPars ); + p->pNtk = pNtk; + p->nFaninMax = nFaninMax; + if ( !pPars->fResub ) + { + pDecPars->nVarsMax = nFaninMax; + pDecPars->fVerbose = pPars->fVerbose; + p->vTruth = Vec_IntAlloc( 0 ); + p->pManDec = Bdc_ManAlloc( pDecPars ); + } + + // compute don't-cares for each node + nNodes = 0; + p->nTotalNodesBeg = nTotalNodesBeg; + p->nTotalEdgesBeg = nTotalEdgesBeg; + if ( pPars->fResub ) + { +// pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) ); + Nwk_ManForEachNode( pNtk, pObj, i ) + { + if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax ) + continue; + if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax ) + continue; +// if ( !p->pPars->fVeryVerbose ) +// Extra_ProgressBarUpdate( pProgress, i, NULL ); + Mfx_Resub( p, pObj ); + } +// Extra_ProgressBarStop( pProgress ); + } + else + { +// pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) ); + vLevels = Nwk_ManLevelize( pNtk ); + Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 ) + { +// if ( !p->pPars->fVeryVerbose ) +// Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + p->nNodesGainedLevel = 0; + p->nTotConfLevel = 0; + p->nTimeOutsLevel = 0; + clk2 = clock(); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax ) + break; + if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax ) + continue; + Mfx_Node( p, pObj ); + } + nNodes += Vec_PtrSize(vNodes); + if ( pPars->fVerbose ) + { + printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %% ", + k, Vec_PtrSize(vNodes), + 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes), + 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes), + 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) ); + PRT( "Time", clock() - clk2 ); + } + } +// Extra_ProgressBarStop( pProgress ); + Vec_VecFree( vLevels ); + } + p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk); + p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk); +/* + // reset the timing manager + if ( pNtk->pManTime ) + { + Tim_ManStop( pNtk->pManTime ); + pNtk->pManTime = pManTimeOld; + } + Nwk_ManVerifyLevel( pNtk ); +*/ + // free the manager + p->timeTotal = clock() - clk; + Mfx_ManStop( p ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxDiv.c b/src/aig/mfx/mfxDiv.c new file mode 100644 index 00000000..b7b76031 --- /dev/null +++ b/src/aig/mfx/mfxDiv.c @@ -0,0 +1,303 @@ +/**CFile**************************************************************** + + FileName [mfxDiv.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: mfxDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Marks and collects the TFI cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfxWinMarkTfi_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vCone ) +{ + Nwk_Obj_t * pFanin; + int i; + if ( Nwk_ObjIsTravIdCurrent(pObj) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + if ( Nwk_ObjIsCi(pObj) ) + { + Vec_PtrPush( vCone, pObj ); + return; + } + assert( Nwk_ObjIsNode(pObj) ); + // visit the fanins of the node + Nwk_ObjForEachFanin( pObj, pFanin, i ) + Abc_MfxWinMarkTfi_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_MfxWinMarkTfi( Nwk_Obj_t * pNode ) +{ + Vec_Ptr_t * vCone; + vCone = Vec_PtrAlloc( 100 ); + Abc_MfxWinMarkTfi_rec( pNode, vCone ); + return vCone; +} + +/**Function************************************************************* + + Synopsis [Marks the TFO of the collected nodes up to the given level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit ) +{ + Nwk_Obj_t * pFanout; + int i; + if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) + return; + if ( Nwk_ObjIsTravIdCurrent(pObj) ) + return; + Nwk_ObjSetTravIdCurrent( pObj ); + Nwk_ObjForEachFanout( pObj, pFanout, i ) + Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit ); +} + +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfxNodeDeref_rec( Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i, Counter = 1; + if ( Nwk_ObjIsCi(pNode) ) + return 0; + Nwk_ObjSetTravIdCurrent( pNode ); + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + assert( pFanin->nFanouts > 0 ); + if ( --pFanin->nFanouts == 0 ) + Counter += Abc_MfxNodeDeref_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfxNodeRef_rec( Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i, Counter = 1; + if ( Nwk_ObjIsCi(pNode) ) + return 0; + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pFanin->nFanouts++ == 0 ) + Counter += Abc_MfxNodeRef_rec( pFanin ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Labels MFFC of the node with the current trav ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode ) +{ + int Count1, Count2; + assert( Nwk_ObjIsNode(pNode) ); + // dereference the node (mark with the current trav ID) + Count1 = Abc_MfxNodeDeref_rec( pNode ); + // reference it back + Count2 = Abc_MfxNodeRef_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 * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax ) +{ + Vec_Ptr_t * vCone, * vDivs; + Nwk_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 + Nwk_ManIncrementTravId( pNode->pMan ); + vCone = Abc_MfxWinMarkTfi( pNode ); + + // count the number of PIs + nTrueSupp = 0; + Vec_PtrForEachEntry( vCone, pObj, k ) + nTrueSupp += Nwk_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) + Nwk_ManIncrementTravId( pNode->pMan ); + Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax ); + Abc_MfxWinVisitMffc( pNode ); + Nwk_ObjForEachFanin( pNode, pObj, k ) + Nwk_ObjSetTravIdCurrent( 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 ( !Nwk_ObjIsTravIdPrevious(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 + Nwk_ObjForEachFanout( pObj, pFanout, f ) + { + // stop if there are too many fanouts + if ( f > 20 ) + break; + // skip nodes that are already added + if ( Nwk_ObjIsTravIdPrevious(pFanout) ) + continue; + // skip nodes in the TFO or in the MFFC of node + if ( Nwk_ObjIsTravIdCurrent(pFanout) ) + continue; + // skip COs + if ( !Nwk_ObjIsNode(pFanout) ) + continue; + // skip nodes with large level + if ( (int)pFanout->Level > nLevDivMax ) + continue; + // skip nodes whose fanins are not divisors + Nwk_ObjForEachFanin( pFanout, pFanin, m ) + if ( !Nwk_ObjIsTravIdPrevious(pFanin) ) + break; + if ( m < Nwk_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 ); + Nwk_ObjSetTravIdPrevious( 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, Nwk_NodeCompareLevelsIncrease ); + + // add the fanins of the node + Nwk_ObjForEachFanin( pNode, pFanin, k ) + Vec_PtrPush( vDivs, pFanin ); + +/* + printf( "Node level = %d. ", Nwk_ObjLevel(p->pNode) ); + Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus ) + printf( "%d ", Nwk_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/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h new file mode 100644 index 00000000..88792bf2 --- /dev/null +++ b/src/aig/mfx/mfxInt.h @@ -0,0 +1,160 @@ +/**CFile**************************************************************** + + FileName [mfxInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFX_INT_H__ +#define __MFX_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "nwk.h" +#include "mfx.h" +#include "aig.h" +#include "cnf.h" +#include "satSolver.h" +#include "satStore.h" +#include "bdc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define MFX_FANIN_MAX 12 + +typedef struct Mfx_Man_t_ Mfx_Man_t; +struct Mfx_Man_t_ +{ + // input data + Mfx_Par_t * pPars; + Nwk_Man_t * pNtk; + Aig_Man_t * pCare; + Vec_Ptr_t * vSuppsInv; + int nFaninMax; + // intermeditate data for the node + 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; + // used for bidecomposition + Vec_Int_t * vTruth; + Bdc_Man_t * pManDec; + int nNodesDec; + int nNodesGained; + int nNodesGainedLevel; + // 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 + int nTotConfLim; // total conflict limit + int nTotConfLevel; // total conflicts on this level + // the result of solving + int nFanins; // the number of fanins + int nWords; // the number of words + int nCares; // the number of care minterms + unsigned uCare[(MFX_FANIN_MAX<=5)?1:1<<(MFX_FANIN_MAX-5)]; // the computed care-set + // performance statistics + int nNodesTried; + int nNodesResub; + int nMintsCare; + int nMintsTotal; + int nNodesBad; + int nTotalDivs; + int nTimeOuts; + int nTimeOutsLevel; + int nDcMints; + double dTotalRatios; + // 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; +}; + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfxDiv.c ==========================================================*/ +extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax ); +/*=== mfxInter.c ==========================================================*/ +extern sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert ); +extern Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands ); +extern int Mfx_InterplateEval( Mfx_Man_t * p, int * pCands, int nCands ); +/*=== mfxMan.c ==========================================================*/ +extern Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ); +extern void Mfx_ManStop( Mfx_Man_t * p ); +extern void Mfx_ManClean( Mfx_Man_t * p ); +/*=== mfxResub.c ==========================================================*/ +extern void Mfx_PrintResubStats( Mfx_Man_t * p ); +extern int Mfx_EdgeSwapEval( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +extern int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +extern int Mfx_ResubNode2( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +/*=== mfxSat.c ==========================================================*/ +extern int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +/*=== mfxStrash.c ==========================================================*/ +extern Aig_Man_t * Mfx_ConstructAig( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +extern double Mfx_ConstraintRatio( Mfx_Man_t * p, Nwk_Obj_t * pNode ); +/*=== mfxWin.c ==========================================================*/ +extern Vec_Ptr_t * Mfx_ComputeRoots( Nwk_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c new file mode 100644 index 00000000..a42e02fe --- /dev/null +++ b/src/aig/mfx/mfxInter.c @@ -0,0 +1,361 @@ +/**CFile**************************************************************** + + FileName [mfxInter.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: mfxInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" +#include "kit.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds constraints for the two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_SatAddXor( 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 * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert ) +{ + 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], fInvert ); + + // 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 ( !Mfx_SatAddXor( 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 ( !Mfx_SatAddXor( 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( "Mfx_CreateSolverResub(): 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 [] + +***********************************************************************/ +unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fInvert ) +{ + sat_solver * pSat; + Sto_Man_t * pCnf = NULL; + unsigned * puTruth; + int nFanins, status; + int c, i, * pGloVars; + + // derive the SAT solver for interpolation + pSat = Mfx_CreateSolverResub( p, pCands, nCands, fInvert ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( status != l_False ) + { + p->nTimeOuts++; + return NULL; + } + // get the learned clauses + pCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + + // set the global variables + pGloVars = Int_ManSetGlobalVars( p->pMan, nCands ); + 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 + pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + } + + // derive the interpolant + nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth ); + Sto_ManFree( pCnf ); + assert( nFanins == nCands ); + return puTruth; +} + +/**Function************************************************************* + + Synopsis [Performs interpolation.] + + Description [Derives the new function of the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_InterplateEval( Mfx_Man_t * p, int * pCands, int nCands ) +{ + unsigned * pTruth, uTruth0[2], uTruth1[2]; + int nCounter; + pTruth = Mfx_InterplateTruth( p, pCands, nCands, 0 ); + if ( nCands == 6 ) + { + uTruth1[0] = pTruth[0]; + uTruth1[1] = pTruth[1]; + } + else + { + uTruth1[0] = pTruth[0]; + uTruth1[1] = pTruth[0]; + } + pTruth = Mfx_InterplateTruth( p, pCands, nCands, 1 ); + if ( nCands == 6 ) + { + uTruth0[0] = ~pTruth[0]; + uTruth0[1] = ~pTruth[1]; + } + else + { + uTruth0[0] = ~pTruth[0]; + uTruth0[1] = ~pTruth[0]; + } + nCounter = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] ); + nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] ); +// printf( "%d ", nCounter ); + return nCounter; +} + + +/**Function************************************************************* + + Synopsis [Performs interpolation.] + + Description [Derives the new function of the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Mfx_Interplate( Mfx_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; + int c, i, * pGloVars; + +// p->nDcMints += Mfx_InterplateEval( p, pCands, nCands ); + + // derive the SAT solver for interpolation + pSat = Mfx_CreateSolverResub( p, pCands, nCands, 0 ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( status != l_False ) + { + p->nTimeOuts++; + return NULL; + } + // get the learned clauses + pCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + + // set the global variables + pGloVars = Int_ManSetGlobalVars( p->pMan, nCands ); + 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 + pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + } + + // 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->pManHop, pGraph ); + Kit_GraphFree( pGraph ); + return pFunc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c new file mode 100644 index 00000000..1b536f8c --- /dev/null +++ b/src/aig/mfx/mfxMan.c @@ -0,0 +1,186 @@ +/**CFile**************************************************************** + + FileName [mfxMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures working with the manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ) +{ + Mfx_Man_t * p; + // start the manager + p = ALLOC( Mfx_Man_t, 1 ); + memset( p, 0, sizeof(Mfx_Man_t) ); + p->pPars = pPars; + p->vProjVars = Vec_IntAlloc( 100 ); + p->vDivLits = Vec_IntAlloc( 100 ); + p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX); + p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManClean( Mfx_Man_t * p ) +{ + if ( p->pAigWin ) + Aig_ManStop( p->pAigWin ); + if ( p->pCnf ) + Cnf_DataFree( p->pCnf ); + if ( p->pSat ) + sat_solver_delete( p->pSat ); + if ( p->vRoots ) + Vec_PtrFree( p->vRoots ); + if ( p->vSupp ) + 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->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; + p->vDivs = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManPrint( Mfx_Man_t * p ) +{ + 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. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", + Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); + if ( p->pPars->fSwapEdge ) + printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", + p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) ); + else + Mfx_PrintResubStats( p ); +// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); + } + else + { + printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", + Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, + 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); +// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", +// 1.0-(p->dTotalRatios/p->nNodesTried) ); + printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); + } +/* + 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************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManStop( Mfx_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Mfx_ManPrint( p ); + if ( p->vTruth ) + Vec_IntFree( p->vTruth ); + if ( p->pManDec ) + Bdc_ManFree( p->pManDec ); + if ( p->pCare ) + Aig_ManStop( p->pCare ); + if ( p->vSuppsInv ) + Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv ); + Mfx_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 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c new file mode 100644 index 00000000..2eafc559 --- /dev/null +++ b/src/aig/mfx/mfxResub.c @@ -0,0 +1,529 @@ +/**CFile**************************************************************** + + FileName [mfxResub.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: mfxResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Updates the network after resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc ) +{ + Nwk_Obj_t * pObjNew, * pFanin; + int k; + // create the new node + pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) ); +if ( pObjNew->Id == 19969 ) +{ + int x = 0; +} + pObjNew->pFunc = pFunc; + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Nwk_ObjAddFanin( pObjNew, pFanin ); + // replace the old node by the new node +//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj ); +//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew ); + // update the level of the node + Nwk_ManUpdate( pObj, pObjNew, p->vLevels ); +} + +/**Function************************************************************* + + Synopsis [Prints resub candidate stats.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_PrintResubStats( Mfx_Man_t * p ) +{ + Nwk_Obj_t * pFanin, * pNode; + int i, k, nAreaCrits = 0, nAreaExpanse = 0; + int nFaninMax = Nwk_ManGetFaninMax(p->pNtk); + Nwk_ManForEachNode( p->pNtk, pNode, i ) + Nwk_ObjForEachFanin( pNode, pFanin, k ) + { + if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 ) + { + nAreaCrits++; + nAreaExpanse += (int)(Nwk_ObjFaninNum(pNode) < nFaninMax); + } + } + printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", + nAreaCrits, nAreaExpanse ); +} + +/**Function************************************************************* + + Synopsis [Tries resubstitution.] + + Description [Returns 1 if it is feasible, or 0 if c-ex is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands ) +{ + unsigned * pData; + int RetValue, iVar, i; + p->nSatCalls++; + RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +// assert( RetValue == l_False || RetValue == l_True ); + if ( RetValue == l_False ) + return 1; + if ( RetValue != l_True ) + { + p->nTimeOuts++; + return -1; + } + p->nSatCexes++; + // store the counter-example + Vec_IntForEachEntry( p->vProjVars, iVar, i ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! + { + assert( Aig_InfoHasBit(pData, p->nCexes) ); + Aig_InfoXorBit( pData, p->nCexes ); + } + } + p->nCexes++; + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate ) +{ + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData; + int pCands[MFX_FANIN_MAX]; + int RetValue, iVar, i, nCands, nWords, w, clk; + Nwk_Obj_t * pFanin; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, 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)-Nwk_ObjFaninNum(pNode), + iFanin, Nwk_ObjFaninNum(pNode), + Nwk_ObjFanoutNum(Nwk_ObjFanin(pNode, iFanin)) == 1 ? Nwk_ObjMffcLabel(Nwk_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == iFanin ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + RetValue = Mfx_TryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); + p->nNodesResub++; + p->nNodesGainedLevel++; + if ( fSkipUpdate ) + return 1; +clk = clock(); + // derive the function + pFunc = Mfx_Interplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; + // update the network + Mfx_UpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fOnlyRemove ) + return 0; + + if ( fVeryVerbose ) + { + for ( i = 0; i < 8; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Nwk_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 ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode); iVar++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( w = 0; w < nWords; w++ ) + if ( pData[w] != ~0 ) + break; + if ( w == nWords ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); + p->nNodesResub++; + p->nNodesGainedLevel++; + if ( fSkipUpdate ) + return 1; +clk = clock(); + // derive the function + pFunc = Mfx_Interplate( p, pCands, nCands+1 ); + if ( pFunc == NULL ) + return 0; + // update the network + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + Mfx_UpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin2 ) +{ + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData, * pData2; + int pCands[MFX_FANIN_MAX]; + int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak; + Nwk_Obj_t * pFanin; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + assert( iFanin2 >= 0 || iFanin2 == -1 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); + p->nCexes = 0; + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode), + iFanin, iFanin2, Nwk_ObjFaninNum(pNode), + Nwk_ObjFanoutNum(Nwk_ObjFanin(pNode, iFanin)) == 1 ? Nwk_ObjMffcLabel(Nwk_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + if ( i == iFanin || i == iFanin2 ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + RetValue = Mfx_TryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); + p->nNodesResub++; + p->nNodesGainedLevel++; +clk = clock(); + // derive the function + pFunc = Mfx_Interplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; + // update the network + Mfx_UpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fVeryVerbose ) + { + for ( i = 0; i < 11; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Nwk_ObjFaninNum(pNode); i++ ) + if ( i == iFanin || i == iFanin2 ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = iVar2 = -1; + while ( 1 ) + { + if ( fVeryVerbose ) + { + printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + fBreak = 0; + for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode); iVar++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( iVar2 = 0; iVar2 < iVar; iVar2++ ) + { + pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 ); + for ( w = 0; w < nWords; w++ ) + if ( (pData[w] | pData2[w]) != ~0 ) + break; + if ( w == nWords ) + { + fBreak = 1; + break; + } + } + if ( fBreak ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); + p->nNodesResub++; + p->nNodesGainedLevel++; +clk = clock(); + // derive the function + pFunc = Mfx_Interplate( p, pCands, nCands+2 ); + if ( pFunc == NULL ) + return 0; + // update the network + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + assert( Vec_PtrSize(p->vFanins) == nCands + 2 ); + Mfx_UpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the possibility of replacing given edge by another edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_EdgeSwapEval( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i; + Nwk_ObjForEachFanin( pNode, pFanin, i ) + Mfx_SolveSatResub( p, pNode, i, 0, 1 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + int i; + // try replacing area critical fanins + Nwk_ObjForEachFanin( pNode, pFanin, i ) + if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 ) + { + if ( Mfx_SolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } + // try removing redundant edges + if ( !p->pPars->fArea ) + { + Nwk_ObjForEachFanin( pNode, pFanin, i ) + if ( Nwk_ObjIsCi(pFanin) || Nwk_ObjFanoutNum(pFanin) != 1 ) + { + if ( Mfx_SolveSatResub( p, pNode, i, 1, 0 ) ) + return 1; + } + } + if ( Nwk_ObjFaninNum(pNode) == p->nFaninMax ) + return 0; + // try replacing area critical fanins while adding two new fanins + Nwk_ObjForEachFanin( pNode, pFanin, i ) + if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 ) + { + if ( Mfx_SolveSatResub2( p, pNode, i, -1 ) ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_ResubNode2( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin, * pFanin2; + int i, k; +/* + Nwk_ObjForEachFanin( pNode, pFanin, i ) + if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 ) + { + if ( Mfx_SolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } +*/ + if ( Nwk_ObjFaninNum(pNode) < 2 ) + return 0; + // try replacing one area critical fanin and one other fanin while adding two new fanins + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 ) + { + // consider second fanin to remove at the same time + Nwk_ObjForEachFanin( pNode, pFanin2, k ) + { + if ( i != k && Mfx_SolveSatResub2( p, pNode, i, k ) ) + return 1; + } + } + } + return 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c new file mode 100644 index 00000000..9dd42e8c --- /dev/null +++ b/src/aig/mfx/mfxSat.c @@ -0,0 +1,140 @@ +/**CFile**************************************************************** + + FileName [mfxSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures to compute don't-cares using SAT.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Enumerates through the SAT assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_SolveSat_iter( Mfx_Man_t * p ) +{ + int Lits[MFX_FANIN_MAX]; + int RetValue, nBTLimit, iVar, b, Mint; + if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts ) + return -1; + nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0; + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False ); + if ( RetValue == l_Undef ) + return -1; + if ( RetValue == l_False ) + return 0; + p->nCares++; + // add SAT assignment to the solver + Mint = 0; + Vec_IntForEachEntry( p->vProjVars, iVar, b ) + { + Lits[b] = toLit( iVar ); + if ( sat_solver_var_value( p->pSat, iVar ) ) + { + Mint |= (1 << b); + Lits[b] = lit_neg( Lits[b] ); + } + } + assert( !Aig_InfoHasBit(p->uCare, Mint) ); + Aig_InfoSetBit( p->uCare, Mint ); + // add the blocking clause + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + if ( RetValue == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Enumerates through the SAT assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Aig_Obj_t * pObjPo; + int RetValue, i; + // collect projection variables + Vec_IntClear( p->vProjVars ); + Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) ) + { + assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); + Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + } + + // prepare the truth table of care set + p->nFanins = Vec_IntSize( p->vProjVars ); + p->nWords = Aig_TruthWordNum( p->nFanins ); + memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); + + // iterate through the SAT assignments + p->nCares = 0; + p->nTotConfLim = p->pPars->nBTLimit; + while ( (RetValue = Mfx_SolveSat_iter(p)) == 1 ); + if ( RetValue == -1 ) + return 0; + + // write statistics + p->nMintsCare += p->nCares; + p->nMintsTotal += (1<nFanins); + + if ( p->pPars->fVeryVerbose ) + { + printf( "Node %4d : Care = %2d. Total = %2d. ", pNode->Id, p->nCares, (1<nFanins) ); +// Kit_TruthPrintBinary( stdout, p->uCare, (1<nFanins) ); + printf( "\n" ); + } + + // map the care + if ( p->nFanins > 4 ) + return 1; + if ( p->nFanins == 4 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16); + if ( p->nFanins == 3 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24); + if ( p->nFanins == 2 ) + p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) | + (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28); + assert( p->nFanins != 1 ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxStrash.c b/src/aig/mfx/mfxStrash.c new file mode 100644 index 00000000..5cb6452f --- /dev/null +++ b/src/aig/mfx/mfxStrash.c @@ -0,0 +1,339 @@ +/**CFile**************************************************************** + + FileName [mfxStrash.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Structural hashing of the window with ODCs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Construct BDDs and mark AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Nwk_ConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); + Nwk_ConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan ); + pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Converts the network from AIG to BDD representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ConvertHopToAig( Nwk_Obj_t * pObjOld, Aig_Man_t * pMan ) +{ + Hop_Man_t * pHopMan; + Hop_Obj_t * pRoot; + Nwk_Obj_t * pFanin; + int i; + // get the local AIG + pHopMan = pObjOld->pMan->pManHop; + pRoot = pObjOld->pFunc; + // check the case of a constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + { + pObjOld->pCopy = (Nwk_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) ); + pObjOld->pNext = pObjOld->pCopy; + return; + } + + // assign the fanin nodes + Nwk_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy; + // construct the AIG + Nwk_ConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pCopy = (Nwk_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + + // assign the fanin nodes + Nwk_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pNext; + // construct the AIG + Nwk_ConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pNext = (Nwk_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Computes the care set of the node under ODCs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Mfx_ConstructAig_rec( Mfx_Man_t * p, Nwk_Obj_t * pNode, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pRoot, * pExor; + Nwk_Obj_t * pObj; + int i; + // assign AIG nodes to the leaves + Vec_PtrForEachEntry( p->vSupp, pObj, i ) + pObj->pCopy = pObj->pNext = (Nwk_Obj_t *)Aig_ObjCreatePi( pMan ); + // strash intermediate nodes + Nwk_ManIncrementTravId( pNode->pMan ); + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + { + Nwk_ConvertHopToAig( pObj, pMan ); + if ( pObj == pNode ) + pObj->pNext = Aig_Not(pObj->pNext); + } + // create the observability condition + pRoot = Aig_ManConst0(pMan); + Vec_PtrForEachEntry( p->vRoots, pObj, i ) + { + pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext ); + pRoot = Aig_Or( pMan, pRoot, pExor ); + } + return pRoot; +} + +/**Function************************************************************* + + Synopsis [Adds relevant constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Mfx_ConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pObj0, * pObj1; + if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent( pCare, pObj ); + if ( Aig_ObjIsPi(pObj) ) + return pObj->pData = NULL; + pObj0 = Mfx_ConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan ); + if ( pObj0 == NULL ) + return pObj->pData = NULL; + pObj1 = Mfx_ConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan ); + if ( pObj1 == NULL ) + return pObj->pData = NULL; + pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) ); + pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) ); + return pObj->pData = Aig_And( pMan, pObj0, pObj1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManVerifyManager( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + int i; + Nwk_ManForEachObj( pNtk, pObj, i ) + { + assert( pObj->pMan == pNtk ); + } +} + +/**Function************************************************************* + + Synopsis [Creates AIG for the window with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Mfx_ConstructAig( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Aig_Man_t * pMan; + Nwk_Obj_t * pFanin; + Aig_Obj_t * pObjAig, * pPi, * pPo; + Vec_Int_t * vOuts; + int i, k, iOut; +// Nwk_ManVerifyManager( p->pNtk ); + // start the new manager + pMan = Aig_ManStart( 1000 ); + // construct the root node's AIG cone + pObjAig = Mfx_ConstructAig_rec( p, pNode, pMan ); +// assert( Aig_ManConst1(pMan) == pObjAig ); + Aig_ObjCreatePo( pMan, pObjAig ); + if ( p->pCare ) + { + // mark the care set + Aig_ManIncrementTravId( p->pCare ); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + pPi = Aig_ManPi( p->pCare, pFanin->PioId ); + Aig_ObjSetTravIdCurrent( p->pCare, pPi ); + pPi->pData = pFanin->pCopy; + } + // construct the constraints + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + vOuts = Vec_PtrEntry( p->vSuppsInv, pFanin->PioId ); + Vec_IntForEachEntry( vOuts, iOut, k ) + { + pPo = Aig_ManPo( p->pCare, iOut ); + if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) ) + continue; + Aig_ObjSetTravIdCurrent( p->pCare, pPo ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pMan, pObjAig ); + } + } +/* + Aig_ManForEachPo( p->pCare, pPo, i ) + { +// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pMan, pObjAig ); + } +*/ + } + if ( p->pPars->fResub ) + { + // 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 + Nwk_ObjForEachFanin( pNode, pFanin, i ) + { + pObjAig = (Aig_Obj_t *)pFanin->pCopy; + Aig_ObjCreatePo( pMan, pObjAig ); + } + } + Aig_ManCleanup( pMan ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Creates AIG for the window with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Nwk_AigForConstraints( Mfx_Man_t * p, Nwk_Obj_t * pNode ) +{ + Nwk_Obj_t * pFanin; + Aig_Man_t * pMan; + Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot; + Vec_Int_t * vOuts; + int i, k, iOut; + if ( p->pCare == NULL ) + return NULL; + pMan = Aig_ManStart( 1000 ); + // mark the care set + Aig_ManIncrementTravId( p->pCare ); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + pPi = Aig_ManPi( p->pCare, pFanin->PioId ); + Aig_ObjSetTravIdCurrent( p->pCare, pPi ); + pPi->pData = Aig_ObjCreatePi(pMan); + } + // construct the constraints + pObjRoot = Aig_ManConst1(pMan); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + vOuts = Vec_PtrEntry( p->vSuppsInv, pFanin->PioId ); + Vec_IntForEachEntry( vOuts, iOut, k ) + { + pPo = Aig_ManPo( p->pCare, iOut ); + if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) ) + continue; + Aig_ObjSetTravIdCurrent( p->pCare, pPo ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + pObjRoot = Aig_And( pMan, pObjRoot, pObjAig ); + } + } + Aig_ObjCreatePo( pMan, pObjRoot ); + Aig_ManCleanup( pMan ); + return pMan; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfxWin.c b/src/aig/mfx/mfxWin.c new file mode 100644 index 00000000..e84a9b90 --- /dev/null +++ b/src/aig/mfx/mfxWin.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [mfxWin.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures to compute windows stretching to the PIs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the node should be a root.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Mfx_ComputeRootsCheck( Nwk_Obj_t * pNode, int nLevelMax, int nFanoutLimit ) +{ + Nwk_Obj_t * pFanout; + int i; + // the node is the root if one of the following is true: + // (1) the node has more than fanouts than the limit + if ( Nwk_ObjFanoutNum(pNode) > nFanoutLimit ) + return 1; + // (2) the node has CO fanouts + // (3) the node has fanouts above the cutoff level + Nwk_ObjForEachFanout( pNode, pFanout, i ) + if ( Nwk_ObjIsCo(pFanout) || pFanout->Level > nLevelMax ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ComputeRoots_rec( Nwk_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots ) +{ + Nwk_Obj_t * pFanout; + int i; + assert( Nwk_ObjIsNode(pNode) ); + if ( Nwk_ObjIsTravIdCurrent(pNode) ) + return; + Nwk_ObjSetTravIdCurrent( pNode ); + // check if the node should be the root + if ( Mfx_ComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) ) + Vec_PtrPush( vRoots, pNode ); + else // if not, explore its fanouts + Nwk_ObjForEachFanout( pNode, pFanout, i ) + Mfx_ComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots ); +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [Returns 1 if the only root is this node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Mfx_ComputeRoots( Nwk_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ) +{ + Vec_Ptr_t * vRoots; + vRoots = Vec_PtrAlloc( 10 ); + Nwk_ManIncrementTravId( pNode->pMan ); + Mfx_ComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots ); + assert( Vec_PtrSize(vRoots) > 0 ); +// if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode ) +// return 0; + return vRoots; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/mfx_.c b/src/aig/mfx/mfx_.c new file mode 100644 index 00000000..32caf7ff --- /dev/null +++ b/src/aig/mfx/mfx_.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [mfs_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfs_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/mfx/module.make b/src/aig/mfx/module.make new file mode 100644 index 00000000..22b9b72a --- /dev/null +++ b/src/aig/mfx/module.make @@ -0,0 +1,8 @@ +SRC += src/aig/mfx/mfxCore.c \ + src/aig/mfx/mfxDiv.c \ + src/aig/mfx/mfxInter.c \ + src/aig/mfx/mfxMan.c \ + src/aig/mfx/mfxResub.c \ + src/aig/mfx/mfxSat.c \ + src/aig/mfx/mfxStrash.c \ + src/aig/mfx/mfxWin.c -- cgit v1.2.3