Recognizing async reset in blasting.

6 files changed, 69 insertions, 1 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index bb134757..abea47a4 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -142,11 +142,13 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vCos;               // combinational outputs
     Vec_Int_t              vFfs;               // flops
     Vec_Int_t              vFfs2;              // flops
+    Vec_Int_t *            vArsts;             // async resets
     Vec_Int_t *            vInits;             // initial values
     char *                 pInits;             // initial values
     int                    nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
     int                    nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
     int                    fSmtLib;            // the network comes from an SMT-LIB file
+    int                    fAsyncRst;          // the network has asynchronous reset
     int                    fMemPorts;          // the network contains memory ports
     int                    fEasyFfs;           // the network contains simple flops
     int                    nAssert;            // the number of asserts
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 9af2f54d..dce2d00f 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2112,7 +2112,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                 char Buffer[1000];
                 sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
-                printf( "Writing %s\n", Buffer );
+                //printf( "Writing %s\n", Buffer );
             }
     }
     if ( p->pInits )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index ad41d000..afd30169 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1133,6 +1133,11 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
         return 0;
     }
+    if ( pNtk->fAsyncRst )
+    {
+        Abc_Print( 1, "Abc_CommandBlast(): Trying to bit-blast network with asynchronous reset.\n" );
+        return 0;
+    }
     if ( fPrintInputInfo )
         Wlc_NtkPrintInputInfo(pNtk); 
     if ( pPar->fMulti )
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index 09b7312b..da0fc846 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -141,6 +141,7 @@ Wlc_Ntk_t * Wlc_NtkMemBlast( Wlc_Ntk_t * p )
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachCi( p, pObj, i )
@@ -529,6 +530,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
     pNew->vInits = Vec_IntAlloc( 100 );
@@ -1399,6 +1401,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose )
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
     pNew->fSmtLib   = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs  = p->fEasyFfs;
     pNew->vInits    = Vec_IntAlloc( 100 );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index ba8dcdc4..a61d72f0 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -266,6 +266,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
     ABC_FREE( p->vFfs.pArray );
     ABC_FREE( p->vFfs2.pArray );
     Vec_IntFreeP( &p->vInits );
+    Vec_IntFreeP( &p->vArsts );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vNameIds.pArray );
     ABC_FREE( p->vValues.pArray );
@@ -961,6 +962,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachCi( p, pObj, i )
@@ -989,6 +991,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachCi( p, pObj, i )
@@ -1056,6 +1059,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vP
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
 
@@ -1239,6 +1243,7 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fAsyncRst = p->fAsyncRst;
     pNew->fMemPorts = p->fMemPorts;
     pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachObj( p, pObj, i )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 0eca5c26..d831cb07 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -481,6 +481,32 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Wlc_PrsCheckBitConst0( Wlc_Ntk_t * p, int NameId )
+{
+    Wlc_Obj_t * pObj = Wlc_NtkObj( p, NameId );
+    int * pInits;
+    if ( Wlc_ObjRange(pObj) != 1 )
+        return 0;
+    while ( pObj->Type == WLC_OBJ_BUF )
+        pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
+    if ( pObj->Type != WLC_OBJ_CONST )
+        return 0;
+    pInits = Wlc_ObjConstValue(pObj);
+    return Abc_InfoHasBit((unsigned *)pInits, 0) == 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline char * Wlc_PrsFindRange( char * pStr, int * End, int * Beg )
 {
     *End = *Beg = 0;
@@ -1033,6 +1059,18 @@ startword:
                 p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
                 //printf( "%s\n", p->pNtk->pInits );
             }
+            if ( p->pNtk->vArsts )
+            {
+                int i, NameIdArst;
+                Vec_IntForEachEntry( p->pNtk->vArsts, NameIdArst, i )
+                {
+                    if ( Wlc_PrsCheckBitConst0(p->pNtk, NameIdArst) )
+                        continue;
+                    p->pNtk->fAsyncRst = 1;
+                    printf( "Detected async reset \"%s\".\n", Abc_NamStr(p->pNtk->pManName, NameIdArst) );
+                    break;
+                }
+            }
             if ( p->vPoPairs )
             {
                 assert( Vec_StrEntryLast(p->vPoPairs) == 0 );
@@ -1236,6 +1274,21 @@ startword:
                 if ( pStart == NULL )
                     break;
                 pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                if ( !p->pNtk->fAsyncRst && !strncmp(pStart, "arst", 4) && pStart[4] != 'v' )
+                {
+                    int NameIdArst;
+                    pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                    if ( pStart == NULL )
+                        return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis in the flop description." );
+                    pStart = Wlc_PrsFindName( pStart+1, &pName );
+                    if ( pStart == NULL )
+                        return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
+                    NameIdArst = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                    if ( p->pNtk->vArsts == NULL )
+                        p->pNtk->vArsts = Vec_IntAlloc( 100 );
+                    Vec_IntPushUnique( p->pNtk->vArsts, NameIdArst );
+                    continue;
+                }
                 if ( pStart[0] != 'd' && (pStart[0] != 'q' || pStart[1] == 'b') && strncmp(pStart, "arstval", 7) )
                     continue;
                 fFlopIn = (pStart[0] == 'd');