diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaShrink7.c | 198 | ||||
-rw-r--r-- | src/misc/util/utilTruth.h | 197 |
2 files changed, 198 insertions, 197 deletions
diff --git a/src/aig/gia/giaShrink7.c b/src/aig/gia/giaShrink7.c index ddc7da4a..e5556d27 100644 --- a/src/aig/gia/giaShrink7.c +++ b/src/aig/gia/giaShrink7.c @@ -52,202 +52,6 @@ extern word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * v /**Function************************************************************* - Synopsis [Check if the function is decomposable with the given pair.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Unm_ManCheckAnd( word t, int i, int j, word * pOut ) -{ - word c0 = Abc_Tt6Cofactor0( t, i ); - word c1 = Abc_Tt6Cofactor1( t, i ); - word c00 = Abc_Tt6Cofactor0( c0, j ); - word c01 = Abc_Tt6Cofactor1( c0, j ); - word c10 = Abc_Tt6Cofactor0( c1, j ); - word c11 = Abc_Tt6Cofactor1( c1, j ); - if ( c00 == c01 && c00 == c10 ) // i * j - { - if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11); - return 0; - } - if ( c11 == c00 && c11 == c10 ) // i * !j - { - if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01); - return 1; - } - if ( c11 == c00 && c11 == c01 ) // !i * j - { - if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10); - return 2; - } - if ( c11 == c01 && c11 == c10 ) // !i * !j - { - if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00); - return 3; - } - if ( c00 == c11 && c01 == c10 ) - { - if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10); - return 4; - } - return -1; -} -static inline int Unm_ManCheckMux( word t, int i, word * pOut ) -{ - word c0 = Abc_Tt6Cofactor0( t, i ); - word c1 = Abc_Tt6Cofactor1( t, i ); - word c00, c01, c10, c11; - int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1; - for ( k = 0; k < 6; k++ ) - { - if ( k == i ) continue; - fPres0 = Abc_Tt6HasVar( c0, k ); - fPres1 = Abc_Tt6HasVar( c1, k ); - if ( fPres0 && !fPres1 ) - { - if ( iVar0 >= 0 ) - return -1; - iVar0 = k; - } - if ( !fPres0 && fPres1 ) - { - if ( iVar1 >= 0 ) - return -1; - iVar1 = k; - } - } - if ( iVar0 == -1 || iVar1 == -1 ) - return -1; - c00 = Abc_Tt6Cofactor0( c0, iVar0 ); - c01 = Abc_Tt6Cofactor1( c0, iVar0 ); - c10 = Abc_Tt6Cofactor0( c1, iVar1 ); - c11 = Abc_Tt6Cofactor1( c1, iVar1 ); - if ( c00 == c10 && c01 == c11 ) // ITE(i, iVar1, iVar0) - { - if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11); - return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0); - } - if ( c00 == ~c10 && c01 == ~c11 ) // ITE(i, iVar1, !iVar0) - { - if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11); - return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1); - } - return -1; -} -void Unm_ManCheckTest2() -{ - word t, t1, Out, Var0, Var1, Var0_, Var1_; - int iVar0, iVar1, i, Res; - for ( iVar0 = 0; iVar0 < 6; iVar0++ ) - for ( iVar1 = 0; iVar1 < 6; iVar1++ ) - { - if ( iVar0 == iVar1 ) - continue; - Var0 = s_Truths6[iVar0]; - Var1 = s_Truths6[iVar1]; - for ( i = 0; i < 5; i++ ) - { - Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0; - Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1; - - t = Var0_ & Var1_; - if ( i == 4 ) - t = ~(Var0_ ^ Var1_); - -// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" ); - - Res = Unm_ManCheckAnd( t, iVar0, iVar1, &Out ); - if ( Res == -1 ) - { - printf( "No decomposition\n" ); - continue; - } - - Var0_ = s_Truths6[iVar0]; - Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_; - - Var1_ = s_Truths6[iVar1]; - Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_; - - t1 = Var0_ & Var1_; - if ( Res == 4 ) - t1 = Var0_ ^ Var1_; - - t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0)); - -// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); - - if ( t1 != t ) - printf( "Verification failed.\n" ); - else - printf( "Verification succeeded.\n" ); - } - } -} -void Unm_ManCheckTest() -{ - word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_; - int iVar0, iVar1, iCtrl, i, Res; - for ( iCtrl = 0; iCtrl < 6; iCtrl++ ) - for ( iVar0 = 0; iVar0 < 6; iVar0++ ) - for ( iVar1 = 0; iVar1 < 6; iVar1++ ) - { - if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 ) - continue; - Ctrl = s_Truths6[iCtrl]; - Var0 = s_Truths6[iVar0]; - Var1 = s_Truths6[iVar1]; - for ( i = 0; i < 8; i++ ) - { - Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl; - Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0; - Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1; - - t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_); - -// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" ); - - Res = Unm_ManCheckMux( t, iCtrl, &Out ); - if ( Res == -1 ) - { - printf( "No decomposition\n" ); - continue; - } - -// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" ); - - Ctrl_ = s_Truths6[iCtrl]; - Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)]; - Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_; - - Res >>= 16; - Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)]; - Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_; - - t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_); - -// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); -// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" ); - - t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl)); - -// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); - - if ( t1 != t ) - printf( "Verification failed.\n" ); - else - printf( "Verification succeeded.\n" ); - } - } -} - - -/**Function************************************************************* - Synopsis [] Description [] @@ -474,7 +278,7 @@ Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbos assert( FanK < FanJ ); iUsed = Vec_IntEntry( p->vId2Used, iObj ); uTruth = Vec_WrdEntry( p->vTruths, iUsed ); - Res = Unm_ManCheckAnd( uTruth, k, j, NULL ); + Res = Abc_TtCheckDsdAnd( uTruth, k, j, NULL ); if ( Res == -1 ) continue; // derive literals diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 14b13234..5561a2c6 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1404,6 +1404,203 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars ) return uRes2; } + +/**Function************************************************************* + + Synopsis [Check if the function is decomposable with the given pair.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCheckDsdAnd( word t, int i, int j, word * pOut ) +{ + word c0 = Abc_Tt6Cofactor0( t, i ); + word c1 = Abc_Tt6Cofactor1( t, i ); + word c00 = Abc_Tt6Cofactor0( c0, j ); + word c01 = Abc_Tt6Cofactor1( c0, j ); + word c10 = Abc_Tt6Cofactor0( c1, j ); + word c11 = Abc_Tt6Cofactor1( c1, j ); + if ( c00 == c01 && c00 == c10 ) // i * j + { + if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11); + return 0; + } + if ( c11 == c00 && c11 == c10 ) // i * !j + { + if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01); + return 1; + } + if ( c11 == c00 && c11 == c01 ) // !i * j + { + if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10); + return 2; + } + if ( c11 == c01 && c11 == c10 ) // !i * !j + { + if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00); + return 3; + } + if ( c00 == c11 && c01 == c10 ) + { + if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10); + return 4; + } + return -1; +} +static inline int Abc_TtCheckDsdMux( word t, int i, word * pOut ) +{ + word c0 = Abc_Tt6Cofactor0( t, i ); + word c1 = Abc_Tt6Cofactor1( t, i ); + word c00, c01, c10, c11; + int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1; + for ( k = 0; k < 6; k++ ) + { + if ( k == i ) continue; + fPres0 = Abc_Tt6HasVar( c0, k ); + fPres1 = Abc_Tt6HasVar( c1, k ); + if ( fPres0 && !fPres1 ) + { + if ( iVar0 >= 0 ) + return -1; + iVar0 = k; + } + if ( !fPres0 && fPres1 ) + { + if ( iVar1 >= 0 ) + return -1; + iVar1 = k; + } + } + if ( iVar0 == -1 || iVar1 == -1 ) + return -1; + c00 = Abc_Tt6Cofactor0( c0, iVar0 ); + c01 = Abc_Tt6Cofactor1( c0, iVar0 ); + c10 = Abc_Tt6Cofactor0( c1, iVar1 ); + c11 = Abc_Tt6Cofactor1( c1, iVar1 ); + if ( c00 == c10 && c01 == c11 ) // ITE(i, iVar1, iVar0) + { + if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11); + return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0); + } + if ( c00 == ~c10 && c01 == ~c11 ) // ITE(i, iVar1, !iVar0) + { + if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11); + return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1); + } + return -1; +} +static inline void Unm_ManCheckTest2() +{ + word t, t1, Out, Var0, Var1, Var0_, Var1_; + int iVar0, iVar1, i, Res; + for ( iVar0 = 0; iVar0 < 6; iVar0++ ) + for ( iVar1 = 0; iVar1 < 6; iVar1++ ) + { + if ( iVar0 == iVar1 ) + continue; + Var0 = s_Truths6[iVar0]; + Var1 = s_Truths6[iVar1]; + for ( i = 0; i < 5; i++ ) + { + Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0; + Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1; + + t = Var0_ & Var1_; + if ( i == 4 ) + t = ~(Var0_ ^ Var1_); + +// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" ); + + Res = Abc_TtCheckDsdAnd( t, iVar0, iVar1, &Out ); + if ( Res == -1 ) + { + printf( "No decomposition\n" ); + continue; + } + + Var0_ = s_Truths6[iVar0]; + Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_; + + Var1_ = s_Truths6[iVar1]; + Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_; + + t1 = Var0_ & Var1_; + if ( Res == 4 ) + t1 = Var0_ ^ Var1_; + + t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0)); + +// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); + + if ( t1 != t ) + printf( "Verification failed.\n" ); + else + printf( "Verification succeeded.\n" ); + } + } +} +static inline void Unm_ManCheckTest() +{ + word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_; + int iVar0, iVar1, iCtrl, i, Res; + for ( iCtrl = 0; iCtrl < 6; iCtrl++ ) + for ( iVar0 = 0; iVar0 < 6; iVar0++ ) + for ( iVar1 = 0; iVar1 < 6; iVar1++ ) + { + if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 ) + continue; + Ctrl = s_Truths6[iCtrl]; + Var0 = s_Truths6[iVar0]; + Var1 = s_Truths6[iVar1]; + for ( i = 0; i < 8; i++ ) + { + Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl; + Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0; + Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1; + + t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_); + +// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" ); + + Res = Abc_TtCheckDsdMux( t, iCtrl, &Out ); + if ( Res == -1 ) + { + printf( "No decomposition\n" ); + continue; + } + +// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" ); + + Ctrl_ = s_Truths6[iCtrl]; + Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)]; + Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_; + + Res >>= 16; + Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)]; + Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_; + + t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_); + +// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); +// Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" ); + + t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl)); + +// Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" ); + + if ( t1 != t ) + printf( "Verification failed.\n" ); + else + printf( "Verification succeeded.\n" ); + } + } +} + + /*=== utilTruth.c ===========================================================*/ |