diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 0c0fd3d1e..ba0b7d78c 100644 --- a/src/aig/gia/giaDup.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c index f2f6f8ca6..ea3c2d09a 100644 --- a/src/base/abc/abcHieGia.c +++ b/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 " ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dbb5ed99e..2071b9d57 100644 --- a/src/base/abci/abc.c +++ b/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", "÷", 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] \n" ); + Abc_Print( -2, "usage: &get [-cmnrvh] \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 : 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: ÷ [-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 [] diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c4744ebe0..3ec0e929a 100644 --- a/src/base/abci/abcVerify.c +++ b/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, - const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, +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 * 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 );