From 8da52b6f202444711da6b1f1baac92e0a516c8e6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 Feb 2007 08:01:00 -0800 Subject: Version abc70202 --- abc.dsp | 12 ++ abc.rc | 4 + src/aig/ivy/ivy.h | 2 + src/aig/ivy/ivySeq.c | 34 +++-- src/aig/ivy/ivyUtil.c | 80 +++++++++++ src/base/abc/abc.h | 1 + src/base/abc/abcUtil.c | 22 ++- src/base/abci/abc.c | 7 +- src/base/abci/abcIvy.c | 28 +++- src/base/abci/abcPrint.c | 3 + src/base/abci/abcSat.c | 6 +- src/opt/bdc/bdc.h | 73 ++++++++++ src/opt/bdc/bdcCore.c | 157 +++++++++++++++++++++ src/opt/bdc/bdcDec.c | 76 ++++++++++ src/opt/bdc/bdcInt.h | 127 +++++++++++++++++ src/opt/bdc/bdc_.c | 50 +++++++ src/opt/bdc/module.make | 8 ++ src/opt/res/resCore.c | 73 ++++++---- src/opt/res/resDivs.c | 170 +++++++++++++++------- src/opt/res/resFilter.c | 10 +- src/opt/res/resInt.h | 70 ++++----- src/opt/res/resSat.c | 62 +++++++- src/opt/res/resSim.c | 6 +- src/opt/res/resStrash.c | 22 ++- src/opt/res/resUpdate.c | 8 +- src/opt/res/resWin.c | 358 ++++++++++++++++++++++++++++++----------------- src/sat/bsat/satInter.c | 42 +++--- src/sat/bsat/satSolver.c | 4 +- 28 files changed, 1214 insertions(+), 301 deletions(-) create mode 100644 src/opt/bdc/bdc.h create mode 100644 src/opt/bdc/bdcCore.c create mode 100644 src/opt/bdc/bdcDec.c create mode 100644 src/opt/bdc/bdcInt.h create mode 100644 src/opt/bdc/bdc_.c create mode 100644 src/opt/bdc/module.make diff --git a/abc.dsp b/abc.dsp index 47e870d7..62245a6d 100644 --- a/abc.dsp +++ b/abc.dsp @@ -1697,6 +1697,18 @@ SOURCE=.\src\opt\res\resUpdate.c SOURCE=.\src\opt\res\resWin.c # End Source File # End Group +# Begin Group "bdc" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\bdc\bdc.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\bdc\bdcInt.h +# End Source File +# End Group # End Group # Begin Group "map" diff --git a/abc.rc b/abc.rc index bbe7a6d4..82ef85de 100644 --- a/abc.rc +++ b/abc.rc @@ -102,6 +102,10 @@ alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" +# experimental implementation of don't-cares +alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b" +alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l" + # temporaries #alias t "rvl th/lib.v; rvv th/t2.v" #alias t "so c/pure_sat/test.c" diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h index 9e944028..6aa7fa9f 100644 --- a/src/aig/ivy/ivy.h +++ b/src/aig/ivy/ivy.h @@ -152,6 +152,7 @@ struct Ivy_FraigParams_t_ typedef struct Ivy_Cut_t_ Ivy_Cut_t; struct Ivy_Cut_t_ { + int nLatches; short nSize; short nSizeMax; int pArray[IVY_CUT_INPUT]; @@ -541,6 +542,7 @@ extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ); extern void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig ); extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig ); +extern int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ); #ifdef __cplusplus } diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c index 263a4398..0ee29fee 100644 --- a/src/aig/ivy/ivySeq.c +++ b/src/aig/ivy/ivySeq.c @@ -41,6 +41,11 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +//int nMoves; +//int nMovesS; +//int nClauses; +//int timeInv; + /**Function************************************************************* Synopsis [Performs incremental rewriting of the AIG.] @@ -58,6 +63,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) Ivy_Obj_t * pNode; int i, nNodes, nGain; int clk, clkStart = clock(); + // set the DC latch values Ivy_ManForEachLatch( p, pNode, i ) pNode->Init = IVY_INIT_DC; @@ -81,7 +87,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) // if ( Ivy_ObjIsBuf(pNode) ) // continue; // stop if all nodes have been tried once - if ( i > nNodes ) + if ( i > nNodes ) break; // for each cut, try to resynthesize it nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost ); @@ -114,6 +120,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); return 1; } + /**Function************************************************************* Synopsis [Performs rewriting for one node.] @@ -140,11 +147,11 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int Ivy_Cut_t * pCut; Ivy_Obj_t * pFanin;//, * pFanout; Vec_Ptr_t * vFanout; - unsigned uPhase, uTruthBest, uTruth; + unsigned uPhase, uTruthBest, uTruth;//, nNewClauses; char * pPerm; int nNodesSaved, nNodesSaveCur; int i, c, GainCur, GainBest = -1; - int clk, clk2; + int clk, clk2;//, clk3; p->nNodesConsidered++; // get the node's cuts @@ -201,18 +208,6 @@ clk2 = clock(); Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); p->timeMffc += clock() - clk2; -/* -if ( pNode->Id == 8648 ) -{ - int i; - printf( "Trying cut : {" ); - for ( i = 0; i < pCut->nSize; i++ ) - printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); -// printf( " }\n" ); - printf( " } " ); - Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" ); -} -*/ // evaluate the cut clk2 = clock(); @@ -252,6 +247,15 @@ p->timeRes += clock() - clk; } */ +//clk3 = clock(); +//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth ); +//timeInv += clock() - clk; + +// nClauses += nNewClauses; +// nMoves++; +// if ( nNewClauses > 0 ) +// nMovesS++; + // copy the leaves Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm ); diff --git a/src/aig/ivy/ivyUtil.c b/src/aig/ivy/ivyUtil.c index 0e44c216..ab62a276 100644 --- a/src/aig/ivy/ivyUtil.c +++ b/src/aig/ivy/ivyUtil.c @@ -731,6 +731,86 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig ) printf( "\n" ); } +/**Function************************************************************* + + Synopsis [Performs incremental rewriting of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ) +{ + int i; + printf( "Trying cut : {" ); + for ( i = 0; i < pCut->nSize; i++ ) + printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); + printf( " } " ); + Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs incremental rewriting of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ) +{ + Vec_Ptr_t * vArray; + Ivy_Obj_t * pObj, * pFanout; + int nLatches = 0; + int nPresent = 0; + int i, k; + int fVerbose = 0; + + if ( fVerbose ) + printf( "Trying cut : {" ); + for ( i = 0; i < pCut->nSize; i++ ) + { + if ( fVerbose ) + printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); + nLatches += Ivy_LeafLat(pCut->pArray[i]); + } + if ( fVerbose ) + printf( " } " ); + if ( fVerbose ) + printf( "Latches = %d. ", nLatches ); + + // check if there are latches on the fanout edges + vArray = Vec_PtrAlloc( 100 ); + for ( i = 0; i < pCut->nSize; i++ ) + { + pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) ); + Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k ) + { + if ( Ivy_ObjIsLatch(pFanout) ) + { + nPresent++; + break; + } + } + } + Vec_PtrSize( vArray ); + if ( fVerbose ) + { + printf( "Present = %d. ", nPresent ); + if ( nLatches > nPresent ) + printf( "Clauses = %d. ", 2*(nLatches - nPresent) ); + printf( "\n" ); + } + return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index ce1947a9..3d46cdf0 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -814,6 +814,7 @@ extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ); +extern int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk ); extern int Abc_NtkCountCopy( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index b86dc88f..3070e01a 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -105,7 +105,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; - if ( pNtk->nTravIds == (1<<30)-1 ) + if ( pNtk->nTravIds >= (1<<30)-1 ) { pNtk->nTravIds = 0; Abc_NtkForEachObj( pNtk, pObj, i ) @@ -445,6 +445,26 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ) return nFaninsMax; } +/**Function************************************************************* + + Synopsis [Reads the total number of all fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, nFanins = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + nFanins += Abc_ObjFaninNum(pNode); + return nFanins; +} + /**Function************************************************************* Synopsis [Cleans the copy field of all objects.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c2a6214d..3a6874ca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2569,6 +2569,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) Res_Par_t Pars, * pPars = &Pars; int c; +// printf( "Implementation of this command is not finished.\n" ); +// return 1; + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2641,8 +2644,8 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: mfs [-W ] [-S ] [-vwh]\n" ); fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" ); - fprintf( pErr, "\t-W : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); - fprintf( pErr, "\t-S : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords ); + fprintf( pErr, "\t-W : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); + fprintf( pErr, "\t-S : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 243067ce..00f8c183 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -187,18 +187,44 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int { Abc_Ntk_t * pNtkAig; Ivy_Man_t * pMan; + int clk; // int i; - +/* +extern int nMoves; +extern int nMovesS; +extern int nClauses; +extern int timeInv; + +nMoves = 0; +nMovesS = 0; +nClauses = 0; +timeInv = 0; +*/ pMan = Abc_NtkIvyBefore( pNtk, 1, 1 ); if ( pMan == NULL ) return NULL; //timeRetime = clock(); +clk = clock(); Ivy_ManHaigStart( pMan, fVerbose ); // Ivy_ManRewriteSeq( pMan, 0, 0 ); // for ( i = 0; i < nIters; i++ ) // Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 ); + +//printf( "%d ", Ivy_ManNodeNum(pMan) ); Ivy_ManRewriteSeq( pMan, 0, 0 ); + Ivy_ManRewriteSeq( pMan, 0, 0 ); + Ivy_ManRewriteSeq( pMan, 1, 0 ); +//printf( "%d ", Ivy_ManNodeNum(pMan) ); +//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) ); +//PRT( " ", clock() - clk ); +//printf( "\n" ); +/* + printf( "Moves = %d. ", nMoves ); + printf( "MovesS = %d. ", nMovesS ); + printf( "Clauses = %d. ", nClauses ); + PRT( "Time", timeInv ); +*/ // Ivy_ManRewriteSeq( pMan, 1, 0 ); //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) ); // Ivy_ManHaigPostprocess( pMan, fVerbose ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e66ce018..177c269b 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -77,7 +77,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) // fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 ); } else + { fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); + fprintf( pFile, " net = %5d", Abc_NtkGetTotalFanins(pNtk) ); + } if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) ) { diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 96540269..d9cae254 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -65,6 +65,10 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int pSat = Abc_NtkMiterSatCreate( pNtk, 0 ); if ( pSat == NULL ) return 1; +//printf( "%d \n", pSat->clauses.size ); +//sat_solver_delete( pSat ); +//return 1; + // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); @@ -619,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes ) nMuxes = 0; pSat = sat_solver_new(); -sat_solver_store_alloc( pSat ); +//sat_solver_store_alloc( pSat ); RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk ); sat_solver_store_mark_roots( pSat ); diff --git a/src/opt/bdc/bdc.h b/src/opt/bdc/bdc.h new file mode 100644 index 00000000..f0976bfe --- /dev/null +++ b/src/opt/bdc/bdc.h @@ -0,0 +1,73 @@ +/**CFile**************************************************************** + + FileName [bdc.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 30, 2007.] + + Revision [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __BDC_H__ +#define __BDC_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Bdc_Man_t_ Bdc_Man_t; +typedef struct Bdc_Par_t_ Bdc_Par_t; +struct Bdc_Par_t_ +{ + // general parameters + int nVarsMax; // the maximum support + int fVerbose; // enable basic stats + int fVeryVerbose; // enable detailed stats +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== bdcCore.c ==========================================================*/ +extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); +extern void Bdc_ManAlloc( Bdc_Man_t * p ); +extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/bdc/bdcCore.c b/src/opt/bdc/bdcCore.c new file mode 100644 index 00000000..f120ac3f --- /dev/null +++ b/src/opt/bdc/bdcCore.c @@ -0,0 +1,157 @@ +/**CFile**************************************************************** + + FileName [bdcCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [The gateway to bi-decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 30, 2007.] + + Revision [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "bdcInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) +{ + Bdc_Man_t * p; + int i; + p = ALLOC( Bdc_Man_t, 1 ); + memset( p, 0, sizeof(Bdc_Man_t) ); + assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 ); + p->pPars = pPars; + // memory + p->vMemory = Vec_IntStart( 1 << 16 ); + // internal nodes + p->nNodesAlloc = 256; + p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc ); + // set up hash table + p->nTableSize = (1 << p->pPars->nVarsMax); + p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize ); + p->vSpots = Vec_IntAlloc( 256 ); + // set up constant 1 and elementary variables + for ( i = 0; i < pPars->nVarsMax; i++ ) + { + } + p->nNodes = pPars->nVarsMax + 1; + // remember the current place in memory + p->nMemStart = Vec_IntSize( p->vMemory ); + return p; +} + + +/**Function************************************************************* + + Synopsis [Deallocate resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManAlloc( Bdc_Man_t * p ) +{ +} + +/**Function************************************************************* + + Synopsis [Sets up the divisors.] + + Description [The first n+1 entries are const1 and elem variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) +{ + Bdc_Fun_t ** pSpot, * pFunc; + unsigned * puTruth; + int i; + // clean hash table + Vec_PtrForEachEntry( p->vSpots, pSpot, i ) + *pSpot = NULL; + // reset nodes + p->nNodes = p->pPars->nVarsMax + 1; + // reset memory + Vec_IntShrink( p->vMemory, p->nMemStart ); + // add new nodes to the hash table + Vec_PtrForEachEntry( vDivs, puTruth, i ) + { + pFunc = Bdc_ManNewNode( p ); + pFunc->Type = BDC_TYPE_PI; + pFunc->puFunc = puTruth; + pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars ); + } +} + +/**Function************************************************************* + + Synopsis [Performs decomposition of one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit ) +{ + Bdc_Isf_t Isf, * pIsf = &Isf; + // set current manager parameters + p->nVars = nVars; + p->nWords = Kit_TruthWordNum( nVars ); + p->nNodeLimit = nNodeLimit; + Bdc_ManPrepare( p, vDivs ); + // copy the function + pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars ); + pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords ); + pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords ); + Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars ); + Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars ); + // call decomposition + p->pRoot = Bdc_ManDecompose_rec( p, pIsf ); + if ( p->pRoot == NULL ) + return -1; + return p->nNodes - (p->pPars->nVarsMax + 1); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/bdc/bdcDec.c b/src/opt/bdc/bdcDec.c new file mode 100644 index 00000000..1fbea911 --- /dev/null +++ b/src/opt/bdc/bdcDec.c @@ -0,0 +1,76 @@ +/**CFile**************************************************************** + + FileName [bdc_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 30, 2007.] + + Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "bdcInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs one step of bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) +{ + Bdc_Fun_t * pFunc; + Bdc_Isf_t IsfA, * pIsfA = &IsfA; + Bdc_Isf_t IsfB, * pIsfB = &IsfB; + int Type; + Bdc_SuppMinimize( p, pIsf ); + if ( pFunc = Bdc_TableLookup( p, pIsf ) ) + return pFunc; + pFunc = Bdc_ManNewNode( p ); + pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfA, pIsfB ); + pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfA ); + if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfA, pIsfB, pFunc->pFan0->puFunc ) ) + { + p->nNodes--; + return pFunc->pFan0; + } + pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfA ); + pFunc->puFunc = Vec_IntFetch( p->vMemory, p->nWords ); + pFunc->puFunc = + + + + + +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/bdc/bdcInt.h b/src/opt/bdc/bdcInt.h new file mode 100644 index 00000000..39d50ae9 --- /dev/null +++ b/src/opt/bdc/bdcInt.h @@ -0,0 +1,127 @@ +/**CFile**************************************************************** + + FileName [bdcInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 15, 2007.] + + Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __BDC_INT_H__ +#define __BDC_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "dec.h" +#include "bdc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// network types +typedef enum { + BDC_TYPE_NONE = 0, // 0: unknown + BDC_TYPE_CONST1, // 1: constant 1 + BDC_TYPE_PI, // 2: primary input + BDC_TYPE_AND, // 4: AND-gate + BDC_TYPE_XOR, // 5: XOR-gate + BDC_TYPE_MUX, // 6: MUX-gate + BDC_TYPE_OTHER // 7: unused +} Bdc_Type_t; + +typedef struct Bdc_Fun_t_ Bdc_Fun_t; +struct Bdc_Fun_t_ +{ + int Type; // Const1, PI, AND, XOR, MUX + Bdc_Fun_t * pFan0; // next function with same support + Bdc_Fun_t * pFan1; // next function with same support + Bdc_Fun_t * pFan2; // next function with same support + unsigned uSupp; // bit mask of current support + unsigned * puFunc; // the function of the node + Bdc_Fun_t * pNext; // next function with same support + void * pCopy; // the copy field +}; + +typedef struct Bdc_Isf_t_ Bdc_Isf_t; +struct Bdc_Isf_t_ +{ + unsigned uSupp; // bit mask of current support + unsigned uUnique; // bit mask of unique support + unsigned * puOn; // on-set + unsigned * puOff; // off-set + int Cost; // cost of this component +}; + +typedef struct Bdc_Man_t_ Bdc_Man_t; +struct Bdc_Man_t_ +{ + // external parameters + Bdc_Par_t * pPars; // parameter set + int nVars; // the number of variables + int nWords; // the number of words + int nNodeLimit; // the limit on the number of new nodes + // internal nodes + Bdc_Fun_t * pNodes; // storage for decomposition nodes + int nNodes; // the number of nodes used + int nNodesAlloc; // the number of nodes allocated + Bdc_Fun_t * pRoot; // the root node + // resub candidates + Bdc_Fun_t ** pTable; // hash table of candidates + int nTableSize; // hash table size (1 << nVarsMax) + // internal memory manager + Vec_Int_t * vMemory; // memory for internal truth tables + int nMemStart; // the starting memory size +}; + +// working with complemented attributes of objects +static inline bool Bdc_IsComplement( Bdc_Fun_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); } +static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); } +static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); } +static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); } + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== bdcSupp.c ==========================================================*/ +extern int Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); +/*=== bdcTable.c ==========================================================*/ +extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/bdc/bdc_.c b/src/opt/bdc/bdc_.c new file mode 100644 index 00000000..0fa51092 --- /dev/null +++ b/src/opt/bdc/bdc_.c @@ -0,0 +1,50 @@ +/**CFile**************************************************************** + + FileName [bdc_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Truth-table-based bi-decomposition engine.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 30, 2007.] + + Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "bdcInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/bdc/module.make b/src/opt/bdc/module.make new file mode 100644 index 00000000..85936f5b --- /dev/null +++ b/src/opt/bdc/module.make @@ -0,0 +1,8 @@ +SRC += src/opt/res/resCore.c \ + src/opt/res/resDivs.c \ + src/opt/res/resFilter.c \ + src/opt/res/resSat.c \ + src/opt/res/resSim.c \ + src/opt/res/resStrash.c \ + src/opt/res/resUpdate.c \ + src/opt/res/resWin.c diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 5f814c3a..609addf9 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -39,15 +39,19 @@ struct Res_Man_t_ Sto_Man_t * pCnf; // the CNF of the SAT problem Int_Man_t * pMan; // interpolation manager; Vec_Int_t * vMem; // memory for intermediate SOPs - Vec_Vec_t * vResubs; // resubstitution candidates + Vec_Vec_t * vResubs; // resubstitution candidates of the AIG + Vec_Vec_t * vResubsW; // resubstitution candidates of the window Vec_Vec_t * vLevels; // levelized structure for updating // statistics int nWins; // the number of windows tried int nWinNodes; // the total number of window nodes int nDivNodes; // the total number of divisors + int nWinsTriv; // the total number of trivial windows + int nWinsUsed; // the total number of useful windows (with at least one candidate) int nCandSets; // the total number of candidates int nProvedSets; // the total number of proved groups int nSimEmpty; // the empty simulation info + int nTotalNets; // the total number of nets // runtime int timeWin; // windowing int timeDiv; // divisors @@ -90,6 +94,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars ) p->pMan = Int_ManAlloc( 512 ); p->vMem = Vec_IntAlloc( 0 ); p->vResubs = Vec_VecStart( pPars->nCands ); + p->vResubsW = Vec_VecStart( pPars->nCands ); p->vLevels = Vec_VecStart( 32 ); return p; } @@ -113,9 +118,11 @@ void Res_ManFree( Res_Man_t * p ) printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins ); printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins ); printf( "\n" ); - printf( "SimEmpt = %d. ", p->nSimEmpty ); + printf( "WinsTriv = %d. ", p->nWinsTriv ); + printf( "SimsEmpt = %d. ", p->nSimEmpty ); + printf( "WindUsed = %d. ", p->nWinsUsed ); printf( "Cands = %d. ", p->nCandSets ); - printf( "Proved = %d. ", p->nProvedSets ); + printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets ); printf( "\n" ); PRT( "Windowing ", p->timeWin ); @@ -135,6 +142,7 @@ void Res_ManFree( Res_Man_t * p ) Int_ManFree( p->pMan ); Vec_IntFree( p->vMem ); Vec_VecFree( p->vResubs ); + Vec_VecFree( p->vResubsW ); Vec_VecFree( p->vLevels ); free( p ); } @@ -164,6 +172,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) // start the manager p = Res_ManAlloc( pPars ); + p->nTotalNets = Abc_NtkGetTotalFanins(pNtk); // set the number of levels Abc_NtkLevel( pNtk ); @@ -182,15 +191,32 @@ clk = clock(); p->timeWin += clock() - clk; if ( !RetValue ) continue; + p->nWinsTriv += Res_WinIsTrivial( p->pWin ); - p->nWins++; - p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels ); + if ( p->pPars->fVeryVerbose ) + { + printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level ); + printf( "Win = %3d/%3d/%4d/%3d ", + Vec_PtrSize(p->pWin->vLeaves), + Vec_PtrSize(p->pWin->vBranches), + Vec_PtrSize(p->pWin->vNodes), + Vec_PtrSize(p->pWin->vRoots) ); + } // collect the divisors clk = clock(); Res_WinDivisors( p->pWin, pObj->Level - 1 ); p->timeDiv += clock() - clk; - p->nDivNodes += Vec_PtrSize( p->pWin->vDivs ); + + p->nWins++; + p->nWinNodes += Vec_PtrSize(p->pWin->vNodes); + p->nDivNodes += Vec_PtrSize( p->pWin->vDivs); + + if ( p->pPars->fVeryVerbose ) + { + printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) ); + printf( "D+ = %3d ", p->pWin->nDivsPlus ); + } // create the AIG for the window clk = clock(); @@ -200,13 +226,6 @@ p->timeAig += clock() - clk; if ( p->pPars->fVeryVerbose ) { - printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level ); - printf( "Win = %3d/%3d/%4d/%3d ", - Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus, - p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels), - Vec_PtrSize(p->pWin->vRoots) ); - printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) ); - printf( "D+ = %3d ", p->pWin->nDivsPlus ); printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) ); printf( "\n" ); } @@ -223,12 +242,14 @@ p->timeSim += clock() - clk; // find resub candidates for the node clk = clock(); - RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs ); + RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW ); p->timeCand += clock() - clk; p->nCandSets += RetValue; if ( RetValue == 0 ) continue; + p->nWinsUsed++; + // iterate through candidate resubstitutions Vec_VecForEachLevel( p->vResubs, vFanins, k ) { @@ -247,26 +268,19 @@ p->timeSat += clock() - clk; } p->nProvedSets++; // printf( " Unsat\n" ); - continue; +// continue; // write it into a file // Sto_ManDumpClauses( p->pCnf, "trace.cnf" ); - - // interplate the problem if it was UNSAT + // interpolate the problem if it was UNSAT clk = clock(); - RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth ); + nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth ); p->timeInt += clock() - clk; - assert( RetValue == Vec_PtrSize(vFanins) - 2 ); - - if ( puTruth ) - { - Extra_PrintBinary( stdout, puTruth, 1 << RetValue ); - printf( "\n" ); - } - - continue; - + assert( nFanins == Vec_PtrSize(vFanins) - 2 ); + assert( puTruth ); +// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" ); + // transform interpolant into the AIG pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem ); @@ -276,10 +290,11 @@ p->timeInt += clock() - clk; // update the network clk = clock(); - Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels ); + Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels ); p->timeUpd += clock() - clk; break; } + } // quit resubstitution manager diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c index bff91983..af30592c 100644 --- a/src/opt/res/resDivs.c +++ b/src/opt/res/resDivs.c @@ -25,6 +25,9 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static void Res_WinMarkTfi( Res_Win_t * p ); +static int Res_WinVisitMffc( Res_Win_t * p ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -43,84 +46,155 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) { Abc_Obj_t * pObj, * pFanout, * pFanin; - int i, k, f, m; + int k, f, m; + // set the maximum level of the divisors p->nLevDivMax = nLevDivMax; - // mark the leaves and the internal nodes - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - pObj->fMarkA = 1; - Vec_VecForEachEntry( p->vLevels, pObj, i, k ) - pObj->fMarkA = 1; + // mark the TFI with the current trav ID + Abc_NtkIncrementTravId( p->pNode->pNtk ); + Res_WinMarkTfi( p ); - // prepare the new trav ID + // mark with the current trav ID those nodes that should not be divisors: + // (1) the node and its TFO + // (2) the MFFC of the node + // (3) the node's fanins (these are treated as a special case) Abc_NtkIncrementTravId( p->pNode->pNtk ); - // mark the TFO of the node (does not increment trav ID) - Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL ); - // mark the MFFC of the node (does not increment trav ID) + Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax ); Res_WinVisitMffc( p ); + Abc_ObjForEachFanin( p->pNode, pObj, k ) + Abc_NodeSetTravIdCurrent( pObj ); - // what about the fanouts of the leaves!!! + // 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 - // go through all the legal levels and check if their fanouts can be divisors - p->nDivsPlus = 0; - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 ) + // start collecting the divisors + Vec_PtrClear( p->vDivs ); + Vec_PtrForEachEntry( p->vLeaves, pObj, k ) + { + assert( (int)pObj->Level >= p->nLevLeafMin ); + if ( !Abc_NodeIsTravIdPrevious(pObj) ) + continue; + if ( (int)pObj->Level > p->nLevDivMax ) + continue; + Vec_PtrPush( p->vDivs, pObj ); + } + // add the internal nodes to the data structure + Vec_PtrForEachEntry( p->vNodes, pObj, k ) { - // skip nodes in the TFO or in the MFFC of node - if ( Abc_NodeIsTravIdCurrent(pObj) ) + if ( !Abc_NodeIsTravIdPrevious(pObj) ) + continue; + if ( (int)pObj->Level > p->nLevDivMax ) continue; + Vec_PtrPush( p->vDivs, pObj ); + } + + // explore the fanouts of already collected divisors + p->nDivsPlus = 0; + Vec_PtrForEachEntry( p->vDivs, pObj, k ) + { // consider fanouts of this node Abc_ObjForEachFanout( pObj, pFanout, f ) { + // stop if there are too many fanouts + if ( f > 20 ) + break; // skip nodes that are already added - if ( pFanout->fMarkA ) - continue; - // skip COs - if ( !Abc_ObjIsNode(pFanout) ) + if ( Abc_NodeIsTravIdPrevious(pFanout) ) continue; // skip nodes in the TFO or in the MFFC of node if ( Abc_NodeIsTravIdCurrent(pFanout) ) continue; + // skip COs + if ( !Abc_ObjIsNode(pFanout) ) + continue; // skip nodes with large level - if ( (int)pFanout->Level > p->nLevDivMax ) + if ( (int)pFanout->Level >= p->nLevDivMax ) continue; - // skip nodes whose fanins are not in the cone + // skip nodes whose fanins are not divisors Abc_ObjForEachFanin( pFanout, pFanin, m ) - if ( !pFanin->fMarkA ) + if ( !Abc_NodeIsTravIdPrevious(pFanin) ) break; if ( m < Abc_ObjFaninNum(pFanout) ) continue; - // add the node - Res_WinAddNode( p, pFanout ); + // add the node to the divisors + Vec_PtrPush( p->vDivs, pFanout ); + Vec_PtrPush( p->vNodes, pFanout ); + Abc_NodeSetTravIdPrevious( pFanout ); p->nDivsPlus++; } } +} - // unmark the leaves and the internal nodes - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - pObj->fMarkA = 0; - Vec_VecForEachEntry( p->vLevels, pObj, i, k ) - pObj->fMarkA = 0; +/**Function************************************************************* - // collect the divisors below the line - Vec_PtrClear( p->vDivs ); - // collect the node fanins first and mark the fanins - Abc_ObjForEachFanin( p->pNode, pFanin, m ) - { - Vec_PtrPush( p->vDivs, pFanin ); - Abc_NodeSetTravIdCurrent( pFanin ); - } - // collect the remaining leaves + Synopsis [Marks the TFI cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanin; + int i; + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent( pObj ); + assert( Abc_ObjIsNode(pObj) ); + // visit the fanins of the node + Abc_ObjForEachFanin( pObj, pFanin, i ) + Res_WinMarkTfi_rec( p, pFanin ); +} + +/**Function************************************************************* + + Synopsis [Marks the TFI cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Res_WinMarkTfi( Res_Win_t * p ) +{ + Abc_Obj_t * pObj; + int i; + // mark the leaves Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - if ( !Abc_NodeIsTravIdCurrent(pObj) ) - Vec_PtrPush( p->vDivs, pObj ); - // collect remaining unvisited divisors - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax ) - if ( !Abc_NodeIsTravIdCurrent(pObj) ) - Vec_PtrPush( p->vDivs, pObj ); - - // verify the resulting window -// Res_WinVerify( p ); + Abc_NodeSetTravIdCurrent( pObj ); + // start from the node + Res_WinMarkTfi_rec( p, p->pNode ); +} + +/**Function************************************************************* + + Synopsis [Marks the TFO of the collected nodes up to the given level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ) +{ + Abc_Obj_t * pFanout; + int i; + if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) + return; + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent( pObj ); + Abc_ObjForEachFanout( pObj, pFanout, i ) + Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit ); } /**Function************************************************************* diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c index 4f1be833..38f64815 100644 --- a/src/opt/res/resFilter.c +++ b/src/opt/res/resFilter.c @@ -42,7 +42,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim SeeAlso [] ***********************************************************************/ -int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs ) +int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ) { Abc_Obj_t * pFanin, * pFanin2; unsigned * pInfo; @@ -52,18 +52,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); if ( RetValue == 0 ) - printf( "Failed 1!" ); + printf( "Failed 1!\n" ); // collect the fanin info pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 ); RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); if ( RetValue == 0 ) - printf( "Failed 2!" ); + printf( "Failed 2!\n" ); // try removing fanins // printf( "Fanins: " ); Counter = 0; Vec_VecClear( vResubs ); + Vec_VecClear( vResubsW ); Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) { pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); @@ -78,7 +79,10 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Abc_ObjForEachFanin( pWin->pNode, pFanin2, k ) { if ( k != i ) + { Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); + Vec_VecPush( vResubsW, Counter, pFanin2 ); + } } Counter++; } diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h index 54251722..9d17cb1c 100644 --- a/src/opt/res/resInt.h +++ b/src/opt/res/resInt.h @@ -42,49 +42,48 @@ extern "C" { typedef struct Res_Win_t_ Res_Win_t; struct Res_Win_t_ { - // the general data - int nWinTfiMax; // the fanin levels - int nWinTfoMax; // the fanout levels - int nLevLeaves; // the level where leaves begin - int nLevDivMax; // the maximum divisor level - int nDivsPlus; // the number of additional divisors - int nLeavesPlus;// the number of additional leaves - Abc_Obj_t * pNode; // the node in the center + // windowing parameters + Abc_Obj_t * pNode; // the node in the center + int nWinTfiMax; // the fanin levels + int nWinTfoMax; // the fanout levels + int nLevDivMax; // the maximum divisor level + // internal windowing parameters + int nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root) + int nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves + // derived windowing parameters + int nLevLeafMin; // the minimum level of a leaf + int nLevTravMin; // the minimum level to search from TFO + int nDivsPlus; // the number of additional divisors // the window data - Vec_Vec_t * vLevels; // nodes by level - Vec_Ptr_t * vLeaves; // leaves of the window - Vec_Ptr_t * vRoots; // roots of the window - Vec_Ptr_t * vDivs; // the candidate divisors of the node + Vec_Ptr_t * vRoots; // outputs of the window + Vec_Ptr_t * vLeaves; // inputs of the window + Vec_Ptr_t * vBranches; // side nodes of the window + Vec_Ptr_t * vNodes; // internal nodes of the window + Vec_Ptr_t * vDivs; // candidate divisors of the node + // temporary data + Vec_Vec_t * vMatrix; // TFI nodes below the given node }; typedef struct Res_Sim_t_ Res_Sim_t; struct Res_Sim_t_ { - Abc_Ntk_t * pAig; // AIG for simulation + Abc_Ntk_t * pAig; // AIG for simulation // simulation parameters - int nWords; // the number of simulation words - int nPats; // the number of patterns - int nWordsOut; // the number of simulation words in the output patterns - int nPatsOut; // the number of patterns in the output patterns + int nWords; // the number of simulation words + int nPats; // the number of patterns + int nWordsOut; // the number of simulation words in the output patterns + int nPatsOut; // the number of patterns in the output patterns // simulation info - Vec_Ptr_t * vPats; // input simulation patterns - Vec_Ptr_t * vPats0; // input simulation patterns - Vec_Ptr_t * vPats1; // input simulation patterns - Vec_Ptr_t * vOuts; // output simulation info - int nPats0; // the number of 0-patterns accumulated - int nPats1; // the number of 1-patterns accumulated + Vec_Ptr_t * vPats; // input simulation patterns + Vec_Ptr_t * vPats0; // input simulation patterns + Vec_Ptr_t * vPats1; // input simulation patterns + Vec_Ptr_t * vOuts; // output simulation info + int nPats0; // the number of 0-patterns accumulated + int nPats1; // the number of 1-patterns accumulated // resub candidates - Vec_Vec_t * vCands; // resubstitution candidates + Vec_Vec_t * vCands; // resubstitution candidates }; -// adds one node to the window -static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj ) -{ - assert( !pObj->fMarkA ); - pObj->fMarkA = 1; - Vec_VecPush( p->vLevels, pObj->Level, pObj ); -} - //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -95,11 +94,12 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj ) /*=== resDivs.c ==========================================================*/ extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); -extern int Res_WinVisitMffc( Res_Win_t * p ); +extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ); /*=== resFilter.c ==========================================================*/ -extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs ); +extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ); /*=== resSat.c ==========================================================*/ extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); +extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); /*=== resSim.c ==========================================================*/ extern Res_Sim_t * Res_SimAlloc( int nWords ); extern void Res_SimFree( Res_Sim_t * p ); @@ -111,7 +111,7 @@ extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, H /*=== resWnd.c ==========================================================*/ extern Res_Win_t * Res_WinAlloc(); extern void Res_WinFree( Res_Win_t * p ); -extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode ); +extern int Res_WinIsTrivial( Res_Win_t * p ); extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p ); diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index ec609445..f9558c97 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -37,7 +37,7 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int /**Function************************************************************* - Synopsis [Loads AIG into the SAT solver.] + Synopsis [Loads AIG into the SAT solver for checking resubstitution.] Description [] @@ -124,6 +124,66 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) return pCnf; } +/**Function************************************************************* + + Synopsis [Loads AIG into the SAT solver for constrained simulation.] + + Description [The array of fanins contains exactly two entries: the + care set and the functions.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) +{ + sat_solver * pSat; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, nNodes; + + // make sure fanins contain POs of the AIG + pObj = Vec_PtrEntry( vFanins, 0 ); + assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) ); + assert( Vec_PtrSize(vFanins) == 2 ); + + // collect reachable nodes + vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); + + // assign unique numbers to each node + nNodes = 0; + Abc_AigConst1(pAig)->pCopy = (void *)nNodes++; + Abc_NtkForEachPi( pAig, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs + pObj->pCopy = (void *)nNodes++; + + // start the solver + pSat = sat_solver_new(); + + // add clause for the constant node + Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 ); + // add clauses for AND gates + Vec_PtrForEachEntry( vNodes, pObj, i ) + Res_SatAddAnd( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + Vec_PtrFree( vNodes ); + // add clauses for POs + Vec_PtrForEachEntry( vFanins, pObj, i ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + + // add trivial clauses + pObj = Vec_PtrEntry(vFanins, 0); + Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set + pObj = Vec_PtrEntry(vFanins, 1); + Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set + return pSat; +} + /**Function************************************************************* Synopsis [Asserts equality of the variable to a constant.] diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c index 81267540..cc896ec0 100644 --- a/src/opt/res/resSim.c +++ b/src/opt/res/resSim.c @@ -484,13 +484,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig ) Res_SimProcessPats( p ); if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) ) break; - } // printf( "%d ", Limit ); // report the last set of patterns - Res_SimReportOne( p ); - printf( "\n" ); +// Res_SimReportOne( p ); +// printf( "\n" ); // quit if there is not enough +// if ( p->nPats0 < 4 || p->nPats1 < 4 ) if ( p->nPats0 < 4 || p->nPats1 < 4 ) { // Res_SimReportOne( p ); diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c index d3a8efa8..fde842a4 100644 --- a/src/opt/res/resStrash.c +++ b/src/opt/res/resStrash.c @@ -48,22 +48,25 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) Vec_Ptr_t * vPairs; Abc_Ntk_t * pAig; Abc_Obj_t * pObj, * pMiter; - int i, k; + int i; assert( Abc_NtkHasAig(p->pNode->pNtk) ); +// Abc_NtkCleanCopy( p->pNode->pNtk ); // create the network pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pAig->pName = Extra_UtilStrsav( "window" ); // create the inputs Vec_PtrForEachEntry( p->vLeaves, pObj, i ) pObj->pCopy = Abc_NtkCreatePi( pAig ); + Vec_PtrForEachEntry( p->vBranches, pObj, i ) + pObj->pCopy = Abc_NtkCreatePi( pAig ); // go through the nodes in the topological order - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax ) + Vec_PtrForEachEntry( p->vNodes, pObj, i ) { pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); if ( pObj == p->pNode ) pObj->pCopy = Abc_ObjNot( pObj->pCopy ); } - // collect the PO outputs + // collect the POs vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) ); Vec_PtrForEachEntry( p->vRoots, pObj, i ) { @@ -72,15 +75,17 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) } // mark the TFO of the node Abc_NtkIncrementTravId( p->pNode->pNtk ); - Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL ); - // redo strashing in the TFO + Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax ); + // update strashing of the node p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy ); - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax ) + Abc_NodeSetTravIdPrevious( p->pNode ); + // redo strashing in the TFO + Vec_PtrForEachEntry( p->vNodes, pObj, i ) { if ( Abc_NodeIsTravIdCurrent(pObj) ) pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj ); } - // collect the PO outputs + // collect the POs Vec_PtrForEachEntry( p->vRoots, pObj, i ) Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy ); // add the miter @@ -89,6 +94,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) Vec_PtrFree( vPairs ); // add the node Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy ); + // add the fanins + Abc_ObjForEachFanin( p->pNode, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); // add the divisors Vec_PtrForEachEntry( p->vDivs, pObj, i ) Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c index 06704b1c..01400ead 100644 --- a/src/opt/res/resUpdate.c +++ b/src/opt/res/resUpdate.c @@ -45,11 +45,11 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj ); void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels ) { Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp; - int i, k, m; + int Lev, k, m; // create the new node pObjNew = Abc_NtkCreateNode( pObj->pNtk ); pObjNew->pData = pFunc; - Vec_PtrForEachEntry( vFanins, pFanin, i ) + Vec_PtrForEachEntry( vFanins, pFanin, k ) Abc_ObjAddFanin( pObjNew, pFanin ); // replace the old node by the new node pObjNew->Level = pObj->Level; @@ -62,12 +62,12 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc Vec_VecPush( vLevels, pObjNew->Level, pObjNew ); pObjNew->fMarkA = 1; // recursively update level - Vec_VecForEachEntryStart( vLevels, pTemp, i, k, pObjNew->Level ) + Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level ) { pTemp->fMarkA = 0; pTemp->Level = Res_UpdateNetworkLevelNew( pTemp ); // if the level did not change, to need to check the fanout levels - if ( (int)pTemp->Level == i ) + if ( (int)pTemp->Level == Lev ) continue; // schedule fanout for level update Abc_ObjForEachFanout( pTemp, pFanout, m ) diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c index fa74b219..80a65ea8 100644 --- a/src/opt/res/resWin.c +++ b/src/opt/res/resWin.c @@ -43,12 +43,19 @@ Res_Win_t * Res_WinAlloc() { Res_Win_t * p; + // start the manager p = ALLOC( Res_Win_t, 1 ); memset( p, 0, sizeof(Res_Win_t) ); - p->vLevels = Vec_VecStart( 128 ); - p->vLeaves = Vec_PtrAlloc( 512 ); - p->vRoots = Vec_PtrAlloc( 512 ); - p->vDivs = Vec_PtrAlloc( 512 ); + // set internal parameters + p->nFanoutLimit = 10; + p->nLevTfiMinus = 3; + // allocate storage + p->vRoots = Vec_PtrAlloc( 256 ); + p->vLeaves = Vec_PtrAlloc( 256 ); + p->vBranches = Vec_PtrAlloc( 256 ); + p->vNodes = Vec_PtrAlloc( 256 ); + p->vDivs = Vec_PtrAlloc( 256 ); + p->vMatrix = Vec_VecStart( 128 ); return p; } @@ -65,48 +72,87 @@ Res_Win_t * Res_WinAlloc() ***********************************************************************/ void Res_WinFree( Res_Win_t * p ) { - Vec_VecFree( p->vLevels ); - Vec_PtrFree( p->vLeaves ); Vec_PtrFree( p->vRoots ); + Vec_PtrFree( p->vLeaves ); + Vec_PtrFree( p->vBranches ); + Vec_PtrFree( p->vNodes ); Vec_PtrFree( p->vDivs ); + Vec_VecFree( p->vMatrix ); free( p ); } + + /**Function************************************************************* - Synopsis [Collects nodes in the limited TFI of the node.] + Synopsis [Collect the limited TFI cone of the node.] - Description [Marks the collected nodes.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Res_WinCollectNodeTfi( Res_Win_t * p ) +void Res_WinCollectLeavesAndNodes( Res_Win_t * p ) { Vec_Ptr_t * vFront; - Abc_Obj_t * pObj, * pFanin; + Abc_Obj_t * pObj, * pTemp; int i, k, m; - // expand storage for levels - if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax ) - Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax ); - // start the frontier - Vec_VecClear( p->vLevels ); - Res_WinAddNode( p, p->pNode ); - // add one level at a time - Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 ) + + assert( p->nWinTfiMax > 0 ); + assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax ); + + // start matrix with the node + Vec_VecClear( p->vMatrix ); + Vec_VecPush( p->vMatrix, 0, p->pNode ); + Abc_NtkIncrementTravId( p->pNode->pNtk ); + Abc_NodeSetTravIdCurrent( p->pNode ); + + // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax") + Vec_PtrClear( p->vLeaves ); + Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax ) { Vec_PtrForEachEntry( vFront, pObj, k ) - Abc_ObjForEachFanin( pObj, pFanin, m ) - if ( !pFanin->fMarkA ) - Res_WinAddNode( p, pFanin ); + { + Abc_ObjForEachFanin( pObj, pTemp, m ) + { + if ( Abc_NodeIsTravIdCurrent( pTemp ) ) + continue; + Abc_NodeSetTravIdCurrent( pTemp ); + if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax ) + Vec_PtrPush( p->vLeaves, pTemp ); + else + Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp ); + } + } } + assert( Vec_PtrSize(p->vLeaves) > 0 ); + + // collect the nodes in the reverse order + Vec_PtrClear( p->vNodes ); + Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 ) + { + Vec_PtrForEachEntry( vFront, pObj, k ) + Vec_PtrPush( p->vNodes, pObj ); + Vec_PtrClear( vFront ); + } + + // get the lowest leaf level + p->nLevLeafMin = ABC_INFINITY; + Vec_PtrForEachEntry( p->vLeaves, pObj, k ) + p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level ); + + // set minimum traversal level + p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin ); + assert( p->nLevTravMin >= 0 ); } + + /**Function************************************************************* - Synopsis [Collect all the nodes that fanin into the window nodes.] + Synopsis [Returns 1 if the node should be a root.] Description [] @@ -115,24 +161,25 @@ void Res_WinCollectNodeTfi( Res_Win_t * p ) SeeAlso [] ***********************************************************************/ -void Res_WinCollectLeaves( Res_Win_t * p ) +static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit ) { - Vec_Ptr_t * vLevel; - Abc_Obj_t * pObj; - int i, k; - // add the leaves - Vec_PtrClear( p->vLeaves ); - // collect the nodes below the given level - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves ) - Vec_PtrPush( p->vLeaves, pObj ); - // remove leaves from the set - Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves ) - Vec_PtrClear( vLevel ); + 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 [Marks the TFO of the collected nodes up to the given level.] + Synopsis [Recursively collects the root candidates.] Description [] @@ -141,22 +188,85 @@ void Res_WinCollectLeaves( Res_Win_t * p ) SeeAlso [] ***********************************************************************/ -void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode ) +void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots ) { Abc_Obj_t * pFanout; int i; - if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode ) - return; - if ( Abc_NodeIsTravIdCurrent(pObj) ) + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_NodeIsTravIdCurrent(pNode) ) return; - Abc_NodeSetTravIdCurrent( pObj ); - Abc_ObjForEachFanout( pObj, pFanout, i ) - Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode ); + Abc_NodeSetTravIdCurrent( pNode ); + // check if the node should be the root + if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) ) + Vec_PtrPush( vRoots, pNode ); + else // if not, explore its fanouts + Abc_ObjForEachFanout( pNode, pFanout, i ) + Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots ); +} + +/**Function************************************************************* + + Synopsis [Recursively collects the root candidates.] + + Description [Returns 1 if the only root is this node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_WinComputeRoots( Res_Win_t * p ) +{ + Vec_PtrClear( p->vRoots ); + Abc_NtkIncrementTravId( p->pNode->pNtk ); + Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots ); + assert( Vec_PtrSize(p->vRoots) > 0 ); + if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode ) + return 0; + return 1; +} + + + +/**Function************************************************************* + + Synopsis [Marks the paths from the roots to the leaves.] + + Description [Returns 1 if the the node can reach a leaf.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin ) +{ + Abc_Obj_t * pFanin; + int i, RetValue; + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return 1; + if ( Abc_NodeIsTravIdPrevious(pNode) ) + return 0; + // assume that the node does not have access to the leaves + Abc_NodeSetTravIdPrevious( pNode ); + // skip nodes below the given level + if ( pNode == pPivot || (int)pNode->Level <= nLevelMin ) + return 0; + assert( Abc_ObjIsNode(pNode) ); + // check if the fanins have access to the leaves + RetValue = 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin ); + // relabel the node if it has access to the leaves + if ( RetValue ) + Abc_NodeSetTravIdCurrent( pNode ); + return RetValue; } /**Function************************************************************* - Synopsis [Marks the TFO of the collected nodes up to the given level.] + Synopsis [Marks the paths from the roots to the leaves.] Description [] @@ -165,15 +275,25 @@ void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNo SeeAlso [] ***********************************************************************/ -void Res_WinSweepLeafTfo( Res_Win_t * p ) +void Res_WinMarkPaths( Res_Win_t * p ) { Abc_Obj_t * pObj; int i; + // mark the leaves + Abc_NtkIncrementTravId( p->pNode->pNtk ); Abc_NtkIncrementTravId( p->pNode->pNtk ); Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Res_WinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode ); + Abc_NodeSetTravIdCurrent( pObj ); + // traverse from the roots and mark the nodes that can reach leaves + // the nodes that do not reach leaves have previous trav ID + // the nodes that reach leaves have current trav ID + Vec_PtrForEachEntry( p->vRoots, pObj, i ) + Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin ); } + + + /**Function************************************************************* Synopsis [Recursively collects the roots.] @@ -185,29 +305,27 @@ void Res_WinSweepLeafTfo( Res_Win_t * p ) SeeAlso [] ***********************************************************************/ -void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) +void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) { Abc_Obj_t * pFanout; int i; assert( Abc_ObjIsNode(pObj) ); + assert( Abc_NodeIsTravIdCurrent(pObj) ); // check if the node has all fanouts marked Abc_ObjForEachFanout( pObj, pFanout, i ) if ( !Abc_NodeIsTravIdCurrent(pFanout) ) break; - // if some of the fanouts are unmarked, add the node to the root + // if some of the fanouts are unmarked, add the node to the roots if ( i < Abc_ObjFanoutNum(pObj) ) - { Vec_PtrPushUnique( vRoots, pObj ); - return; - } - // otherwise, call recursively - Abc_ObjForEachFanout( pObj, pFanout, i ) - Res_WinCollectRoots_rec( pFanout, vRoots ); + else // otherwise, call recursively + Abc_ObjForEachFanout( pObj, pFanout, i ) + Res_WinFinalizeRoots_rec( pFanout, vRoots ); } /**Function************************************************************* - Synopsis [Collects the roots of the window.] + Synopsis [Finalizes the roots of the window.] Description [Roots of the window are the nodes that have at least one fanout that it not in the TFO of the leaves.] @@ -217,13 +335,21 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) SeeAlso [] ***********************************************************************/ -void Res_WinCollectRoots( Res_Win_t * p ) +int Res_WinFinalizeRoots( Res_Win_t * p ) { assert( !Abc_NodeIsTravIdCurrent(p->pNode) ); + // mark the node with the old traversal ID + Abc_NodeSetTravIdCurrent( p->pNode ); + // recollect the roots Vec_PtrClear( p->vRoots ); - Res_WinCollectRoots_rec( p->pNode, p->vRoots ); + Res_WinFinalizeRoots_rec( p->pNode, p->vRoots ); + assert( Vec_PtrSize(p->vRoots) > 0 ); + if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode ) + return 0; + return 1; } + /**Function************************************************************* Synopsis [Recursively adds missing nodes and leaves.] @@ -235,23 +361,27 @@ void Res_WinCollectRoots( Res_Win_t * p ) SeeAlso [] ***********************************************************************/ -void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj ) +void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin ) { Abc_Obj_t * pFanin; int i; - if ( pObj->fMarkA ) + // skip the already collected leaves, nodes, and branches + if ( Abc_NodeIsTravIdCurrent(pObj) ) return; - if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves ) + // if this is not an internal node - make it a new branch + if ( !Abc_NodeIsTravIdPrevious(pObj) ) { - p->nLeavesPlus++; - Vec_PtrPush( p->vLeaves, pObj ); - pObj->fMarkA = 1; + Abc_NodeSetTravIdCurrent( pObj ); + Vec_PtrPush( p->vBranches, pObj ); return; } - Res_WinAddNode( p, pObj ); + assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect! + Abc_NodeSetTravIdCurrent( pObj ); // visit the fanins of the node Abc_ObjForEachFanin( pObj, pFanin, i ) - Res_WinAddMissing_rec( p, pFanin ); + Res_WinAddMissing_rec( p, pFanin, nLevTravMin ); + // collect the node + Vec_PtrPush( p->vNodes, pObj ); } /**Function************************************************************* @@ -269,34 +399,25 @@ void Res_WinAddMissing( Res_Win_t * p ) { Abc_Obj_t * pObj; int i; + // mark the leaves + Abc_NtkIncrementTravId( p->pNode->pNtk ); + Vec_PtrForEachEntry( p->vLeaves, pObj, i ) + Abc_NodeSetTravIdCurrent( pObj ); + // mark the already collected nodes + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + Abc_NodeSetTravIdCurrent( pObj ); + // explore from the roots + Vec_PtrClear( p->vBranches ); Vec_PtrForEachEntry( p->vRoots, pObj, i ) - Res_WinAddMissing_rec( p, pObj ); + Res_WinAddMissing_rec( p, pObj, p->nLevTravMin ); } -/**Function************************************************************* - - Synopsis [Unmarks the leaves and nodes of the window.] - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Res_WinUnmark( Res_Win_t * p ) -{ - Abc_Obj_t * pObj; - int i, k; - Vec_VecForEachEntry( p->vLevels, pObj, i, k ) - pObj->fMarkA = 0; - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - pObj->fMarkA = 0; -} + /**Function************************************************************* - Synopsis [Verifies the window.] + Synopsis [Returns 1 if the window is trivial (without TFO).] Description [] @@ -305,30 +426,9 @@ void Res_WinUnmark( Res_Win_t * p ) SeeAlso [] ***********************************************************************/ -void Res_WinVerify( Res_Win_t * p ) +int Res_WinIsTrivial( Res_Win_t * p ) { - Abc_Obj_t * pObj, * pFanin; - int i, k, f; - // make sure the nodes are not marked - Abc_NtkForEachObj( p->pNode->pNtk, pObj, i ) - assert( !pObj->fMarkA ); - // mark the leaves - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - pObj->fMarkA = 1; - // make sure all nodes in the topological order have their fanins in the set - Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax ) - { - assert( (int)pObj->Level == i ); - assert( !pObj->fMarkA ); - Abc_ObjForEachFanin( pObj, pFanin, f ) - assert( pFanin->fMarkA ); - pObj->fMarkA = 1; - } - // make sure the roots are marked - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - assert( pObj->fMarkA ); - // unmark - Res_WinUnmark( p ); + return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode; } /**Function************************************************************* @@ -345,31 +445,29 @@ void Res_WinVerify( Res_Win_t * p ) int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p ) { assert( Abc_ObjIsNode(pNode) ); - assert( nWinTfiMax > 0 && nWinTfoMax > 0 ); + assert( nWinTfiMax > 0 && nWinTfiMax < 10 ); + assert( nWinTfoMax >= 0 && nWinTfoMax < 10 ); + // initialize the window - p->pNode = pNode; + p->pNode = pNode; p->nWinTfiMax = nWinTfiMax; p->nWinTfoMax = nWinTfoMax; - p->nLeavesPlus = 0; - p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 ); - // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves) - Res_WinCollectNodeTfi( p ); - // find the leaves of the window - Res_WinCollectLeaves( p ); - // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax) - Res_WinSweepLeafTfo( p ); - // find the roots of the window - Res_WinCollectRoots( p ); - // add the nodes in the TFI of the roots that are not yet in the window - Res_WinAddMissing( p ); - // unmark window nodes - Res_WinUnmark( p ); - // clear the divisor information - p->nLevDivMax = 0; - p->nDivsPlus = 0; - Vec_PtrClear( p->vDivs ); - // verify the resulting window -// Res_WinVerify( p ); + Vec_PtrClear( p->vRoots ); + Vec_PtrPush( p->vRoots, pNode ); + + // compute the leaves + Res_WinCollectLeavesAndNodes( p ); + + // compute the candidate roots + if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) ) + { + // mark the paths from the roots to the leaves + Res_WinMarkPaths( p ); + // refine the roots and add branches and missing nodes + if ( Res_WinFinalizeRoots( p ) ) + Res_WinAddMissing( p ); + } + return 1; } diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index 32a011b9..b52cd6c7 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -771,7 +771,8 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause ) { // construct the proof Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); - printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + if ( p->fVerbose ) + printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); return 0; } @@ -827,7 +828,7 @@ int Int_ManProcessRoots( Int_Man_t * p ) if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); + printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" ); assert( 0 ); return 0; } @@ -838,8 +839,9 @@ int Int_ManProcessRoots( Int_Man_t * p ) if ( pClause ) { // detected root level conflict - printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); -// assert( 0 ); + Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } @@ -925,17 +927,12 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); p->pCnf = pCnf; + p->fVerbose = fVerbose; + *ppResult = NULL; // adjust the manager Int_ManResize( p ); - // propagate root level assignments - if ( !Int_ManProcessRoots( p ) ) - { - *ppResult = NULL; - return p->nVarsAB; - } - // prepare the interpolant computation Int_ManPrepareInter( p ); @@ -951,15 +948,19 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned Sto_ManForEachClauseRoot( p->pCnf, pClause ) Int_ManProofWriteOne( p, pClause ); - // consider each learned clause - Sto_ManForEachClause( p->pCnf, pClause ) + // propagate root level assignments + if ( Int_ManProcessRoots( p ) ) { - if ( pClause->fRoot ) - continue; - if ( !Int_ManProofRecordOne( p, pClause ) ) + // if there is no conflict, consider learned clauses + Sto_ManForEachClause( p->pCnf, pClause ) { - RetValue = 0; - break; + if ( pClause->fRoot ) + continue; + if ( !Int_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } } } @@ -970,12 +971,15 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned p->pFile = NULL; } + if ( fVerbose ) + { printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); - p->timeTotal += clock() - clkTotal; + } + *ppResult = Int_ManTruthRead( p, p->pCnf->pTail ); return p->nVarsAB; } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 1756b5df..c4847be4 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1264,7 +1264,7 @@ void sat_solver_store_alloc( sat_solver * s ) void sat_solver_store_write( sat_solver * s, char * pFileName ) { extern void Sto_ManDumpClauses( void * p, char * pFileName ); - Sto_ManDumpClauses( s->pStore, pFileName ); + if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName ); } void sat_solver_store_free( sat_solver * s ) @@ -1273,7 +1273,7 @@ void sat_solver_store_free( sat_solver * s ) if ( s->pStore ) Sto_ManFree( s->pStore ); s->pStore = NULL; } - + void sat_solver_store_mark_roots( sat_solver * s ) { extern void Sto_ManMarkRoots( void * p ); -- cgit v1.2.3