Version abc60305

abc.rc

@@ -50,8 +50,10 @@ alias rw rewrite
 alias rwz rewrite -z
 alias rf refactor
 alias rfz refactor -z
-alias rs restructure
-alias rsz restructure -z
+alias re restructure
+alias rez restructure -z
+alias rs resub
+alias rsz resub -z
 alias sa set autoexec ps
 alias so source -x
 alias st strash
@@ -80,4 +82,12 @@ alias rwsat     "st; rw -l; b -l; rw -l; rf -l"
 alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
 alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 
+# resubstitution scripts for the IWLS paper
+alias src_rw      "st; rw -l; rwz -l; rwz -l" 
+alias src_rs1     "st; rs -K 6 -l; rs -K 9 -l; rs -K 12 -l" 
+alias src_rs2     "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
+alias src_rws1    "st; rw -l; rs -K 6 -l; rwz -l; rs -K 9 -l; rwz -l; rs -K 12 -l" 
+alias src_rws2    "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
+alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
+
 

src/base/abc/abcRefs.c

@@ -271,14 +271,14 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t *
     // add to the new support nodes
     if ( !fTopmost && (Abc_ObjIsCi(pNode) || pNode->vFanouts.nSize > 0) )
     {
-        Vec_PtrPush( vSupp, pNode );
+        if ( vSupp ) Vec_PtrPush( vSupp, pNode );
         return;
     }
     // recur on the children
     Abc_ObjForEachFanin( pNode, pFanin, i )
         Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 );
     // collect the internal node
-    Vec_PtrPush( vCone, pNode );
+    if ( vCone ) Vec_PtrPush( vCone, pNode );
 }
 
 /**Function*************************************************************
@@ -296,8 +296,8 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
 {
     assert( Abc_ObjIsNode(pNode) );
     assert( !Abc_ObjIsComplement(pNode) );
-    Vec_PtrClear( vCone );
-    Vec_PtrClear( vSupp );
+    if ( vCone ) Vec_PtrClear( vCone );
+    if ( vSupp ) Vec_PtrClear( vSupp );
     Abc_NtkIncrementTravId( pNode->pNtk );
     Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
 }
@@ -326,6 +326,36 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
     Vec_PtrFree( vSupp );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal nodes of the MFFC limited by cut.]
+
+  Description []
+               
+  SideEffects [Increments the trav ID and marks visited nodes.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside )
+{
+    Abc_Obj_t * pObj;
+    int i, Count1, Count2;
+    // increment the fanout counters for the leaves
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->vFanouts.nSize++;
+    // dereference the node
+    Count1 = Abc_NodeDeref_rec( pNode );
+    // collect the nodes inside the MFFC
+    Abc_NodeMffsConeSupp( pNode, vInside, NULL );
+    // reference it back
+    Count2 = Abc_NodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    // remove the extra counters
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->vFanouts.nSize--;
+    return Count1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abci/abc.c

@@ -63,6 +63,7 @@ static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandRewrite      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRestructure  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -165,6 +166,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
 
 //    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
@@ -2574,7 +2576,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'K':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
             nCutMax = atoi(argv[globalUtilOptind]);
@@ -2638,6 +2640,125 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int RS_CUT_MIN =  4;
+    int RS_CUT_MAX = 16;
+    int c;
+    int nCutMax;
+    int nNodesMax;
+    bool fUpdateLevel;
+    bool fUseZeros;
+    bool fVerbose;
+    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nCutMax      =  8;
+    nNodesMax    =  1;
+    fUpdateLevel =  1;
+    fUseZeros    =  0;
+    fVerbose     =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KNlzvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCutMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutMax < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodesMax < 0 ) 
+                goto usage;
+            break;
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'z':
+            fUseZeros ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( nCutMax < RS_CUT_MIN || nCutMax > RS_CUT_MAX )
+    {
+        fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
+        return 1;
+    }
+    if ( Abc_NtkGetChoiceNum(pNtk) )
+    {
+        fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+        return 1;
+    }
+
+    // modify the current network
+    if ( !Abc_NtkResubstitute( pNtk, nCutMax, nNodesMax, fUpdateLevel, fVerbose ) )
+    {
+        fprintf( pErr, "Refactoring has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" );
+    fprintf( pErr, "\t         performs technology-independent restructuring of the AIG\n" );
+    fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutMax );  
+    fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax );  
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 

src/base/abci/abcVerify.c

@@ -112,8 +112,8 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
 ***********************************************************************/
 void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
-    Fraig_Params_t Params;
-    Fraig_Man_t * pMan;
+//    Fraig_Params_t Params;
+//    Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
     int RetValue;
 
@@ -141,7 +141,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
         Abc_NtkDelete( pMiter );
         return;
     }
-
+/*
     // convert the miter into a FRAIG
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
@@ -169,6 +169,18 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ManFree( pMan );
     // delete the miter
     Abc_NtkDelete( pMiter );
+*/
+    // solve the CNF using the SAT solver
+    RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 );
+    if ( RetValue == -1 )
+        printf( "Networks are undecided (resource limits is reached).\n" );
+    else if ( RetValue == 0 )
+        printf( "Networks are NOT EQUIVALENT.\n" );
+    else
+        printf( "Networks are equivalent.\n" );
+    if ( pMiter->pModel )
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+    Abc_NtkDelete( pMiter );
 }
 
 /**Function*************************************************************