From 6b55bf0205f414ca711d92baea115a808fff3dc9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 26 Nov 2016 14:28:12 -0800 Subject: New SAT-based optimization package. --- src/base/abci/abc.c | 129 +++++++++++++ src/base/io/ioWriteDot.c | 2 +- src/misc/util/utilTruth.h | 28 +++ src/opt/sbd/sbd.h | 52 ++--- src/opt/sbd/sbdCore.c | 479 +++++++++++++++++++++++++++++++++++++++++++++- src/opt/sbd/sbdInt.h | 1 + src/opt/sbd/sbdSat.c | 173 +++++++++++++++++ 7 files changed, 821 insertions(+), 43 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4dcea33a..25bcc306 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -55,6 +55,7 @@ #include "sat/bmc/bmc.h" #include "proof/ssc/ssc.h" #include "opt/sfm/sfm.h" +#include "opt/sbd/sbd.h" #include "bool/rpo/rpo.h" #include "map/mpm/mpm.h" #include "opt/fret/fretime.h" @@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -40824,6 +40827,132 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ); + Gia_Man_t * pTemp; int c; + Sbd_Par_t Pars, * pPars = &Pars; + Sbd_ParSetDefault( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutSize < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTfoLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTfoLevels < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTfoFanMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTfoFanMax < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nWinSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nWinSizeMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'a': + pPars->fArea ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManBufNum(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" ); + return 1; + } + if ( Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" ); + return 0; + } + pTemp = Sbd_NtkPerform( pAbc->pGia, pPars ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &mfsd [-KWFMC ] [-avwh]\n" ); + Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" ); + Abc_Print( -2, "\t-K : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize ); + Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels ); + Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax ); + Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); + Abc_Print( -2, "\t-C : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 7de6bd81..3431c761 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -74,7 +74,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho Abc_Obj_t * pNode, * pFanin; char * pSopString; int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev; - int Limit = 300; + int Limit = 500; assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 5a4ef545..b8a34da7 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -266,6 +266,28 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] & pIn2[w]; } +static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords ) +{ + int w; + if ( fCompl1 ) + { + if ( fCompl2 ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pIn1[w] & ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pIn1[w] & pIn2[w]; + } + else + { + if ( fCompl2 ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & pIn2[w]; + } +} static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) { int w; @@ -288,6 +310,12 @@ static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords ) for ( w = 0; w < nWords; w++ ) pOut[w] = pIn1[w] | pIn2[w]; } +static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] |= pIn1[w] ^ pIn2[w]; +} static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) { int w; diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h index 946a2ee4..e1e39a3b 100644 --- a/src/opt/sbd/sbd.h +++ b/src/opt/sbd/sbd.h @@ -35,42 +35,21 @@ ABC_NAMESPACE_HEADER_START /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -typedef struct Sbd_Ntk_t_ Sbd_Ntk_t; typedef struct Sbd_Par_t_ Sbd_Par_t; struct Sbd_Par_t_ { - int nTfoLevMax; // the maximum fanout levels - int nTfiLevMax; // the maximum fanin levels - int nFanoutMax; // the maximum number of fanouts - int nDepthMax; // the maximum depth to try - int nVarMax; // the maximum variable count - int nMffcMin; // the minimum MFFC size - int nMffcMax; // the maximum MFFC size - int nDecMax; // the maximum number of decompositions - int nWinSizeMax; // the maximum window size - int nGrowthLevel; // the maximum allowed growth in level - int nBTLimit; // the maximum number of conflicts in one SAT run - int nNodesMax; // the maximum number of nodes to try - int iNodeOne; // one particular node to try - int nFirstFixed; // the number of first nodes to be treated as fixed - int nTimeWin; // the size of timing window in percents - int DeltaCrit; // delay delta in picoseconds - int DelAreaRatio; // delay/area tradeoff (how many ps we trade for a unit of area) - int fRrOnly; // perform redundance removal - int fArea; // performs optimization for area - int fAreaRev; // performs optimization for area in reverse order - int fMoreEffort; // performs high-affort minimization - int fUseAndOr; // enable internal detection of AND/OR gates - int fZeroCost; // enable zero-cost replacement - int fUseSim; // enable simulation - int fPrintDecs; // enable printing decompositions - int fAllBoxes; // enable preserving all boxes - int fLibVerbose; // enable library stats - int fDelayVerbose; // enable delay stats - int fVerbose; // enable basic stats - int fVeryVerbose; // enable detailed stats + int nLutSize; // target LUT size + int nTfoLevels; // the number of TFO levels (windowing) + int nTfoFanMax; // the max number of fanouts (windowing) + int nWinSizeMax; // maximum window size (windowing) + int nBTLimit; // maximum number of SAT conflicts + int nWords; // simulation word count + int fArea; // area-oriented optimization + int fVerbose; // verbose flag + int fVeryVerbose; // verbose flag }; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -82,16 +61,7 @@ struct Sbd_Par_t_ /*=== sbdCnf.c ==========================================================*/ /*=== sbdCore.c ==========================================================*/ extern void Sbd_ParSetDefault( Sbd_Par_t * pPars ); -extern int Sbd_NtkPerform( Sbd_Ntk_t * p, Sbd_Par_t * pPars ); -/*=== sbdNtk.c ==========================================================*/ -extern Sbd_Ntk_t * Sbd_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths ); -extern void Sbd_NtkFree( Sbd_Ntk_t * p ); -extern Vec_Int_t * Sbd_NodeReadFanins( Sbd_Ntk_t * p, int i ); -extern word * Sbd_NodeReadTruth( Sbd_Ntk_t * p, int i ); -extern int Sbd_NodeReadFixed( Sbd_Ntk_t * p, int i ); -extern int Sbd_NodeReadUsed( Sbd_Ntk_t * p, int i ); -/*=== sbdWin.c ==========================================================*/ -extern Vec_Int_t * Sbd_NtkDfs( Sbd_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes ); +extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * p, Sbd_Par_t * pPars ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index 4d86d2ee..2120a8f9 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -19,14 +19,44 @@ ***********************************************************************/ #include "sbdInt.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define SBD_MAX_LUTSIZE 6 + + +typedef struct Sbd_Man_t_ Sbd_Man_t; +struct Sbd_Man_t_ +{ + Sbd_Par_t * pPars; // user's parameters + Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes) + Vec_Wec_t * vTfos; // TFO for each node (roots are marked) (windowing) + Vec_Int_t * vLutLevs; // LUT level for each node after resynthesis + Vec_Int_t * vLutCuts; // LUT cut for each nodes after resynthesis + Vec_Int_t * vMirrors; // alternative node + Vec_Wrd_t * vSims[3]; // simulation information (main, backup, controlability) + Vec_Int_t * vCover; // temporary + // target node + int Pivot; // target node + int nTfiLeaves; // TFI leaves + int nTfiNodes; // TFI nodes + Vec_Int_t * vTfo; // TFO (excludes node, includes roots) + Vec_Int_t * vLeaves; // leaves (TFI leaves + extended leaves) + Vec_Int_t * vTfi; // TFI (TFI + node + extended TFI) + Vec_Int_t * vCounts[2]; // counters of zeros and ones +}; + +static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); } + +static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i ); } +static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i ); } +static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i ); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -42,7 +72,454 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +void Sbd_ParSetDefault( Sbd_Par_t * pPars ) +{ + memset( pPars, 0, sizeof(Sbd_Par_t) ); + pPars->nLutSize = 4; // target LUT size + pPars->nTfoLevels = 4; // the number of TFO levels (windowing) + pPars->nTfoFanMax = 4; // the max number of fanouts (windowing) + pPars->nWinSizeMax = 0; // maximum window size (windowing) + pPars->nBTLimit = 0; // maximum number of SAT conflicts + pPars->nWords = 1; // simulation word count + pPars->fArea = 0; // area-oriented optimization + pPars->fVerbose = 0; // verbose flag + pPars->fVeryVerbose = 0; // verbose flag +} + +/**Function************************************************************* + + Synopsis [Computes window roots for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) +{ + Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked + Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage + Vec_Int_t * vNodes, * vNodes0, * vNodes1; + int i, k, k2, Id, Fan; + Gia_ManLevelNum( p ); + Gia_ManCreateRefs( p ); + Gia_ManCleanMark0( p ); + Gia_ManForEachCiId( p, Id, i ) + { + vNodes = Vec_WecEntry( vTemp, Id ); + Vec_IntGrow( vNodes, 1 ); + Vec_IntPush( vNodes, Id ); + } + Gia_ManForEachAndId( p, Id ) + { + int fAlwaysRoot = Gia_ObjRefNumId(p, Id) >= nTfoFanMax; + vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) ); + vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) ); + vNodes = Vec_WecEntry( vTemp, Id ); + Vec_IntTwoMerge2( vNodes, vNodes0, vNodes1 ); + k2 = 0; + Vec_IntForEachEntry( vNodes, Fan, k ) + { + int fRoot = fAlwaysRoot || (Gia_ObjLevelId(p, Id) - Gia_ObjLevelId(p, Fan) >= nTfoLevels); + Vec_WecPush( vTfos, Fan, Abc_Var2Lit(Id, fRoot) ); + if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan ); + } + Vec_IntShrink( vNodes, k2 ); + Vec_IntPush( vNodes, Id ); + } + Vec_WecFree( vTemp ); + // print the results + Vec_WecForEachLevel( vTfos, vNodes, i ) + { + if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) + continue; + printf( "Node %3d : ", i ); + Vec_IntForEachEntry( vNodes, Fan, k ) + printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" ); + printf( "\n" ); + + } + return vTfos; +} + +/**Function************************************************************* + + Synopsis [Manager manipulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars ) +{ + int i, w, Id; + Sbd_Man_t * p = ABC_CALLOC( Sbd_Man_t, 1 ); + p->pPars = pPars; + p->pGia = pGia; + p->vTfos = Sbd_ManWindowRoots( pGia, pPars->nTfoLevels, pPars->nTfoFanMax ); + p->vLutLevs = Vec_IntStart( Gia_ManObjNum(pGia) ); + p->vLutCuts = Vec_IntStart( Gia_ManObjNum(pGia) * (p->pPars->nLutSize + 1) ); + p->vMirrors = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + for ( i = 0; i < 3; i++ ) + p->vSims[i] = Vec_WrdStart( Gia_ManObjNum(pGia) * p->pPars->nWords ); + // target node + p->vCover = Vec_IntStart( 100 ); + p->vLeaves = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vTfi = Vec_IntAlloc( Gia_ManAndNum(pGia) ); + p->vCounts[0] = Vec_IntAlloc( 100 ); + p->vCounts[1] = Vec_IntAlloc( 100 ); + // start input cuts + Gia_ManForEachCiId( pGia, Id, i ) + { + int * pCut = Sbd_ObjCut( p, Id ); + pCut[0] = 1; + pCut[1] = Id; + } + // generate random input + Gia_ManRandom( 1 ); + Gia_ManForEachCiId( pGia, Id, i ) + for ( w = 0; w < p->pPars->nWords; w++ ) + Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 ); + return p; +} +void Sbd_ManStop( Sbd_Man_t * p ) +{ + int i; + Vec_WecFree( p->vTfos ); + Vec_IntFree( p->vLutLevs ); + Vec_IntFree( p->vLutCuts ); + Vec_IntFree( p->vMirrors ); + for ( i = 0; i < 3; i++ ) + Vec_WrdFree( p->vSims[i] ); + Vec_IntFree( p->vCover ); + Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vTfi ); + Vec_IntFree( p->vCounts[0] ); + Vec_IntFree( p->vCounts[1] ); +} + + +/**Function************************************************************* + + Synopsis [Constructing window.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node ) +{ + Gia_Obj_t * pObj; + if ( Vec_IntEntry(p->vMirrors, Node) >= 0 ) + Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) ); + if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) || Node == 0 ) + return; + Gia_ObjSetTravIdCurrentId(p->pGia, Node); + pObj = Gia_ManObj( p->pGia, Node ); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( p->vLeaves, Node ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) ); + Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) ); + Vec_IntPush( p->vTfi, Node ); + // simulate + Abc_TtAndCompl( Sbd_ObjSim0(p, Node), + Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), + Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), + p->pPars->nWords ); + if ( pObj->fMark0 ) + Abc_TtAndCompl( Sbd_ObjSim1(p, Node), + Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), + Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), + p->pPars->nWords ); +} +void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node ) +{ + int iObj0 = Gia_ObjFaninId0(Gia_ManObj(p->pGia, Node), Node); + int iObj1 = Gia_ObjFaninId1(Gia_ManObj(p->pGia, Node), Node); + word * pCtrl = Sbd_ObjSim2(p, Node); + word * pCtrl0 = Sbd_ObjSim2(p, iObj0); + word * pCtrl1 = Sbd_ObjSim2(p, iObj1); + word * pSims = Sbd_ObjSim0(p, Node); + word * pSims0 = Sbd_ObjSim0(p, iObj0); + word * pSims1 = Sbd_ObjSim0(p, iObj1); + int w; + for ( w = 0; w < p->pPars->nWords; w++ ) + { + pCtrl0[w] = pCtrl[w] & (pSims[w] | pSims1[w]); + pCtrl1[w] = pCtrl[w] & (pSims[w] | pSims0[w] | (~pSims0[w] & ~pSims1[w])); + } +} +void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) +{ + int i, Node; + // assign pivot and TFO (assume siminfo is assigned at the PIs) + p->Pivot = Pivot; + p->vTfo = Vec_WecEntry( p->vTfos, Pivot ); + Vec_IntClear( p->vLeaves ); + Vec_IntClear( p->vTfi ); + // simulate TFI cone + Gia_ManIncrementTravId( p->pGia ); + Sbd_ManWindowSim_rec( p, Pivot ); + p->nTfiLeaves = Vec_IntSize( p->vLeaves ); + p->nTfiNodes = Vec_IntSize( p->vTfi ); + // simulate node + Gia_ManObj(p->pGia, Pivot)->fMark0 = 1; + Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 ); + // simulate extended TFI cone + Vec_IntForEachEntry( p->vTfo, Node, i ) + { + Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1; + if ( Abc_LitIsCompl(Node) ) + Sbd_ManWindowSim_rec( p, Node ); + } + // remove marks + Gia_ManObj(p->pGia, Pivot)->fMark0 = 0; + Vec_IntForEachEntry( p->vTfo, Node, i ) + Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 0; + // compute controlability for node + Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords ); + Vec_IntForEachEntry( p->vTfo, Node, i ) + if ( Abc_LitIsCompl(Node) ) // root + Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Node), Sbd_ObjSim1(p, Node), p->pPars->nWords ); + // propagate controlability to TFI + for ( i = p->nTfiNodes; i >= 0 && (Node = Vec_IntEntry(p->vTfi, i)); i-- ) + Sbd_ManPropagateControl( p, Node ); +} + +/**Function************************************************************* + + Synopsis [Profiling divisor candidates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) +{ + int i, k, k0, k1, Id, Bit0, Bit1; + assert( p->Pivot == Pivot ); + Vec_IntClear( p->vCounts[0] ); + Vec_IntClear( p->vCounts[1] ); + // sampling matrix + for ( k = 0; k < p->pPars->nWords * 64; k++ ) + { + printf( "%3d : ", k ); + Vec_IntForEachEntry( p->vTfi, Id, i ) + { + word * pSims = Sbd_ObjSim0( p, Id ); + word * pCtrl = Sbd_ObjSim2( p, Id ); + if ( i == Vec_IntSize(p->vTfi)-1 ) + { + if ( Abc_TtGetBit(pCtrl, k) ) + Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k ); + printf( " " ); + } + printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' ); + } + printf( "\n" ); + } + // covering table + printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) ); + Vec_IntForEachEntry( p->vCounts[0], Bit0, k0 ) + Vec_IntForEachEntry( p->vCounts[1], Bit1, k1 ) + { + printf( "%3d %3d : ", Bit0, Bit1 ); + Vec_IntForEachEntry( p->vTfi, Id, i ) + { + word * pSims = Sbd_ObjSim0( p, Id ); + word * pCtrl = Sbd_ObjSim2( p, Id ); + if ( i == Vec_IntSize(p->vTfi)-1 ) + printf( " " ); + printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' ); + } + printf( "\n" ); + } +} +int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, int * pCut, word * pTruth ) +{ + Sbd_ManPrintObj( p, Pivot ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Computes delay-oriented k-feasible cut at the node.] + + Description [Return 1 if node's LUT level does not exceed those of the fanins.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sbd_CutMergeSimple( Sbd_Man_t * p, int * pCut1, int * pCut2, int * pCut ) +{ + int * pBeg = pCut + 1; + int * pBeg1 = pCut1 + 1; + int * pBeg2 = pCut2 + 1; + int * pEnd1 = pCut1 + 1 + pCut1[0]; + int * pEnd2 = pCut2 + 1 + pCut2[0]; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg++ = *pBeg1++; + else + *pBeg++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg++ = *pBeg2++; + return (pCut[0] = pBeg - pCut - 1); +} +int Sbd_ManComputeCut( Sbd_Man_t * p, int Node ) +{ + int pCut[2*SBD_MAX_LUTSIZE]; + int iFan0 = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node ); + int iFan1 = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node ); + int Level0 = Vec_IntEntry( p->vLutLevs, iFan0 ); + int Level1 = Vec_IntEntry( p->vLutLevs, iFan1 ); + int LevMax = Abc_MaxInt( Level0, Level1 ); + int * pCut0 = Sbd_ObjCut( p, iFan0 ); + int * pCut1 = Sbd_ObjCut( p, iFan1 ); + int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0; + int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1; + int nSize = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut ); + int Result = 1; // no need to resynthesize + assert( iFan0 != iFan1 ); + if ( nSize > p->pPars->nLutSize ) + { + pCut[0] = 2; + pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1; + pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0; + Result = LevMax ? 0 : 1; + LevMax++; + } + assert( Vec_IntEntry(p->vLutLevs, Node) == 0 ); + Vec_IntWriteEntry( p->vLutLevs, Node, LevMax ); + memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) ); + return Result; +} +int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, int * pCut, word Truth ) +{ + Vec_Int_t vLeaves = { pCut[0], pCut[0], pCut+1 }; + int iLit = Dsm_ManTruthToGia( p->pGia, &Truth, &vLeaves, p->vCover ); + int i, k, w, iObjLast = Gia_ManObjNum(p->pGia); + assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 ); + Vec_IntWriteEntry( p->vMirrors, Pivot, iLit ); + assert( Vec_IntSize(p->vLutLevs) == iObjLast ); + for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ ) + { + Vec_IntPush( p->vLutLevs, 0 ); + Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 ); + Sbd_ManComputeCut( p, i ); + for ( k = 0; k < 3; k++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) + Vec_WrdPush( p->vSims[k], 0 ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives new AIG after resynthesis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors ) +{ + Gia_Obj_t * pObj; + int Obj = Node; + if ( Vec_IntEntry(vMirrors, Node) >= 0 ) + Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) ); + pObj = Gia_ManObj( p, Obj ); + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors ); + Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors ); + if ( Gia_ObjIsXor(pObj) ) + pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // set the original node as well + if ( Obj != Node ) + Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) ); +} +Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAndId( p, i ) + Sbd_ManDerive_rec( pNew, p, i, vMirrors ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs delay optimization for the given LUT size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) +{ + Gia_Man_t * pNew; word Truth; + Sbd_Man_t * p = Sbd_ManStart( pGia, pPars ); + int Pivot, pCut[2*SBD_MAX_LUTSIZE]; + assert( pPars->nLutSize <= 6 ); + Gia_ManForEachAndId( pGia, Pivot ) + { + if ( Sbd_ManComputeCut( p, Pivot ) ) + continue; + Sbd_ManWindow( p, Pivot ); + if ( Sbd_ManExplore( p, Pivot, pCut, &Truth ) ) + Sbd_ManImplement( p, Pivot, pCut, Truth ); + } + pNew = Sbd_ManDerive( pGia, p->vMirrors ); + Sbd_ManStop( p ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h index 1157d02c..8211610c 100644 --- a/src/opt/sbd/sbdInt.h +++ b/src/opt/sbd/sbdInt.h @@ -34,6 +34,7 @@ #include "misc/vec/vec.h" #include "sat/bsat/satSolver.h" #include "misc/util/utilNam.h" +#include "misc/util/utilTruth.h" #include "map/scl/sclLib.h" #include "map/scl/sclCon.h" #include "bool/kit/kit.h" diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c index bd49c50e..ae865627 100644 --- a/src/opt/sbd/sbdSat.c +++ b/src/opt/sbd/sbdSat.c @@ -37,6 +37,179 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define SBD_LUTS_MAX 2 +#define SBD_SIZE_MAX 4 +#define SBD_DIV_MAX 16 + +// new AIG manager +typedef struct Sbd_Pro_t_ Sbd_Pro_t; +struct Sbd_Pro_t_ +{ + int nLuts; // LUT count + int nSize; // LUT size + int nDivs; // divisor count + int nVars; // intermediate variables (nLuts * nSize) + int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs) + int pPars1[SBD_LUTS_MAX][1<= 1 && nLuts <= 2 ); + memset( p, 0, sizeof(Sbd_Pro_t) ); + p->nLuts = nLuts; + p->nSize = nSize; + p->nDivs = nDivs; + p->nVars = nLuts * nSize; + p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs; + // set parameters + for ( i = 0; i < nLuts; i++ ) + for ( k = 0; k < (1 << nSize); k++ ) + p->pPars1[i][k] = iVar++; + for ( i = 0; i < nLuts; i++ ) + for ( k = 0; k < nSize; k++ ) + for ( d = 0; d < nDivs; d++ ) + p->pPars2[i][k][d] = iVar++; + // set intermediate variables + for ( i = 0; i < nLuts; i++ ) + for ( k = 0; k < nSize; k++ ) + p->pVars[i][k] = iVar++; + // set top variables + for ( i = 1; i < nLuts; i++ ) + p->pVars[i][nSize] = p->pVars[i-1][0]; + // set divisor variables + for ( d = 0; d < nDivs; d++ ) + p->pDivs[d] = iVar++; + assert( iVar == p->nPars + p->nVars + p->nDivs ); + + // input compatiblity clauses + for ( i = 0; i < nLuts; i++ ) + for ( k = (i > 0); k < nSize; k++ ) + for ( d = 0; d < nDivs; d++ ) + for ( n = 0; n < nDivs; n++ ) + { + if ( n < d ) + { + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) ); + Vec_IntPush( vCnf, -1 ); + } + else if ( k < nSize-1 ) + { + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) ); + Vec_IntPush( vCnf, -1 ); + } + } + + // create LUT clauses + for ( i = 0; i < nLuts; i++ ) + for ( k = 0; k < (1 << nSize); k++ ) + for ( n = 0; n < 2; n++ ) + { + for ( v = 0; v < nSize; v++ ) + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) ); + Vec_IntPush( vCnf, -1 ); + } + + // create input clauses + for ( i = 0; i < nLuts; i++ ) + for ( k = (i > 0); k < nSize; k++ ) + for ( d = 0; d < nDivs; d++ ) + for ( n = 0; n < 2; n++ ) + { + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) ); + Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) ); + Vec_IntPush( vCnf, -1 ); + } + + return vCnf; +} +// add clauses to the don't-care computation solver +void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat ) +{ + int pLits[8], nLits, i, k, iLit, RetValue; + int ThisTopVar = p->pVars[0][p->nSize]; + int FirstDivVar = p->nPars + p->nVars; + // add clauses + for ( i = 0; i < Vec_IntSize(vCnf); i++ ) + { + assert( Vec_IntEntry(vCnf, i) != -1 ); + for ( k = i+1; k < Vec_IntSize(vCnf); k++ ) + if ( Vec_IntEntry(vCnf, i) == -1 ) + break; + nLits = 0; + Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) { + if ( Abc_Lit2Var(iLit) == ThisTopVar ) + pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) ); + else if ( Abc_Lit2Var(iLit) >= FirstDivVar ) + pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) ); + else + pLits[nLits++] = iLit + 2 * iStartVar; + } + assert( nLits <= 8 ); + RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits ); + assert( RetValue ); + } +} +// add clauses to the functionality evaluation solver +void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat ) +{ + Vec_Int_t * vLevel; + int pLits[8], nLits, i, k, iLit, RetValue; + int ThisTopVar = p->pVars[0][p->nSize]; + int FirstDivVar = p->nPars + p->nVars; + int FirstIntVar = p->nPars; + // add clauses + Vec_WecForEachLevel( vCnf, vLevel, i ) + { + nLits = 0; + Vec_IntForEachEntry( vLevel, iLit, k ) { + if ( Abc_Lit2Var(iLit) == ThisTopVar ) + { + if ( Abc_LitIsCompl(iLit) == iTopVarValue ) + break; + continue; + } + else if ( Abc_Lit2Var(iLit) >= FirstDivVar ) + { + if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] ) + break; + continue; + } + else if ( Abc_Lit2Var(iLit) >= FirstIntVar ) + pLits[nLits++] = iLit + 2 * iStartVar; + else + pLits[nLits++] = iLit; + } + if ( k < Vec_IntSize(vLevel) ) + continue; + assert( nLits <= 8 ); + RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits ); + assert( RetValue ); + } +} + + /**Function************************************************************* Synopsis [] -- cgit v1.2.3