Adding support for flop init-states in extended AIG.

8 files changed, 66 insertions, 2 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b36b6278..51c373c8 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -144,6 +144,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vObjClasses;   // classes of objects for abstraction
     Vec_Int_t *    vInitClasses;  // classes of flops for retiming/merging/etc
     Vec_Int_t *    vRegClasses;   // classes of registers for sequential synthesis
+    Vec_Int_t *    vRegInits;     // initial state
     Vec_Int_t *    vDoms;         // dominators
     Vec_Int_t *    vBarBufs;      // barrier buffers
     unsigned char* pSwitching;    // switching activity for each object
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 7ceff2fb..fb7717b4 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -671,6 +671,19 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
                 assert( pCur == pCurTemp );
                 if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
             }
+            // read register inits
+            else if ( *pCur == 's' )
+            {
+                int i, nRegs;
+                pCur++;
+                pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4;           pCur += 4;
+                nRegs = Gia_AigerReadInt(pCur);                         pCur += 4;
+                pNew->vRegInits = Vec_IntAlloc( nRegs );
+                for ( i = 0; i < nRegs; i++ )
+                    Vec_IntPush( pNew->vRegInits, Gia_AigerReadInt(pCur) ), pCur += 4;
+                assert( pCur == pCurTemp );
+                if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
+            }
             // read configuration data
             else if ( *pCur == 'b' )
             {
@@ -1285,6 +1298,16 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
     }
+    // write register inits
+    if ( p->vRegInits )
+    {
+        int i;
+        fprintf( pFile, "s" );
+        Gia_FileWriteBufferSize( pFile, 4*(Vec_IntSize(p->vRegInits)+1) );
+        Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegInits) );
+        for ( i = 0; i < Vec_IntSize(p->vRegInits); i++ )
+            Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegInits, i) );
+    }
     // write configuration data
     if ( p->vConfigs )
     {
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 38adfb41..ff57fedb 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -656,6 +656,8 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
         pNew->nAnd2Delay = p->nAnd2Delay;
     if ( p->vRegClasses )
         pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
+    if ( p->vRegInits )
+        pNew->vRegInits = Vec_IntDup( p->vRegInits );
     if ( p->vConfigs )
         pNew->vConfigs = Vec_IntDup( p->vConfigs );
     if ( p->pCellStr )
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 956d9d2d..8383433f 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -2062,6 +2062,7 @@ void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia )
     p->pManTime    = pGia->pManTime;    pGia->pManTime    = NULL;
     p->pAigExtra   = pGia->pAigExtra;   pGia->pAigExtra   = NULL;
     p->vRegClasses = pGia->vRegClasses; pGia->vRegClasses = NULL;
+    p->vRegInits   = pGia->vRegInits;   pGia->vRegInits = NULL;
     p->nAnd2Delay  = pGia->nAnd2Delay;  pGia->nAnd2Delay  = 0;
 }
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index f88feb8d..78c9e42f 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -102,6 +102,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vObjClasses );
     Vec_IntFreeP( &p->vInitClasses );
     Vec_IntFreeP( &p->vRegClasses );
+    Vec_IntFreeP( &p->vRegInits );
     Vec_IntFreeP( &p->vDoms );
     Vec_IntFreeP( &p->vBarBufs );
     Vec_IntFreeP( &p->vLevels );
diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index 039b6654..ca5d4038 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -348,6 +348,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk )
     // duplicated flops
     if ( p->vRegClasses )
         pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
+    // duplicated initial state
+    if ( p->vRegInits )
+        pNew->vRegInits = Vec_IntDup( p->vRegInits );
 
     // cleanup
     Vec_WecFree( vGroups );
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index e6ee618e..06e49f1f 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -154,13 +154,24 @@ Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, int fSeq )
     if ( fSeq )
     {
         pNew->vRegClasses = Vec_IntAlloc( Gia_ManRegBoxNum(p) );
+        if ( p->vRegInits )
+            pNew->vRegInits = Vec_IntAlloc( Gia_ManRegBoxNum(p) );
         iShift = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p);
         for ( i = 0; i < Gia_ManRegBoxNum(p); i++ )
             if ( Gia_ObjIsTravIdCurrent(p, Gia_ManCo(p, iShift + i)) )
+            {
                 Vec_IntPush( pNew->vRegClasses, Vec_IntEntry(p->vRegClasses, i) );
+                if ( p->vRegInits )
+                    Vec_IntPush( pNew->vRegInits, Vec_IntEntry(p->vRegInits, i) );
+            }
+    }
+    else 
+    {
+        if ( p->vRegClasses )
+            pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
+        if ( p->vRegInits )
+            pNew->vRegInits = Vec_IntDup( p->vRegInits );
     }
-    else if ( p->vRegClasses )
-        pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
     // collect remaining boxes
     vBoxesLeft = Vec_IntAlloc( Gia_ManBoxNum(p) );
     curCi = Tim_ManPiNum(pManTime);
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index bd77847b..d48f2637 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -842,6 +842,28 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
     Gia_ManStop( pTemp );
     assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) );
     assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) );
+    // implement initial state if given
+    if ( p->vRegInits && Vec_IntSum(p->vRegInits) )
+    {
+        char * pInit = ABC_ALLOC( char, Vec_IntSize(p->vRegInits) + 1 );
+        Gia_Obj_t * pObj;
+        int i;
+        assert( Vec_IntSize(p->vRegInits) == Gia_ManRegNum(pNew) );
+        Gia_ManForEachRo( pNew, pObj, i )
+        {
+            if ( Vec_IntEntry(p->vRegInits, i) == 0 )
+                pInit[i] = '0';
+            else if ( Vec_IntEntry(p->vRegInits, i) == 1 )
+                pInit[i] = '1';
+            else 
+                pInit[i] = 'X';
+        }
+        pInit[i] = 0;
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+        pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
+        Gia_ManStop( pTemp );
+        ABC_FREE( pInit );
+    }
     return pNew;
 }