From a8d3b9a59e9d18f5e8924f9b007f2113b31f96d4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 7 Sep 2018 18:11:46 +0300 Subject: Expriments with functions. --- src/base/abci/abc.c | 67 +++++++++++++ src/opt/dau/dauNpn.c | 258 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 325 insertions(+) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5280f5fc..67d361ac 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -317,6 +317,7 @@ static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCubeEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPathEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFunEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1005,6 +1006,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "unpermute", Abc_CommandUnpermute, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "cubeenum", Abc_CommandCubeEnum, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "pathenum", Abc_CommandPathEnum, 0 ); + Cmd_CommandAdd( pAbc, "Sequential", "funenum", Abc_CommandFunEnum, 0 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 ); @@ -22973,6 +22975,71 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ); + int c, nInputs = 4, nVars = 4, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "SNvh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nInputs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nInputs < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + Dau_FunctionEnum( nInputs, nVars, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: funenum [-SN num] [-vh]\n" ); + Abc_Print( -2, "\t enumerates minimum 2-input-gate implementations\n" ); + Abc_Print( -2, "\t-S num : the maximum intermediate support size [default = %d]\n", nInputs ); + Abc_Print( -2, "\t-N num : the number of inputs of Boolean functions [default = %d]\n", nVars ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c index fb3d5db1..a9fbca10 100644 --- a/src/opt/dau/dauNpn.c +++ b/src/opt/dau/dauNpn.c @@ -21,6 +21,7 @@ #include "dauInt.h" #include "misc/util/utilTruth.h" #include "misc/extra/extra.h" +#include "bool/lucky/lucky.h" ABC_NAMESPACE_IMPL_START @@ -384,6 +385,263 @@ void Dau_NetworkEnumTest() } + +/**Function************************************************************* + + Synopsis [Performs exact canonicization of semi-canonical classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs ) +{ + Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) ); + word pAuxWord[1024], pAuxWord1[1024]; + word uTruth; int i, Entry; + permInfo * pi = setPermInfoPtr(nVars); + Vec_IntForEachEntry( vNodSup, Entry, i ) + { + if ( (Entry & 0xF) > nVars ) + continue; + uTruth = *Vec_MemReadEntry( vTtMem, i ); + simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars); + Vec_WrdWriteEntry( vCanons, i, uTruth ); + } + freePermInfoPtr(pi); + return vCanons; +} +void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax ) +{ + abctime clk = Abc_Clock(); int n, nTotal = 0; + Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs ); + Vec_Mem_t * vTtMem2 = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 ); + Vec_MemHashAlloc( vTtMem2, 1<<10 ); + Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk ); + printf( "Final results:\n" ); + for ( n = 0; n <= nNodesMax; n++ ) + { + int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0; + Vec_IntForEachEntry( vNodSup, Entry, i ) + { + if ( (Entry & 0xF) > nVars || (Entry >> 16) != n ) + continue; + Counter++; + nEntries2 = Vec_MemEntryNum(vTtMem2); + Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) ); + if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new + continue; + Counter2++; + } + nTotal += Counter2; + printf( "Nodes = %2d. ", n ); + printf( "Semi-canonical = %8d. ", Counter ); + printf( "Canonical = %8d. ", Counter2 ); + printf( "Total = %8d.", nTotal ); + printf( "\n" ); + } + Vec_MemHashFree( vTtMem2 ); + Vec_MemFreeP( &vTtMem2 ); + Vec_WrdFree( vCanons ); + fflush(stdout); +} + +/**Function************************************************************* + + Synopsis [Function enumeration.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars ) +{ + int i, Entry, Count = 0; + Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop ) + Count += ((Entry & 0xF) <= nVars); + return Count; +} +int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, abctime clk ) +{ + int nNew; + printf("Nodes = %2d. ", nNodes ); + printf("New%d = %8d. ", nInputs, iStop-iStart ); + printf("Total%d = %8d. ", nInputs, iStop ); + printf("New%d = %8d. ", nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) ); + printf("Total%d = %8d. ", nVars, Dau_CountFuncs(vNodSup, 0, iStop, nVars) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + fflush(stdout); + return nNew; +} +int Dau_InsertFunction( word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup ) +{ + char Perm[16] = {0}; + int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs ); + unsigned Phase = Abc_TtCanonicize( pCur, nVarsNew, Perm ); + int nEntries = Vec_MemEntryNum(vTtMem); + int Entry = Vec_MemHashInsert( vTtMem, pCur ); + if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new + return 0; + // this is a new class + Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew ); + assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) ); + return 1; +} +void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) +{ + abctime clk = Abc_Clock(); + int nWords = Abc_TtWordNum(nInputs); + Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 ); + Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 ); + int v, g, k, m, n, Entry, nNew, iStart = 1, iStop = 2; + word Truth[4] = {0}; + assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 ); + Vec_MemHashAlloc( vTtMem, 1<<16 ); + // add constant 0 + Vec_MemHashInsert( vTtMem, Truth ); + Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0 + // add buffer/inverter + Abc_TtIthVar( Truth, 0, nInputs ); + Abc_TtNot( Truth, nWords ); + Vec_MemHashInsert( vTtMem, Truth ); + Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1 + Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, clk ); + // numerate other functions based on how many nodes they have + for ( n = 1; n < 32; n++ ) + { + for ( Entry = iStart; Entry < iStop; Entry++ ) + { + word * pTruth = Vec_MemReadEntry( vTtMem, Entry ); + int NodSup = Vec_IntEntry(vNodSup, Entry); + int nSupp = 0xF & NodSup; + assert( n-1 == (NodSup >> 16) ); + assert( !Abc_Tt6HasVar(*pTruth, nSupp) ); + //printf( "Exploring function %4d with %d vars: ", i, nSupp ); + //printf( " %04x\n", (int)uTruth ); + //Dau_DsdPrintFromTruth( &uTruth, 4 ); + for ( v = 0; v < nSupp; v++ ) + { + word tGate, tCur; + word Cof0 = Abc_Tt6Cofactor0( *pTruth, v ); + word Cof1 = Abc_Tt6Cofactor1( *pTruth, v ); + if ( nSupp < nInputs ) + { + // add one extra variable to support + for ( g = 0; g < 2; g++ ) + { + if ( g == 0 ) + { + tGate = s_Truths6[v] & s_Truths6[nSupp]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + } + else + { + tGate = s_Truths6[v] ^ s_Truths6[nSupp]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + } + } + } + for ( g = 0; g < 2; g++ ) + { + // add one cross bar + for ( k = 0; k < nSupp; k++ ) if ( k != v ) + { + if ( g == 0 ) + { + tGate = s_Truths6[v] & s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tGate = s_Truths6[v] & ~s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + } + else + { + tGate = s_Truths6[v] ^ s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + } + } + } + for ( g = 0; g < 2; g++ ) + { + // add two cross bars + for ( k = 0; k < nSupp; k++ ) if ( k != v ) + for ( m = k+1; m < nSupp; m++ ) if ( m != v ) + { + if ( g == 0 ) + { + tGate = s_Truths6[m] & s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tGate = s_Truths6[m] & ~s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tGate = ~s_Truths6[m] & s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tGate = ~s_Truths6[m] & ~s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + + tCur = (tGate & Cof0) | (~tGate & Cof1); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + } + else + { + tGate = s_Truths6[m] ^ s_Truths6[k]; + tCur = (tGate & Cof1) | (~tGate & Cof0); + Dau_InsertFunction( &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + } + } + } + } + } + iStart = iStop; + iStop = Vec_IntSize(vNodSup); + nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, iStart, iStop, clk ); + if ( nNew == 0 ) + break; + } + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n ); + Vec_MemHashFree( vTtMem ); + Vec_MemFreeP( &vTtMem ); + Vec_IntFree( vNodSup ); + fflush(stdout); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3