Adding command &miter2 to derive a specified sequential miter.

5 files changed, 96 insertions, 42 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fead1c8b..23afc45e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -853,7 +853,7 @@ extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fVerbose );
-extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit );
+extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index c861f23b..74867eff 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1827,12 +1827,12 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit )
+Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int CountPis = Gia_ManPiNum(p), * pPiLits;
-    int i, iResetFlop = -1;
+    int i, iResetFlop = -1, Count1 = 0;
     // map X-valued flops into new PIs
     assert( (int)strlen(pInit) == Gia_ManRegNum(p) );
     pPiLits = ABC_FALLOC( int, Gia_ManRegNum(p) );
@@ -1860,7 +1860,7 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit )
     Gia_ManForEachRo( p, pObj, i )
     {
         if ( pInit[i] == '1' )
-            pObj->Value = Abc_LitNot(pObj->Value);
+            pObj->Value = Abc_LitNot(pObj->Value), Count1++;
         else if ( pInit[i] == 'x' || pInit[i] == 'X' )
             pObj->Value = Gia_ManAppendMux( pNew, iResetFlop, pObj->Value, Gia_Obj2Lit(pNew, Gia_ManPi(pNew, pPiLits[i])) );
         else if ( pInit[i] != '0' )
@@ -1883,6 +1883,8 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit )
     if ( CountPis > Gia_ManPiNum(p) )
         Gia_ManAppendCo( pNew, 1 );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) + (int)(CountPis > Gia_ManPiNum(p)) );
+    if ( fVerbose )
+        printf( "Converted %d 1-valued FFs and %d DC-valued FFs.\n", Count1, CountPis-Gia_ManPiNum(p) );
     return pNew;
 }
 
@@ -1899,21 +1901,21 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit )
 ***********************************************************************/
 Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
 {
-    Vec_Int_t * vCoValues0, * vCoValues1;
+    Vec_Int_t * vCiValues, * vCoValues0, * vCoValues1;
     Gia_Man_t * pNew, * pUndc, * pTemp;
     Gia_Obj_t * pObj;
     char * pInitNew;
     int i, k;
+    // check PI values
+    for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
+        assert( pInit[i] == 'x' || pInit[i] == 'X' );
     // normalize the manager
-    pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManRegNum(pStart) );
+    pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), fVerbose );
     // create new init string
-    pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc) );
-    for ( i = 0; i < Gia_ManPiNum(pUndc); i++ )
-    {
-        assert( pInit[i] == 'x' || pInit[i] == 'X' );
+    pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
+    for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
         pInitNew[i] = pInit[i];
-    }
-    for ( i = k = Gia_ManPiNum(pUndc); i < Gia_ManCiNum(pUndc); i++ )
+    for ( i = k = Gia_ManPiNum(pStart); i < Gia_ManCiNum(pStart); i++ )
         if ( pInit[i] == 'x' || pInit[i] == 'X' )
             pInitNew[k++] = pInit[i];
     pInitNew[k] = 0;
@@ -1924,9 +1926,18 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
     pNew->pSpec = Abc_UtilStrsav( pUndc->pSpec );
     Gia_ManConst0(pUndc)->Value = 0;
     Gia_ManHashAlloc( pNew );
-    // build one side
+    // add PIs of the first side
     Gia_ManForEachPi( pUndc, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
+    // add PIs of the second side
+    vCiValues = Vec_IntAlloc( Gia_ManPiNum(pUndc) );
+    Gia_ManForEachPi( pUndc, pObj, i )
+        if ( pInitNew[i] == 'x' )
+            Vec_IntPush( vCiValues, Gia_Obj2Lit( pNew, Gia_ManPi(pNew, i) ) );
+        else if ( pInitNew[i] == 'X' ) 
+            Vec_IntPush( vCiValues, Gia_ManAppendCi( pNew ) );
+        else assert( 0 );
+    // build flops and internal nodes
     Gia_ManForEachRo( pUndc, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( pUndc, pObj, i )
@@ -1937,10 +1948,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
         Vec_IntPush( vCoValues0, Gia_ObjFanin0Copy(pObj) );
     // build the other side
     Gia_ManForEachPi( pUndc, pObj, i )
-        if ( pInitNew[i] == 'x' )
-            pObj->Value = Gia_Obj2Lit( pNew, Gia_ManPi(pNew, i) );
-        else
-            pObj->Value = Gia_ManAppendCi( pNew );
+        pObj->Value = Vec_IntEntry( vCiValues, i );
     Gia_ManForEachRo( pUndc, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( pUndc, pObj, i )
@@ -1954,15 +1962,17 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashXor( pNew, Vec_IntEntry(vCoValues0, i), Vec_IntEntry(vCoValues1, i) ) );
     // create flop inputs
     Gia_ManForEachRi( pUndc, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues0, Gia_ManPiNum(pUndc)+i) );
+        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues0, Gia_ManPoNum(pUndc)+i) );
     Gia_ManForEachRi( pUndc, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues1, Gia_ManPiNum(pUndc)+i) );
+        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues1, Gia_ManPoNum(pUndc)+i) );
     Vec_IntFree( vCoValues0 );
     Vec_IntFree( vCoValues1 );
+    Vec_IntFree( vCiValues );
     ABC_FREE( pInitNew );
     // cleanup
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, 2*Gia_ManRegNum(pUndc) );
+    Gia_ManStop( pUndc );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     return pNew;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e5b57ec8..fe8a116d 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -639,6 +639,7 @@ extern ABC_DLL int                Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern ABC_DLL int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+extern ABC_DLL char *             Abc_NtkCollectLatchValuesStr( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
 extern ABC_DLL Abc_Obj_t *        Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
 extern ABC_DLL void               Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 61cae164..c6e9b9d5 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -197,6 +197,38 @@ Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives latch init string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_NtkCollectLatchValuesStr( Abc_Ntk_t * pNtk )
+{
+    char * pInits;
+    Abc_Obj_t * pLatch;
+    int i;
+    pInits = ABC_ALLOC( char, Abc_NtkLatchNum(pNtk) + 1 );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_LatchIsInit0(pLatch) )
+            pInits[i] = '0';
+        else if ( Abc_LatchIsInit1(pLatch) )
+            pInits[i] = '1';
+        else if ( Abc_LatchIsInitDc(pLatch) )
+            pInits[i] = 'x';
+        else
+            assert( 0 );
+    }
+    pInits[i] = 0;
+    return pInits;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Strashes one logic node using its SOP.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fa160963..1763d165 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23867,10 +23867,11 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
     extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
     extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
-    Gia_Man_t * pAig;
-    Aig_Man_t * pMan;
-    int c, fVerbose = 0;
-    int fNames = 0;
+    Abc_Ntk_t * pStrash;
+    Aig_Man_t * pAig;
+    Gia_Man_t * pGia, * pTemp;
+    char * pInits;
+    int c, fNames = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
     {
@@ -23893,31 +23894,41 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash( pAbc->pNtkCur ) )
     {
-        Abc_Print( -1, "The current network should be strashed.\n" );
-        return 1;
+        // derive comb GIA
+        pStrash = Abc_NtkStrash( pAbc->pNtkCur, 0, 1, 0 );
+        pAig = Abc_NtkToDar( pStrash, 0, 0 );
+        Abc_NtkDelete( pStrash );
+        pGia = Gia_ManFromAig( pAig );
+        Aig_ManStop( pAig );
+        // perform undc/zero
+        pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
+        pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, fVerbose );
+        Gia_ManStop( pTemp );
+        ABC_FREE( pInits );
     }
-//    if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
-//    {
-//        Abc_Print( -1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
-//        Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
-//    }
-    if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
-        pMan = Abc_NtkToDarChoices( pAbc->pNtkCur );
     else
-        pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
-    pAig = Gia_ManFromAig( pMan );
-    Aig_ManStop( pMan );
-    Abc_FrameUpdateGia( pAbc, pAig );
+    {
+        if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
+            pAig = Abc_NtkToDarChoices( pAbc->pNtkCur );
+        else
+            pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+        pGia = Gia_ManFromAig( pAig );
+        Aig_ManStop( pAig );
+    }
+    // replace
     if ( fNames )
     {
-        pAig->vNamesIn  = Abc_NtkCollectCiNames( pAbc->pNtkCur );
-        pAig->vNamesOut = Abc_NtkCollectCoNames( pAbc->pNtkCur );
+        pGia->vNamesIn  = Abc_NtkCollectCiNames( pAbc->pNtkCur );
+        pGia->vNamesOut = Abc_NtkCollectCoNames( pAbc->pNtkCur );
     }
+    Abc_FrameUpdateGia( pAbc, pGia );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: &get [-nvh] <file>\n" );
-    Abc_Print( -2, "\t         converts the network into an AIG and moves to the new ABC\n" );
+    Abc_Print( -2, "\t         converts the current network into GIA and moves it to the &-space\n" );
+    Abc_Print( -2, "\t         (if the network is a sequential logic network, normalizes the flops\n" );
+    Abc_Print( -2, "\t         to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
     Abc_Print( -2, "\t-n     : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -26307,9 +26318,9 @@ int Abc_CommandAbc9Miter2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // extract string
     pInit = Extra_FileReadContents( FileName );
     Extra_StringClean( pInit, "01xX" );
-    if ( (int)strlen(pInit) != Gia_ManCoNum(pAbc->pGia) )
+    if ( (int)strlen(pInit) != Gia_ManCiNum(pAbc->pGia) )
     {
-        Abc_Print( -1, "Init string length (%d) differs from PI and flop count (%d).\n", strlen(pInit), Gia_ManCoNum(pAbc->pGia) );
+        Abc_Print( -1, "Init string length (%d) differs from PI and flop count (%d).\n", strlen(pInit), Gia_ManCiNum(pAbc->pGia) );
         ABC_FREE( pInit );
         return 1;
     }
@@ -26324,7 +26335,7 @@ usage:
     Abc_Print( -2, "\t         creates miter of two copies of the design\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");
-    Abc_Print( -2, "\t<file> : file name with initialiation string [default = none]\n" );
+    Abc_Print( -2, "\t<file> : file name with flop initial values (0/1/x/X) [default = required]\n" );
     return 1;
 }