diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 88 | ||||
-rw-r--r-- | src/base/io/io.c | 33 | ||||
-rw-r--r-- | src/base/io/ioAbc.h | 2 | ||||
-rw-r--r-- | src/base/io/ioUtil.c | 2 | ||||
-rw-r--r-- | src/base/io/ioWriteAiger.c | 20 |
5 files changed, 132 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a4b5d566..8a95e252 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -278,6 +278,7 @@ static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDualRail ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBlockPo ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIso ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -690,6 +691,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dualrail", Abc_CommandDualRail, 1 ); Cmd_CommandAdd( pAbc, "Verification", "blockpo", Abc_CommandBlockPo, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "iso", Abc_CommandIso, 1 ); Cmd_CommandAdd( pAbc, "ABC9", "&get", Abc_CommandAbc9Get, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&put", Abc_CommandAbc9Put, 0 ); @@ -8839,17 +8841,26 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkSuppSizeTest( Abc_Ntk_t * p ); extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ); extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); if ( pNtk ) { Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Aig_Man_t * pRes; - Abc_Ntk_t * pNtkRes; +// Abc_Ntk_t * pNtkRes; // Aig_ManInterRepar( pAig, 1 ); // Aig_ManInterTest( pAig, 1 ); // Aig_ManSupportsTest( pAig ); // Aig_SupportSizeTest( pAig ); + if ( !fNewAlgo ) + Saig_IsoDetectFast( pAig ); + else + { + pRes = Iso_ManTest( pAig, fVerbose ); + Aig_ManStopP( &pRes ); + } + +/* pRes = Iso_ManTest( pAig, fVerbose ); - Aig_ManStop( pAig ); if ( pRes != NULL ) { pNtkRes = Abc_NtkFromAigPhase( pRes ); @@ -8859,6 +8870,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) pNtkRes->pName = Extra_UtilStrsav(pNtk->pName); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } +*/ + Aig_ManStop( pAig ); } } @@ -21300,6 +21313,77 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + Abc_Ntk_t * pNtk, * pNtkNew = NULL; + Aig_Man_t * pAig, * pTemp; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + // check the main AIG + pNtk = Abc_FrameReadNtk(pAbc); + if ( pNtk == NULL ) + { + Abc_Print( 1, "Main AIG: There is no current network.\n"); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( 1, "Main AIG: The current network is not an AIG.\n"); + return 0; + } + if ( Abc_NtkPoNum(pNtk) == 1 ) + { + Abc_Print( 1, "Current AIG has only one PO. Transformation is not performed.\n"); + return 0; + } + + // transform + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + pTemp = Saig_ManIsoReduce( pAig, fVerbose ); + pNtkNew = Abc_NtkFromAigPhase( pTemp ); + Aig_ManStop( pTemp ); + Aig_ManStop( pAig ); + + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); + return 0; + +usage: + Abc_Print( -2, "usage: iso [-vh]\n" ); + Abc_Print( -2, "\t removes POs with isomorphic sequential COI\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); diff --git a/src/base/io/io.c b/src/base/io/io.c index 92dbe9fc..550ff7dd 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1382,12 +1382,16 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) char * pFileName; int fWriteSymbols; int fCompact; + int fUnique; + int fVerbose; int c; - fCompact = 1; fWriteSymbols = 0; + fCompact = 1; + fUnique = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "scuvh" ) ) != EOF ) { switch ( c ) { @@ -1397,6 +1401,12 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) case 'c': fCompact ^= 1; break; + case 'u': + fUnique ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -1418,14 +1428,29 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" ); return 1; } - Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact ); + if ( fUnique ) + { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); + Aig_Man_t * pCan = Saig_ManDupIsoCanonical( pAig, fVerbose ); + Abc_Ntk_t * pTemp = Abc_NtkFromAigPhase( pCan ); + Aig_ManStop( pCan ); + Aig_ManStop( pAig ); + Io_WriteAiger( pTemp, pFileName, fWriteSymbols, fCompact, fUnique ); + Abc_NtkDelete( pTemp ); + } + else + Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact, fUnique ); return 0; usage: - fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" ); + fprintf( pAbc->Err, "usage: write_aiger [-scuvh] <file>\n" ); fprintf( pAbc->Err, "\t writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" ); fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" ); fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" ); + fprintf( pAbc->Err, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" ); + fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" ); return 1; diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h index 7a38ae5c..14d688f0 100644 --- a/src/base/io/ioAbc.h +++ b/src/base/io/ioAbc.h @@ -96,7 +96,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck ) /*=== abcReadVerilog.c ========================================================*/ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcWriteAiger.c =========================================================*/ -extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ); +extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique ); extern void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName ); /*=== abcWriteBaf.c ===========================================================*/ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index e8a018c2..dbaa9138 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -320,7 +320,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) return; } if ( FileType == IO_FILE_AIGER ) - Io_WriteAiger( pNtk, pFileName, 1, 0 ); + Io_WriteAiger( pNtk, pFileName, 1, 0, 0 ); else //if ( FileType == IO_FILE_BAF ) Io_WriteBaf( pNtk, pFileName ); return; diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 0f725be3..93b17c37 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -581,7 +581,7 @@ int fprintfBz2Aig( bz2file * b, char * fmt, ... ) { SeeAlso [] ***********************************************************************/ -void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ) +void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique ) { ProgressBar * pProgress; // FILE * pFile; @@ -591,6 +591,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f unsigned uLit0, uLit1, uLit; bz2file b; + // define unique writing + if ( fUnique ) + { + fWriteSymbols = 0; + fCompact = 0; + } + // check that the network is valid assert( Abc_NtkIsStrash(pNtk) ); Abc_NtkForEachLatch( pNtk, pObj, i ) @@ -750,10 +757,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f // write the comment fprintfBz2Aig( &b, "c" ); - if ( pNtk->pName && strlen(pNtk->pName) > 0 ) - fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' ); - fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() ); - fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); + if ( !fUnique ) + { + if ( pNtk->pName && strlen(pNtk->pName) > 0 ) + fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' ); + fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() ); + fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); + } // close the file if (b.b) { |