diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 14 | ||||
| -rw-r--r-- | src/base/abci/abcDec.c | 469 | ||||
| -rw-r--r-- | src/bool/bdc/bdc.h | 2 | ||||
| -rw-r--r-- | src/bool/bdc/bdcCore.c | 66 | ||||
| -rw-r--r-- | src/bool/kit/kit.h | 13 | ||||
| -rw-r--r-- | src/bool/kit/kitDsd.c | 88 |
6 files changed, 630 insertions, 22 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index efbc888c..74fe7fc2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4811,7 +4811,7 @@ usage: ***********************************************************************/ int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_DecTest( char * pFileName, int DecType ); + extern int Abc_DecTest( char * pFileName, int DecType, int fVerbose ); char * pFileName; int c; int fVerbose = 0; @@ -4849,17 +4849,17 @@ int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the output file name pFileName = argv[globalUtilOptind]; // call the testbench - Abc_DecTest( pFileName, DecType ); + Abc_DecTest( pFileName, DecType, fVerbose ); return 0; usage: Abc_Print( -2, "usage: testdec [-A <num>] [-vh] <file_name>\n" ); Abc_Print( -2, "\t testbench for Boolean decomposition algorithms\n" ); - Abc_Print( -2, "\t-A <num> : number of decomposition algorithm [default = %d]\n", DecType ); - Abc_Print( -2, "\t 0 : none (just read the input file)\n" ); - Abc_Print( -2, "\t 1 : algebraic factoring applied to ISOP\n" ); - Abc_Print( -2, "\t 2 : bi-decomposition with cofactoring\n" ); - Abc_Print( -2, "\t 3 : disjoint-support decomposition\n" ); + Abc_Print( -2, "\t-A <num> : decomposition algorithm [default = %d]\n", DecType ); + Abc_Print( -2, "\t 0: none (reading and writing the file)\n" ); + Abc_Print( -2, "\t 1: algebraic factoring applied to ISOP\n" ); + Abc_Print( -2, "\t 2: bi-decomposition with cofactoring\n" ); + Abc_Print( -2, "\t 3: disjoint-support decomposition with cofactoring\n" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 916866ad..8f0d1df8 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -18,7 +18,12 @@ ***********************************************************************/ -#include "base/abc/abc.h" +#include "misc/extra/extra.h" +#include "misc/vec/vec.h" + +#include "bool/bdc/bdc.h" +#include "bool/dec/dec.h" +#include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START @@ -33,10 +38,460 @@ ABC_NAMESPACE_IMPL_START // 2 - bi-decomposition // 3 - DSD +// data-structure to store a bunch of truth tables +typedef struct Abc_TtStore_t_ Abc_TtStore_t; +struct Abc_TtStore_t_ +{ + int nVars; + int nwords; + int nFuncs; + word ** pFuncs; +}; + +// read/write/flip i-th bit of a bit string table: +static inline int Abc_TruthGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; } +static inline void Abc_TruthSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); } +static inline void Abc_TruthXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); } + +// read/write k-th digit d of a hexadecimal number: +static inline int Abc_TruthGetHex( word * p, int k ) { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15; } +static inline void Abc_TruthSetHex( word * p, int k, int d ) { p[k>>4] |= (((word)d)<<((k<<2) & 63)); } +static inline void Abc_TruthXorHex( word * p, int k, int d ) { p[k>>4] ^= (((word)d)<<((k<<2) & 63)); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +// read one hex character +static inline int Abc_TruthReadHexDigit( char HexChar ) +{ + if ( HexChar >= '0' && HexChar <= '9' ) + return HexChar - '0'; + if ( HexChar >= 'A' && HexChar <= 'F' ) + return HexChar - 'A' + 10; + if ( HexChar >= 'a' && HexChar <= 'f' ) + return HexChar - 'a' + 10; + assert( 0 ); // not a hexadecimal symbol + return -1; // return value which makes no sense +} + +// write one hex character +static inline void Abc_TruthWriteHexDigit( FILE * pFile, int HexDigit ) +{ + assert( HexDigit >= 0 && HexDigit < 16 ); + if ( HexDigit < 10 ) + fprintf( pFile, "%d", HexDigit ); + else + fprintf( pFile, "%c", 'A' + HexDigit-10 ); +} + +// read one truth table in hexadecimal +void Abc_TruthReadHex( word * pTruth, char * pString, int nVars ) +{ + int nwords = (nVars < 7)? 1 : (1 << (nVars-6)); + int k, Digit, nDigits = (nwords << 4); + char EndSymbol; + // skip the first 2 symbols if they are "0x" + if ( pString[0] == '0' && pString[1] == 'x' ) + pString += 2; + // get the last symbol + EndSymbol = pString[nDigits]; + // the end symbol of the TT (the one immediately following hex digits) + // should be one of the following: space, a new-line, or a zero-terminator + // (note that on Windows symbols '\r' can be inserted before each '\n') + assert( EndSymbol == ' ' || EndSymbol == '\n' || EndSymbol == '\r' || EndSymbol == '\0' ); + // read hexadecimal digits in the reverse order + // (the last symbol in the string is the least significant digit) + for ( k = 0; k < nDigits; k++ ) + { + Digit = Abc_TruthReadHexDigit( pString[nDigits - 1 - k] ); + assert( Digit >= 0 && Digit < 16 ); + Abc_TruthSetHex( pTruth, k, Digit ); + } +} + +// write one truth table in hexadecimal (do not add end-of-line!) +void Abc_TruthWriteHex( FILE * pFile, word * pTruth, int nVars ) +{ + int nDigits, Digit, k; + // write hexadecimal digits in the reverse order + // (the last symbol in the string is the least significant digit) + nDigits = (1 << (nVars-2)); + for ( k = 0; k < nDigits; k++ ) + { + Digit = Abc_TruthGetHex( pTruth, nDigits - 1 - k ); + assert( Digit >= 0 && Digit < 16 ); + Abc_TruthWriteHexDigit( pFile, Digit ); + } +} + + +/**Function************************************************************* + + Synopsis [Allocate/Deallocate storage for truth tables..] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_TtStore_t * Abc_TruthStoreAlloc( int nVars, int nFuncs ) +{ + Abc_TtStore_t * p; + int i; + p = (Abc_TtStore_t *)malloc( sizeof(Abc_TtStore_t) ); + p->nVars = nVars; + p->nwords = (nVars < 7) ? 1 : (1 << (nVars-6)); + p->nFuncs = nFuncs; + // alloc array of 'nFuncs' pointers to truth tables + p->pFuncs = (word **)malloc( sizeof(word *) * p->nFuncs ); + // alloc storage for 'nFuncs' truth tables as one chunk of memory + p->pFuncs[0] = (word *)calloc( sizeof(word), p->nFuncs * p->nwords ); + // split it up into individual truth tables + for ( i = 1; i < p->nFuncs; i++ ) + p->pFuncs[i] = p->pFuncs[i-1] + p->nwords; + return p; +} +void Abc_TruthStoreFree( Abc_TtStore_t * p ) +{ + free( p->pFuncs[0] ); + free( p->pFuncs ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Read file contents.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_FileRead( char * pFileName ) +{ + FILE * pFile; + char * pBuffer; + int nFileSize; + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + // get the file size, in bytes + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + // move the file current reading position to the beginning + rewind( pFile ); + // load the contents of the file into memory + pBuffer = (char *)malloc( nFileSize + 3 ); + fread( pBuffer, nFileSize, 1, pFile ); + // add several empty lines at the end + // (these will be used to signal the end of parsing) + pBuffer[ nFileSize + 0] = '\n'; + pBuffer[ nFileSize + 1] = '\n'; + // terminate the string with '\0' + pBuffer[ nFileSize + 2] = '\0'; + fclose( pFile ); + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [Determine the number of variables by reading the first line.] + + Description [Determine the number of functions by counting the lines.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthGetParams( char * pFileName, int * pnVars, int * pnTruths ) +{ + char * pContents; + int i, nVars, nLines; + // prepare the output + if ( pnVars ) + *pnVars = 0; + if ( pnTruths ) + *pnTruths = 0; + // read data from file + pContents = Abc_FileRead( pFileName ); + if ( pContents == NULL ) + return; + // count the number of symbols before the first space or new-line + // (note that on Windows symbols '\r' can be inserted before each '\n') + for ( i = 0; pContents[i]; i++ ) + if ( pContents[i] == ' ' || pContents[i] == '\n' || pContents[i] == '\r' ) + break; + if ( pContents[i] == 0 ) + printf( "Strange, the input file does not have spaces and new-lines...\n" ); + + // acount for the fact that truth tables may have "0x" at the beginning of each line + if ( pContents[0] == '0' && pContents[1] == 'x' ) + i = i - 2; + + // determine the number of variables + for ( nVars = 0; nVars < 32; nVars++ ) + if ( 4 * i == (1 << nVars) ) // the number of bits equal to the size of truth table + break; + if ( nVars < 2 || nVars > 16 ) + { + printf( "Does not look like the input file contains truth tables...\n" ); + return; + } + if ( pnVars ) + *pnVars = nVars; + + // determine the number of functions by counting the lines + nLines = 0; + for ( i = 0; pContents[i]; i++ ) + nLines += (pContents[i] == '\n'); + if ( pnTruths ) + *pnTruths = nLines; + ABC_FREE( pContents ); +} + + +/**Function************************************************************* + + Synopsis [Read truth tables from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthStoreRead( char * pFileName, Abc_TtStore_t * p ) +{ + char * pContents; + int i, nLines; + pContents = Abc_FileRead( pFileName ); + if ( pContents == NULL ) + return; + // here it is assumed (without checking!) that each line of the file + // begins with a string of hexadecimal chars followed by space + + // the file will be read till the first empty line (pContents[i] == '\n') + // (note that Abc_FileRead() added several empty lines at the end of the file contents) + for ( nLines = i = 0; pContents[i] != '\n'; ) + { + // read one line + Abc_TruthReadHex( p->pFuncs[nLines++], &pContents[i], p->nVars ); + // skip till after the end-of-line symbol + // (note that end-of-line symbol is also skipped) + while ( pContents[i++] != '\n' ); + } + // adjust the number of functions read + // (we may have allocated more storage because some lines in the file were empty) + assert( p->nFuncs >= nLines ); + p->nFuncs = nLines; + ABC_FREE( pContents ); +} + +/**Function************************************************************* + + Synopsis [Write truth tables into file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthStoreWrite( char * pFileName, Abc_TtStore_t * p ) +{ + FILE * pFile; + int i; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + for ( i = 0; i < p->nFuncs; i++ ) + { + Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars ); + fprintf( pFile, "\n" ); + } + fclose( pFile ); +} + + +/**Function************************************************************* + + Synopsis [Read truth tables from input file and write them into output file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthStoreTest( char * pFileName ) +{ + Abc_TtStore_t * p; + char * pFileInput = pFileName; + char * pFileOutput = "out.txt"; + int nVars, nTruths; + + // figure out how many truth table and how many variables + Abc_TruthGetParams( pFileInput, &nVars, &nTruths ); + if ( nVars < 2 || nVars > 16 || nTruths == 0 ) + return; + + // allocate data-structure + p = Abc_TruthStoreAlloc( nVars, nTruths ); + + // read info from file + Abc_TruthStoreRead( pFileInput, p ); + + // write into another file + Abc_TruthStoreWrite( pFileOutput, p ); + + // delete data-structure + Abc_TruthStoreFree( p ); + printf( "Input file \"%s\" was copied into output file \"%s\".\n", pFileInput, pFileOutput ); +} + +/**Function************************************************************* + + Synopsis [Apply decomposition to the truth table.] + + Description [Returns the number of AIG nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) +{ + clock_t clk = clock(); + int i, nNodes = 0; + + char * pAlgoName = NULL; + if ( DecType == 1 ) + pAlgoName = "factoring"; + else if ( DecType == 2 ) + pAlgoName = "bi-decomp"; + else if ( DecType == 3 ) + pAlgoName = "DSD"; + + if ( pAlgoName ) + printf( "Applying %-10s to %8d func%s of %2d vars... ", + pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars ); + if ( fVerbose ) + printf( "\n" ); + + if ( DecType == 1 ) + { + // perform algebraic factoring and count AIG nodes + Dec_Graph_t * pFForm; + Vec_Int_t * vCover; + Vec_Str_t * vStr; + char * pSopStr; + vStr = Vec_StrAlloc( 10000 ); + vCover = Vec_IntAlloc( 1 << 16 ); + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + pSopStr = Kit_PlaFromTruthNew( (unsigned *)p->pFuncs[i], p->nVars, vCover, vStr ); + pFForm = Dec_Factor( pSopStr ); + nNodes += Dec_GraphNodeNum( pFForm ); + if ( fVerbose ) + Dec_GraphPrint( stdout, pFForm, NULL, NULL ); + Dec_GraphFree( pFForm ); + } + Vec_IntFree( vCover ); + Vec_StrFree( vStr ); + } + else if ( DecType == 2 ) + { + // perform bi-decomposition and count AIG nodes + Bdc_Man_t * pManDec; + Bdc_Par_t Pars = {0}, * pPars = &Pars; + pPars->nVarsMax = p->nVars; + pManDec = Bdc_ManAlloc( pPars ); + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + Bdc_ManDecompose( pManDec, (unsigned *)p->pFuncs[i], NULL, p->nVars, NULL, 1000 ); + nNodes += Bdc_ManAndNum( pManDec ); + if ( fVerbose ) + Bdc_ManDecPrint( pManDec ); + } + Bdc_ManFree( pManDec ); + } + else if ( DecType == 3 ) + { + // perform disjoint-support decomposition and count AIG nodes + // (non-DSD blocks are decomposed into 2:1 MUXes, each counting as 3 AIG nodes) + Kit_DsdNtk_t * pNtk; + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + pNtk = Kit_DsdDecomposeMux( (unsigned *)p->pFuncs[i], p->nVars, 3 ); + if ( fVerbose ) + Kit_DsdPrintExpanded( pNtk ), printf( "\n" ); + nNodes += Kit_DsdCountAigNodes( pNtk ); + Kit_DsdNtkFree( pNtk ); + } + } + else assert( 0 ); + + printf( "AIG nodes =%9d ", nNodes ); + Abc_PrintTime( 1, "Time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Apply decomposition to truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TruthDecTest( char * pFileName, int DecType, int fVerbose ) +{ + Abc_TtStore_t * p; + int nVars, nTruths; + + // figure out how many truth tables and how many variables + Abc_TruthGetParams( pFileName, &nVars, &nTruths ); + if ( nVars < 2 || nVars > 16 || nTruths == 0 ) + return; + + // allocate data-structure + p = Abc_TruthStoreAlloc( nVars, nTruths ); + + // read info from file + Abc_TruthStoreRead( pFileName, p ); + + // consider functions from the file + Abc_TruthDecPerform( p, DecType, fVerbose ); + + // delete data-structure + Abc_TruthStoreFree( p ); +// printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName ); +} + /**Function************************************************************* @@ -49,14 +504,20 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int Abc_DecTest( char * pFileName, int DecType ) +int Abc_DecTest( char * pFileName, int DecType, int fVerbose ) { - printf( "Trying to read file \"%s\".\n", pFileName ); + if ( fVerbose ) + printf( "Using truth tables from file \"%s\"...\n", pFileName ); + if ( DecType == 0 ) + Abc_TruthStoreTest( pFileName ); + else if ( DecType >= 1 && DecType <= 3 ) + Abc_TruthDecTest( pFileName, DecType, fVerbose ); + else + printf( "Unknown decomposition type value (%d).\n", DecType ); fflush( stdout ); return 0; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h index a7572fe8..bd0f7d7d 100644 --- a/src/bool/bdc/bdc.h +++ b/src/bool/bdc/bdc.h @@ -67,10 +67,12 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_F /*=== bdcCore.c ==========================================================*/ extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); extern void Bdc_ManFree( Bdc_Man_t * p ); +extern void Bdc_ManDecPrint( Bdc_Man_t * p ); extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ); extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ); extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ); extern int Bdc_ManNodeNum( Bdc_Man_t * p ); +extern int Bdc_ManAndNum( Bdc_Man_t * p ); extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ); extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ); extern void * Bdc_FuncCopy( Bdc_Fun_t * p ); diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c index fb318e0d..a810146d 100644 --- a/src/bool/bdc/bdcCore.c +++ b/src/bool/bdc/bdcCore.c @@ -46,6 +46,7 @@ ABC_NAMESPACE_IMPL_START Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); } Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; } int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; } +int Bdc_ManAndNum( Bdc_Man_t * p ) { return p->nNodes-p->nVars-1;} Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; } Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; } void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; } @@ -186,7 +187,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) /**Function************************************************************* - Synopsis [Clears the manager.] + Synopsis [Prints bi-decomposition in a simple format.] Description [] @@ -195,7 +196,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) SeeAlso [] ***********************************************************************/ -void Bdc_ManDecPrint( Bdc_Man_t * p ) +void Bdc_ManDecPrintSimple( Bdc_Man_t * p ) { Bdc_Fun_t * pNode; int i; @@ -211,7 +212,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p ) printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) ); printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) ); } - Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) ); +// Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) ); printf( "\n" ); } printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) ); @@ -219,6 +220,65 @@ void Bdc_ManDecPrint( Bdc_Man_t * p ) /**Function************************************************************* + Synopsis [Prints bi-decomposition recursively.] + + Description [This procedure prints bi-decomposition as a factored form. + In doing so, logic sharing, if present, will be replicated several times.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManDecPrint_rec( Bdc_Man_t * p, Bdc_Fun_t * pNode ) +{ + if ( pNode->Type == BDC_TYPE_PI ) + printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 ); + else if ( pNode->Type == BDC_TYPE_AND ) + { + Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode ); + Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode ); + + if ( Bdc_IsComplement(pNode0) ) + printf( "!" ); + if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI ) + printf( "(" ); + Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) ); + if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI ) + printf( ")" ); + + if ( Bdc_IsComplement(pNode1) ) + printf( "!" ); + if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI ) + printf( "(" ); + Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) ); + if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI ) + printf( ")" ); + } + else assert( 0 ); +} +void Bdc_ManDecPrint( Bdc_Man_t * p ) +{ + Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot); + + printf( "F = " ); + if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0 + printf( "Constant %d", !Bdc_IsComplement(p->pRoot) ); + else if ( pRoot->Type == BDC_TYPE_PI ) // literal + printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 ); + else + { + if ( Bdc_IsComplement(p->pRoot) ) + printf( "!(" ); + Bdc_ManDecPrint_rec( p, pRoot ); + if ( Bdc_IsComplement(p->pRoot) ) + printf( ")" ); + } + printf( "\n" ); +} + +/**Function************************************************************* + Synopsis [Performs decomposition of one function.] Description [] diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h index dfee532e..8151f1d2 100644 --- a/src/bool/kit/kit.h +++ b/src/bool/kit/kit.h @@ -112,17 +112,17 @@ struct Kit_DsdObj_t_ unsigned Offset : 8; // offset to the truth table unsigned nRefs : 8; // offset to the truth table unsigned nFans : 6; // the number of fanins of this node - unsigned char pFans[0]; // the fanin literals + unsigned short pFans[0]; // the fanin literals }; // DSD network typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t; struct Kit_DsdNtk_t_ { - unsigned char nVars; // at most 16 (perhaps 18?) - unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars) - unsigned char nNodes; // the number of nodes - unsigned char Root; // the root of the tree + unsigned short nVars; // at most 16 (perhaps 18?) + unsigned short nNodesAlloc; // the number of allocated nodes (at most nVars) + unsigned short nNodes; // the number of nodes + unsigned short Root; // the root of the tree unsigned * pMem; // memory for the truth tables (memory manager?) unsigned * pSupps; // supports of the nodes Kit_DsdObj_t** pNodes; // the nodes @@ -142,7 +142,7 @@ struct Kit_DsdMan_t_ Vec_Int_t * vNodes; // temporary array for BDD nodes }; -static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); } +static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 1) + ((nFans & 1) > 0); } static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; } static inline int Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; } static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; } @@ -538,6 +538,7 @@ extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ); extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ); extern Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk ); extern unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk ); +extern int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk ); extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] ); diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c index 3df16d8c..d026afbc 100644 --- a/src/bool/kit/kitDsd.c +++ b/src/bool/kit/kitDsd.c @@ -1485,7 +1485,7 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ) SeeAlso [] ***********************************************************************/ -void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, unsigned piLitsRes[] ) +void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] ) { int nSuppSizes[16], Priority[16], pOrder[16]; int i, k, iVarBest, SuppMax, PrioMax; @@ -1827,6 +1827,90 @@ int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size ) /**Function************************************************************* + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id ) +{ + Kit_DsdObj_t * pObj; + unsigned iLit, i, RetValue; + pObj = Kit_DsdNtkObj( pNtk, Id ); + if ( pObj == NULL ) + return 0; + if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR ) + return 0; + if ( pObj->nFans < 2 ) // why this happens? - need to figure out + return 0; + assert( pObj->nFans > 1 ); + if ( pObj->Type == KIT_DSD_AND ) + RetValue = ((int)pObj->nFans - 1); + else if ( pObj->Type == KIT_DSD_XOR ) + RetValue = ((int)pObj->nFans - 1) * 3; + else if ( pObj->Type == KIT_DSD_PRIME ) + { + // assuming MUX decomposition + assert( (int)pObj->nFans == 3 ); + RetValue = 3; + } + else assert( 0 ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk ) +{ + return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if there is a component with more than 3 inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk ) +{ + Kit_DsdObj_t * pObj; + int i, Counter = 0; + for ( i = 0; i < pNtk->nNodes; i++ ) + { + pObj = pNtk->pNodes[i]; + if ( pObj->Type == KIT_DSD_AND ) + Counter += ((int)pObj->nFans - 1); + else if ( pObj->Type == KIT_DSD_XOR ) + Counter += ((int)pObj->nFans - 1) * 3; + else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition + Counter += 3; + } + return Counter; +} + +/**Function************************************************************* + Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.] Description [] @@ -1883,7 +1967,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 ) SeeAlso [] ***********************************************************************/ -void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux ) +void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux ) { Kit_DsdObj_t * pRes, * pRes0, * pRes1; int nWords = Kit_TruthWordNum(pObj->nFans); |