Skip to content

A
abc
Commit 7a1c4ee8 by Alan Mishchenko
Options

Moved the code to a different file.

parent 8a03e530
Showing with 198 additions and 197 deletions
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 ...@@ -52,202 +52,6 @@ extern word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * v
/**Function************************************************************* /**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 [] Synopsis []
Description [] Description []
...@@ -474,7 +278,7 @@ Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbos ...@@ -474,7 +278,7 @@ Vec_Int_t * Unm_ManCollectDecomp( Unm_Man_t * p, Vec_Int_t * vPairs, int fVerbos
assert( FanK < FanJ ); assert( FanK < FanJ );
iUsed = Vec_IntEntry( p->vId2Used, iObj ); iUsed = Vec_IntEntry( p->vId2Used, iObj );
uTruth = Vec_WrdEntry( p->vTruths, iUsed ); uTruth = Vec_WrdEntry( p->vTruths, iUsed );
Res = Unm_ManCheckAnd( uTruth, k, j, NULL ); Res = Abc_TtCheckDsdAnd( uTruth, k, j, NULL );
if ( Res == -1 ) if ( Res == -1 )
continue; continue;
// derive literals // derive literals
......
src/misc/util/utilTruth.h
...@@ -1404,6 +1404,203 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars ) ...@@ -1404,6 +1404,203 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
return uRes2; 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 ===========================================================*/ /*=== utilTruth.c ===========================================================*/
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment