From eb75697fe00a8668f74b3c710dcbf5658e07d167 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 4 Oct 2008 08:01:00 -0700 Subject: Version abc81004 --- src/base/abci/abc.c | 116 +++++++++++++++++++++++++++++++++------ src/base/abci/abc.zip | Bin 0 -> 62408 bytes src/base/abci/abcDar.c | 145 ++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 240 insertions(+), 21 deletions(-) create mode 100644 src/base/abci/abc.zip (limited to 'src/base/abci') 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 ] [-plsfuvh]\n" ); + fprintf( pErr, "usage: scorr [-PQFCLNS ] [-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 new file mode 100644 index 00000000..34df9a63 Binary files /dev/null and b/src/base/abci/abc.zip differ 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 @@ -1238,6 +1238,96 @@ PRT( "Initial fraiging time", clock() - clk ); return pNtkAig; } +/**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; ifFlopVerbose ) + Abc_NtkPrintLatchEquivClasses(pNtk, pTemp); + + Aig_ManStop( pTemp ); if ( pMan == NULL ) return NULL; @@ -1463,6 +1557,47 @@ PRT( "Time", clock() - clk ); return 1; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + 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.] @@ -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 ); } -- cgit v1.2.3