Adding command &miter2 to derive a specified sequential miter.

5 files changed, 263 insertions, 1 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index cf033362..fead1c8b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -853,6 +853,8 @@ 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_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 );
 extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b79f7b8b..c861f23b 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1818,6 +1818,158 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs 'zero' and 'undc' operation.]
+
+  Description [The init string specifies 0/1/X for each flop.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int CountPis = Gia_ManPiNum(p), * pPiLits;
+    int i, iResetFlop = -1;
+    // map X-valued flops into new PIs
+    assert( (int)strlen(pInit) == Gia_ManRegNum(p) );
+    pPiLits = ABC_FALLOC( int, Gia_ManRegNum(p) );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        if ( pInit[i] == 'x' || pInit[i] == 'X' )
+            pPiLits[i] = CountPis++;
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    // create primary inputs
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create additional primary inputs
+    for ( i = Gia_ManPiNum(p); i < CountPis; i++ )
+        Gia_ManAppendCi( pNew );
+    // create flop outputs
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create reset flop output
+    if ( CountPis > Gia_ManPiNum(p) )
+        iResetFlop = Gia_ManAppendCi( pNew );
+    // update flop outputs
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        if ( pInit[i] == '1' )
+            pObj->Value = Abc_LitNot(pObj->Value);
+        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' )
+            assert( 0 );
+    }
+    ABC_FREE( pPiLits );
+    // build internal nodes
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create POs
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    // create flop inputs
+    Gia_ManForEachRi( p, pObj, i )
+        if ( pInit[i] == '1' )
+            pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) );
+        else
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    // create reset flop input
+    if ( CountPis > Gia_ManPiNum(p) )
+        Gia_ManAppendCo( pNew, 1 );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) + (int)(CountPis > Gia_ManPiNum(p)) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates miter of two designs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
+{
+    Vec_Int_t * vCoValues0, * vCoValues1;
+    Gia_Man_t * pNew, * pUndc, * pTemp;
+    Gia_Obj_t * pObj;
+    char * pInitNew;
+    int i, k;
+    // normalize the manager
+    pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManRegNum(pStart) );
+    // 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[i] = pInit[i];
+    }
+    for ( i = k = Gia_ManPiNum(pUndc); i < Gia_ManCiNum(pUndc); i++ )
+        if ( pInit[i] == 'x' || pInit[i] == 'X' )
+            pInitNew[k++] = pInit[i];
+    pInitNew[k] = 0;
+    assert( k == Gia_ManPiNum(pUndc) );
+    // derive miter
+    pNew = Gia_ManStart( Gia_ManObjNum(pUndc) );
+    pNew->pName = Abc_UtilStrsav( pUndc->pName );
+    pNew->pSpec = Abc_UtilStrsav( pUndc->pSpec );
+    Gia_ManConst0(pUndc)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    // build one side
+    Gia_ManForEachPi( pUndc, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( pUndc, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( pUndc, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // collect CO values
+    vCoValues0 = Vec_IntAlloc( Gia_ManPoNum(pUndc) );
+    Gia_ManForEachCo( pUndc, pObj, i )
+        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 );
+    Gia_ManForEachRo( pUndc, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( pUndc, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // collect CO values
+    vCoValues1 = Vec_IntAlloc( Gia_ManPoNum(pUndc) );
+    Gia_ManForEachCo( pUndc, pObj, i )
+        Vec_IntPush( vCoValues1, Gia_ObjFanin0Copy(pObj) );
+    // create POs
+    Gia_ManForEachPo( pUndc, pObj, i )
+        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) );
+    Gia_ManForEachRi( pUndc, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues1, Gia_ManPiNum(pUndc)+i) );
+    Vec_IntFree( vCoValues0 );
+    Vec_IntFree( vCoValues1 );
+    ABC_FREE( pInitNew );
+    // cleanup
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, 2*Gia_ManRegNum(pUndc) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG in the DFS order.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3a6c8b1b..69ab229f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -339,6 +339,7 @@ static int Abc_CommandAbc9Dc2                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Bidec              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Shrink             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Miter              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Miter2             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Append             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Scl                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Lcorr              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -829,6 +830,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&bidec",        Abc_CommandAbc9Bidec,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&shrink",       Abc_CommandAbc9Shrink,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&miter",        Abc_CommandAbc9Miter,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&miter2",       Abc_CommandAbc9Miter2,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&append",       Abc_CommandAbc9Append,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&scl",          Abc_CommandAbc9Scl,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lcorr",        Abc_CommandAbc9Lcorr,        0 );
@@ -26149,7 +26151,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'I':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a char string.\n" );
                 goto usage;
             }
             nInsDup = atoi(argv[globalUtilOptind]);
@@ -26252,6 +26254,85 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Miter2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    Gia_Man_t * pAux;
+    char * FileName, * pTemp, * pInit;
+    char ** pArgvNew;
+    int nArgcNew;
+    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:
+            goto usage;
+        }
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        Abc_Print( -1, "File name is not given on the command line.\n" );
+        return 1;
+    }
+    // get the input file name
+    FileName = pArgvNew[0];
+    // fix the wrong symbol
+    for ( pTemp = FileName; *pTemp; pTemp++ )
+        if ( *pTemp == '>' )
+            *pTemp = '\\';
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+        Abc_Print( 1, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+    // extract string
+    pInit = Extra_FileReadContents( FileName );
+    Extra_StringClean( pInit, "01xX" );
+    if ( (int)strlen(pInit) != Gia_ManCoNum(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Init string length (%d) differs from PI and flop count (%d).\n", strlen(pInit), Gia_ManCoNum(pAbc->pGia) );
+        ABC_FREE( pInit );
+        return 1;
+    }
+    // compute the miter
+    pAux = Gia_ManMiter2( pAbc->pGia, pInit, fVerbose );
+    ABC_FREE( pInit );
+    Abc_FrameUpdateGia( pAbc, pAux );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &miter2 [-vh] <file>\n" );
+    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" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 78a0fa99..c3c9a93d 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -112,6 +112,7 @@ extern char *       Extra_FileReadContents2( char * pFileName, char * pFileName2
 extern int          Extra_FileIsType( char * pFileName, char * pS1, char * pS2, char * pS3 );
 extern char *       Extra_TimeStamp();
 extern char *       Extra_StringAppend( char * pStrGiven, char * pStrAdd );
+extern void         Extra_StringClean( char * pStrGiven, char * pCharKeep );
 extern unsigned     Extra_ReadBinary( char * Buffer );
 extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
 extern int          Extra_ReadHex( unsigned Sign[], char * pString, int nDigits );
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index cab36e29..2e1d60f4 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -630,6 +630,32 @@ char * Extra_StringAppend( char * pStrGiven, char * pStrAdd )
 
 /**Function*************************************************************
 
+  Synopsis    [Only keep characters belonging to the second string.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_StringClean( char * pStrGiven, char * pCharKeep )
+{
+    char * pTemp, * pChar, * pSave = pStrGiven;
+    for ( pTemp = pStrGiven; *pTemp; pTemp++ )
+    {
+        for ( pChar = pCharKeep; *pChar; pChar++ )
+            if ( *pTemp == *pChar )
+                break;
+        if ( *pChar == 0 )
+            continue;
+        *pSave++ = *pTemp;
+    }
+    *pSave = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [String comparison procedure.]
 
   Description []