Version abc81004

3 files changed, 240 insertions, 21 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
new 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 );
 }