New command &divide, etc.

src/aig/gia/giaDup.c

@@ -23,6 +23,7 @@
 #include "misc/vec/vecWec.h"
 #include "proof/cec/cec.h"
 #include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -6844,6 +6845,125 @@ Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t *
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Divides the AIG into 2 parts at middle level.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel )
+{
+    Gia_Man_t * pPart0, * pPart1;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vCutNodes;
+    Vec_Ptr_t * vCutNames;
+    char * pFileName;
+    int i, Lcut;
+    assert( nParts == 2 );
+
+    // Use specified cut level or default to middle
+    if ( nCutLevel > 0 )
+        Lcut = nCutLevel;
+    else
+        Lcut = Gia_ManLevelNum(p) / 2;
+    printf( "Dividing at level %d (total levels = %d).  ", Lcut, Gia_ManLevelNum(p) );
+
+    // mark the nodes pointed to under the cut
+    Gia_ManForEachAnd( p, pObj, i ) {
+        if ( Gia_ObjLevel(p, pObj) <= Lcut )
+            continue;
+        if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) <= Lcut )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+        if ( Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) <= Lcut )
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < Lcut )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+
+    // Collect nodes at the cut (nodes at level Lcut that are needed by upper levels)
+    vCutNodes = Vec_IntAlloc( 100 );
+    Gia_ManForEachObj1( p, pObj, i ) {
+        if ( !pObj->fMark0 )
+            continue;
+        pObj->fMark0 = 0;
+        Vec_IntPush( vCutNodes, i );
+    }
+    printf( "Found %d nodes at the cut\n", Vec_IntSize(vCutNodes) );
+
+    // Create names for cut nodes
+    vCutNames = Vec_PtrAlloc( Vec_IntSize(vCutNodes) );
+    for ( i = 0; i < Vec_IntSize(vCutNodes); i++ ) {
+        char Buffer[100]; sprintf( Buffer, "cut[%d]", i );
+        Vec_PtrPush( vCutNames, Abc_UtilStrsav(Buffer) );
+    }
+
+    // Create Part 0 (bottom part: levels 0 to Lcut)
+    pPart0 = Gia_ManStart( Gia_ManObjNum(p) );
+    pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0" );
+    pPart0->pName = Abc_UtilStrsav( pFileName );
+    pPart0->pSpec = Abc_UtilStrsav( pFileName );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pPart0 );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjLevel(p, pObj) <= Lcut )
+            pObj->Value = Gia_ManAppendAnd( pPart0, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachObjVec( vCutNodes, p, pObj, i )
+        Gia_ManAppendCo( pPart0, pObj->Value );
+
+    // Add names to Part 0
+    if ( p->vNamesIn ) {
+        pPart0->vNamesIn = Vec_PtrDupStr( p->vNamesIn );
+        pPart0->vNamesOut = Vec_PtrDupStr( vCutNames );
+    }
+
+    // Write Part 0
+    pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0.aig" );
+    Gia_AigerWrite( pPart0, pFileName, 0, 0, 0 );
+    printf( "Part 0: PI = %d, PO = %d, AND = %d, written to %s\n",
+        Gia_ManCiNum(pPart0), Gia_ManCoNum(pPart0), Gia_ManAndNum(pPart0), pFileName );
+    Gia_ManStop( pPart0 );
+
+    // Create Part 1 (top part: levels > Lcut)
+    pPart1 = Gia_ManStart( Gia_ManObjNum(p) );
+    pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1" );
+    pPart1->pName = Abc_UtilStrsav( pFileName );
+    pPart1->pSpec = Abc_UtilStrsav( pFileName );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObjVec( vCutNodes, p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pPart1 );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjLevel(p, pObj) > Lcut )
+            pObj->Value = Gia_ManAppendAnd( pPart1, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pPart1, Gia_ObjFanin0Copy(pObj) );
+
+    // Add names to Part 1
+    if ( p->vNamesOut ) {
+        pPart1->vNamesIn = Vec_PtrDupStr( vCutNames );
+        pPart1->vNamesOut = Vec_PtrDupStr( p->vNamesOut );
+    }
+
+    // Write Part 1
+    pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1.aig" );
+    Gia_AigerWrite( pPart1, pFileName, 0, 0, 0 );
+    printf( "Part 1: PI = %d, PO = %d, AND = %d, written to %s\n",
+        Gia_ManCiNum(pPart1), Gia_ManCoNum(pPart1), Gia_ManAndNum(pPart1), pFileName );
+    Gia_ManStop( pPart1 );
+
+    // Clean up
+    Vec_IntFree( vCutNodes );
+    Vec_PtrFreeFree( vCutNames );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcHieGia.c

@@ -1333,6 +1333,7 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName )
     fprintf( pFile, "`timescale 1ns/1ps\n\n" );
 
     // Write LUT module definitions for Yosys compatibility (compact version)
+    fprintf( pFile, "`ifdef LUTSPECS\n" );
     fprintf( pFile, "module LUT2 #( parameter INIT = 04\'h0 ) ( output O, input I0, I1 );\n" );
     fprintf( pFile, "  assign O = INIT[ {I1, I0} ];\n" );
     fprintf( pFile, "endmodule\n" );
@@ -1351,7 +1352,8 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName )
 
     fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0 ) ( output O, input I0, I1, I2, I3, I4, I5 );\n" );
     fprintf( pFile, "  assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" );
-    fprintf( pFile, "endmodule\n\n" );
+    fprintf( pFile, "endmodule\n" );
+    fprintf( pFile, "`endif\n\n" );
 
     // Write main module
     fprintf( pFile, "module " );

src/base/abci/abc.c

@@ -659,6 +659,7 @@ static int Abc_CommandAbc9MulFind3           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9BsFind             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AndCare            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cuts               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Divide             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -1506,8 +1507,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&mulfind3",     Abc_CommandAbc9MulFind3,               0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&bsfind",       Abc_CommandAbc9BsFind,                 0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&andcare",      Abc_CommandAbc9AndCare,                0 );   
-    Cmd_CommandAdd( pAbc, "ABC9",         "&cuts",         Abc_CommandAbc9Cuts,                   0 );   
+    Cmd_CommandAdd( pAbc, "ABC9",         "&cuts",         Abc_CommandAbc9Cuts,                   0 );
-    
+    Cmd_CommandAdd( pAbc, "ABC9",         "&divide",       Abc_CommandAbc9Divide,                 0 );
+
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,                   0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&eslim",        Abc_CommandAbc9eSLIM,                  0 );
@@ -34455,9 +34457,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_Man_t * pAig;
     Gia_Man_t * pGia, * pTemp;
     char * pInits;
-    int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fVerbose = 0;
+    int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fReuseNames = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cmnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cmnrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -34470,6 +34472,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fNames ^= 1;
             break;
+        case 'r':
+            fReuseNames ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -34532,17 +34537,38 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
         pGia->vOutReqs = Vec_FltAllocArray( Abc_NtkGetCoRequiredFloats(pNtk), Abc_NtkCoNum(pNtk) );
         pGia->And2Delay = pNtk->AndGateDelay;
     }
+    if ( fReuseNames ) 
+    {
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( -1, "There is no current AIG to reuse names from.\n" );
+            return 1;
+        }
+        if ( Gia_ManCiNum(pGia) != Gia_ManCiNum(pAbc->pGia) )
+        {
+            Abc_Print( -1, "The number of CIs differ.\n" );
+            return 1;
+        }
+        if ( Gia_ManCoNum(pGia) != Gia_ManCoNum(pAbc->pGia) )
+        {
+            Abc_Print( -1, "The number of COs differ.\n" );
+            return 1;
+        }
+        ABC_SWAP( Vec_Ptr_t *, pGia->vNamesIn,  pAbc->pGia->vNamesIn  );
+        ABC_SWAP( Vec_Ptr_t *, pGia->vNamesOut, pAbc->pGia->vNamesOut );
+    }
     Abc_FrameUpdateGia( pAbc, pGia );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &get [-cmnvh] <file>\n" );
+    Abc_Print( -2, "usage: &get [-cmnrvh] <file>\n" );
     Abc_Print( -2, "\t         converts the current network into GIA and moves it to the &-space\n" );
     Abc_Print( -2, "\t         (if the network is a sequential logic network, normalizes the flops\n" );
     Abc_Print( -2, "\t         to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
     Abc_Print( -2, "\t-c     : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggles reusing CI/CO names of the current AIG [default = %s]\n", fReuseNames? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
@@ -42580,6 +42606,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
     FILE * pFile;
     Gia_Man_t * pGia;
     char * pTemp;
+    char * pOrigFileName = NULL;
     int fVerilog, fSystemVerilog;
 
     *pAbc_ReadAigerOrVerilogFileStatus = 0;
@@ -42607,6 +42634,8 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
     {
         char pCommand[2000];
         int RetValue;
+        // Save the original filename before changing it
+        pOrigFileName = pFileName;
         snprintf( pCommand, sizeof(pCommand),
             "yosys -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"",
             fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top "    : "-auto-top", pTopModule ? pTopModule : "" );
@@ -42625,7 +42654,18 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
 
     pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
     if ( pGia == NULL )
+    {
         Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName );
+        return NULL;
+    }
+
+    // If we read from a Verilog file, keep the original filename as the spec
+    if ( pOrigFileName != NULL )
+    {
+        ABC_FREE( pGia->pSpec );
+        pGia->pSpec = Abc_UtilStrsav( pOrigFileName );
+    }
+
     return pGia;
 }
 
@@ -59447,7 +59487,7 @@ int Abc_CommandAbc9Cuts( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: cuts [-KC num] [-tdbvh]\n" );
+    Abc_Print( -2, "usage: &cuts [-KC num] [-tdbvh]\n" );
     Abc_Print( -2, "\t         computes K-input cuts for the nodes in the current AIG\n" );
     Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", 2, 14, nCutSize );
     Abc_Print( -2, "\t-C num : max number of cuts at a node (%d <= num <= %d) [default = %d]\n", 2, 256, nCutNum );
@@ -59458,6 +59498,76 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Divide( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel );
+    int nParts = 2;
+    int nCutLevel = 0;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PLvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nParts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nParts < 2 )
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCutLevel = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutLevel < 0 )
+                goto usage;
+            break;
+        case 'v':
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Divide(): There is no AIG.\n" );
+        return 0;
+    }
+    Gia_ManDupSplit( pAbc->pGia, nParts, nCutLevel );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &divide [-P num] [-L num] [-vh]\n" );
+    Abc_Print( -2, "\t         divides AIG into N parts at different levels\n" );
+    Abc_Print( -2, "\t-P num : number of parts to divide into [default = %d]\n", nParts );
+    Abc_Print( -2, "\t-L num : cut level (0 = automatic middle level) [default = %d]\n", nCutLevel );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = no]\n" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/base/abci/abcVerify.c

@@ -834,32 +834,51 @@ static void Abc_NtkVerifyPrintWords( Vec_Ptr_t * vWords )
     }
 }
 
-void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, 
+void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2,
-    const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, 
+    const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs,
     const char * pNtkName1, const char * pNtkName2 )
 {
     Vec_Ptr_t * vInputs   = Vec_PtrAlloc( 0 );
     Vec_Ptr_t * vOutputs1 = Vec_PtrAlloc( 0 );
     Vec_Ptr_t * vOutputs2 = Vec_PtrAlloc( 0 );
+    char * pBaseName1 = NULL;
+    char * pBaseName2 = NULL;
+
     Abc_NtkVerifyCollectWords( vInputs, ppInputNames, pModel, nInputs );
     Abc_NtkVerifyCollectWords( vOutputs1, ppOutputNames, pValues1, nOutputs );
     if ( pValues2 )
         Abc_NtkVerifyCollectWords( vOutputs2, ppOutputNames, pValues2, nOutputs );
+
+    // Extract base names for printing
+    if ( pNtkName1 )
+    {
+        char * pFileNameOnly = Extra_FileNameWithoutPath( (char *)pNtkName1 );
+        pBaseName1 = Extra_FileNameGeneric( pFileNameOnly );
+    }
+    if ( pNtkName2 )
+    {
+        char * pFileNameOnly = Extra_FileNameWithoutPath( (char *)pNtkName2 );
+        pBaseName2 = Extra_FileNameGeneric( pFileNameOnly );
+    }
+
     if ( Vec_PtrSize(vInputs) || Vec_PtrSize(vOutputs1) || Vec_PtrSize(vOutputs2) )
     {
         printf( "INPUT: " );
         Abc_NtkVerifyPrintWords( vInputs );
         printf( ".  OUTPUT: " );
         Abc_NtkVerifyPrintWords( vOutputs1 );
-        printf( " (%s)", pNtkName1 ? pNtkName1 : "network1" );
+        printf( " (%s)", pBaseName1 ? pBaseName1 : (pNtkName1 ? pNtkName1 : "network1") );
         if ( pValues2 && Vec_PtrSize(vOutputs2) )
         {
             printf( ", " );
             Abc_NtkVerifyPrintWords( vOutputs2 );
-            printf( " (%s)", pNtkName2 ? pNtkName2 : "network2" );
+            printf( " (%s)", pBaseName2 ? pBaseName2 : (pNtkName2 ? pNtkName2 : "network2") );
         }
         printf( ".\n" );
     }
+
+    ABC_FREE( pBaseName1 );
+    ABC_FREE( pBaseName2 );
     Abc_NtkVerifyFreeWords( vInputs );
     Abc_NtkVerifyFreeWords( vOutputs1 );
     Abc_NtkVerifyFreeWords( vOutputs2 );