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 ++- 6 files changed, 27 insertions(+), 5 deletions(-) (limited to 'src/base') 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" ); } -- cgit v1.2.3