Experiments with iterative synthesis.

2 files changed, 66 insertions, 20 deletions

diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index eced70e7..6d5bdaad 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -145,15 +145,28 @@ char * pLibStr[25] = {
     "GATE zero       0       O=CONST0;\n"
     "GATE one        0       O=CONST1;\n"
 };
-void Acb_IntallLibrary()
+char * pLibStr2[25] = {
+    "GATE buf        1       O=a;            PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE inv        1       O=!a;           PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE and2       1       O=a*b;          PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE or2        1       O=a+b;          PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE nand2      1       O=!(a*b);       PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE nor2       1       O=!(a+b);       PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE xor        1       O=!a*b+a*!b;    PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE xnor       1       O=a*b+!a*!b;    PIN * INV 1 999 1.0 0.0 1.0 0.0\n"
+    "GATE zero       0       O=CONST0;\n"
+    "GATE one        0       O=CONST1;\n"
+};
+void Acb_IntallLibrary( int f2Ins )
 {
     extern Mio_Library_t * Mio_LibraryReadBuffer( char * pBuffer, int fExtendedFormat, st__table * tExcludeGate, int fVerbose );
     Mio_Library_t * pLib;
     int i;
     // create library string
     Vec_Str_t * vLibStr = Vec_StrAlloc( 1000 );
-    for ( i = 0; pLibStr[i]; i++ )
-        Vec_StrAppend( vLibStr, pLibStr[i] );
+    char ** ppLibStr = f2Ins ? pLibStr2 : pLibStr;
+    for ( i = 0; ppLibStr[i]; i++ )
+        Vec_StrAppend( vLibStr, ppLibStr[i] );
     Vec_StrPush( vLibStr, '\0' );
     // create library
     pLib = Mio_LibraryReadBuffer( Vec_StrArray(vLibStr), 0, NULL, 0 );
@@ -2600,7 +2613,7 @@ Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps,
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose, int fVeryVerbose )
+int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fInputs, int fCheck, int fVerbose, int fVeryVerbose )
 {
     extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
 
@@ -2615,7 +2628,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4]
     Vec_Int_t * vSuppF  = Acb_NtkFindSupp( pNtkF, vRoots );
     Vec_Int_t * vSuppG  = Acb_NtkFindSupp( pNtkG, vRoots );
     Vec_Int_t * vSupp   = Vec_IntTwoMerge( vSuppF, vSuppG );
-    Vec_Int_t * vDivs   = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
+    Vec_Int_t * vDivs   = (fCisOnly || fInputs) ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
     Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
     Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
 
@@ -2829,7 +2842,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
     Acb_Ntk_t * pNtk = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
     Acb_VerilogSimpleWrite( pNtk, pFileNameOut );
     Acb_ManFree( pNtk->pDesign );
-    Acb_IntallLibrary();
+    Acb_IntallLibrary( 0 );
 }
 
 /**Function*************************************************************
@@ -2843,7 +2856,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose )
+void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose )
 {
     char Command[1000]; int Result = 1;
     Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
@@ -2863,12 +2876,12 @@ void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose,
     assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
     assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
 
-    Acb_IntallLibrary();
+    Acb_IntallLibrary( Abc_FrameReadSignalNames() != NULL );
 
-    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose, fVeryVerbose ) )
+    if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fInputs, fCheck, fVerbose, fVeryVerbose ) )
     {
 //        printf( "General computation timed out. Trying inputs only.\n\n" );
-//        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose, fVeryVerbose ) )
+//        if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fInputs, fCheck, fVerbose, fVeryVerbose ) )
 //            printf( "Input-only computation also timed out.\n\n" );
         printf( "Computation did not succeed.\n" );
         Result = 0;
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index d707d136..dab8239d 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -167,17 +167,35 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
+int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
 {
     int i, Fanin, * pFanins, Counter = 1;
     if ( Acb_ObjIsCi(p, iObj) )
         return 0;
+    if ( nGates )
+    {
+        int nFan = Acb_ObjFaninNum(p, iObj);
+        int Type = Acb_ObjType( p, iObj );
+        if ( Type == ABC_OPER_CONST_F ) 
+            nGates[0]++;
+        else if ( Type == ABC_OPER_CONST_T ) 
+            nGates[1]++;
+        else if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_CO ) 
+            nGates[2]++;
+        else if ( Type == ABC_OPER_BIT_INV ) 
+            nGates[3]++;
+        else
+        {
+            assert( nFan >= 2 );
+            nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
+        }
+    }
     Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
     {
         assert( Vec_IntEntry(vRefs, Fanin) > 0 );
         Vec_IntAddToEntry( vRefs, Fanin, -1 );
         if ( Vec_IntEntry(vRefs, Fanin) == 0 )
-            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin );
+            Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin, nGates );
     }
     return Counter;
 }
@@ -220,10 +238,10 @@ int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObj
         Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
             Vec_IntAddToEntry( vRefs, Fanin, 1 );
     Vec_IntForEachEntry( vObjsRefed, iObj, i )
-        Acb_NtkNodeRef_rec( vRefs, p, iObj, NULL );
+        Vec_IntAddToEntry( vRefs, iObj, 1 );
     Vec_IntForEachEntry( vObjsDerefed, iObj, i )
-        if ( Vec_IntEntry(vRefs, iObj) == 0 )
-            Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj, nGates );
+        //if ( Vec_IntEntry(vRefs, iObj) != 0 || Acb_ObjIsCo(p, iObj) )
+            Count2 += Acb_NtkNodeDeref_rec( vRefs, p, iObj, nGates );
     Vec_IntFree( vRefs );
     return Count2;
 }
@@ -1133,7 +1151,7 @@ void Acb_Ntk4CollectRing( Acb_Ntk_t * pNtk, Vec_Int_t * vStart, Vec_Int_t * vRes
 }
 void Acb_Ntk4DumpWeightsInt( Acb_Ntk_t * pNtk, Vec_Int_t * vObjs, char * pFileName )
 {
-    int i, iObj;//, Weight;
+    int i, iObj, Count = 0;//, Weight;
     Vec_Int_t * vDists, * vStart, * vNexts;
     FILE * pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
@@ -1165,15 +1183,30 @@ void Acb_Ntk4DumpWeightsInt( Acb_Ntk_t * pNtk, Vec_Int_t * vObjs, char * pFileNa
 //    Vec_IntForEachEntry( vDists, Weight, i )
 //        if ( Weight && Acb_ObjNameStr(pNtk, i)[0] != '1' )
 //            fprintf( pFile, "%s %d\n", Acb_ObjNameStr(pNtk, i), 10000+Weight );
+/*
+    // mark reachable
+    Vec_IntClear( &pNtk->vArray0 );
+    Acb_NtkIncTravId( pNtk );
+    Acb_NtkForEachCo( pNtk, iObj, i )
+        if ( !Vec_IntEntry(vStatus, i) )
+            Acb_ObjCollectTfi_rec( pNtk, iObj, 0 );
+*/
     Acb_NtkForEachObj( pNtk, iObj )
     {
         char * pName = Acb_ObjNameStr(pNtk, iObj);
         int Weight = Vec_IntEntry(vDists, iObj);
         if ( Weight == 0 )
             Weight = 10000;
+/*
+        if ( !Acb_ObjSetTravIdCur(pNtk, iObj) )
+        {
+            Count++;
+            continue;
+        }
+*/
         fprintf( pFile, "%s %d\n", pName, 100000+Weight );
     }
-
+    //printf( "Skipped %d nodes.\n", Count );
     Vec_IntFree( vDists );
     fclose( pFile );
 }
@@ -1205,13 +1238,13 @@ void Acb_Ntk4DumpWeights( char * pFileNameIn, Vec_Ptr_t * vObjNames, char * pFil
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fVerbose, int fVeryVerbose )
+void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fRandom, int fUseWeights, int fInputs, int fVerbose, int fVeryVerbose )
 {
     extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fUseBuf, int fVerbose );
-    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fVerbose, int fVeryVerbose );
+    extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fRandom, int fInputs, int fVerbose, int fVeryVerbose );
     char * pFileNames[4] = { pFileName[2], pFileName[1], fUseWeights ? (char *)"weights.txt" : NULL, pFileName[2] };
     if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fUseBuf, fVerbose ) )
-        Acb_NtkRunEco( pFileNames, 1, fRandom, fVerbose, fVeryVerbose );
+        Acb_NtkRunEco( pFileNames, 1, fRandom, fInputs, fVerbose, fVeryVerbose );
 }