Ongoing changes to the simulator.

6 files changed, 133 insertions, 28 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f75d873c..c3842fe1 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -52,6 +52,7 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Gia_MmFixed_t_        Gia_MmFixed_t;    
 typedef struct Gia_MmFlex_t_         Gia_MmFlex_t;     
 typedef struct Gia_MmStep_t_         Gia_MmStep_t;     
+typedef struct Gia_Dat_t_            Gia_Dat_t;
 
 typedef struct Gia_Rpr_t_ Gia_Rpr_t;
 struct Gia_Rpr_t_
@@ -232,14 +233,7 @@ struct Gia_Man_t_
     Vec_Wrd_t *    vSuppWords;    // support information
     Vec_Int_t      vCopiesTwo;    // intermediate copies
     Vec_Int_t      vSuppVars;     // used variables
-    // additional info
-    char *         pUserFile;
-    Gia_Man_t *    pUserSpec;
-    Gia_Man_t *    pUserAig;
-    Vec_Ptr_t *    vUserNames;
-    Vec_Wec_t *    vUserNodes;
-    Vec_Wec_t *    vUserSupps;
-    Vec_Int_t *    vUserArray;
+    Gia_Dat_t *    pUserData;
 };
 
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index bb8851ec..0958cdfa 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -81,6 +81,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
 ***********************************************************************/
 void Gia_ManStop( Gia_Man_t * p )
 {
+    extern void Gia_DatFree( Gia_Dat_t * p );
+    Gia_DatFree( p->pUserData );
     if ( p->vSeqModelVec )
         Vec_PtrFreeFree( p->vSeqModelVec );
     Gia_ManStaticFanoutStop( p );
@@ -88,13 +90,6 @@ void Gia_ManStop( Gia_Man_t * p )
     assert( p->pManTime == NULL );
     Vec_PtrFreeFree( p->vNamesIn );
     Vec_PtrFreeFree( p->vNamesOut );
-    ABC_FREE( p->pUserFile );
-    Gia_ManStopP( &p->pUserSpec );
-    Gia_ManStopP( &p->pUserAig );
-    Vec_PtrFreeFree( p->vUserNames );
-    Vec_WecFreeP( &p->vUserNodes );
-    Vec_WecFreeP( &p->vUserSupps );
-    Vec_IntFreeP( &p->vUserArray );
     Vec_IntFreeP( &p->vSwitching );
     Vec_IntFreeP( &p->vSuper );
     Vec_IntFreeP( &p->vStore );
diff --git a/src/aig/gia/giaSim5.c b/src/aig/gia/giaSim5.c
index bdfd78b4..ab33c218 100644
--- a/src/aig/gia/giaSim5.c
+++ b/src/aig/gia/giaSim5.c
@@ -29,6 +29,7 @@ ABC_NAMESPACE_IMPL_START
 
 void Sim_Init( Abc_Frame_t * pAbc ) {}
 void Sim_End( Abc_Frame_t * pAbc )  {}
+void Gia_DatFree( Gia_Dat_t * p )   {}
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c
index 9c2db080..cea89809 100644
--- a/src/base/acb/acbAbc.c
+++ b/src/base/acb/acbAbc.c
@@ -167,6 +167,7 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
     Acb_Man_t * pMan = Acb_ManAlloc( pFileName, 1, Abc_NamRef(pNames), NULL, NULL, NULL );
     int k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, pMan->pName, NULL );
     int Mod = 2, Obj, Type, nArray, * pArray, ObjId;
+    int Token0 = Abc_NamStrFind( pMan->pStrs, "1\'b0" );
     Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Ndr_DataCiNum(p, Mod), Ndr_DataCoNum(p, Mod), Ndr_DataObjNum(p, Mod) );
     Vec_Int_t * vMap = Vec_IntStart( nNameIdMax );
     Acb_NtkCleanObjWeights( pNtk );
@@ -198,20 +199,30 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
     }
     Ndr_ModForEachNode( p, Mod, Obj )
     {
-        //char * pName;
-        NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
-        //pName = Abc_NamStr( pMan->pStrs, NameId );
+        int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        char * pName = Abc_NamStr( pMan->pStrs, NameId );
         ObjId  = Vec_IntEntry( vMap, NameId );
         nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
         for ( k = 0; k < nArray; k++ )
+        {
+            if ( Vec_IntEntry(vMap, pArray[k]) == 0 )
+                printf( "Cannot find fanin %d of node \"%s\".\n", k, pName );
             Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) );
+        }
         Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 );
     }
     Ndr_ModForEachPo( p, Mod, Obj )
     {
+        int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        char * pName = Abc_NamStr( pMan->pStrs, NameId );
         nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
         assert( nArray == 1 );
         ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
+        if ( Vec_IntEntry(vMap, pArray[0]) == 0 )
+        {
+            printf( "Adding constant 0 driver to non-driven PO \"%s\".\n", pName );
+            Vec_IntWriteEntry( vMap, pArray[0], Token0 );
+        }
         Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[0]) );
         Acb_ObjSetName( pNtk, ObjId, pArray[0] );
     }
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index d82c270d..dfebd720 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -20,6 +20,7 @@
 
 #include "acb.h"
 #include "base/abc/abc.h"
+#include "base/io/ioAbc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -540,7 +541,7 @@ int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp,
     {
         Res = 0;
         Vec_IntForEachEntry( vTemp, iFanin, k )
-            Res = fUseXors ? Gia_ManAppendXorReal(pNew, Res, iFanin) : Gia_ManAppendXor2(pNew, Res, iFanin);
+            Res = fUseXors ? Gia_ManAppendXorReal2(pNew, Res, iFanin) : Gia_ManAppendXor2(pNew, Res, iFanin);
         return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR );
     }
     assert( 0 );
@@ -660,7 +661,7 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
     extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW );
     Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileName0, NULL );
     Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileName1, NULL );
-    int i, RetValue = 0;
+    int RetValue = -1;
     if ( pNtkF && pNtkG )
     {
         int nTargets = Vec_IntSize(&pNtkF->vTargets);
@@ -671,14 +672,7 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
         *ppGiaF  = pGiaF;
         *ppGiaG  = pGiaG;
         *pvNodes = Acb_NtkCollectCopies( pNtkF, pGiaF, pvNodesR );
-        RetValue = 1;
-        if ( nTargets > 0 )
-        {
-            assert( pGiaF->vUserNodes == NULL );
-            pGiaF->vUserNodes = Vec_WecStart( nTargets );
-            for ( i = 0; i < nTargets; i++ )
-                Vec_WecPush( pGiaF->vUserNodes, i, 1 + Gia_ManCiNum(pGiaF) - nTargets + i );
-        }
+        RetValue = nTargets;
     }
     if ( pNtkF ) Acb_ManFree( pNtkF->pDesign );
     if ( pNtkG ) Acb_ManFree( pNtkG->pDesign );
@@ -696,6 +690,114 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Int_t * Abc_NtkCollectCopies( Abc_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR )
+{
+    int i, iObj, iLit;
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vObjs   = Abc_NtkDfs( p, 0 );
+    Vec_Int_t * vNodes  = Vec_IntAlloc( Abc_NtkObjNumMax(p) );
+    Vec_Ptr_t * vNodesR = Vec_PtrStart( Gia_ManObjNum(pGia) );
+    Vec_Bit_t * vDriver = Vec_BitStart( Gia_ManObjNum(pGia) );
+    Gia_ManForEachCiId( pGia, iObj, i )
+        Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Abc_ObjName(Abc_NtkCi(p, i))) );
+    Gia_ManForEachCoId( pGia, iObj, i )
+    {
+        Vec_BitWriteEntry( vDriver, Gia_ObjFaninId0(Gia_ManObj(pGia, iObj), iObj), 1 );
+        Vec_PtrWriteEntry( vNodesR, iObj, Abc_UtilStrsav(Abc_ObjName(Abc_NtkCo(p, i))) );
+        Vec_IntPush( vNodes, iObj );
+    }
+    Vec_PtrForEachEntry( Abc_Obj_t *, vObjs, pObj, i )
+        if ( (iLit = pObj->iTemp) >= 0 && Gia_ObjIsAnd(Gia_ManObj(pGia, Abc_Lit2Var(iLit))) )
+        {
+            if ( !Vec_BitEntry(vDriver, Abc_Lit2Var(iLit)) && Vec_PtrEntry(vNodesR, Abc_Lit2Var(iLit)) == NULL )
+            {
+                Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Abc_ObjName(pObj)) );
+                Vec_IntPush( vNodes, Abc_Lit2Var(iLit) );
+            }
+        }
+    Vec_BitFree( vDriver );
+    Vec_PtrFree( vObjs );
+    Vec_IntSort( vNodes, 0 );
+    *pvNodesR = vNodesR;
+    return vNodes;
+}
+int Abc_ObjToGia2( Gia_Man_t * pNew, Abc_Ntk_t * p, Abc_Obj_t * pObj, Vec_Int_t * vTemp, int fUseXors )
+{
+    Abc_Obj_t * pFanin; int k;
+    assert( Abc_ObjIsNode(pObj) );
+    Vec_IntClear( vTemp );
+    Abc_ObjForEachFanin( pObj, pFanin, k )
+    {
+        assert( pFanin->iTemp >= 0 );
+        Vec_IntPush( vTemp, pFanin->iTemp );
+    }
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+        return Abc_SopIsConst0( (char*)pObj->pData ) ? 0 : 1;
+    if ( Abc_ObjFaninNum(pObj) == 1 )
+        return Abc_SopIsBuf( (char*)pObj->pData ) ? Vec_IntEntry(vTemp, 0) : Abc_LitNot(Vec_IntEntry(vTemp, 0));
+    if ( Abc_ObjFaninNum(pObj) == 2 ) // nand2
+        return Abc_LitNot( Gia_ManAppendAnd2( pNew, Vec_IntEntry(vTemp, 0), Vec_IntEntry(vTemp, 1) ) );
+    assert( 0 );
+    return -1;
+}
+Gia_Man_t * Abc_NtkToGia2( Abc_Ntk_t * p, int fUseXors )
+{
+    Gia_Man_t * pNew, * pOne;
+    Vec_Int_t * vFanins;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj; int i;
+    pNew = Gia_ManStart( 2 * Abc_NtkObjNumMax(p) + 1000 );
+    pNew->pName = Abc_UtilStrsav(Abc_NtkName(p));
+    Abc_NtkForEachObj( p, pObj, i )
+        pObj->iTemp = -1;
+    Abc_NtkForEachCi( p, pObj, i )
+        pObj->iTemp = Gia_ManAppendCi(pNew);
+    vFanins = Vec_IntAlloc( 4 );
+    vNodes  = Abc_NtkDfs( p, 0 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+        pObj->iTemp = Abc_ObjToGia2(pNew, p, pObj, vFanins, fUseXors);
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vFanins );
+    Abc_NtkForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Abc_ObjFanin0(pObj)->iTemp );
+    pNew = Gia_ManCleanup( pOne = pNew );
+    //Gia_ManUpdateCopy( &p->vObjCopy, pOne );
+    Gia_ManStop( pOne );
+    return pNew;
+}
+int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVerbose, 
+                    Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR )
+{
+    Abc_Ntk_t * pNtkF = Io_Read( pFileName0, Io_ReadFileType(pFileName0), 1, 0 );
+    Abc_Ntk_t * pNtkG = Io_Read( pFileName1, Io_ReadFileType(pFileName1), 1, 0 );
+    int RetValue = -1;
+    if ( pNtkF && pNtkG )
+    {
+        Gia_Man_t * pGiaF = Abc_NtkToGia2( pNtkF, fUseXors );
+        Gia_Man_t * pGiaG = Abc_NtkToGia2( pNtkG, 0 );
+        assert( Abc_NtkCiNum(pNtkF) == Abc_NtkCiNum(pNtkG) );
+        assert( Abc_NtkCoNum(pNtkF) == Abc_NtkCoNum(pNtkG) );
+        *ppGiaF  = pGiaF;
+        *ppGiaG  = pGiaG;
+        *pvNodes = Abc_NtkCollectCopies( pNtkF, pGiaF, pvNodesR );
+        RetValue = 0;
+    }
+    if ( pNtkF ) Abc_NtkDelete( pNtkF );
+    if ( pNtkG ) Abc_NtkDelete( pNtkG );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
 {
     Vec_Int_t * vPlaces; int First = 1, Pos = -1, fComment = 0;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 49e1def1..a5cffbf4 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -231,6 +231,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         sprintf( Command, "read_constr %s", pFileName );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "c" ) )
         sprintf( Command, "so %s", pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "script" ) )
+        sprintf( Command, "so %s", pFileName );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
         sprintf( Command, "dsd_load %s", pFileName );
     if ( Command[0] )