From 3b790eb17e54cd922440a1a3b18a5cfdd5cbcadb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 2 Feb 2008 08:01:00 -0800 Subject: Version abc80202 --- src/opt/mfs/mfs.h | 73 ++++++++++++++++ src/opt/mfs/mfsCore.c | 143 +++++++++++++++++++++++++++++++ src/opt/mfs/mfsInt.h | 110 ++++++++++++++++++++++++ src/opt/mfs/mfsMan.c | 132 ++++++++++++++++++++++++++++ src/opt/mfs/mfsSat.c | 113 ++++++++++++++++++++++++ src/opt/mfs/mfsStrash.c | 224 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/mfs/mfsWin.c | 112 ++++++++++++++++++++++++ src/opt/mfs/mfs_.c | 47 ++++++++++ src/opt/mfs/module.make | 5 ++ 9 files changed, 959 insertions(+) create mode 100644 src/opt/mfs/mfs.h create mode 100644 src/opt/mfs/mfsCore.c create mode 100644 src/opt/mfs/mfsInt.h create mode 100644 src/opt/mfs/mfsMan.c create mode 100644 src/opt/mfs/mfsSat.c create mode 100644 src/opt/mfs/mfsStrash.c create mode 100644 src/opt/mfs/mfsWin.c create mode 100644 src/opt/mfs/mfs_.c create mode 100644 src/opt/mfs/module.make (limited to 'src/opt') diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h new file mode 100644 index 00000000..a7ca3819 --- /dev/null +++ b/src/opt/mfs/mfs.h @@ -0,0 +1,73 @@ +/**CFile**************************************************************** + + FileName [mfs.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: mfs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFS_H__ +#define __MFS_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Mfs_Par_t_ Mfs_Par_t; +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 fArea; // performs optimization for area + int fDelay; // performs optimization for delay + int fVerbose; // enable basic stats + int fVeryVerbose; // enable detailed stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfsCore.c ==========================================================*/ +extern int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c new file mode 100644 index 00000000..fe0d84c3 --- /dev/null +++ b/src/opt/mfs/mfsCore.c @@ -0,0 +1,143 @@ +/**CFile**************************************************************** + + FileName [mfsCore.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: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + int clk; + // 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; + // 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, Abc_ObjFaninNum(pNode) ); +p->timeCnf += clock() - clk; + // create the SAT problem +clk = clock(); + p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + // solve the SAT problem + Abc_NtkMfsSolveSat( p, pNode ); +p->timeSat += clock() - clk; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) +{ + Mfs_Man_t * p; + Abc_Obj_t * pObj; + int i, Counter; + + assert( Abc_NtkIsLogic(pNtk) ); + if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX ) + { + printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); + return 1; + } + // perform the network sweep + Abc_NtkSweep( pNtk, 0 ); + // convert into the AIG + if ( !Abc_NtkToAig(pNtk) ) + { + fprintf( stdout, "Converting to BDD has failed.\n" ); + 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->pNtk = pNtk; + p->pCare = pNtk->pManExdc; + + // 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 ); + } + + // compute don't-cares for each node + Abc_NtkForEachNode( pNtk, pObj, i ) + Abc_NtkMfsNode( p, pObj ); + + // undo labesl + if ( p->pCare ) + { + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pData = NULL; + } + + // free the manager + Mfs_ManStop( p ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h new file mode 100644 index 00000000..6ba5903e --- /dev/null +++ b/src/opt/mfs/mfsInt.h @@ -0,0 +1,110 @@ +/**CFile**************************************************************** + + FileName [mfsInt.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: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MFS_INT_H__ +#define __MFS_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" +#include "mfs.h" +#include "aig.h" +#include "cnf.h" +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define MFS_FANIN_MAX 10 + +typedef struct Mfs_Man_t_ Mfs_Man_t; +struct Mfs_Man_t_ +{ + // input data + Mfs_Par_t * pPars; + Abc_Ntk_t * pNtk; + Aig_Man_t * pCare; + // 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_Int_t * vProjVars; // the projection variables + // 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 + // 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[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set + // performance statistics + int nNodesTried; + int nNodesBad; + int nMintsCare; + int nMintsTotal; + // statistics + int timeWin; + int timeAig; + int timeCnf; + int timeSat; +}; + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== mfsMan.c ==========================================================*/ +extern Mfs_Man_t * Mfs_ManAlloc(); +extern void Mfs_ManStop( Mfs_Man_t * p ); +extern void Mfs_ManClean( Mfs_Man_t * p ); +/*=== mfsSat.c ==========================================================*/ +extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); +/*=== mfsStrash.c ==========================================================*/ +extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ); +/*=== mfsWin.c ==========================================================*/ +extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c new file mode 100644 index 00000000..1341e373 --- /dev/null +++ b/src/opt/mfs/mfsMan.c @@ -0,0 +1,132 @@ +/**CFile**************************************************************** + + FileName [mfsMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedure to manipulation the manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfsMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mfs_Man_t * Mfs_ManAlloc() +{ + Mfs_Man_t * p; + // start the manager + p = ALLOC( Mfs_Man_t, 1 ); + memset( p, 0, sizeof(Mfs_Man_t) ); + p->vProjVars = Vec_IntAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfs_ManClean( Mfs_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 ); + p->pAigWin = NULL; + p->pCnf = NULL; + p->pSat = NULL; + p->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfs_ManStop( Mfs_Man_t * p ) +{ + Mfs_ManPrint( p ); + Mfs_ManClean( p ); + Vec_IntFree( p->vProjVars ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c new file mode 100644 index 00000000..d995000f --- /dev/null +++ b/src/opt/mfs/mfsSat.c @@ -0,0 +1,113 @@ +/**CFile**************************************************************** + + FileName [mfsSat.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: mfsSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Enumerates through the SAT assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ) + return 0; + // 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 [] + +***********************************************************************/ +void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Aig_Obj_t * pObjPo; + int i; + // collect projection variables + Vec_IntClear( p->vProjVars ); + Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_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 + while ( Abc_NtkMfsSolveSat_iter( p ) ); + + // write statistics + p->nCares = 0; + for ( i = 0; i < p->nWords; i++ ) + p->nCares += Aig_WordCountOnes( p->uCare[i] ); + + p->nMintsCare += p->nCares; + p->nMintsTotal += 32 * p->nWords; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c new file mode 100644 index 00000000..7b467936 --- /dev/null +++ b/src/opt/mfs/mfsStrash.c @@ -0,0 +1,224 @@ +/**CFile**************************************************************** + + FileName [mfsStrash.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: mfsStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Construct BDDs and mark AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); + Abc_MfsConvertHopToAig_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 Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan ) +{ + Hop_Man_t * pHopMan; + Hop_Obj_t * pRoot; + Abc_Obj_t * pFanin; + int i; + // get the local AIG + pHopMan = pObjOld->pNtk->pManFunc; + pRoot = pObjOld->pData; + // check the case of a constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + { + pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) ); + pObjOld->pNext = pObjOld->pCopy; + return; + } + + // assign the fanin nodes + Abc_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy; + // construct the AIG + Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + + // assign the fanin nodes + Abc_ObjForEachFanin( pObjOld, pFanin, i ) + Hop_ManPi(pHopMan, i)->pData = pFanin->pNext; + // construct the AIG + Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan ); + pObjOld->pNext = (Abc_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 * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pRoot, * pExor; + Abc_Obj_t * pObj; + int i; + // assign AIG nodes to the leaves + Vec_PtrForEachEntry( p->vSupp, pObj, i ) + pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreatePi( pMan ); + // strash intermediate nodes + Abc_NtkIncrementTravId( pNode->pNtk ); + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + { + Abc_MfsConvertHopToAig( pObj, pMan ); + if ( pObj == pNode ) + pObj->pNext = Abc_ObjNot(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 * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan ) +{ + Aig_Obj_t * pObj0, * pObj1; + if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) ) + return pObj->pData; + Aig_ObjSetTravIdCurrent( pMan, pObj ); + if ( Aig_ObjIsPi(pObj) ) + return pObj->pData = NULL; + pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan ); + if ( pObj0 == NULL ) + return pObj->pData = NULL; + pObj1 = Abc_NtkConstructCare_rec( p, 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 [Creates AIG for the window with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Aig_Man_t * pMan; + Abc_Obj_t * pFanin; + Aig_Obj_t * pObjAig, * pPi, * pPo; + int i; + // start the new manager + pMan = Aig_ManStart( 1000 ); + // construct the root node's AIG cone + pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan ); + Aig_ObjCreatePo( pMan, pObjAig ); + if ( p->pCare ) + { + // mark the care set + Aig_ManIncrementTravId( p->pCare ); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + if ( pFanin->pData == NULL ) + continue; + pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 ); + 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 ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pMan, pObjAig ); + } + } + // construct the fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pObjAig = (Aig_Obj_t *)pFanin->pCopy; + Aig_ObjCreatePo( pMan, pObjAig ); + } + Aig_ManCleanup( pMan ); + return pMan; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c new file mode 100644 index 00000000..b812d44d --- /dev/null +++ b/src/opt/mfs/mfsWin.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [mfsWin.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: mfsWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfsInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the node should be a root.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_MfsComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit ) +{ + Abc_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 ( Abc_ObjFanoutNum(pNode) > nFanoutLimit ) + return 1; + // (2) the node has CO fanouts + // (3) the node has fanouts above the cutoff level + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MfsComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots ) +{ + Abc_Obj_t * pFanout; + int i; + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return; + Abc_NodeSetTravIdCurrent( pNode ); + // check if the node should be the root + if ( Abc_MfsComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) ) + Vec_PtrPush( vRoots, pNode ); + else // if not, explore its fanouts + Abc_ObjForEachFanout( pNode, pFanout, i ) + Abc_MfsComputeRoots_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 * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ) +{ + Vec_Ptr_t * vRoots; + vRoots = Vec_PtrAlloc( 10 ); + Abc_NtkIncrementTravId( pNode->pNtk ); + Abc_MfsComputeRoots_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/opt/mfs/mfs_.c b/src/opt/mfs/mfs_.c new file mode 100644 index 00000000..32caf7ff --- /dev/null +++ b/src/opt/mfs/mfs_.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/opt/mfs/module.make b/src/opt/mfs/module.make new file mode 100644 index 00000000..7b9f1260 --- /dev/null +++ b/src/opt/mfs/module.make @@ -0,0 +1,5 @@ +SRC += src/opt/mfs/mfsCore.c \ + src/opt/mfs/mfsMan.c \ + src/opt/mfs/mfsSat.c \ + src/opt/mfs/mfsStrash.c \ + src/opt/mfs/mfsWin.c -- cgit v1.2.3