diff options
Diffstat (limited to 'src/misc/util/utilBridge.c')
| -rw-r--r-- | src/misc/util/utilBridge.c | 189 |
1 files changed, 101 insertions, 88 deletions
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 <stdlib.h> #include <assert.h> -#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,11 +123,13 @@ 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 ); } @@ -150,24 +145,6 @@ void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer SeeAlso [] ***********************************************************************/ - - -#define BRIDGE_TEXT_MESSAGE 999996 -#define BRIDGE_RESULTS 101 -#define BRIDGE_ABS_NETLIST 107 -#define BRIDGE_BAD_ABS 105 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer ) { Gia_CreateHeader( pFile, BRIDGE_TEXT_MESSAGE, Size, pBuffer ); @@ -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,7 +419,6 @@ 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" ); - } */ @@ -445,6 +433,29 @@ Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit ) 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManFromBridgeTest( char * pFileName ) { Gia_Man_t * p; @@ -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 ); } |