From 200c5cc65951dc48377c6932486e6532944d7e39 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 9 Dec 2011 00:37:05 -0800 Subject: Added support for generating a library of real-life truth-tables. --- src/aig/kit/kit.h | 1 + src/aig/kit/kitDsd.c | 102 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcRec.c | 50 +++++++++++++++++++++-- src/base/io/io.c | 2 + src/base/main/mainUtils.c | 4 +- 5 files changed, 153 insertions(+), 6 deletions(-) diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index 20da1b35..9e15e994 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -539,6 +539,7 @@ extern void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk ); extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ); extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); +extern void Kit_DsdPrintFromTruth2( FILE * pFile, unsigned * pTruth, int nVars ); extern void Kit_DsdWriteFromTruth( char * pBuffer, unsigned * pTruth, int nVars ); extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ); extern Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars ); diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index c8665c2f..413597a1 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -223,6 +223,86 @@ char * Kit_DsdWriteHex( char * pBuff, unsigned * pTruth, int nFans ) return pBuff; } +/**Function************************************************************* + + Synopsis [Recursively print the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdPrint2_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id ) +{ + Kit_DsdObj_t * pObj; + unsigned iLit, i; + char Symbol; + + pObj = Kit_DsdNtkObj( pNtk, Id ); + if ( pObj == NULL ) + { + assert( Id < pNtk->nVars ); + fprintf( pFile, "%c", 'a' + Id ); + return; + } + + if ( pObj->Type == KIT_DSD_CONST1 ) + { + assert( pObj->nFans == 0 ); + fprintf( pFile, "Const1" ); + return; + } + + if ( pObj->Type == KIT_DSD_VAR ) + assert( pObj->nFans == 1 ); + + if ( pObj->Type == KIT_DSD_AND ) + Symbol = '*'; + else if ( pObj->Type == KIT_DSD_XOR ) + Symbol = '+'; + else + Symbol = ','; + + if ( pObj->Type == KIT_DSD_PRIME ) + fprintf( pFile, "[" ); + else + fprintf( pFile, "(" ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + if ( Kit_DsdLitIsCompl(iLit) ) + fprintf( pFile, "!" ); + Kit_DsdPrint2_rec( pFile, pNtk, Kit_DsdLit2Var(iLit) ); + if ( i < pObj->nFans - 1 ) + fprintf( pFile, "%c", Symbol ); + } + if ( pObj->Type == KIT_DSD_PRIME ) + fprintf( pFile, "]" ); + else + fprintf( pFile, ")" ); +} + +/**Function************************************************************* + + Synopsis [Print the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdPrint2( FILE * pFile, Kit_DsdNtk_t * pNtk ) +{ +// fprintf( pFile, "F = " ); + if ( Kit_DsdLitIsCompl(pNtk->Root) ) + fprintf( pFile, "!" ); + Kit_DsdPrint2_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) ); +// fprintf( pFile, "\n" ); +} + /**Function************************************************************* Synopsis [Recursively print the DSD formula.] @@ -420,6 +500,28 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ) Kit_DsdNtkFree( pTemp ); } +/**Function************************************************************* + + Synopsis [Print the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdPrintFromTruth2( FILE * pFile, unsigned * pTruth, int nVars ) +{ + Kit_DsdNtk_t * pTemp, * pTemp2; + pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 0 ); + pTemp2 = Kit_DsdExpand( pTemp ); + Kit_DsdPrint2( pFile, pTemp2 ); + Kit_DsdVerify( pTemp2, pTruth, nVars ); + Kit_DsdNtkFree( pTemp2 ); + Kit_DsdNtkFree( pTemp ); +} + /**Function************************************************************* Synopsis [Print the DSD formula.] diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c index bf83dbb4..a9255ce6 100644 --- a/src/base/abci/abcRec.c +++ b/src/base/abci/abcRec.c @@ -200,12 +200,16 @@ void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts ) p->vTtElems->nSize = p->nVars; p->vTtElems->nCap = p->nVars; p->vTtElems->pArray = (void **)Extra_TruthElementary( p->nVars ); - +/* // allocate room for node truth tables if ( Abc_NtkObjNum(pNtk) > (1<<14) ) p->vTtNodes = Vec_PtrAllocSimInfo( 2 * Abc_NtkObjNum(pNtk), p->nWords ); else p->vTtNodes = Vec_PtrAllocSimInfo( 1<<14, p->nWords ); +*/ + p->vTtNodes = Vec_PtrAlloc( 1000 ); + for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ ) + Vec_PtrPush( p->vTtNodes, ABC_ALLOC(unsigned, p->nWords) ); // create hash table p->nBins = 50011; @@ -267,6 +271,38 @@ p->timeTruth += clock() - clk; p->timeTotal += clock() - clkTotal; } +/**Function************************************************************* + + Synopsis [Dump truth tables into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRecDumpTruthTables( Abc_ManRec_t * p ) +{ + FILE * pFile; + Abc_Obj_t * pObj; + unsigned * pTruth; + int i; + pFile = fopen( "tt16.txt", "wb" ); + for ( i = 0; i < p->nBins; i++ ) + for ( pObj = p->pBins[i]; pObj; pObj = pObj->pCopy ) + { + pTruth = Vec_PtrEntry(p->vTtNodes, pObj->Id); + if ( Kit_TruthSupport(pTruth, 16) != (1<<16)-1 ) + continue; + Extra_PrintHex( pFile, pTruth, 16 ); + fprintf( pFile, " " ); + Kit_DsdPrintFromTruth2( pFile, pTruth, 16 ); + fprintf( pFile, "\n" ); + } + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Returns the given record.] @@ -281,9 +317,12 @@ p->timeTotal += clock() - clkTotal; void Abc_NtkRecStop() { assert( s_pMan != NULL ); + Abc_NtkRecDumpTruthTables( s_pMan ); + if ( s_pMan->pNtk ) Abc_NtkDelete( s_pMan->pNtk ); - Vec_PtrFree( s_pMan->vTtNodes ); +// Vec_PtrFree( s_pMan->vTtNodes ); + Vec_PtrFreeFree( s_pMan->vTtNodes ); Vec_PtrFree( s_pMan->vTtElems ); ABC_FREE( s_pMan->pBins ); @@ -878,8 +917,11 @@ s_pMan->timeCanon += clock() - clk; if ( pObj->Id == nNodes ) { // increase storage for truth tables - if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id ) - Vec_PtrDoubleSimInfo(s_pMan->vTtNodes); +// if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id ) +// Vec_PtrDoubleSimInfo(s_pMan->vTtNodes); + while ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id ) + Vec_PtrPush( s_pMan->vTtNodes, ABC_ALLOC(unsigned, s_pMan->nWords) ); + // compute the truth table RetValue = Abc_NtkRecComputeTruth( pObj, s_pMan->vTtNodes, nInputs ); if ( RetValue == 0 ) diff --git a/src/base/io/io.c b/src/base/io/io.c index 3d1a6ae3..37e7d34f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -929,6 +929,8 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } + c = strlen(argv[globalUtilOptind]); + // convert truth table to SOP if ( fHex ) pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]); diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index dadcbdd1..c849a53d 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -70,7 +70,7 @@ char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc ) ***********************************************************************/ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc ) { - static char Prompt[1000]; + static char Prompt[5000]; #ifndef _WIN32 static char * line = NULL; #endif @@ -78,7 +78,7 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc ) sprintf( Prompt, "abc %02d> ", pAbc->nSteps ); #ifdef _WIN32 fprintf( pAbc->Out, "%s", Prompt ); - fgets( Prompt, 999, stdin ); + fgets( Prompt, 5000, stdin ); return Prompt; #else if (line != NULL) ABC_FREE(line); -- cgit v1.2.3