summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-10-06 16:16:21 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-10-06 16:16:21 -0700
commit7a1c4ee86759bf8f6ba8e78126a7c296bd905f36 (patch)
tree801c3f80fe8536e212946749c117b6e31fb18230 /src/misc
parent8a03e530c299fba1e862a5943207c39fbd52ee06 (diff)
downloadabc-7a1c4ee86759bf8f6ba8e78126a7c296bd905f36.tar.gz
abc-7a1c4ee86759bf8f6ba8e78126a7c296bd905f36.tar.bz2
abc-7a1c4ee86759bf8f6ba8e78126a7c296bd905f36.zip
Moved the code to a different file.
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/util/utilTruth.h197
1 files changed, 197 insertions, 0 deletions
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 ===========================================================*/