From 3b5527b620c943d84ee4ba38d969c114c042ae89 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Nov 2016 20:56:43 -0800 Subject: New SAT-based optimization package. --- src/opt/sbd/sbdCore.c | 516 +++++++++++++++++++++++++++++++++++++++----------- src/opt/sbd/sbdWin.c | 91 +++++++-- 2 files changed, 485 insertions(+), 122 deletions(-) diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index d83ed231..cf46651e 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -42,6 +42,8 @@ struct Sbd_Man_t_ Vec_Wrd_t * vSims[4]; // simulation information (main, backup, controlability) Vec_Int_t * vCover; // temporary Vec_Int_t * vLits; // temporary + int nConsts; // constants + int nChanges; // changes // target node int Pivot; // target node Vec_Int_t * vTfo; // TFO (excludes node, includes roots) - precomputed @@ -82,7 +84,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars ) { memset( pPars, 0, sizeof(Sbd_Par_t) ); pPars->nLutSize = 4; // target LUT size - pPars->nTfoLevels = 3; // the number of TFO levels (windowing) + pPars->nTfoLevels = 2; // 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 @@ -145,7 +147,7 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) Vec_BitFree( vPoDrivers ); // print the results - if ( 1 ) + if ( 0 ) Vec_WecForEachLevel( vTfos, vNodes, i ) { if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) @@ -244,61 +246,9 @@ void Sbd_ManStop( Sbd_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node ) +void Sbd_ManPropagateControlOne( 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_ObjIsAnd(pObj) ) - { - Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) ); - Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) ); - } - if ( !pObj->fMark0 ) - { - Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) ); - Vec_IntPush( p->vWinObjs, Node ); - } - if ( Gia_ObjIsCi(pObj) ) - return; - // simulate - assert( Gia_ObjIsAnd(pObj) ); - if ( Gia_ObjIsXor(pObj) ) - { - Abc_TtXor( Sbd_ObjSim0(p, Node), - Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), - Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), - p->pPars->nWords, - Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); - - if ( pObj->fMark0 ) - Abc_TtXor( Sbd_ObjSim1(p, Node), - Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), - Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), - p->pPars->nWords, - Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); - } - else - { - 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_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), - p->pPars->nWords ); - } -} -void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node ) -{ - Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node); + Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node); int w; int iObj0 = Gia_ObjFaninId0(pNode, Node); int iObj1 = Gia_ObjFaninId1(pNode, Node); @@ -314,20 +264,37 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node ) word * pDtrl0 = Sbd_ObjSim3(p, iObj0); word * pDtrl1 = Sbd_ObjSim3(p, iObj1); -// printf( "Node %2d : %d %d\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) ); - int w; +// Gia_ObjPrint( p->pGia, pNode ); +// printf( "Node %2d : %d %d\n\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) ); + for ( w = 0; w < p->pPars->nWords; w++ ) { word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w]; word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w]; - pCtrl0[w] = pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1)); - pCtrl1[w] = pCtrl[w] & (pSims[w] | Sim0); + pCtrl0[w] |= pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1)); + pCtrl1[w] |= pCtrl[w] & (pSims[w] | Sim0); - pDtrl0[w] = pDtrl[w] & (pSims[w] | Sim1); - pDtrl1[w] = pDtrl[w] & (pSims[w] | Sim0 | (~Sim0 & ~Sim1)); + pDtrl0[w] |= pDtrl[w] & (pSims[w] | Sim1); + pDtrl1[w] |= pDtrl[w] & (pSims[w] | Sim0 | (~Sim0 & ~Sim1)); } } +void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot ) +{ + int i, Node; + Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 ); + // clean controlability + for ( i = 0; i < Vec_IntEntry(p->vObj2Var, Pivot) && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i++ ) + { + Abc_TtClear( Sbd_ObjSim2(p, Node), p->pPars->nWords ); + Abc_TtClear( Sbd_ObjSim3(p, Node), p->pPars->nWords ); + //printf( "Clearing node %d.\n", Node ); + } + // propagate controlability to fanins for the TFI nodes starting from the pivot + for ( i = Vec_IntEntry(p->vObj2Var, Pivot); i >= 0 && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i-- ) + if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Node)) ) + Sbd_ManPropagateControlOne( p, Node ); +} void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot ) { int i, k, Node; @@ -354,7 +321,62 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot ) Vec_IntFill( p->vDivValues, Vec_IntSize(p->vWinObjs), 0 ); } } -void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) +void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit ) +{ + Gia_Obj_t * pObj; + int Node = NodeInit; + if ( Vec_IntEntry(p->vMirrors, Node) >= 0 ) + Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) ); + if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) ) + return; + Gia_ObjSetTravIdCurrentId(p->pGia, Node); + pObj = Gia_ManObj( p->pGia, Node ); + if ( Gia_ObjIsAnd(pObj) ) + { + Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) ); + Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) ); + } + if ( !pObj->fMark0 ) + { + Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) ); + Vec_IntPush( p->vWinObjs, Node ); + } + if ( Gia_ObjIsCi(pObj) ) + return; + // simulate + assert( Gia_ObjIsAnd(pObj) ); + if ( Gia_ObjIsXor(pObj) ) + { + Abc_TtXor( Sbd_ObjSim0(p, Node), + Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), + Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), + p->pPars->nWords, + Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); + + if ( pObj->fMark0 ) + Abc_TtXor( Sbd_ObjSim1(p, Node), + Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), + Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), + p->pPars->nWords, + Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); + } + else + { + 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_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), + p->pPars->nWords ); + } + if ( Node != NodeInit ) + Abc_TtCopy( Sbd_ObjSim0(p, NodeInit), Sbd_ObjSim0(p, Node), p->pPars->nWords, Abc_LitIsCompl(Vec_IntEntry(p->vMirrors, NodeInit)) ); +} +int Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) { int i, Node; // assign pivot and TFO (assume siminfo is assigned at the PIs) @@ -362,7 +384,10 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) p->vTfo = Vec_WecEntry( p->vTfos, Pivot ); // simulate TFI cone Vec_IntClear( p->vWinObjs ); + Vec_IntWriteEntry( p->vObj2Var, 0, Vec_IntSize(p->vWinObjs) ); + Vec_IntPush( p->vWinObjs, 0 ); Gia_ManIncrementTravId( p->pGia ); + Gia_ObjSetTravIdCurrentId(p->pGia, 0); Sbd_ManWindowSim_rec( p, Pivot ); Sbd_ManUpdateOrder( p, Pivot ); // simulate node @@ -394,11 +419,143 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) Vec_IntForEachEntry( p->vTfo, Node, i ) if ( Abc_LitIsCompl(Node) ) // root Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords ); - Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 ); // propagate controlability to fanins for the TFI nodes starting from the pivot - for ( i = Vec_IntEntry(p->vObj2Var, Pivot); i >= 0 && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i-- ) - if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Node)) ) - Sbd_ManPropagateControl( p, Node ); + Sbd_ManPropagateControl( p, Pivot ); + // return 1 if window is too large + if ( p->pPars->fVerbose && Vec_IntSize(p->vDivValues) >= 64 ) + printf( "Window is too large.\n" ); + return (int)(Vec_IntSize(p->vDivValues) >= 64); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot ) +{ + extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ); + int nMintCount = 16; + Vec_Ptr_t * vSims; + word * pSims = Sbd_ObjSim0( p, Pivot ); + word * pCtrl = Sbd_ObjSim2( p, Pivot ); + int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot); + int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0}; + extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds ); + extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ); + p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots ); + //return -1; + //Sbd_ManPrintObj( p, Pivot ); + + // count the number of on-set and off-set care-set minterms + Vec_IntClear( p->vLits ); + for ( i = 0; i < 64; i++ ) + if ( Abc_TtGetBit(pCtrl, i) ) + nCares[Abc_TtGetBit(pSims, i)]++; + else + Vec_IntPush( p->vLits, i ); + fFindOnset = (int)(nCares[0] < nCares[1]); + if ( nCares[0] >= nMintCount && nCares[1] >= nMintCount ) + return -1; + // find how many do we need + nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0; + nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0; + + if ( p->pPars->fVerbose ) + printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot ); + + if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] ) + Vec_IntShrink( p->vLits, nCares[0] + nCares[1] ); + else + { + // collect places to insert new minterms + for ( i = 0; i < 64 && Vec_IntSize(p->vLits) < nCares[0] + nCares[1]; i++ ) + if ( fFindOnset == Abc_TtGetBit(pSims, i) ) + Vec_IntPush( p->vLits, i ); + } + // collect simulation pointers + vSims = Vec_PtrAlloc( PivotVar + 1 ); + Vec_IntForEachEntry( p->vWinObjs, iObj, i ) + { + Vec_PtrPush( vSims, Sbd_ObjSim0(p, iObj) ); + if ( iObj == Pivot ) + break; + } + assert( i == PivotVar ); + // compute patterns + RetValue = Sbd_ManCollectConstants( p->pSat, nCares, PivotVar, (word **)Vec_PtrArray(vSims), p->vLits ); + // print computed miterms + if ( 0 && RetValue < 0 ) + { + Vec_Int_t * vPis = Vec_WecEntry(p->vDivLevels, 0); + int i, k, Ind; + printf( "Additional minterms:\n" ); + Vec_IntForEachEntry( p->vLits, Ind, k ) + { + for ( i = 0; i < Vec_IntSize(vPis); i++ ) + printf( "%d", Abc_TtGetBit( (word *)Vec_PtrEntry(vSims, Vec_IntEntry(p->vWinObjs, i)), Ind ) ); + printf( "\n" ); + } + } + Vec_PtrFree( vSims ); + if ( RetValue >= 0 ) + { + if ( p->pPars->fVerbose ) + printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot ); + p->nConsts++; + return RetValue; + } + // set controlability of these minterms + Vec_IntForEachEntry( p->vLits, Ind, i ) + Abc_TtSetBit( pCtrl, Ind ); + // propagate controlability to fanins for the TFI nodes starting from the pivot + Sbd_ManPropagateControl( p, Pivot ); + // double check that we now have enough minterms + for ( i = 0; i < 64; i++ ) + if ( Abc_TtGetBit(pCtrl, i) ) + nCares[Abc_TtGetBit(pSims, i)]++; + assert( nCares[0] >= nMintCount && nCares[1] >= nMintCount ); + return -1; +} + +/**Function************************************************************* + + Synopsis [Transposing 64-bit matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sbd_TransposeMatrix64( word A[64] ) +{ + int j, k; + word t, m = 0x00000000FFFFFFFF; + for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) + { + for ( k = 0; k < 64; k = (k + j + 1) & ~j ) + { + t = (A[k] ^ (A[k+j] >> j)) & m; + A[k] = A[k] ^ t; + A[k+j] = A[k+j] ^ (t << j); + } + } +} +static inline void Sbd_PrintMatrix64( word A[64] ) +{ + int j, k; + for ( j = 0; j < 64; j++, printf("\n") ) + for ( k = 0; k < 64; k++ ) + printf( "%d", (int)((A[j] >> k) & 1) ); + printf( "\n" ); } /**Function************************************************************* @@ -418,7 +575,7 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) int i, k, k0, k1, Id, Bit0, Bit1; Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs ) - printf( "%d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" ); + printf( "%3d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" ); assert( p->Pivot == Pivot ); Vec_IntClear( p->vCounts[0] ); @@ -561,52 +718,182 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) if ( Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1) ) Abc_TtXorBit( &Row, i ); } - if ( !Vec_WrdPushUnique( p->vMatrix, Row ) ) - Extra_PrintBinary( stdout, (unsigned *)&Row, nDivs ), printf( "\n" ); + if ( Vec_WrdPushUnique( p->vMatrix, Row ) ) + continue; + for ( i = 0; i < nDivs; i++ ) + printf( "%d", (int)((Row >> i) & 1) ); + printf( "\n" ); } - } + + int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) { - extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ); + int fVerbose = 0; extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp ); + word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, Cube0, Cube1, Target; + int c0, c1, c2, c3, i, k, n, Index, nCubes[2] = {0}, nRows = 0, fFound = 0; + int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot); int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots); int RetValue = 0; -// Sbd_ManPrintObj( p, Pivot ); - Vec_IntPrint( p->vObj2Var ); + if ( fVerbose ) + Sbd_ManPrintObj( p, Pivot ); + + // collect bit-matrices + for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ ) + { + MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) ); + MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) ); + MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, i) ); + } + MatrS[63-i] = *Sbd_ObjSim0( p, Pivot ); + MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot ); + MatrC[1][63-i] = *Sbd_ObjSim3( p, Pivot ); + + //Sbd_PrintMatrix64( MatrS ); + Sbd_TransposeMatrix64( MatrS ); + Sbd_TransposeMatrix64( MatrC[0] ); + Sbd_TransposeMatrix64( MatrC[1] ); + //Sbd_PrintMatrix64( MatrS ); + + // collect cubes + for ( i = 0; i < 64; i++ ) + { + assert( Abc_TtGetBit(&MatrC[0][i], Vec_IntSize(p->vDivValues)) == Abc_TtGetBit(&MatrC[1][i], Vec_IntSize(p->vDivValues)) ); + if ( !Abc_TtGetBit(&MatrC[0][i], Vec_IntSize(p->vDivValues)) ) + continue; + Index = Abc_TtGetBit(&MatrS[i], Vec_IntSize(p->vDivValues)); // Index==0 offset; Index==1 onset + for ( n = 0; n < 2; n++ ) + { + if ( n && MatrC[0][i] == MatrC[1][i] ) + continue; + assert( MatrC[n][i] ); + Cube0 = ~MatrS[i] & MatrC[n][i]; + Cube1 = MatrS[i] & MatrC[n][i]; + assert( Cube0 || Cube1 ); + for ( k = 0; k < nCubes[Index]; k++ ) + if ( Cubes[Index][0][k] == Cube0 && Cubes[Index][1][k] == Cube1 ) + break; + if ( k == nCubes[Index] && k < 64 ) + { + Cubes[Index][0][nCubes[Index]] = Cube0; + Cubes[Index][1][nCubes[Index]] = Cube1; + nCubes[Index]++; + } + } + } + + if ( p->pPars->fVerbose ) + printf( "Generated matrix with %d x %d entries.\n", nCubes[0], nCubes[1] ); + + if ( fVerbose ) + for ( n = 0; n < 2; n++ ) + { + printf( "%s:\n", n ? "Onset" : "Offset" ); + for ( i = 0; i < nCubes[n]; i++, printf( "\n" ) ) + for ( k = 0; k < 64; k++ ) + if ( Abc_TtGetBit(&Cubes[n][0][i], k) ) + printf( "0" ); + else if ( Abc_TtGetBit(&Cubes[n][1][i], k) ) + printf( "1" ); + else + printf( "." ); + printf( "\n" ); + } + + // collect cover + for ( i = 0; i < nCubes[0]; i++ ) + for ( k = 0; k < nCubes[1]; k++ ) + { + Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]); + assert( Cube ); + for ( n = 0; n < nRows; n++ ) + if ( Cover[63-n] == Cube ) + break; + if ( n == nRows && n < 64 ) + Cover[63-nRows++] = Cube; + } + + if ( p->pPars->fVerbose ) + printf( "Generated cover with %d entries.\n", nRows ); + + + //Sbd_PrintMatrix64( Cover ); + Sbd_TransposeMatrix64( Cover ); + //Sbd_PrintMatrix64( Cover ); + + // swap + for ( i = 0; i < 32; i++ ) + { + Cube = Cover[i]; + Cover[i] = Cover[63-i]; + Cover[63-i] = Cube; + } + + if ( fVerbose ) + { + for ( i = 0; i <= nRows; i++, printf( "\n") ) + for ( k = 0; k < 64; k++ ) + printf( "%d", (int)((Cover[i] >> k) & 1) ); + } + + Target = Cover[Vec_IntSize(p->vDivValues)]; + for ( c0 = 0; c0 < Vec_IntSize(p->vDivValues); c0++ ) + for ( c1 = c0+1; c1 < Vec_IntSize(p->vDivValues); c1++ ) + for ( c2 = c1+1; c2 < Vec_IntSize(p->vDivValues); c2++ ) + for ( c3 = c2+1; c3 < Vec_IntSize(p->vDivValues); c3++ ) + { + if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target ) + goto finish; + } +finish: + if ( c0 == Vec_IntSize(p->vDivValues) ) + { + if ( p->pPars->fVerbose ) + printf( "Cannot find a feasible cover.\n" ); + return RetValue; + } Vec_IntClear( p->vDivVars ); - Vec_IntPush( p->vDivVars, 0 ); - Vec_IntPush( p->vDivVars, 1 ); - Vec_IntPush( p->vDivVars, 2 ); - Vec_IntPush( p->vDivVars, 4 ); + Vec_IntPush( p->vDivVars, c0 ); + Vec_IntPush( p->vDivVars, c1 ); + Vec_IntPush( p->vDivVars, c2 ); + Vec_IntPush( p->vDivVars, c3 ); + + if ( p->pPars->fVerbose ) + printf( "Feasible cover: " ); + if ( p->pPars->fVerbose ) + Vec_IntPrint( p->vDivVars ); - p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots ); *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar, p->vDivVars, p->vDivValues, p->vLits ); if ( *pTruth == SBD_SAT_UNDEC ) printf( "Node %d: Undecided.\n", Pivot ); else if ( *pTruth == SBD_SAT_SAT ) { - int i; - printf( "Node %d: SAT.\n", Pivot ); - for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ ) - printf( "%d", Vec_IntEntry(p->vDivValues, i) & 1 ); - printf( "\n" ); - for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ ) - printf( "%d", Vec_IntEntry(p->vDivValues, i) >> 1 ); - printf( "\n" ); + if ( p->pPars->fVerbose ) + { + int i; + printf( "Node %d: SAT.\n", Pivot ); + for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ ) + printf( "%d", Vec_IntEntry(p->vDivValues, i) & 1 ); + printf( "\n" ); + for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ ) + printf( "%d", Vec_IntEntry(p->vDivValues, i) >> 1 ); + printf( "\n" ); + } } else { - printf( "Node %d: UNSAT.\n", Pivot ); + if ( p->pPars->fVerbose ) + printf( "Node %d: UNSAT.\n", Pivot ); + if ( p->pPars->fVerbose ) + Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" ); RetValue = 1; } - Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" ); - return RetValue; } @@ -669,7 +956,7 @@ int Sbd_ManComputeCut( Sbd_Man_t * p, int Node ) assert( Vec_IntEntry(p->vLutLevs, Node) == 0 ); Vec_IntWriteEntry( p->vLutLevs, Node, LevMax ); memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) ); - printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result ); + //printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result ); return Result; } int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth ) @@ -697,11 +984,15 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth ) // remember this function assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 ); Vec_IntWriteEntry( p->vMirrors, Pivot, iLit ); + if ( p->pPars->fVerbose ) + printf( "Replacing node %d by literal %d.\n", Pivot, iLit ); // extend data-structure for new nodes assert( Vec_IntSize(p->vLutLevs) == iObjLast ); for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ ) { Vec_IntPush( p->vLutLevs, 0 ); + Vec_IntPush( p->vObj2Var, 0 ); + Vec_IntPush( p->vMirrors, -1 ); Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 ); Sbd_ManComputeCut( p, i ); for ( k = 0; k < 4; k++ ) @@ -710,6 +1001,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth ) } // make sure delay reduction is achieved assert( Vec_IntEntry(p->vLutLevs, Abc_Lit2Var(iLit)) < iCurLev ); + p->nChanges++; return 0; } @@ -728,18 +1020,19 @@ void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * v { Gia_Obj_t * pObj; int Obj = Node; - if ( Node < Vec_IntSize(vMirrors) && Vec_IntEntry(vMirrors, Node) >= 0 ) + 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) ); + if ( !~pObj->Value ) + { + 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)) ); @@ -766,7 +1059,6 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors ) return pNew; } - /**Function************************************************************* Synopsis [Performs delay optimization for the given LUT size.] @@ -782,18 +1074,28 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) { Gia_Man_t * pNew; Sbd_Man_t * p = Sbd_ManStart( pGia, pPars ); - int Pivot; word Truth = 0; + int nNodesOld = Gia_ManObjNum(pGia); + int RetValue, Pivot; word Truth = 0; assert( pPars->nLutSize <= 6 ); Gia_ManForEachAndId( pGia, Pivot ) { + if ( Pivot >= nNodesOld ) + break; if ( Sbd_ManComputeCut( p, Pivot ) ) continue; - printf( "Looking at node %d\n", Pivot ); - Sbd_ManWindow( p, Pivot ); - if ( Sbd_ManExplore( p, Pivot, &Truth ) ) + //if ( Pivot != 313 ) + // continue; + if ( p->pPars->fVerbose ) + printf( "\nLooking at node %d\n", Pivot ); + if ( Sbd_ManWindow( p, Pivot ) ) + continue; + RetValue = Sbd_ManCheckConst( p, Pivot ); + if ( RetValue >= 0 ) + Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue ); + else if ( Sbd_ManExplore( p, Pivot, &Truth ) ) Sbd_ManImplement( p, Pivot, Truth ); - break; } + printf( "Found %d constants and %d replacements.\n", p->nConsts, p->nChanges ); pNew = Sbd_ManDerive( pGia, p->vMirrors ); Sbd_ManStop( p ); return pNew; diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c index 8f320038..50837e1f 100644 --- a/src/opt/sbd/sbdWin.c +++ b/src/opt/sbd/sbdWin.c @@ -46,46 +46,62 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) +sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) { Gia_Obj_t * pObj; - int i, iObj, Fan0, Fan1, Node, fCompl0, fCompl1, RetValue; + int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue; + int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo); int PivotVar = Vec_IntEntry(vObj2Var, Pivot); + //Vec_IntPrint( vWinObjs ); + //Vec_IntPrint( vTfo ); + //Vec_IntPrint( vRoots ); // create SAT solver if ( pSat == NULL ) pSat = sat_solver_new(); else sat_solver_restart( pSat ); sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 ); + // create constant 0 clause + sat_solver_addclause( pSat, &iLit, &iLit + 1 ); // add clauses for all nodes - Vec_IntForEachEntry( vWinObjs, iObj, i ) + Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 ) { pObj = Gia_ManObj( p, iObj ); if ( Gia_ObjIsCi(pObj) ) continue; assert( Gia_ObjIsAnd(pObj) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ); - Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) ); - Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) ); - fCompl0 = Gia_ObjFaninC0(pObj); - fCompl1 = Gia_ObjFaninC1(pObj); + Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + Fan0 = Vec_IntEntry( vObj2Var, Fan0 ); + Fan1 = Vec_IntEntry( vObj2Var, Fan1 ); + fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m)); + fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m)); if ( Gia_ObjIsXor(pObj) ) sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 ); else sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 ); } // add second clauses for the TFO - Vec_IntForEachEntryStart( vWinObjs, iObj, i, Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo) ) + Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart ) { pObj = Gia_ManObj( p, iObj ); assert( Gia_ObjIsAnd(pObj) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo); - Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) ); - Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) ); - Fan0 = Fan0 <= PivotVar ? Fan0 : Fan0 + Vec_IntSize(vTfo); - Fan1 = Fan1 <= PivotVar ? Fan1 : Fan1 + Vec_IntSize(vTfo); - fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar); - fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar); + Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + Fan0 = Vec_IntEntry( vObj2Var, Fan0 ); + Fan1 = Vec_IntEntry( vObj2Var, Fan1 ); + Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo); + Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo); + fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m)); + fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m)); if ( Gia_ObjIsXor(pObj) ) sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 ); else @@ -98,8 +114,9 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_ Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) ); Vec_IntForEachEntry( vRoots, iObj, i ) { - Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ); + Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) ); sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 ); } // make OR clause for the last nRoots variables @@ -190,6 +207,50 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi return SBD_SAT_SAT; } +/**Function************************************************************* + + Synopsis [Returns a bunch of positive/negative random care minterms.] + + Description [Returns 0/1 if the functions is const 0/1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void sat_solver_random_polarity(sat_solver* s) +{ + int i, k; + for ( i = 0; i < s->size; i += 64 ) + { + word Polar = Gia_ManRandomW(0); + for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ ) + s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k); + } +} +int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds ) +{ + int nBTLimit = 0; + int i, Ind; + assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] ); + Vec_IntForEachEntry( vInds, Ind, i ) + { + int fOffSet = (int)(i < nCareMints[0]); + int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet ); + sat_solver_random_polarity( pSat ); + status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -2; + if ( status == l_False ) + return fOffSet; + for ( k = 0; k <= PivotVar; k++ ) + if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) ) + Abc_TtXorBit(pVarSims[k], Ind); + } + return -1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3