diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 116 | ||||
-rw-r--r-- | src/base/abci/abc.zip | bin | 0 -> 62408 bytes | |||
-rw-r--r-- | src/base/abci/abcDar.c | 145 | ||||
-rw-r--r-- | src/base/cmd/cmd.c | 20 | ||||
-rw-r--r-- | src/base/cmd/cmd.h | 13 | ||||
-rw-r--r-- | src/base/io/io.c | 48 | ||||
-rw-r--r-- | src/base/main/mainUtils.c | 18 |
7 files changed, 310 insertions, 50 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4f46f3a2..50fb11ac 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -254,6 +254,7 @@ static int Abc_CommandAbc8Zero ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8DSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -518,6 +519,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*cec", Abc_CommandAbc8Cec, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*dsec", Abc_CommandAbc8DSec, 0 ); + Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); @@ -4919,22 +4921,24 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk;//, * pNtkRes; - int fComb; + int fSeq; int c; extern int Abc_NtkDemiter( Abc_Ntk_t * pNtk ); + extern int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fSeq = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { - case 'c': - fComb ^= 1; + case 's': + fSeq ^= 1; break; default: goto usage; @@ -4947,12 +4951,6 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( Abc_NtkPoNum(pNtk) != 1 ) - { - fprintf( pErr, "The network is not a miter.\n" ); - return 1; - } - if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) ) { fprintf( pErr, "The miter's PO is not an EXOR.\n" ); @@ -4960,19 +4958,35 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( !Abc_NtkDemiter( pNtk ) ) + if ( fSeq ) { - fprintf( pErr, "Demitering has failed.\n" ); - return 1; + if ( !Abc_NtkDarDemiter( pNtk ) ) + { + fprintf( pErr, "Demitering has failed.\n" ); + return 1; + } + } + else + { + if ( Abc_NtkPoNum(pNtk) != 1 ) + { + fprintf( pErr, "The network is not a single-output miter.\n" ); + return 1; + } + if ( !Abc_NtkDemiter( pNtk ) ) + { + fprintf( pErr, "Demitering has failed.\n" ); + return 1; + } } // replace the current network // Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: demiter [-h]\n" ); + fprintf( pErr, "usage: demiter [-sh]\n" ); fprintf( pErr, "\t removes topmost EXOR from the miter to create two POs\n" ); -// fprintf( pErr, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + fprintf( pErr, "\t-s : applied multi-output algorithm [default = %s]\n", fSeq? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -7720,7 +7734,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Aig_ProcedureTest(); extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ); - + extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7922,6 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ +/* pNtkRes = Abc_NtkDarTestNtk( pNtk ); if ( pNtkRes == NULL ) { @@ -7930,6 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ + + Abc_NtkDarTest( pNtk ); return 0; usage: @@ -13541,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvwh" ) ) != EOF ) { switch ( c ) { @@ -13640,6 +13658,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pPars->fVerbose ^= 1; break; + case 'w': + pPars->fFlopVerbose ^= 1; + break; case 'h': goto usage; default: @@ -13689,7 +13710,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvh]\n" ); + fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvwh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -13704,6 +13725,7 @@ usage: fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" ); fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -19634,6 +19656,64 @@ usage: } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbcTestNew( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_NtkTestProcedure( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); + + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( stdout, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash( pNtk) ) + { + fprintf( stdout, "The current network is not an AIG. Cannot continue.\n" ); + return 1; + } + +// Abc_NtkTestProcedure( pNtk, NULL ); + + return 0; + +usage: + fprintf( stdout, "usage: testnew [-h]\n" ); + fprintf( stdout, "\t new testing procedure\n" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.zip b/src/base/abci/abc.zip Binary files differnew file mode 100644 index 00000000..34df9a63 --- /dev/null +++ b/src/base/abci/abc.zip diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 98228c56..c64fb0f5 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1240,6 +1240,96 @@ PRT( "Initial fraiging time", clock() - clk ); /**Function************************************************************* + Synopsis [Print Latch Equivalence Classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig ) +{ + bool header_dumped = false; + int num_orig_latches = Abc_NtkLatchNum(pNtk); + char **pNames = ALLOC( char *, num_orig_latches ); + bool *p_irrelevant = ALLOC( bool, num_orig_latches ); + char * pFlopName, * pReprName; + Aig_Obj_t * pFlop, * pRepr; + Abc_Obj_t * pNtkFlop; + int repr_idx; + int i; + + Abc_NtkForEachLatch( pNtk, pNtkFlop, i ) + { + char *temp_name = Abc_ObjName( Abc_ObjFanout0(pNtkFlop) ); + pNames[i] = ALLOC( char , strlen(temp_name)+1); + strcpy(pNames[i], temp_name); + } + i = 0; + + Aig_ManSetPioNumbers( pAig ); + Saig_ManForEachLo( pAig, pFlop, i ) + { + p_irrelevant[i] = false; + + pFlopName = pNames[i]; + + pRepr = Aig_ObjRepr(pAig, pFlop); + + if ( pRepr == NULL ) + { + // printf("Nothing equivalent to flop %s\n", pFlopName); + p_irrelevant[i] = true; + continue; + } + + if (!header_dumped) + { + printf("Here are the flop equivalences:\n"); + header_dumped = true; + } + + // pRepr is representative of the equivalence class, to which pFlop belongs + if ( Aig_ObjIsConst1(pRepr) ) + { + printf( "Original flop %s is proved equivalent to constant.\n", pFlopName ); + // printf( "Original flop # %d is proved equivalent to constant.\n", i ); + continue; + } + + assert( Saig_ObjIsLo( pAig, pRepr ) ); + repr_idx = Aig_ObjPioNum(pRepr) - Saig_ManPiNum(pAig); + pReprName = pNames[repr_idx]; + printf( "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName ); + // printf( "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx ); + } + + header_dumped = false; + for (i=0; i<num_orig_latches; ++i) + { + if (p_irrelevant[i]) + { + if (!header_dumped) + { + printf("The following flops have been deemed irrelevant:\n"); + header_dumped = true; + } + printf("%s ", pNames[i]); + } + + FREE(pNames[i]); + } + if (header_dumped) + printf("\n"); + + FREE(pNames); + FREE(p_irrelevant); +} + +/**Function************************************************************* + Synopsis [Gives the current ABC network to AIG manager for processing.] Description [] @@ -1259,7 +1349,11 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars ) return NULL; pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars ); - Aig_ManStop( pTemp ); + + if ( pPars->fFlopVerbose ) + Abc_NtkPrintLatchEquivClasses(pNtk, pTemp); + + Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; @@ -1474,6 +1568,47 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ +int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk ) +{ + Aig_Man_t * pMan, * pPart0, * pPart1, * pMiter; + // derive the AIG manager + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + { + printf( "Converting network into AIG has failed.\n" ); + return 0; + } + if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) ) + { + printf( "Demitering has failed.\n" ); + return 0; + } + Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); + Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); + printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); + // create two-level miter + pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 ); + Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL ); + Aig_ManStop( pMiter ); + printf( "The new miter is written into file \"%s\".\n", "miter01.blif" ); + + Aig_ManStop( pPart0 ); + Aig_ManStop( pPart1 ); + Aig_ManStop( pMan ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) { Aig_Man_t * pMan; @@ -2457,9 +2592,9 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio ***********************************************************************/ void Abc_NtkDarTest( Abc_Ntk_t * pNtk ) { - extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); +// extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); - Aig_Man_t * pMan, * pTemp; + Aig_Man_t * pMan;//, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -2472,9 +2607,13 @@ Aig_ManStop( pMan ); pMan = Saig_ManReadBlif( "_temp_.blif" ); Aig_ManPrintStats( pMan ); */ +/* Aig_ManSetRegNum( pMan, pMan->nRegs ); pTemp = Ssw_SignalCorrespondeceTestPairs( pMan ); Aig_ManStop( pTemp ); +*/ + Ssw_SecSpecialMiter( pMan, 0 ); + Aig_ManStop( pMan ); } diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 75aa0064..4e0a4c95 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -50,6 +50,7 @@ static int CmdCommandEmpty ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandLs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandScrGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); #endif +static int CmdCommandVersion ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandSis ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -68,7 +69,7 @@ static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv ******************************************************************************/ void Cmd_Init( Abc_Frame_t * pAbc ) -{ +{ pAbc->tCommands = st_init_table(strcmp, st_strhash); pAbc->tAliases = st_init_table(strcmp, st_strhash); pAbc->tFlags = st_init_table(strcmp, st_strhash); @@ -91,6 +92,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "ls", CmdCommandLs, 0 ); Cmd_CommandAdd( pAbc, "Basic", "scrgen", CmdCommandScrGen, 0 ); #endif + Cmd_CommandAdd( pAbc, "Basic", "version", CmdCommandVersion, 0); Cmd_CommandAdd( pAbc, "Various", "sis", CmdCommandSis, 1); Cmd_CommandAdd( pAbc, "Various", "mvsis", CmdCommandMvsis, 1); @@ -1910,6 +1912,22 @@ usage: return 1; // error exit } +/**Function******************************************************************** + + Synopsis [Print the version string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int CmdCommandVersion( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + printf("%s\n", Abc_UtilsGetVersion(pAbc)); + return 0; +} //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cmd/cmd.h b/src/base/cmd/cmd.h index 030b77e8..9d0b8703 100644 --- a/src/base/cmd/cmd.h +++ b/src/base/cmd/cmd.h @@ -40,6 +40,17 @@ extern "C" { typedef struct MvCommand Abc_Command; // one command typedef struct MvAlias Abc_Alias; // one alias +#ifdef WIN32 +#define DLLEXPORT __declspec(dllexport) +#define DLLIMPORT __declspec(dllimport) +#else /* defined(WIN32) */ +#define DLLIMPORT +#endif /* defined(WIN32) */ + +#ifndef ABC_DLL +#define ABC_DLL DLLIMPORT +#endif + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -53,7 +64,7 @@ extern void Cmd_Init(); extern void Cmd_End(); /*=== cmdApi.c ========================================================*/ extern void Cmd_CommandAdd( Abc_Frame_t * pAbc, char * sGroup, char * sName, void * pFunc, int fChanges ); -extern int Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand ); +extern ABC_DLL int Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand ); /*=== cmdFlag.c ========================================================*/ extern char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag ); extern void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key ); diff --git a/src/base/io/io.c b/src/base/io/io.c index 6d7948ab..6f326a27 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1710,30 +1710,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) } // write the counter-example into the file - if ( pNtk->pModel ) - { - Abc_Obj_t * pObj; - FILE * pFile = fopen( pFileName, "w" ); - int i; - if ( pFile == NULL ) - { - fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName ); - return 1; - } - if ( fNames ) - { - Abc_NtkForEachPi( pNtk, pObj, i ) - fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); - } - else - { - Abc_NtkForEachPi( pNtk, pObj, i ) - fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) ); - } - fprintf( pFile, "\n" ); - fclose( pFile ); - } - else + if ( pNtk->pSeqModel ) { Fra_Cex_t * pCex = pNtk->pSeqModel; Abc_Obj_t * pObj; @@ -1771,6 +1748,29 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( pFile, "\n" ); fclose( pFile ); } + else + { + Abc_Obj_t * pObj; + FILE * pFile = fopen( pFileName, "w" ); + int i; + if ( pFile == NULL ) + { + fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName ); + return 1; + } + if ( fNames ) + { + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) ); + } + else + { + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) ); + } + fprintf( pFile, "\n" ); + fclose( pFile ); + } return 0; diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index d69055a4..46469490 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -200,14 +200,26 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc ) if ( sPath1 && sPath2 ) { /* ~/.rc == .rc : Source the file only once */ - (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc"); + char *tmp_cmd = ALLOC(char, strlen(sPath1)+12); + (void) sprintf(tmp_cmd, "source -s %s", sPath1); + // (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc"); + (void) Cmd_CommandExecute(pAbc, tmp_cmd); + FREE(tmp_cmd); } else { if (sPath1) { - (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc"); + char *tmp_cmd = ALLOC(char, strlen(sPath1)+12); + (void) sprintf(tmp_cmd, "source -s %s", sPath1); + // (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc"); + (void) Cmd_CommandExecute(pAbc, tmp_cmd); + FREE(tmp_cmd); } if (sPath2) { - (void) Cmd_CommandExecute(pAbc, "source -s .abc.rc"); + char *tmp_cmd = ALLOC(char, strlen(sPath2)+12); + (void) sprintf(tmp_cmd, "source -s %s", sPath2); + // (void) Cmd_CommandExecute(pAbc, "source -s .abc.rc"); + (void) Cmd_CommandExecute(pAbc, tmp_cmd); + FREE(tmp_cmd); } } if ( sPath1 ) FREE(sPath1); |