From a4a1053d9851cf9ef52a5b52818e66b9c1bdba4d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 5 Oct 2013 22:44:02 -0700 Subject: Towards better Boolean matching. --- abclib.dsp | 148 +---------- src/aig/gia/gia.h | 3 +- src/aig/gia/giaIf.c | 15 +- src/aig/gia/giaMan.c | 2 +- src/base/abci/abc.c | 37 ++- src/map/if/ifDec07.c | 296 +++++++++++++++++---- src/misc/util/utilTruth.h | 13 + src/opt/dau/dauDsd.c | 4 +- src/opt/dau/dauNonDsd.c | 642 ++++++++++++++++++++++++++++++++++++++++++++++ src/opt/dau/module.make | 1 + 10 files changed, 949 insertions(+), 212 deletions(-) create mode 100644 src/opt/dau/dauNonDsd.c diff --git a/abclib.dsp b/abclib.dsp index 236bbe42..275f3896 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -733,154 +733,10 @@ SOURCE=.\src\base\test\test.c # Begin Group "abc2" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abc2\abc2.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2_.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Blifi.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Blifo.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Core.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Dup.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Equiv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Extract.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Flatten.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Func.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Fx.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Gia.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Hash.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Insert.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Logic.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Map.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Mfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Multi.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Ntk.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Part.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Print.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Rec.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Slack.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Strash.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Time.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Truth.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Util.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Veri.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Verify.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Vero.c -# End Source File # End Group # Begin Group "abc2d" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abc2d\abc2d.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\ast2.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\magic.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\magic.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\util.c -# End Source File # End Group # End Group # Begin Group "bdd" @@ -2227,6 +2083,10 @@ SOURCE=.\src\opt\dau\dauMerge.c # End Source File # Begin Source File +SOURCE=.\src\opt\dau\dauNonDsd.c +# End Source File +# Begin Source File + SOURCE=.\src\opt\dau\dauTree.c # End Source File # End Group diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fb93e0c2..b10a0677 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -193,6 +193,7 @@ struct Gps_Par_t_ int fCut; int fNpn; int fLutProf; + int fDumpFile; }; typedef struct Emb_Par_t_ Emb_Par_t; @@ -1077,7 +1078,7 @@ extern void Gia_ManHashProfile( Gia_Man_t * p ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ); /*=== giaIf.c ===========================================================*/ -extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); +extern void Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); extern void Gia_ManPrintLutStats( Gia_Man_t * p ); extern int Gia_ManLutFaninCount( Gia_Man_t * p ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index d50e34c9..425445c9 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -303,7 +303,7 @@ int Gia_ManComputeOverlap( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManPrintMappingStats( Gia_Man_t * p ) +void Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile ) { int * pLevels; int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0; @@ -328,7 +328,8 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p ) Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) ); Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) ); Abc_Print( 1, "\n" ); -/* + + if ( fDumpFile ) { char * pFileName = "stats_map.txt"; static char FileNameOld[1000] = {0}; @@ -355,7 +356,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p ) } fclose( pTable ); } -*/ + } /**Function************************************************************* @@ -782,6 +783,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t for ( i = 0; i < 4; i++ ) { int v = (int)((z >> (16+(i<<2))) & 7); + if ( v == 6 && Vec_IntSize(vLeaves) == 5 ) + continue; Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v) ); } Truth = (z & 0xffff); @@ -793,6 +796,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t for ( i = 0; i < 4; i++ ) { int v = (int)((z >> (48+(i<<2))) & 7); + if ( v == 6 && Vec_IntSize(vLeaves) == 5 ) + continue; if ( v == 7 ) Vec_IntPush( vLeavesTemp, iObjLit1 ); else @@ -1204,8 +1209,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) word Truth = 0, * pTruthTable; int i, k, Entry; assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth ); - if ( pIfMan->pPars->fEnableCheck07 ) - pIfMan->pPars->fDeriveLuts = 0; +// if ( pIfMan->pPars->fEnableCheck07 ) +// pIfMan->pPars->fDeriveLuts = 0; // start mapping and packing vMapping = Vec_IntStart( If_ManObjNum(pIfMan) ); vMapping2 = Vec_IntStart( 1 ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index e57fe27d..2eaf8eee 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -366,7 +366,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) if ( p->pSibls ) Gia_ManPrintChoiceStats( p ); if ( Gia_ManHasMapping(p) ) - Gia_ManPrintMappingStats( p ); + Gia_ManPrintMappingStats( p, pPars->fDumpFile ); if ( pPars && pPars->fNpn && Gia_ManHasMapping(p) && Gia_ManLutSizeMax(p) <= 4 ) Gia_ManPrintNpnClasses( p ); if ( p->vPacking ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c9633158..eb8c2a89 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -994,10 +994,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) if ( Sdm_ManCanRead() ) Sdm_ManRead(); - { -// extern void Scl_LibertyTest(); -// Scl_LibertyTest(); - } } /**Function************************************************************* @@ -2221,16 +2217,19 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCofactor; int nCofLevel; int fProfile; + int fPrintDec; extern void Kit_DsdTest( unsigned * pTruth, int nVars ); extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose ); + extern void Dau_DecTrySets( word * p, int nVars ); // set defaults nCofLevel = 1; fCofactor = 0; fProfile = 0; + fPrintDec = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Npch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Npcdh" ) ) != EOF ) { switch ( c ) { @@ -2245,11 +2244,14 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCofLevel < 0 ) goto usage; break; + case 'p': + fProfile ^= 1; + break; case 'c': fCofactor ^= 1; break; - case 'p': - fProfile ^= 1; + case 'd': + fPrintDec ^= 1; break; case 'h': goto usage; @@ -2291,6 +2293,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) ); // Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); // Abc_Print( -1, "\n" ); + if ( fPrintDec && Abc_ObjFaninNum(pObj) <= 6 ) + Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) ); if ( fProfile ) Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) ); else if ( fCofactor ) @@ -2302,10 +2306,11 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: print_dsd [-pch] [-N ]\n" ); + Abc_Print( -2, "usage: print_dsd [-pcdh] [-N ]\n" ); Abc_Print( -2, "\t print DSD formula for a single-output function with less than 16 variables\n" ); Abc_Print( -2, "\t-p : toggle printing profile [default = %s]\n", fProfile? "yes": "no" ); Abc_Print( -2, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle printing decompositions [default = %s]\n", fPrintDec? "yes": "no" ); Abc_Print( -2, "\t-N : the number of levels to cofactor [default = %d]\n", nCofLevel ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -25318,7 +25323,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; memset( pPars, 0, sizeof(Gps_Par_t) ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnlh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnldh" ) ) != EOF ) { switch ( c ) { @@ -25337,6 +25342,9 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': pPars->fLutProf ^= 1; break; + case 'd': + pPars->fDumpFile ^= 1; + break; case 'h': goto usage; default: @@ -25352,13 +25360,14 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &ps [-tpcnlh]\n" ); + Abc_Print( -2, "usage: &ps [-tpcnldh]\n" ); Abc_Print( -2, "\t prints stats of the current AIG\n" ); - Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" ); - Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" ); + Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" ); Abc_Print( -2, "\t-c : toggle printing the size of frontier cut [default = %s]\n", pPars->fCut? "yes": "no" ); Abc_Print( -2, "\t-n : toggle printing NPN classes of functions [default = %s]\n", pPars->fNpn? "yes": "no" ); - Abc_Print( -2, "\t-l : toggle printing LUT size profile [default = %s]\n", pPars->fLutProf? "yes": "no" ); + Abc_Print( -2, "\t-l : toggle printing LUT size profile [default = %s]\n", pPars->fLutProf? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping statistics into a file [default = %s]\n", pPars->fDumpFile? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -33697,7 +33706,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // pTemp = Llb_ReachableStatesGia( pAbc->pGia ); // Abc_FrameUpdateGia( pAbc, pTemp ); // Unm_ManTest( pAbc->pGia ); - Agi_ManTest( pAbc->pGia ); +// Agi_ManTest( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-F num] [-svh]\n" ); diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c index 1bbc93fb..6059b772 100644 --- a/src/map/if/ifDec07.c +++ b/src/map/if/ifDec07.c @@ -21,6 +21,7 @@ #include "if.h" #include "misc/extra/extra.h" #include "bool/kit/kit.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -115,7 +116,7 @@ static word If_Dec6ComposeLut4( int t, word f[4] ) } return r; } -void If_Dec6Verify( word t, word z ) +word If_Dec6Truth( word z ) { word r, q, f[4]; int i, v; @@ -124,20 +125,29 @@ void If_Dec6Verify( word t, word z ) { v = (z >> (16+(i<<2))) & 7; assert( v != 7 ); + if ( v == 6 ) + continue; f[i] = Truth6[v]; } q = If_Dec6ComposeLut4( (int)(z & 0xffff), f ); for ( i = 0; i < 4; i++ ) { v = (z >> (48+(i<<2))) & 7; + if ( v == 6 ) + continue; f[i] = (v == 7) ? q : Truth6[v]; } r = If_Dec6ComposeLut4( (int)((z >> 32) & 0xffff), f ); + return r; +} +void If_Dec6Verify( word t, word z ) +{ + word r = If_Dec6Truth( z ); if ( r != t ) { If_DecPrintConfig( z ); Kit_DsdPrintFromTruth( (unsigned*)&t, 6 ); printf( "\n" ); - Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" ); +// Kit_DsdPrintFromTruth( (unsigned*)&q, 6 ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)&r, 6 ); printf( "\n" ); printf( "Verification failed!\n" ); } @@ -677,43 +687,191 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] ) ***********************************************************************/ // count the number of unique cofactors -static inline int If_Dec5CofCount2( word t, int x, int y ) +static inline word If_Dec5CofCount2( word t, int x, int y, int * Pla2Var, word t0, int fDerive ) { - int i, Mask; + int m, i, Mask; assert( x >= 0 && x < 4 ); assert( y >= 0 && y < 4 ); + for ( m = 0; m < 4; m++ ) + { + for ( Mask = i = 0; i < 16; i++ ) + if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) ) + Mask |= (1 << ((t >> (i<<1)) & 3)); + if ( BitCount8[Mask & 0xF] > 2 ) + return 0; + } +// Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" ); + if ( !fDerive ) + return 1; + else + { + int fHas2, fHas3; + // composition function C depends on {x, y, Out, v[0]} + // decomposed function D depends on {x, y, z1, z2} + word F[4] = { 0, ABC_CONST(0x5555555555555555), ABC_CONST(0xAAAAAAAAAAAAAAAA), ~((word)0) }; + word C2[4], D2[4] = {0}, C1[2], D1[2], C, D, z; + int v, zz1 = -1, zz2 = -1; + // find two variables + for ( v = 0; v < 4; v++ ) + if ( v != x && v != y ) + { zz1 = v; break; } + for ( v = 1; v < 4; v++ ) + if ( v != x && v != y && v != zz1 ) + { zz2 = v; break; } + assert( zz1 != -1 && zz2 != -1 ); + // find the cofactors + for ( m = 0; m < 4; m++ ) + { + // for each cofactor, derive C2 and D2 + for ( Mask = i = 0; i < 16; i++ ) + if ( ((i >> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) ) + Mask |= (1 << ((t >> (i<<1)) & 3)); + // find the values + if ( BitCount8[Mask & 0xF] == 1 ) + { + C2[m] = F[Abc_Tt6FirstBit( Mask )]; + D2[m] = ~(word)0; + } + else if ( BitCount8[Mask & 0xF] == 2 ) + { + int Bit0 = Abc_Tt6FirstBit( Mask ); + int Bit1 = Abc_Tt6FirstBit( Mask ^ (((word)1)<> x) & 1) == ((m >> 0) & 1) && ((i >> y) & 1) == ((m >> 1) & 1) ) + if ( Bit1 == ((t >> (i<<1)) & 3) ) + D2[m] |= (((word)1) << ( (((i >> zz2) & 1) << 1) | ((i >> zz1) & 1) )); + } + else assert( 0 ); + D2[m] = Abc_Tt6Stretch( D2[m], 2 ); + } - for ( Mask = i = 0; i < 16; i++ ) - if ( !((i >> x) & 1) && !((i >> y) & 1) ) - Mask |= (1 << ((t >> (i<<1)) & 3)); - if ( BitCount8[Mask & 0xF] > 2 ) - return 0; - - for ( Mask = i = 0; i < 16; i++ ) - if ( ((i >> x) & 1) && !((i >> y) & 1) ) - Mask |= (1 << ((t >> (i<<1)) & 3)); - if ( BitCount8[Mask & 0xF] > 2 ) - return 0; - - for ( Mask = i = 0; i < 16; i++ ) - if ( !((i >> x) & 1) && ((i >> y) & 1) ) - Mask |= (1 << ((t >> (i<<1)) & 3)); - if ( BitCount8[Mask & 0xF] > 2 ) - return 0; + // combine + C1[0] = (C2[1] & Truth6[2]) | (C2[0] & ~Truth6[2]); + C1[1] = (C2[3] & Truth6[2]) | (C2[2] & ~Truth6[2]); + C = (C1[1] & Truth6[3]) | (C1[0] & ~Truth6[3]); + + // combine + D1[0] = (D2[1] & Truth6[2]) | (D2[0] & ~Truth6[2]); + D1[1] = (D2[3] & Truth6[2]) | (D2[2] & ~Truth6[2]); + D = (D1[1] & Truth6[3]) | (D1[0] & ~Truth6[3]); + +// printf( "\n" ); +// Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n"); +// Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n"); + + // create configuration + // find one + fHas2 = Abc_TtHasVar(&D, 5, 2); + fHas3 = Abc_TtHasVar(&D, 5, 3); + if ( fHas2 && fHas3 ) + { + z = D & 0xFFFF; + z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0)); + z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1)); + z |= (((word)Pla2Var[x+1]) << (16 + 4*2)); + z |= (((word)Pla2Var[y+1]) << (16 + 4*3)); + } + else if ( fHas2 && !fHas3 ) + { + z = D & 0xFFFF; + z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0)); + z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1)); + z |= (((word)Pla2Var[x+1]) << (16 + 4*2)); + z |= (((word)6) << (16 + 4*3)); + } + else if ( !fHas2 && fHas3 ) + { + Abc_TtSwapVars( &D, 5, 2, 3 ); + z = D & 0xFFFF; + z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0)); + z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1)); + z |= (((word)Pla2Var[y+1]) << (16 + 4*2)); + z |= (((word)6) << (16 + 4*3)); + } + else + { + z = D & 0xFFFF; + z |= (((word)Pla2Var[zz1+1]) << (16 + 4*0)); + z |= (((word)Pla2Var[zz2+1]) << (16 + 4*1)); + z |= (((word)6) << (16 + 4*2)); + z |= (((word)6) << (16 + 4*3)); + } - for ( Mask = i = 0; i < 16; i++ ) - if ( ((i >> x) & 1) && ((i >> y) & 1) ) - Mask |= (1 << ((t >> (i<<1)) & 3)); - if ( BitCount8[Mask & 0xF] > 2 ) - return 0; + // second one + fHas2 = Abc_TtHasVar(&C, 5, 2); + fHas3 = Abc_TtHasVar(&C, 5, 3); + if ( fHas2 && fHas3 ) + { + z |= ((C & 0xFFFF) << 32); + z |= (((word)Pla2Var[0]) << (48 + 4*0)); + z |= (((word)7) << (48 + 4*1)); + z |= (((word)Pla2Var[x+1]) << (48 + 4*2)); + z |= (((word)Pla2Var[y+1]) << (48 + 4*3)); + } + else if ( fHas2 && !fHas3 ) + { + z |= ((C & 0xFFFF) << 32); + z |= (((word)Pla2Var[0]) << (48 + 4*0)); + z |= (((word)7) << (48 + 4*1)); + z |= (((word)Pla2Var[x+1]) << (48 + 4*2)); + z |= (((word)6) << (48 + 4*3)); + } + else if ( !fHas2 && fHas3 ) + { + Abc_TtSwapVars( &C, 5, 2, 3 ); + z |= ((C & 0xFFFF) << 32); + z |= (((word)Pla2Var[0]) << (48 + 4*0)); + z |= (((word)7) << (48 + 4*1)); + z |= (((word)Pla2Var[y+1]) << (48 + 4*2)); + z |= (((word)6) << (48 + 4*3)); + } + else + { + z |= ((C & 0xFFFF) << 32); + z |= (((word)Pla2Var[0]) << (48 + 4*0)); + z |= (((word)7) << (48 + 4*1)); + z |= (((word)6) << (48 + 4*2)); + z |= (((word)6) << (48 + 4*3)); + } - return 1; + // verify + { + word t1 = If_Dec6Truth( z ); + if ( t1 != t0 ) + { + printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)&C2[0], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&C2[1], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&C2[2], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&C2[3], 5 ); printf("\n"); + + printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)&D2[0], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&D2[1], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&D2[2], 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&D2[3], 5 ); printf("\n"); + + printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)&C, 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&D, 5 ); printf("\n"); + + printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)&t1, 5 ); printf("\n"); + Kit_DsdPrintFromTruth( (unsigned *)&t0, 5 ); printf("\n"); + } + assert( t1 == t0 ); + } + return z; + } } word If_Dec5Perform( word t, int fDerive ) { int Pla2Var[7], Var2Pla[7]; int i, j, v; -// word t0 = t; + word t0 = t; +/* word c0, c1, c00, c01, c10, c11; for ( i = 0; i < 5; i++ ) { @@ -752,6 +910,7 @@ word If_Dec5Perform( word t, int fDerive ) return 1; } } +*/ // start arrays for ( i = 0; i < 7; i++ ) Pla2Var[i] = Var2Pla[i] = i; @@ -762,9 +921,21 @@ word If_Dec5Perform( word t, int fDerive ) If_DecVerifyPerm( Pla2Var, Var2Pla ); for ( i = 0; i < 4; i++ ) for ( j = i + 1; j < 4; j++ ) - if ( If_Dec5CofCount2( t, i, j ) ) - return 1; + { + word z = If_Dec5CofCount2( t, i, j, Pla2Var, t0, fDerive ); + if ( z ) + { +/* + if ( v == 0 && i == 1 && j == 2 ) + { + Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" ); + } +*/ + return z; + } + } } + /* // start arrays for ( i = 0; i < 7; i++ ) @@ -808,10 +979,42 @@ word If_Dec5Perform( word t, int fDerive ) } } */ + // Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf( "\n" ); return 0; } +word If_Dec5PerformEx() +{ + word z; + // find one + z = 0x17ac & 0xFFFF; + z |= (((word)3) << (16 + 4*0)); + z |= (((word)4) << (16 + 4*1)); + z |= (((word)1) << (16 + 4*2)); + z |= (((word)2) << (16 + 4*3)); + // second one + z |= ((0x179a & 0xFFFF) << 32); + z |= (((word)0) << (48 + 4*0)); + z |= (((word)7) << (48 + 4*1)); + z |= (((word)1) << (48 + 4*2)); + z |= (((word)2) << (48 + 4*3)); + return z; +} +void If_Dec5PerformTest() +{ + word z, t, t1; +// s = If_Dec5PerformEx(); +// t = If_Dec6Truth( s ); + t = 0xB0F3B0FFB0F3B0FF; + + Kit_DsdPrintFromTruth( (unsigned *)&t, 5 ); printf("\n"); + + z = If_Dec5Perform( t, 1 ); + t1 = If_Dec6Truth( z ); + assert( t == t1 ); +} + /**Function************************************************************* @@ -830,18 +1033,14 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea return 1; if ( nLeaves == 5 ) { - word z, t = ((word *)pTruth)[0]; -// if ( If_Dec6CheckMux(t) >= 0 ) -// return 1; - z = If_Dec6Perform( t, 1 ); + word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0]; + z = If_Dec5Perform( t, 1 ); If_Dec6Verify( t, z ); return z; } if ( nLeaves == 6 ) { word z, t = ((word *)pTruth)[0]; -// if ( If_Dec6CheckMux(t) >= 0 ) -// return 1; z = If_Dec6Perform( t, 1 ); If_Dec6Verify( t, z ); return z; @@ -851,8 +1050,6 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea word z, t[2]; t[0] = ((word *)pTruth)[0]; t[1] = ((word *)pTruth)[1]; - if ( If_Dec7CheckMux(t) >= 0 ) - return 1; z = If_Dec7Perform( t, 1 ); If_Dec7Verify( t, z ); return z; @@ -875,26 +1072,33 @@ word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLea int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) { int fDerive = 0; + int v; + // skip non-support minimal + for ( v = 0; v < nLeaves; v++ ) + if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) ) + return 0; + // check if ( nLeaves < 5 ) return 1; if ( nLeaves == 5 ) { - word t = ((word)pTruth[0] << 32) | (word)pTruth[0]; - if ( If_Dec5Perform( t, fDerive ) ) - return 1; - return 0; + word z, t = ((word)pTruth[0] << 32) | (word)pTruth[0]; + z = If_Dec5Perform( t, fDerive ); + if ( fDerive && z ) + If_Dec6Verify( t, z ); + return z != 0; } if ( nLeaves == 6 ) { word z, t = ((word *)pTruth)[0]; - if ( If_Dec6CheckMux(t) >= 0 ) - return 1; z = If_Dec6Perform( t, fDerive ); if ( fDerive && z ) { // If_DecPrintConfig( z ); If_Dec6Verify( t, z ); } + if ( z == 0 ) + Extra_PrintHex(stdout, (unsigned *)&t, 6), printf( " " ), Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" ); return z != 0; } if ( nLeaves == 7 ) @@ -902,8 +1106,8 @@ int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave word z, t[2]; t[0] = ((word *)pTruth)[0]; t[1] = ((word *)pTruth)[1]; - if ( If_Dec7CheckMux(t) >= 0 ) - return 1; +// if ( If_Dec7CheckMux(t) >= 0 ) +// return 1; z = If_Dec7Perform( t, fDerive ); if ( fDerive && z ) If_Dec7Verify( t, z ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 07f36382..cded2ce8 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1064,6 +1064,19 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar return; } } +// moves one var (v) to the given position (p) +static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p ) +{ + int iVar = V2P[v], jVar = p; + if ( iVar == jVar ) + return; + Abc_TtSwapVars( pF, nVars, iVar, jVar ); + V2P[P2V[iVar]] = jVar; + V2P[P2V[jVar]] = iVar; + P2V[iVar] ^= P2V[jVar]; + P2V[jVar] ^= P2V[iVar]; + P2V[iVar] ^= P2V[jVar]; +} /**Function************************************************************* diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index dc34a22a..7ffe63be 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -1900,7 +1900,9 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteT void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit ) { char pRes[DAU_MAX_STR]; - Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes ); + word pTemp[DAU_MAX_WORD]; + Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 ); + Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes ); fprintf( pFile, "%s\n", pRes ); } diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c new file mode 100644 index 00000000..65821027 --- /dev/null +++ b/src/opt/dau/dauNonDsd.c @@ -0,0 +1,642 @@ +/**CFile**************************************************************** + + FileName [dauNonDsd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware unmapping.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: dauNonDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dauInt.h" +#include "misc/util/utilTruth.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the bit count for the first 256 integer numbers +static int BitCount8[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; +static inline BitCount16( int i ) { return BitCount8[i & 0xFF] + BitCount8[i >> 8]; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks decomposability with given BS variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dau_DecGetMinterm( word * p, int g, int nVarsS, int uMaskAll ) +{ + int m, c, v; + for ( m = c = v = 0; v < nVarsS; v++ ) + if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable + { + if ( (g >> v) & 1 ) + m |= (1 << c); + c++; + } + assert( c >= 2 ); + p[m>>6] |= (((word)1)<<(m & 63)); +} +static inline int Dau_DecCheckSet5( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec ) +{ + int fFound0 = 0, fFound1 = 0; + int g, gMax = (1 << (nVars - nVarsF)); + int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1; + word Mask2 = (((word)1) << (1 << nVarsF)) - 1; + word Cof0 = 0, Cof1 = 0, Value; + assert( nVarsF >= 1 && nVarsF <= 5 ); + if ( pDec ) *pDec = 0; + for ( g = 0; g < gMax; g++ ) + if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue + { + Value = (p[g>>Shift] >> ((g&Mask)<= 6 && nVarsF <= nVars - 2 ); + if ( pDec ) *pDec = 0; + for ( g = 0; g < gMax; g++ ) + if ( (g & uMaskAll) == uMaskValue ) + { + if ( !fFound0 ) + Cof0 = p + g * nWords, fFound0 = 1; + else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) ) + continue; + else if ( !fFound1 ) + { + Cof1 = p + g * nWords, fFound1 = 1; + if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); + } + else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) ) + { + if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll ); + continue; + } + else + return 0; + } + if ( pCof0 ) + { + assert( fFound0 ); + Cof1 = fFound1 ? Cof1 : Cof0; + memcpy( pCof0, Cof0, sizeof(word) * nWords ); + memcpy( pCof1, Cof1, sizeof(word) * nWords ); + } + return 1; +} +static inline int Dau_DecCheckSetAny( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec ) +{ + assert( nVarsF >= 1 && nVarsF <= nVars - 2 ); + if ( nVarsF < 6 ) + return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec ); + else + return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec ); +} +int Dau_DecCheckSetTop( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word ** pCof0, word ** pCof1, word ** pDec ) +{ + int i, pVarsS[16]; + int v, m, mMax = (1 << nVarsS), uMaskValue; + assert( nVars >= 3 && nVars <= 16 ); + assert( nVars == nVarsF + nVarsB ); + assert( nVarsF >= 1 && nVarsF <= nVars - 2 ); + assert( nVarsB >= 2 && nVarsB <= nVars - 1 ); + assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 ); + if ( nVarsS == 0 ) + return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 ); + // collect shared variables + assert( maskS > 0 && maskS < (1 << nVarsB) ); + for ( i = 0, v = 0; v < nVarsB; v++ ) + if ( (maskS >> v) & 1 ) + pVarsS[i++] = v; + assert( i == nVarsS ); + // go through shared set minterms + for ( m = 0; m < mMax; m++ ) + { + // generate share set mask + uMaskValue = 0; + for ( v = 0; v < nVarsS; v++ ) + if ( (m >> v) & 1 ) + uMaskValue |= (1 << pVarsS[v]); + assert( (maskS & uMaskValue) == uMaskValue ); + // check decomposition + if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) ) + return 0; + } + return 1; +} + + +/**Function************************************************************* + + Synopsis [Variable sets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Dau_DecCreateSet( int * pVarsB, int sizeB, int maskS ) +{ + unsigned uSet = 0; int v; + for ( v = 0; v < sizeB; v++ ) + { + uSet |= (1 << (pVarsB[v] << 1)); + if ( (maskS >> v) & 1 ) + uSet |= (1 << ((pVarsB[v] << 1)+1)); + } + return uSet; +} +static inline int Dau_DecSetHas01( unsigned Mask ) +{ + return (Mask & ((~Mask) >> 1) & 0x55555555); +} +static inline int Dau_DecSetIsContained( Vec_Int_t * vSets, unsigned New ) +// Old=abcD contains New=abcDE +// Old=abcD contains New=abCD +{ + unsigned Old; + int i, Entry; + Vec_IntForEachEntry( vSets, Entry, i ) + { + Old = (unsigned)Entry; + if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New)) + return 1; + } + return 0; +} +void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine ) +{ + int v, Counter = 0; + int nUnique = 0, nShared = 0, nFree = 0; + for ( v = 0; v < nVars; v++ ) + { + int Value = ((set >> (v << 1)) & 3); + if ( Value == 1 ) + nUnique++; + else if ( Value == 3 ) + nShared++; + else if ( Value == 0 ) + nFree++; + else assert( 0 ); + } + printf( "S =%2d D =%2d C =%2d ", nShared, nUnique+nShared, nShared+nFree+1 ); + + printf( "x=" ); + for ( v = 0; v < nVars; v++ ) + { + int Value = ((set >> (v << 1)) & 3); + if ( Value == 1 ) + printf( "%c", 'a' + v ), Counter++; + else if ( Value == 3 ) + printf( "%c", 'A' + v ), Counter++; + else assert( Value == 0 ); + } + printf( " y=x" ); + for ( v = 0; v < nVars; v++ ) + { + int Value = ((set >> (v << 1)) & 3); + if ( Value == 0 ) + printf( "%c", 'a' + v ), Counter++; + else if ( Value == 3 ) + printf( "%c", 'A' + v ), Counter++; + } + for ( ; Counter < 15; Counter++ ) + printf( " " ); + if ( fNewLine ) + printf( "\n" ); +} +unsigned Dau_DecReadSet( char * pStr ) +{ + unsigned uSet = 0; int v; + for ( v = 0; pStr[v]; v++ ) + { + if ( pStr[v] >= 'a' && pStr[v] <= 'z' ) + uSet |= (1 << ((pStr[v] - 'a') << 1)); + else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' ) + uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1)); + else break; + } + return uSet; +} +void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars ) +{ + int i, Entry; + printf( "The set contains %d entries:\n", Vec_IntSize(vSets) ); + Vec_IntForEachEntry( vSets, Entry, i ) + Dau_DecPrintSet( (unsigned)Entry, nVars, 1 ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Find decomposable bound-sets of the given function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, int sizeB ) +{ + int v, c = 0; + for ( v = 0; v < nVars; v++ ) + if ( !((maskB >> v) & 1) ) + Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ ); + assert( c == nVars - sizeB ); +} +Vec_Int_t * Dau_DecFindSets( word * p, int nVars ) +{ + Vec_Int_t * vSets = Vec_IntAlloc( 32 ); + int V2P[16], P2V[16], pVarsB[16]; + int Limit = (1 << nVars); + int c, v, sizeB, sizeS, maskB, maskS; + unsigned setMixed; + for ( v = 0; v < nVars; v++ ) + assert( Abc_TtHasVar( p, nVars, v ) ); + // initialize permutation + for ( v = 0; v < nVars; v++ ) + V2P[v] = P2V[v] = v; + // iterate through bound sets of each size in increasing order + for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size + for ( maskB = 0; maskB < Limit; maskB++ ) // bound set + if ( BitCount16(maskB) == sizeB ) + { + // permute variables to have bound set on top + Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB ); + // collect bound set vars on levels nVars-sizeB to nVars-1 + for ( c = 0; c < sizeB; c++ ) + pVarsB[c] = P2V[nVars-sizeB+c]; + // check disjoint + if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) ) + { + Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) ); + continue; + } + if ( sizeB == 2 ) + continue; + // iterate through shared sets of each size in the increasing order + for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ ) // shared set size +// sizeS = 1; + for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set + if ( BitCount16(maskS) == sizeS ) + { + setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS ); +// printf( "Considering %10d ", setMixed ); +// Dau_DecPrintSet( setMixed, nVars ); + // check if it exists + if ( Dau_DecSetIsContained(vSets, setMixed) ) + continue; + // check if it can be added + if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) ) + Vec_IntPush( vSets, setMixed ); + } + } + return vSets; +} +void Dau_DecFindSetsTest2() +{ + Vec_Int_t * vSets; + word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); + word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); + word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); +// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2) +// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct +// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000 +// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) +// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def) + int nVars = 5; + + vSets = Dau_DecFindSets( &t, nVars ); + Dau_DecPrintSets( vSets, nVars ); + Vec_IntFree( vSets ); +} + + +/**Function************************************************************* + + Synopsis [Replaces variables in the string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DecVarReplace( char * pStr, int * pPerm, int nVars ) +{ + int v; + for ( v = 0; pStr[v]; v++ ) + if ( pStr[v] >= 'a' && pStr[v] <= 'z' ) + { + assert( pStr[v] - 'a' < nVars ); + pStr[v] = 'a' + pPerm[pStr[v] - 'a']; + } +} + +/**Function************************************************************* + + Synopsis [Decomposes with the given bound-set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DecDecomposeSet( word * pInit, int nVars, unsigned uSet, word * pComp, word * pDec, int * pPermC, int * pPermD, int * pnVarsC, int * pnVarsD ) +{ + word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64]; + word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD; + int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16]; + int nVarsU = 0, nVarsS = 0, nVarsF = 0; + int nWords = Abc_TtWordNum(nVars); + int v, d, c, Status, nDecs; + assert( nVars <= 16 ); + for ( v = 0; v < nVars; v++ ) + V2P[v] = P2V[v] = v; + memcpy( p, pInit, sizeof(word) * nWords ); + // sort variables + for ( v = 0; v < nVars; v++ ) + { + int Value = (uSet >> (v<<1)) & 3; + if ( Value == 0 ) + pVarsF[nVarsF++] = v; + else if ( Value == 1 ) + pVarsU[nVarsU++] = v; + else if ( Value == 3 ) + pVarsS[nVarsS++] = v; + else assert(0); + } + assert( nVarsS >= 0 && nVarsS <= 6 ); + assert( nVarsF + nVarsS + 1 <= 6 ); + assert( nVarsU + nVarsS <= 6 ); + // init space for decomposition functions + nDecs = (1 << nVarsS); + for ( d = 0; d < nDecs; d++ ) + { + pCof0[d] = Cof0 + d; + pCof1[d] = Cof1 + d; + pDecs[d] = Decs + d; + } + // permute variables + c = 0; + for ( v = 0; v < nVarsF; v++ ) + Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ ); + for ( v = 0; v < nVarsS; v++ ) + Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ ); + for ( v = 0; v < nVarsU; v++ ) + Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ ); + assert( c == nVars ); + // check decomposition + Status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs ); + if ( !Status ) + return 0; + // compute cofactors + assert( nVarsF + nVarsS < 6 ); + for ( d = 0; d < nDecs; d++ ) + { + Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]); + pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU ); + } + // compute the resulting functions + pComp[0] = 0; + pDec[0] = 0; + for ( d = 0; d < nDecs; d++ ) + { + // compute minterms for composition/decomposition function + MintC = MintD = ~((word)0); + for ( v = 0; v < nVarsS; v++ ) + { + MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v]; + MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v]; + } + // derive functions + pComp[0] |= MintC & Cof[d]; + pDec[0] |= MintD & pDecs[d][0]; + } + // derive variable permutations + if ( pPermC ) + { + for ( v = 0; v < nVarsF; v++ ) + pPermC[v] = pVarsF[v]; + for ( v = 0; v < nVarsS; v++ ) + pPermC[nVarsF+v] = pVarsS[v]; + pPermC[nVarsF + nVarsS] = nVars; + } + if ( pPermD ) + { + for ( v = 0; v < nVarsU; v++ ) + pPermD[v] = pVarsU[v]; + for ( v = 0; v < nVarsS; v++ ) + pPermD[nVarsU+v] = pVarsS[v]; + } + if ( pnVarsC ) + *pnVarsC = nVarsF + nVarsS + 1; + if ( pnVarsD ) + *pnVarsD = nVarsU + nVarsS; + return 1; +} + + +/**Function************************************************************* + + Synopsis [Testing procedures.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD ) +{ + word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16 + int nWordsC = Abc_TtWordNum(nVars+1); + int nWordsD = Abc_TtWordNum(nVars); + assert( nVars < 16 ); + memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC ); + memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD ); +// Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" ); +// Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" ); + if ( nVars >= 6 ) + { + assert( nWordsD >= 1 ); + assert( nWordsC > 1 ); + Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD ); + } + else + { + word pC0 = Abc_Tt6Stretch( pC[0], nVars ); + word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars ); + Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD ); + } + if ( Abc_TtEqual(pInit, pRes, nWordsD) ) + printf( " Verification successful\n" ); + else + printf( " Verification failed\n" ); + return 1; +} +int Dau_DecPerform( word * p, int nVars, unsigned uSet ) +{ + word tComp = 0, tDec = 0; + char pDsdC[1000], pDsdD[1000]; + int pPermC[16], pPermD[16], nVarsC, nVarsD; + int status, ResC, ResD; + status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec, pPermC, pPermD, &nVarsC, &nVarsD ); +// Dau_DecPrintSet( uSet, nVars ); +// printf( "Decomposition %s\n", status ? "exists" : "does not exist" ); + if ( !status ) + { + printf( " Decomposition does not exist\n" ); + return 0; + } +// Dau_DsdPrintFromTruth( stdout, p, nVars ); //printf( "\n" ); +// Dau_DsdPrintFromTruth( stdout, &tComp, nVars ); //printf( "\n" ); +// Dau_DsdPrintFromTruth( stdout, &tDec, nVars ); //printf( "\n" ); + // decompose + ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC ); + ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD ); +/* + printf( "%s\n", pDsdC ); + printf( "%s\n", pDsdD ); + for ( v = 0; v < nVarsC; v++ ) + printf( "%d ", pPermC[v] ); + printf( "\n" ); + for ( v = 0; v < nVarsD; v++ ) + printf( "%d ", pPermD[v] ); + printf( "\n" ); +*/ + // replace variables + Dau_DecVarReplace( pDsdD, pPermD, nVarsD ); + Dau_DecVarReplace( pDsdC, pPermC, nVarsC ); + printf( "%24s ", pDsdD ); + printf( "%24s ", pDsdC ); + Dau_DecVerify( p, nVars, pDsdC, pDsdD ); + return 1; +} +void Dau_DecTrySets( word * p, int nVars ) +{ + Vec_Int_t * vSets; + word t0 = *p; + int i, Entry; + vSets = Dau_DecFindSets( p, nVars ); + Dau_DsdPrintFromTruth( stdout, &t0, nVars ); + printf( "There are %d support-reducing decompositions:\n", Vec_IntSize(vSets) ); + Vec_IntForEachEntry( vSets, Entry, i ) + { + unsigned uSet = (unsigned)Entry; + Dau_DecPrintSet( uSet, nVars, 0 ); + Dau_DecPerform( &t0, nVars, uSet ); + } +// printf( "\n" ); + Vec_IntFree( vSets ); +} + +void Dau_DecFindSetsTest3() +{ + word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); + word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); + word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); +// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) + int nVars = 6; + char * pStr = "Bcd"; +// char * pStr = "Abcd"; +// char * pStr = "ab"; + unsigned uSet = Dau_DecReadSet( pStr ); + Dau_DecPerform( &t, nVars, uSet ); +} + +void Dau_DecFindSetsTest() +{ + int nVars = 6; +// word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]); +// word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]); +// word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1); +// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2) +// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct +// word t = ABC_CONST(0x00000000901FFFFF); // some funct + word t = ABC_CONST(0x000030F00D0D3FFF); // some funct +// word t = ABC_CONST(0x00000000690006FF); // some funct +// word t = ABC_CONST(0x7000F80007FF0FFF); // some funct +// word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var +// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000 +// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) +// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def) + Dau_DecTrySets( &t, nVars ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make index f339810b..190e30e4 100644 --- a/src/opt/dau/module.make +++ b/src/opt/dau/module.make @@ -5,4 +5,5 @@ SRC += src/opt/dau/dauCanon.c \ src/opt/dau/dauEnum.c \ src/opt/dau/dauGia.c \ src/opt/dau/dauMerge.c \ + src/opt/dau/dauNonDsd.c \ src/opt/dau/dauTree.c -- cgit v1.2.3