From ff6f0943362c30176fd1f961bcbd19e188cee520 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 14 Mar 2008 08:01:00 -0700 Subject: Version abc80314 --- src/opt/mfs/mfsCore.c | 44 +++++++++++++++++++++++++++++++++++++------- src/opt/mfs/mfsInt.h | 8 +++++++- src/opt/mfs/mfsMan.c | 6 ++++++ src/opt/mfs/mfsSat.c | 12 ++++++++++++ 4 files changed, 62 insertions(+), 8 deletions(-) (limited to 'src/opt/mfs') diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 4e4f7490..bde2ad42 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -100,7 +100,10 @@ p->timeSat += clock() - clk; ***********************************************************************/ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { - int clk; + Hop_Obj_t * pObj; + extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ); + + int nGain, clk; p->nNodesTried++; // prepare data structure for this node Mfs_ManClean( p ); @@ -128,6 +131,16 @@ clk = clock(); // solve the SAT problem Abc_NtkMfsSolveSat( p, pNode ); p->timeSat += clock() - clk; + // minimize the local function of the node using bi-decomposition + assert( p->nFanins == Abc_ObjFaninNum(pNode) ); + pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare ); + nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj); + if ( nGain >= 0 ) + { + p->nNodesDec++; + p->nNodesGained += nGain; + pNode->pData = pObj; + } return 1; } @@ -146,6 +159,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ); + Bdc_Par_t Pars = {0}, * pDecPars = &Pars; ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; @@ -157,8 +171,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) nFaninMax = Abc_NtkGetFaninMax(pNtk); if ( nFaninMax > MFS_FANIN_MAX ) { - printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); - return 1; + printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX ); + nFaninMax = MFS_FANIN_MAX; } // perform the network sweep Abc_NtkSweep( pNtk, 0 ); @@ -186,11 +200,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { if ( p->pCare != NULL ) printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); - else - printf( "Performing optimization without constraints.\n" ); +// else +// printf( "Performing optimization without constraints.\n" ); } if ( !pPars->fResub ) - printf( "Currently don't-cares are not used but the stats are printed.\n" ); + { + pDecPars->nVarsMax = nFaninMax; + pDecPars->fVerbose = pPars->fVerbose; + p->vTruth = Vec_IntAlloc( 0 ); + p->pManDec = Bdc_ManAlloc( pDecPars ); + } // label the register outputs if ( p->pCare ) @@ -211,15 +230,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) { if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) continue; + if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) + continue; if ( !p->pPars->fVeryVerbose ) Extra_ProgressBarUpdate( pProgress, i, NULL ); if ( pPars->fResub ) Abc_NtkMfsResub( p, pObj ); - else + else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) Abc_NtkMfsNode( p, pObj ); } Extra_ProgressBarStop( pProgress ); Abc_NtkStopReverseLevels( pNtk ); + + // perform the sweeping + if ( !pPars->fResub ) + { + extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ); + Abc_NtkSweep( pNtk, 0 ); + Abc_NtkBidecResyn( pNtk, 0 ); + } + p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk); p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk); diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 91395d03..f4da45ef 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -35,12 +35,13 @@ extern "C" { #include "cnf.h" #include "satSolver.h" #include "satStore.h" +#include "bdc.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#define MFS_FANIN_MAX 10 +#define MFS_FANIN_MAX 12 typedef struct Mfs_Man_t_ Mfs_Man_t; struct Mfs_Man_t_ @@ -64,6 +65,11 @@ struct Mfs_Man_t_ 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; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 17ca40fc..f1b3f44c 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -131,6 +131,8 @@ void Mfs_ManPrint( Mfs_Man_t * p ) 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.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained ); } /* PRTP( "Win", p->timeWin , p->timeTotal ); @@ -158,6 +160,10 @@ void Mfs_ManStop( Mfs_Man_t * p ) { if ( p->pPars->fVerbose ) Mfs_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 ) diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index efb09b39..2529e207 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -110,6 +110,18 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) Extra_PrintBinary( stdout, p->uCare, (1<nFanins) ); printf( "\n" ); } + + // map the care + if ( p->nFanins > 4 ) + return; + 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 ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3