From 7926d75ecb4ffd4441bea0c2d731e5b533534ee3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 Mar 2012 00:57:48 -0800 Subject: Adding features related to the communication bridge. --- src/base/abci/abc.c | 9 ++- src/base/main/main.c | 14 +++- src/base/main/main.h | 2 + src/base/main/mainFrame.c | 3 + src/base/main/mainInt.h | 1 + src/base/main/mainUtils.c | 3 +- src/misc/util/abc_global.h | 16 ++-- src/misc/util/utilBridge.c | 189 ++++++++++++++++++++++++--------------------- 8 files changed, 136 insertions(+), 101 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c8090460..c4d5df4c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -379,6 +379,12 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, ***********************************************************************/ void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex ) { + // update bridge + if ( Abc_FrameIsBridgeMode() ) + { + extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex ); + Gia_ManToBridgeResult( stdout, pAbc->Status, *ppCex ); + } // update CEX ABC_FREE( pAbc->pCex ); pAbc->pCex = *ppCex; @@ -23473,8 +23479,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) // else // pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; - if ( pAbc->pGia->pCexSeq ) - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: diff --git a/src/base/main/main.c b/src/base/main/main.c index 0e2ff9f4..1572af91 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -35,7 +35,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - + static int TypeCheck( Abc_Frame_t * pAbc, const char * s); //////////////////////////////////////////////////////////////////////// @@ -111,7 +111,7 @@ int Abc_RealMain( int argc, char * argv[] ) sprintf( sWriteCmd, "write" ); Extra_UtilGetoptReset(); - while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) { + while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:xb")) != EOF) { switch(c) { case 'c': strcpy( sCommandUsr, globalUtilOptarg ); @@ -177,10 +177,20 @@ int Abc_RealMain( int argc, char * argv[] ) fBatch = 1; break; + case 'b': + Abc_FrameSetBridgeMode(); + break; + default: goto usage; } } + + if ( Abc_FrameIsBridgeMode() ) + { + extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit ); + pAbc->pGia = Gia_ManFromBridge( stdin, NULL ); + } if ( fBatch ) { diff --git a/src/base/main/main.h b/src/base/main/main.h index ac30f358..5d777b23 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -104,6 +104,8 @@ extern ABC_DLL void * Abc_FrameReadManDd(); extern ABC_DLL void * Abc_FrameReadManDec(); extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag ); extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag ); +extern ABC_DLL int Abc_FrameIsBridgeMode(); +extern ABC_DLL void Abc_FrameSetBridgeMode(); extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 6a63cdd6..fe9aff6a 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -78,6 +78,9 @@ void Abc_FrameSetLibVer( void * pLib ) { s_GlobalFrame->pL void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); } void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; } +int Abc_FrameIsBridgeMode() { return s_GlobalFrame->fBridgeMode; } +void Abc_FrameSetBridgeMode() { s_GlobalFrame->fBridgeMode = 0; } + /**Function************************************************************* Synopsis [Returns 1 if the flag is enabled without value or with value 1.] diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 2eca004e..d8a6c93e 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -70,6 +70,7 @@ struct Abc_Frame_t_ int nSteps; // the counter of different network processed int fAutoexac; // marks the autoexec mode int fBatchMode; // are we invoked in batch mode? + int fBridgeMode; // are we invoked in bridge mode? // output streams FILE * Out; FILE * Err; diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index e263bc94..5b6dc893 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -120,7 +120,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName ) { fprintf( pAbc->Err, "\n" ); fprintf( pAbc->Err, - "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [file]\n", + "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [-b] [file]\n", ProgName); fprintf( pAbc->Err, " -c cmd\texecute commands `cmd'\n"); fprintf( pAbc->Err, " -F script\texecute commands from a script file and echo commands\n"); @@ -131,6 +131,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName ) fprintf( pAbc->Err, " -t type\tspecify input type (blif_mv (default), blif_mvs, blif, or none)\n"); fprintf( pAbc->Err, " -T type\tspecify output type (blif_mv (default), blif_mvs, blif, or none)\n"); fprintf( pAbc->Err, " -x\t\tequivalent to '-t none -T none'\n"); + fprintf( pAbc->Err, " -b\t\trunning in bridge mode\n"); fprintf( pAbc->Err, "\n" ); } diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 9a5ee9de..318bc912 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -256,23 +256,19 @@ enum Abc_VerbLevel ABC_VERBOSE = 2 }; -extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer ); - -// string printing -extern char * vnsprintf(const char* format, va_list args); -extern char * nsprintf(const char* format, ...); - static inline void Abc_Print( int level, const char * format, ... ) { - extern int in_bridge_mode; + extern ABC_DLL int Abc_FrameIsBridgeMode(); va_list args; if ( level == ABC_ERROR ) printf( "Error: " ); else if ( level == ABC_WARNING ) printf( "Warning: " ); va_start( args, format ); - if ( in_bridge_mode ) + if ( Abc_FrameIsBridgeMode() ) { + extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer ); + extern char * vnsprintf(const char* format, va_list args); unsigned char * tmp = vnsprintf( format, args ); Gia_ManToBridgeText( stdout, strlen(tmp), tmp ); free( tmp ); @@ -345,6 +341,10 @@ extern void Abc_QuickSort3( word * pData, int nSize, int fDecrease ); extern void Abc_QuickSortCostData( int * pCosts, int nSize, int fDecrease, word * pData, int * pResult ); extern int * Abc_QuickSortCost( int * pCosts, int nSize, int fDecrease ); +// string printing +extern char * vnsprintf(const char* format, va_list args); +extern char * nsprintf(const char* format, ...); + ABC_NAMESPACE_HEADER_END diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c index 07760393..9de38a63 100644 --- a/src/misc/util/utilBridge.c +++ b/src/misc/util/utilBridge.c @@ -23,9 +23,7 @@ #include #include -#include "abc_global.h" #include "src/aig/gia/gia.h" -#include "src/misc/vec/vec.h" ABC_NAMESPACE_IMPL_START @@ -33,14 +31,20 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define BRIDGE_TEXT_MESSAGE 999996 +#define BRIDGE_RESULTS 101 +#define BRIDGE_ABS_NETLIST 107 +#define BRIDGE_BAD_ABS 105 + +#define BRIDGE_VALUE_X 0 +#define BRIDGE_VALUE_0 2 +#define BRIDGE_VALUE_1 3 + extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos ); extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); -// this variable determines where the output goes -int in_bridge_mode = 0; - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -58,63 +62,52 @@ int in_bridge_mode = 0; ***********************************************************************/ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p ) { - Vec_Str_t * vBuffer; + Vec_Str_t * vStr; Gia_Obj_t * pObj; - int nNodes = 0, i, uLit, uLit0, uLit1; - // set the node numbers to be used in the output file - Gia_ManConst0(p)->Value = nNodes++; + int i, uLit0, uLit1, nNodes; + assert( Gia_ManPoNum(p) > 0 ); + + // start with const1 node (number 1) + nNodes = 1; + // assign literals(!!!) to the value field + Gia_ManConst0(p)->Value = Abc_Var2Lit( nNodes++, 1 ); Gia_ManForEachCi( p, pObj, i ) - pObj->Value = nNodes++; + pObj->Value = Abc_Var2Lit( nNodes++, 0 ); Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = nNodes++; - - // write the header "M I L O A" where M = I + L + A - vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) ); - Vec_StrPrintStr( vBuffer, "aig " ); - Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) ); - Vec_StrPrintStr( vBuffer, " " ); - Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) ); - Vec_StrPrintStr( vBuffer, "\n" ); + pObj->Value = Abc_Var2Lit( nNodes++, 0 ); + + // write header + vStr = Vec_StrAlloc( 1000 ); + Gia_WriteAigerEncodeStr( vStr, Gia_ManPiNum(p) ); + Gia_WriteAigerEncodeStr( vStr, Gia_ManRegNum(p) ); + Gia_WriteAigerEncodeStr( vStr, Gia_ManAndNum(p) ); + + // write the nodes + Gia_ManForEachAnd( p, pObj, i ) + { + uLit0 = Gia_ObjFanin0Copy( pObj ); + uLit1 = Gia_ObjFanin1Copy( pObj ); + assert( uLit0 != uLit1 ); + Gia_WriteAigerEncodeStr( vStr, uLit0 << 1 ); + Gia_WriteAigerEncodeStr( vStr, uLit1 ); + } // write latch drivers Gia_ManForEachRi( p, pObj, i ) { - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); + uLit0 = Gia_ObjFanin0Copy( pObj ); + Gia_WriteAigerEncodeStr( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 ); } // write PO drivers + Gia_WriteAigerEncodeStr( vStr, Gia_ManPoNum(p) ); Gia_ManForEachPo( p, pObj, i ) { - uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - Vec_StrPrintNum( vBuffer, uLit ); - Vec_StrPrintStr( vBuffer, "\n" ); - } - // write the nodes into the buffer - Gia_ManForEachAnd( p, pObj, i ) - { - uLit = Abc_Var2Lit( Gia_ObjValue(pObj), 0 ); - uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); - uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) ); - assert( uLit0 != uLit1 ); - if ( uLit0 > uLit1 ) - { - int Temp = uLit0; - uLit0 = uLit1; - uLit1 = Temp; - } - Gia_WriteAigerEncodeStr( vBuffer, uLit - uLit1 ); - Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 ); + uLit0 = Gia_ObjFanin0Copy( pObj ); + // complement property output!!! + Gia_WriteAigerEncodeStr( vStr, Abc_LitNot(uLit0) ); } - Vec_StrPrintStr( vBuffer, "c" ); - return vBuffer; + return vStr; } /**Function************************************************************* @@ -130,33 +123,17 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p ) ***********************************************************************/ void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer ) { + int RetValue; fprintf( pFile, "%.6d", Type ); fprintf( pFile, " " ); fprintf( pFile, "%.16d", Size ); fprintf( pFile, " " ); - fwrite( pBuffer, Size, 1, pFile ); + RetValue = fwrite( pBuffer, Size, 1, pFile ); + assert( RetValue == 1 ); fflush( pFile ); } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - -#define BRIDGE_TEXT_MESSAGE 999996 -#define BRIDGE_RESULTS 101 -#define BRIDGE_ABS_NETLIST 107 -#define BRIDGE_BAD_ABS 105 - /**Function************************************************************* Synopsis [] @@ -187,24 +164,35 @@ int Gia_ManToBridgeBadAbs( FILE * pFile ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManFromBridgeHolds( FILE * pFile ) { - fputc( (char)3, pFile ); // true + fputc( (char)BRIDGE_VALUE_1, pFile ); // true fputc( (char)1, pFile ); // size of vector (Armin's encoding) fputc( (char)0, pFile ); // number of the property (Armin's encoding) fputc( (char)0, pFile ); // no invariant } void Gia_ManFromBridgeUnknown( FILE * pFile ) { - fputc( (char)0, pFile ); // undef + fputc( (char)BRIDGE_VALUE_X, pFile ); // undef fputc( (char)1, pFile ); // size of vector (Armin's encoding) fputc( (char)0, pFile ); // number of the property (Armin's encoding) } void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex ) { - int i, f, iBit; + int i, f, iBit, RetValue; Vec_Str_t * vStr = Vec_StrAlloc( 1000 ); - Vec_StrPush( vStr, (char)2 ); // false + Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding) Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) @@ -215,14 +203,15 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex ) for ( f = 0; f <= pCex->iFrame; f++ ) { Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs - for ( i = 0; i < pCex->nPis; i++ ) - Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit++)?3:2) ); // value + for ( i = 0; i < pCex->nPis; i++, iBit++ ) + Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value } assert( iBit == pCex->nBits ); Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example) for ( i = 0; i < pCex->nRegs; i++ ) - Vec_StrPush( vStr, (char)2 ); // always zero ?????????????? - fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); + Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!! + RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); + assert( RetValue == 1 ); Vec_StrFree( vStr ); } int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex ) @@ -238,7 +227,6 @@ int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex ) } - /**Function************************************************************* Synopsis [] @@ -264,11 +252,11 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I nGates = Gia_ReadAigerDecode( &pBuffer ); vLits = Vec_IntAlloc( 1000 ); - Vec_IntPush( vLits, -1 ); + Vec_IntPush( vLits, -999 ); Vec_IntPush( vLits, 1 ); // start the AIG package - p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); + p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); // PI+FO+FI+AND+PO+1 p->pName = Abc_UtilStrsav( "temp" ); // create PIs @@ -286,11 +274,10 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I { iFan0 = Gia_ReadAigerDecode( &pBuffer ); iFan1 = Gia_ReadAigerDecode( &pBuffer ); - assert( (iFan0 & 1)==0 ); + assert( !(iFan0 & 1) ); iFan0 >>= 1; - iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); - iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan0 & 1 ); + iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan1 & 1 ); if ( fHash ) Vec_IntPush( vLits, Gia_ManHashAnd(p, iFan0, iFan1) ); else @@ -302,7 +289,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I // remember where flops begin pBufferPivot = pBuffer; - // stroll through flops + // scroll through flops for ( i = 0; i < nFlops; i++ ) Gia_ReadAigerDecode( &pBuffer ); @@ -312,8 +299,9 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I for ( i = 0; i < nProps; i++ ) { iFan0 = Gia_ReadAigerDecode( &pBuffer ); - iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); - Gia_ManAppendCo( p, iFan0 ); + iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); + // complement property output!!! + Gia_ManAppendCo( p, Abc_LitNot(iFan0) ); } // make sure the end of buffer is reached assert( pBufferEnd == pBuffer ); @@ -324,7 +312,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I for ( i = 0; i < nFlops; i++ ) { iFan0 = Gia_ReadAigerDecode( &pBuffer ); - assert( (iFan0 & 3) == 2 ); + assert( (iFan0 & 3) == BRIDGE_VALUE_0 ); Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true iFan0 >>= 2; iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); @@ -349,6 +337,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I return p; } + /**Function************************************************************* Synopsis [] @@ -430,10 +419,32 @@ Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit ) { extern void Gia_ManFromBridgeTest( char * pFileName ); Gia_ManFromBridgeTest( "C:\\_projects\\abc\\_TEST\\bug\\65\\par.dump" ); - } */ +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManToBridgeAbsNetlistTest( char * pFileName, Gia_Man_t * p ) +{ + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + return; + } + Gia_ManToBridgeAbsNetlist( pFile, p ); + fclose ( pFile ); +} + /**Function************************************************************* Synopsis [] @@ -459,7 +470,9 @@ void Gia_ManFromBridgeTest( char * pFileName ) fclose ( pFile ); Gia_ManPrintStats( p, 0, 0 ); -// Gia_WriteAiger( p, "temp.aig", 0, 0 ); + Gia_WriteAiger( p, "temp.aig", 0, 0 ); + + Gia_ManToBridgeAbsNetlistTest( "par_.dump", p ); Gia_ManStop( p ); } -- cgit v1.2.3