From 362661f00d0ee8b8f15feb6dd2d14c10c4c03640 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 10 Dec 2025 14:12:22 -0800 Subject: [PATCH 01/11] Command "genpop". --- src/aig/gia/giaTruth.c | 66 ++++++++++- src/base/abci/abc.c | 77 ++++++++++++ src/base/abci/abcCas.c | 261 ++++++++++++++++++++++++++++++++++++++++- src/sat/bmc/bmcMaj8.c | 13 +- 4 files changed, 411 insertions(+), 6 deletions(-) diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c index 0845eae96..c716ffb3d 100644 --- a/src/aig/gia/giaTruth.c +++ b/src/aig/gia/giaTruth.c @@ -22,6 +22,7 @@ #include "misc/vec/vecMem.h" #include "misc/vec/vecWec.h" #include "misc/util/utilTruth.h" +#include "bool/lucky/lucky.h" #include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START @@ -809,10 +810,73 @@ Gia_Man_t * Gia_ManIsoNpnReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fV return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManNodeFunctionProfile( Gia_Man_t * p, int nVars ) +{ + int fCanonicize = 1; + Gia_Obj_t * pObj; + Vec_Int_t * vLeaves = Vec_IntAlloc( 100 ); + int nWords = Abc_Truth6WordNum( nVars ); + Vec_Mem_t * pTtMem = Vec_MemAlloc( nWords, 12 ); // supports up to nVars words + Vec_MemHashAlloc( pTtMem, 1000 ); + Vec_Int_t * vCounts = Vec_IntAlloc( 100 ); + permInfo * pi = setPermInfoPtr( nVars ); + word pAuxWord[DAU_MAX_WORD], pAuxWord1[DAU_MAX_WORD], Truth[DAU_MAX_WORD], * pTruth; int i; + assert( nVars <= 7 ); + Gia_ObjComputeTruthTableStart( p, nVars ); + Gia_ManForEachAnd( p, pObj, i ) { + if ( Gia_ManSuppSize(p, &i, 1) != nVars ) + continue; + Gia_ManCollectCis( p, &i, 1, vLeaves ); + assert( Vec_IntSize(vLeaves) == nVars ); + pTruth = Gia_ObjComputeTruthTableCut( p, pObj, vLeaves ); + if ( fCanonicize ) { + memcpy( Truth, pTruth, sizeof(word) * nWords ); + simpleMinimal( Truth, pAuxWord, pAuxWord1, pi, nVars ); // NPN canonical form + } + else { + memcpy( Truth, pTruth, sizeof(word) * nWords ); + } + { + int nEntries = Vec_MemEntryNum( pTtMem ); + int Value = Vec_MemHashInsert( pTtMem, Truth ); + if ( Vec_MemEntryNum( pTtMem ) == nEntries ) + Vec_IntAddToEntry( vCounts, Value, 1 ); + else + { + assert( Value == nEntries ); + Vec_IntPush( vCounts, 1 ); + } + } + } + for ( i = 0; i < Vec_MemEntryNum(pTtMem); i++ ) { + word * pCanon = Vec_MemReadEntry( pTtMem, i ); + int Count = Vec_IntEntry( vCounts, i ); + Abc_TtPrintHexRev( stdout, pCanon, nVars ); + printf( " %d\n", Count ); + } + Gia_ObjComputeTruthTableStop( p ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCounts ); + Vec_MemHashFree( pTtMem ); + Vec_MemFree( pTtMem ); + freePermInfoPtr( pi ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 67685e00a..ba77e7ad7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -229,6 +229,7 @@ static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandGenTF ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandGenAT ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandGenPop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandGenFsm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCover ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1060,6 +1061,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 ); Cmd_CommandAdd( pAbc, "Various", "gentf", Abc_CommandGenTF, 0 ); Cmd_CommandAdd( pAbc, "Various", "genat", Abc_CommandGenAT, 0 ); + Cmd_CommandAdd( pAbc, "Various", "genpop", Abc_CommandGenPop, 0 ); Cmd_CommandAdd( pAbc, "Various", "genfsm", Abc_CommandGenFsm, 0 ); Cmd_CommandAdd( pAbc, "Various", "cover", Abc_CommandCover, 1 ); Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 ); @@ -16031,6 +16033,81 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandGenPop( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Abc_NtkLutCascadeFromPopcountLuts( int nVars, int nLutSize, int fVerbose, char * pFileName ); + char * pFileName = NULL; + Abc_Ntk_t * pNtk = NULL; + int c, nVars = 10, nLutSize = 6, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NKvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + pFileName = argv[globalUtilOptind]; + pNtk = Abc_NtkLutCascadeFromPopcountLuts( nVars, nLutSize, fVerbose, pFileName ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "Deriving the network has failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + return 0; + +usage: + Abc_Print( -2, "usage: genpop [-NK num] [-vh] \n" ); + Abc_Print( -2, "\t generates the adder tree\n" ); + Abc_Print( -2, "\t-N : the number of support variables [default = %d]\n", nVars ); + Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t- : (optional) Verilog file name\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c index 50e4a18d8..bec78ad02 100644 --- a/src/base/abci/abcCas.c +++ b/src/base/abci/abcCas.c @@ -1703,10 +1703,269 @@ void Abc_NtkRandFile( char * pFileName, int nVars, int nFuncs, int nMints ) Vec_WrdFree( vTruths ); } +/**Function************************************************************* + + Synopsis [Dump popcount LUT cascades into a Verilog file.] + + Description [Emits one LUT6CY per LUT with placement attributes and + preserves cascade ordering via RLOC/BEL tags.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_LutCascadeDumpName( FILE * pFile, int Obj, int iCas, int nVars ) +{ + if ( Obj < nVars ) + fprintf( pFile, "pi%d", Obj ); + else + fprintf( pFile, "w%d_%d", iCas, Obj ); +} +static void Abc_LutCascadeDumpOneVerilog( FILE * pFile, word * pLuts, int nVars, int iCas ) +{ + static const char * pBels[6] = { "A5LUT", "B5LUT", "C5LUT", "D5LUT", "E5LUT", "F5LUT" }; + Vec_Int_t * vWires = Vec_IntAlloc( 32 ); + word n, i; + for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] ) + { + word nIns = pLuts[i+1]; + word * pIns = pLuts+i+2; + int OutId = (int)pIns[nIns]; + if ( OutId >= nVars ) + Vec_IntPushUnique( vWires, OutId ); + } + if ( Vec_IntSize(vWires) ) + { + fprintf( pFile, " // cascade %d wires\n", iCas ); + int Id; int k; + Vec_IntForEachEntry( vWires, Id, k ) + fprintf( pFile, " wire w%d_%d;\n", iCas, Id ); + fprintf( pFile, "\n" ); + } + Vec_IntClear( vWires ); + + int iLastLut = -1; + for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] ) + { + word nIns = pLuts[i+1]; + word * pIns = pLuts+i+2; + word * pT = pLuts+i+2+nIns+1; + iLastLut = (int)pIns[nIns]; + fprintf( pFile, " (* HU_SET = \"hu_set_%d\", RLOC = \"X%dY%u\", BEL = \"%s\", DONT_TOUCH = \"yes\", IS_BEL_FIXED = \"yes\" *)\n", + iCas, iCas, (unsigned)n, pBels[n % 6] ); + fprintf( pFile, " LUT6CY #(.INIT(64'h" ); + Abc_TtPrintHexRev( pFile, pT, 6 ); + fprintf( pFile, ")) lut_%d_%u (\n", iCas, (unsigned)n ); + int k; + for ( k = 0; k < 6; k++ ) + { + fprintf( pFile, " .I%d(", k ); + if ( k < (int)nIns ) + Abc_LutCascadeDumpName( pFile, (int)pIns[k], iCas, nVars ); + else + fprintf( pFile, "1'b0" ); + fprintf( pFile, "),\n" ); + } + fprintf( pFile, " .O(" ); + Abc_LutCascadeDumpName( pFile, iLastLut, iCas, nVars ); + fprintf( pFile, ")\n );\n\n" ); + } + assert( iLastLut >= 0 ); + fprintf( pFile, " assign pc%d = ", iCas ); + Abc_LutCascadeDumpName( pFile, iLastLut, iCas, nVars ); + fprintf( pFile, ";\n\n" ); + Vec_IntFree( vWires ); +} +void Abc_LutCascadeDumpVerilog( Vec_Ptr_t * vLuts, int nVars, const char * pFileName ) +{ + if ( vLuts == NULL || pFileName == NULL ) + { + printf( "Abc_LutCascadeDumpVerilog(): Null input.\n" ); + return; + } + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Abc_LutCascadeDumpVerilog(): Cannot open \"%s\" for writing.\n", pFileName ); + return; + } + int nOuts = Vec_PtrSize( vLuts ); + fprintf( pFile, "// Auto-generated LUT cascade\n" ); + fprintf( pFile, "module lut_cascade_%d (\n", nVars ); + int i; + fprintf( pFile, " input " ); + for ( i = 0; i < nVars; i++ ) + { + if ( i ) fprintf( pFile, ", " ); + fprintf( pFile, "pi%d", i ); + } + fprintf( pFile, ",\n output " ); + for ( i = 0; i < nOuts; i++ ) + { + if ( i ) fprintf( pFile, ", " ); + fprintf( pFile, "pc%d", i ); + } + fprintf( pFile, "\n);\n\n" ); + + word * pLuts; + Vec_PtrForEachEntry( word *, vLuts, pLuts, i ) + { + if ( pLuts == NULL ) + continue; + fprintf( pFile, " // cascade %d\n", i ); + Abc_LutCascadeDumpOneVerilog( pFile, pLuts, nVars, i ); + } + fprintf( pFile, "endmodule\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Generates popcount as a set of LUT cascades.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Exa8_ManExactSynthesisPopcountAsLuts( int nVars, int nLutSize, int fVerbose ) +{ + extern Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int nLutSize, int fVerbose ); + Vec_Ptr_t * vTruthSets = Exa8_ManExactSynthesisPopcount( nVars, nLutSize, fVerbose ); + if ( vTruthSets == NULL ) + return NULL; + int nWordsNode = Abc_TtWordNum( nLutSize ); + int nOuts = Abc_Base2Log( nVars + 1 ); + if ( Vec_PtrSize(vTruthSets) != nOuts && fVerbose ) + printf( "Exa8_ManExactSynthesisPopcountAsLuts(): Expecting %d outputs, got %d.\n", nOuts, Vec_PtrSize(vTruthSets) ); + Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_PtrSize(vTruthSets) ); + Vec_Wrd_t * vTruths; int o; + Vec_PtrForEachEntry( Vec_Wrd_t *, vTruthSets, vTruths, o ) + { + if ( vTruths == NULL ) + continue; + int nObjs = Vec_WrdSize( vTruths ) / nWordsNode; + int nNodes = nObjs - nVars; + if ( nNodes <= 0 ) + { + Vec_WrdFree( vTruths ); + continue; + } + Vec_Wrd_t * vLutVec = Vec_WrdStart( 1 ); + int pIns[6]; int i, k; + for ( i = 0; i < nNodes; i++ ) + { + word * pTruth = Vec_WrdEntryP( vTruths, (nVars + i) * nWordsNode ); + if ( i == 0 ) + { + for ( k = 0; k < nLutSize; k++ ) + pIns[k] = nLutSize-1-k; + } + else + { + pIns[0] = nVars + i - 1; + if ( i & 1 ) + for ( k = 0; k < nLutSize-1; k++ ) + pIns[k+1] = nVars - 1 - k; + else + for ( k = 0; k < nLutSize-1; k++ ) + pIns[k+1] = nLutSize - 2 - k; + } + Abc_LutCascadeGenOne( vLutVec, nLutSize, pIns, nVars + i, pTruth ); + } + if ( fVerbose ) + Abc_LutCascadePrint( Vec_WrdArray(vLutVec), nLutSize ); + Vec_PtrPush( vRes, Vec_WrdReleaseArray(vLutVec) ); + Vec_WrdFree( vLutVec ); + Vec_WrdFree( vTruths ); + } + Vec_PtrFree( vTruthSets ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Builds network for popcount cascades.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkLutCascadeFromPopcountLuts( int nVars, int nLutSize, int fVerbose, char * pFileName ) +{ + Vec_Ptr_t * vLuts = Exa8_ManExactSynthesisPopcountAsLuts( nVars, nLutSize, fVerbose ); + if ( vLuts == NULL ) + return NULL; + if ( pFileName && nLutSize == 6 ) { + Abc_LutCascadeDumpVerilog( vLuts, nVars, pFileName ); + printf( "Wrote the resulting network into a Verilog file \"%s\".\n", pFileName ); + } + Abc_Ntk_t * pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 0 ); + Abc_Obj_t * pObj; int Id; char pName[32]; + pNtkNew->pName = Extra_UtilStrsav( "pop" ); + Vec_PtrPush( pNtkNew->vObjs, NULL ); + for ( Id = 0; Id < nVars; Id++ ) + { + pObj = Abc_NtkCreatePi( pNtkNew ); + pName[0] = 'a' + Id; + pName[1] = 0; + Abc_ObjAssignName( pObj, pName, NULL ); + } + Vec_Int_t * vCover = Vec_IntAlloc( 1000 ); + if ( Vec_PtrSize(vLuts) != Abc_Base2Log(nVars + 1) ) + printf( "Abc_NtkLutCascadeFromPopcountLuts(): Expecting %d outputs, got %d.\n", Abc_Base2Log(nVars + 1), Vec_PtrSize(vLuts) ); + word * pLuts; int o; + Vec_PtrForEachEntry( word *, vLuts, pLuts, o ) + { + if ( pLuts == NULL ) + continue; + Vec_Ptr_t * vCopy = Vec_PtrStart( nVars + pLuts[0] + 100 ); + Abc_NtkForEachCi( pNtkNew, pObj, Id ) + Vec_PtrWriteEntry( vCopy, Id, pObj ); + word n, i, k; int iLastLut = -1; + for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] ) + { + word nIns = pLuts[i+1]; + word * pIns = pLuts+i+2; + word * pT = pLuts+i+2+nIns+1; + Abc_Obj_t * pNodeNew = Abc_NtkCreateNode( pNtkNew ); + for ( k = 0; k < nIns; k++ ) + Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vCopy, pIns[k]) ); + Abc_Obj_t * pObjNew = Abc_NtkLutCascadeDeriveSop( pNtkNew, pNodeNew, pT, nIns, vCover ); + Vec_PtrWriteEntry( vCopy, pIns[nIns], pObjNew ); + iLastLut = pIns[nIns]; + } + if ( iLastLut == -1 ) + { + Vec_PtrFree( vCopy ); + continue; + } + Abc_Obj_t * pPo = Abc_NtkCreatePo( pNtkNew ); + Abc_ObjAddFanin( pPo, (Abc_Obj_t *)Vec_PtrEntry(vCopy, iLastLut) ); + snprintf( pName, sizeof(pName), "pc%d", o ); + Abc_ObjAssignName( pPo, pName, NULL ); + Vec_PtrFree( vCopy ); + } + Vec_IntFree( vCover ); + Vec_PtrFreeFree( vLuts ); + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkLutCascadeFromPopcountLuts: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index 465453d81..a80f97330 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -905,26 +905,30 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose ) +Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int nLutSize, int fVerbose ) { + assert( nVars > nLutSize ); Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); + pPars->nVars = nVars; + pPars->nLutSize = nLutSize; pPars->fKissat = 1; pPars->fLutCascade = 1; - pPars->fMinNodes = 1; pPars->fUsePerm = 1; pPars->fGenTruths = 1; pPars->fSilent = !fVerbose; - pPars->nLutSize = 6; int v, o, nOuts = Abc_Base2Log(nVars+1); Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts ); for ( o = 0; o < nOuts; o++ ) { + pPars->nNodes = 10; + ABC_FREE( pPars->pPermStr ); + pPars->pPermStr = NULL; char pBuffer[100]; for ( v = 0; v <= nVars; v++ ) pBuffer[v] = '0' + ((v >> o) & 1); pBuffer[nVars+1] = '\0'; pPars->pSymStr = pBuffer; - int status = Exa8_ManExactSynthesis( pPars ); + int status = Exa8_ManExactSynthesisIter( pPars ); if ( status != 1 ) { printf( "Synthesis failed for output %d.\n", o ); break; @@ -932,6 +936,7 @@ Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose ) Vec_PtrPush( vRes, pPars->vTruths ); pPars->vTruths = NULL; } + ABC_FREE( pPars->pPermStr ); return vRes; } From 94d0b0dbbb439022aaaa1da721f15a3ed70160f9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 12 Dec 2025 20:35:42 -0800 Subject: [PATCH 02/11] Command "write_jsonc". --- src/base/io/io.c | 50 +++++++++++++++ src/base/io/ioJsonc.c | 142 +++++++++++++++++++++++++++++++++++++++++- 2 files changed, 191 insertions(+), 1 deletion(-) diff --git a/src/base/io/io.c b/src/base/io/io.c index 7bb789ae6..b30b70fca 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -93,6 +93,7 @@ static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteJsonC ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteResub ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteMM ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteMMGia ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -176,6 +177,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_jsonc", IoCommandWriteJsonC, 0 ); Cmd_CommandAdd( pAbc, "I/O", "&write_resub", IoCommandWriteResub, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_mm", IoCommandWriteMM, 0 ); Cmd_CommandAdd( pAbc, "I/O", "&write_mm", IoCommandWriteMMGia, 0 ); @@ -4395,6 +4397,54 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteJsonC( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + extern void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + char * pFileName; + int c; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL || !Abc_NtkHasMapping(pNtk) ) + { + fprintf( pAbc->Out, "No curent network or network is not mapped.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + pFileName = argv[globalUtilOptind]; + Jsonc_WriteTest( pNtk, pFileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_jsonc [-ch] \n" ); + fprintf( pAbc->Err, "\t write the network in JSONC format\n" ); + fprintf( pAbc->Err, "\t-h : print the help message\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .jsonc)\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/ioJsonc.c b/src/base/io/ioJsonc.c index 52699b71a..52d1cd3d9 100644 --- a/src/base/io/ioJsonc.c +++ b/src/base/io/ioJsonc.c @@ -23,8 +23,10 @@ #include #include #include +#include #include "ioAbc.h" +#include "map/mio/mio.h" ABC_NAMESPACE_IMPL_START @@ -605,9 +607,147 @@ int Jsonc_ReadTest( char * pFileName ) return 0; } +static int Jsonc_ParseNameBit( const char * pName, char * pBase, int nBase ) +{ + const char * pOpen; + const char * pClose; + int nCopy; + if ( pBase && nBase > 0 ) + pBase[0] = '\0'; + if ( pName == NULL || pBase == NULL || nBase <= 1 ) + return 0; + pOpen = strrchr( pName, '[' ); + pClose = pOpen ? strchr( pOpen, ']' ) : NULL; + if ( pOpen && pClose && pClose > pOpen + 1 ) + { + nCopy = (int)(pOpen - pName); + if ( nCopy > nBase - 1 ) + nCopy = nBase - 1; + memcpy( pBase, pName, nCopy ); + pBase[nCopy] = '\0'; + return atoi( pOpen + 1 ); + } + strncpy( pBase, pName, nBase - 1 ); + pBase[nBase - 1] = '\0'; + return 0; +} +static const char * Jsonc_GetPortName( Abc_Obj_t * pObj ) +{ + if ( Abc_ObjIsCi(pObj) && Abc_NtkIsNetlist(pObj->pNtk) && Abc_ObjFanoutNum(pObj) ) + return Abc_ObjName( Abc_ObjFanout0(pObj) ); + if ( Abc_ObjIsCo(pObj) && Abc_NtkIsNetlist(pObj->pNtk) && Abc_ObjFaninNum(pObj) ) + return Abc_ObjName( Abc_ObjFanin0(pObj) ); + return Abc_ObjName(pObj); +} +static const char * Jsonc_GetNodeOutName( Abc_Obj_t * pObj ) +{ + static char Buffer[1024]; + if ( Abc_ObjFanoutNum(pObj) ) + { + Abc_Obj_t * pFan0 = Abc_ObjFanout0(pObj); + if ( Abc_ObjIsNet(pFan0) || Abc_ObjIsCo(pFan0) ) + return Abc_ObjName(pFan0); + } + if ( Abc_ObjName(pObj) ) + return Abc_ObjName(pObj); + snprintf( Buffer, sizeof(Buffer), "n%d", Abc_ObjId(pObj) ); + return Buffer; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) +{ + Vec_Ptr_t * vNodes; + Vec_Int_t * vObj2Num; + Abc_Obj_t * pObj; + FILE * pFile; + int i, Counter, Total; + assert( Abc_NtkHasMapping(p) ); + vNodes = Abc_NtkDfs2( p ); + vObj2Num = Vec_IntStartFull( Abc_NtkObjNumMax(p) ); + Total = Abc_NtkPiNum(p) + Vec_PtrSize(vNodes) + Abc_NtkPoNum(p); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Jsonc_WriteTest(): Cannot open output file \"%s\" for writing.\n", pFileName ); + Vec_IntFree( vObj2Num ); + Vec_PtrFree( vNodes ); + return; + } + fprintf( pFile, "{\n" ); + fprintf( pFile, " \"name\": \"%s\",\n", Abc_NtkName(p) ? Abc_NtkName(p) : "" ); + fprintf( pFile, " \"nodes\": [\n" ); + Counter = 0; + Abc_NtkForEachPi( p, pObj, i ) + { + char Name[1024]; + int Bit = Jsonc_ParseNameBit( Jsonc_GetPortName(pObj), Name, sizeof(Name) ); + Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter ); + fprintf( pFile, " {\n" ); + fprintf( pFile, " \"type\": \"pi\",\n" ); + fprintf( pFile, " \"name\": \"%s\",\n", Name ); + fprintf( pFile, " \"bit\": %d\n", Bit ); + fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," ); + } + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + { + Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData; + Mio_Pin_t * pPin; + int k; + assert( pGate != NULL ); + Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter ); + fprintf( pFile, " {\n" ); + fprintf( pFile, " \"type\": \"%s\",\n", Mio_GateReadName(pGate) ); + fprintf( pFile, " \"name\": \"%s\",\n", Jsonc_GetNodeOutName(pObj) ); + fprintf( pFile, " \"fanins\": [\n" ); + fprintf( pFile, " {\n" ); + for ( pPin = Mio_GateReadPins(pGate), k = 0; pPin; pPin = Mio_PinReadNext(pPin), k++ ) + { + Abc_Obj_t * pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pObj, k) ); + int FanId = Vec_IntEntry( vObj2Num, Abc_ObjId(pFanin) ); + assert( FanId >= 0 ); + fprintf( pFile, " \"%s\": { \"node\": %d }%s\n", Mio_PinReadName(pPin), FanId, Mio_PinReadNext(pPin) ? "," : "" ); + } + fprintf( pFile, " }\n" ); + fprintf( pFile, " ]\n" ); + fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," ); + } + Abc_NtkForEachPo( p, pObj, i ) + { + Abc_Obj_t * pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) ); + char Name[1024]; + int Bit = Jsonc_ParseNameBit( Jsonc_GetPortName(pObj), Name, sizeof(Name) ); + int FanId = Vec_IntEntry( vObj2Num, Abc_ObjId(pDriver) ); + assert( FanId >= 0 ); + fprintf( pFile, " {\n" ); + fprintf( pFile, " \"type\": \"PO\",\n" ); + fprintf( pFile, " \"name\": \"%s\",\n", Name ); + fprintf( pFile, " \"bit\": %d,\n", Bit ); + fprintf( pFile, " \"fanin\": { \"node\": %d", FanId ); + //if ( Abc_ObjIsNode(pDriver) && pDriver->pData != NULL ) + // fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pDriver->pData) ); + fprintf( pFile, " }\n" ); + fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," ); + } + fprintf( pFile, " ]\n" ); + fprintf( pFile, "}\n" ); + fclose( pFile ); + Vec_IntFree( vObj2Num ); + Vec_PtrFree( vNodes ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - From a8a58c63ba2046a7f1c4d23d915d939465debdaa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 14 Dec 2025 22:54:25 -0800 Subject: [PATCH 03/11] Updateing "topoexact". --- src/base/abci/abc.c | 14 +++++++++----- src/base/abci/abcTopo.c | 38 +++++++++++++++++++++++++++++++++++--- 2 files changed, 44 insertions(+), 8 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ba77e7ad7..2a96f7213 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -11406,15 +11406,15 @@ usage: ***********************************************************************/ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose ); Abc_Ntk_t * pNtkRes = NULL; Abc_Ntk_t * pTopo = NULL; int nTimeOut = 0; int nSeed = 0; char * pFileName = NULL; - int c, fVerbose = 0; + int c, fAndGates = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TSavh" ) ) != EOF ) { switch ( c ) { @@ -11440,6 +11440,9 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nSeed < 0 ) goto usage; break; + case 'a': + fAndGates ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11492,7 +11495,7 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } pTopo = Abc_NtkDupDfs( pNtkRes = pTopo ); Abc_NtkDelete( pNtkRes ); - pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fVerbose ); + pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fAndGates, fVerbose ); Abc_NtkDelete( pTopo ); if ( pNtkRes == NULL ) { @@ -11503,10 +11506,11 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: topoexact [-TS num] \n" ); + Abc_Print( -2, "usage: topoexact [-TS num] [-avh] \n" ); Abc_Print( -2, "\t exact synthesis solution for the fixed topology\n" ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-S : the random seed to randomize the SAT solver [default = %d]\n", nSeed ); + Abc_Print( -2, "\t-a : toggle using only and-gates (not xor-gates) [default = %s]\n", fAndGates ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : BLIF file name with the topology\n" ); diff --git a/src/base/abci/abcTopo.c b/src/base/abci/abcTopo.c index aa5bcf75e..ded7c069f 100644 --- a/src/base/abci/abcTopo.c +++ b/src/base/abci/abcTopo.c @@ -65,17 +65,18 @@ Abc_Ntk_t * Abc_NtkTopoDup( Abc_Ntk_t * pTopo, Vec_Wrd_t * vTruths ) } return pNew; } -Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose ) +Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose ) { Abc_Ntk_t * pRes = NULL; abctime clkTotal = Abc_Clock(); assert( Abc_NtkIsSopLogic(pTopo) ); // count how many variables we need to encode minterms of each node - Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0; + Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0, nTwoFaninNodes = 0; Abc_NtkForEachNode( pTopo, pObj, i ) { assert( Abc_ObjFaninNum(pObj) <= 6 ); nMints += 1 << Abc_ObjFaninNum(pObj); nNodeClausesPerMint += 2 * (1 << Abc_ObjFaninNum(pObj)); // two clauses per minterm + nTwoFaninNodes += (Abc_ObjFaninNum(pObj) == 2); } // derive input/output mapping of the original function, which will be synthesized Gia_Man_t * pGia = Abc_NtkClpGia( pFunc ); @@ -107,7 +108,38 @@ Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut // and add constraints that tell us that the value of the node's output agrees with the values of its fanins // while the value of the primary outputs is realized correctly by those internal nodes that drive the outputs int m, n, k, f, nTopoMints = 1 << Abc_NtkCiNum(pTopo); - int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint); + int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint) + + (fAndGates ? 2 * nTwoFaninNodes : 0); + if ( fAndGates && nTwoFaninNodes ) + { + // block XOR/XNOR truth tables for two-input nodes + int iMint = 0; + Abc_NtkForEachNode( pTopo, pObj, i ) + { + int nFanins = Abc_ObjFaninNum(pObj); + if ( nFanins == 2 ) + { + int pLits[4], j; + // forbid 0110 + pLits[0] = Abc_Var2Lit( iMint + 0, 0 ); + pLits[1] = Abc_Var2Lit( iMint + 1, 1 ); + pLits[2] = Abc_Var2Lit( iMint + 2, 1 ); + pLits[3] = Abc_Var2Lit( iMint + 3, 0 ); + for ( j = 0; j < 4; j++ ) + kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) ); + kissat_add( pSat, 0 ); + // forbid 1001 + pLits[0] = Abc_Var2Lit( iMint + 0, 1 ); + pLits[1] = Abc_Var2Lit( iMint + 1, 0 ); + pLits[2] = Abc_Var2Lit( iMint + 2, 0 ); + pLits[3] = Abc_Var2Lit( iMint + 3, 1 ); + for ( j = 0; j < 4; j++ ) + kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) ); + kissat_add( pSat, 0 ); + } + iMint += 1 << nFanins; + } + } for ( m = 0; m < nTopoMints; m++ ) { int iVarBase = nMints + m * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo)); // set PI values for this minterm From ee04349aee0a11d5ce0ad39b0de80e3cb366087e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 14 Dec 2025 23:06:33 -0800 Subject: [PATCH 04/11] Dumping symbol table when blasting by Yosys. --- src/base/wln/wlnRtl.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index 988a88047..05e8be4d0 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -178,7 +178,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * char * pFileTemp = "_temp_.aig"; int fRtlil = strstr(pFileName, ".rtl") != NULL; int fSVlog = strstr(pFileName, ".sv") != NULL; - sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; %saigmap; write_aiger %s\"", + sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; %saigmap; write_aiger -symbols %s\"", Wln_GetYosysName(), fRtlil ? "read_rtlil" : "read_verilog", pDefines ? "-D" : "", From 15abe445f48a5207d3ec6648e856eb138d16d7b6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 15 Dec 2025 17:15:46 -0800 Subject: [PATCH 05/11] Updates to the jsonc writer. --- src/base/io/ioJsonc.c | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/base/io/ioJsonc.c b/src/base/io/ioJsonc.c index 52d1cd3d9..90cc52b65 100644 --- a/src/base/io/ioJsonc.c +++ b/src/base/io/ioJsonc.c @@ -707,8 +707,8 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) assert( pGate != NULL ); Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter ); fprintf( pFile, " {\n" ); - fprintf( pFile, " \"type\": \"%s\",\n", Mio_GateReadName(pGate) ); - fprintf( pFile, " \"name\": \"%s\",\n", Jsonc_GetNodeOutName(pObj) ); + fprintf( pFile, " \"type\": \"%s\",\n", "instance" ); + fprintf( pFile, " \"name\": \"%s\",\n", Mio_GateReadName(pGate) ); fprintf( pFile, " \"fanins\": [\n" ); fprintf( pFile, " {\n" ); for ( pPin = Mio_GateReadPins(pGate), k = 0; pPin; pPin = Mio_PinReadNext(pPin), k++ ) @@ -716,7 +716,10 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) Abc_Obj_t * pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pObj, k) ); int FanId = Vec_IntEntry( vObj2Num, Abc_ObjId(pFanin) ); assert( FanId >= 0 ); - fprintf( pFile, " \"%s\": { \"node\": %d }%s\n", Mio_PinReadName(pPin), FanId, Mio_PinReadNext(pPin) ? "," : "" ); + fprintf( pFile, " \"%s\": { \"node\": %d", Mio_PinReadName(pPin), FanId ); + if ( Abc_ObjIsNode(pFanin) && pFanin->pData != NULL ) + fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pFanin->pData) ); + fprintf( pFile, " }%s\n", Mio_PinReadNext(pPin) ? "," : "" ); } fprintf( pFile, " }\n" ); fprintf( pFile, " ]\n" ); @@ -734,8 +737,8 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) fprintf( pFile, " \"name\": \"%s\",\n", Name ); fprintf( pFile, " \"bit\": %d,\n", Bit ); fprintf( pFile, " \"fanin\": { \"node\": %d", FanId ); - //if ( Abc_ObjIsNode(pDriver) && pDriver->pData != NULL ) - // fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pDriver->pData) ); + if ( Abc_ObjIsNode(pDriver) && pDriver->pData != NULL ) + fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pDriver->pData) ); fprintf( pFile, " }\n" ); fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," ); } From 9a2cf907da07c38d266cf7db2ddadd82c602bb0a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 17 Dec 2025 15:05:12 -0800 Subject: [PATCH 06/11] Fix to the jsonc writer. --- src/base/io/ioJsonc.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/base/io/ioJsonc.c b/src/base/io/ioJsonc.c index 90cc52b65..43ce5c271 100644 --- a/src/base/io/ioJsonc.c +++ b/src/base/io/ioJsonc.c @@ -709,7 +709,7 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) fprintf( pFile, " {\n" ); fprintf( pFile, " \"type\": \"%s\",\n", "instance" ); fprintf( pFile, " \"name\": \"%s\",\n", Mio_GateReadName(pGate) ); - fprintf( pFile, " \"fanins\": [\n" ); + fprintf( pFile, " \"fanins\":\n" ); fprintf( pFile, " {\n" ); for ( pPin = Mio_GateReadPins(pGate), k = 0; pPin; pPin = Mio_PinReadNext(pPin), k++ ) { @@ -722,7 +722,7 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName ) fprintf( pFile, " }%s\n", Mio_PinReadNext(pPin) ? "," : "" ); } fprintf( pFile, " }\n" ); - fprintf( pFile, " ]\n" ); + //fprintf( pFile, " ]\n" ); fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," ); } Abc_NtkForEachPo( p, pObj, i ) From f8726e5e977b173e5450e67917c94655586f71d8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 17 Dec 2025 15:06:20 -0800 Subject: [PATCH 07/11] Fixing a compiler problem. --- src/aig/gia/giaDecGraph.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/aig/gia/giaDecGraph.cpp b/src/aig/gia/giaDecGraph.cpp index 0efbe7bf8..f467d4cdc 100644 --- a/src/aig/gia/giaDecGraph.cpp +++ b/src/aig/gia/giaDecGraph.cpp @@ -38,6 +38,7 @@ #include #include #include +#include #include "gia.h" #include "misc/vec/vecHash.h" From 1e9cc528be326f8f840b6730347687163def6797 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 18 Dec 2025 16:41:25 -0800 Subject: [PATCH 08/11] Temporarily commenting out this line which causes BLIF reader to fail. --- src/base/io/ioReadBlifMv.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 51ad65bec..3059d851b 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -746,7 +746,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p ) { char * pCur, * pPrev; int i, fComment = 0; - Io_MvReplaceBuffersByShorts( p->pBuffer ); + //Io_MvReplaceBuffersByShorts( p->pBuffer ); // parse the buffer into lines and remove comments Vec_PtrPush( p->vLines, p->pBuffer ); From 99bde47c574f13214c177c973d561de95857c317 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 18 Dec 2025 21:54:22 -0800 Subject: [PATCH 09/11] Adding callbacks to verification engines. --- src/proof/cec/cecProve.c | 98 ++++++++++++++++++++++++++++++++------- src/proof/pdr/pdr.h | 3 +- src/proof/pdr/pdrCore.c | 4 ++ src/proof/pdr/pdrSat.c | 5 +- src/proof/ssw/ssw.h | 2 + src/proof/ssw/sswRarity.c | 6 +++ src/sat/bmc/bmc.h | 6 ++- src/sat/bmc/bmcBmc3.c | 9 +++- src/sat/bmc/bmcBmcAnd.c | 13 +++++- src/sat/bmc/bmcBmcG.c | 3 +- 10 files changed, 126 insertions(+), 23 deletions(-) diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 1b5a0fa43..ff10e8cae 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -49,12 +49,52 @@ ABC_NAMESPACE_IMPL_START extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars ); extern int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ); +typedef struct Par_Share_t_ Par_Share_t; +typedef struct Par_ThData_t_ Par_ThData_t; +static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ); + #ifndef ABC_USE_PTHREADS int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } #else // pthreads are used +#define PAR_THR_MAX 8 +struct Par_Share_t_ +{ + volatile int fSolved; + volatile unsigned Result; + volatile int iEngine; +}; +typedef struct Par_ThData_t_ +{ + Gia_Man_t * p; + int iEngine; + int fWorking; + int nTimeOut; + int Result; + int fVerbose; + Par_Share_t * pShare; +} Par_ThData_t; +static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) +{ + Par_ThData_t * pThData = (Par_ThData_t *)pUser; + Par_Share_t * pShare = pThData ? pThData->pShare : NULL; + if ( pShare == NULL ) + return 0; + if ( fSolved ) + { + if ( pShare->fSolved == 0 ) + { + pShare->fSolved = 1; + pShare->Result = Result; + pShare->iEngine = pThData->iEngine; + } + return 0; + } + return pShare->fSolved != 0; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -70,7 +110,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in SeeAlso [] ***********************************************************************/ -int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) +int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par_ThData_t * pThData ) { abctime clk = Abc_Clock(); int RetValue = -1; @@ -84,6 +124,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) Ssw_RarSetDefaultParams( pPars ); pPars->TimeOut = nTimeOut; pPars->fSilent = 1; + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } RetValue = Ssw_RarSimulateGia( p, pPars ); } else if ( iEngine == 1 ) @@ -92,6 +137,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) Saig_ParBmcSetDefaultParams( pPars ); pPars->nTimeOut = nTimeOut; pPars->fSilent = 1; + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); RetValue = Saig_ManBmcScalable( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -103,6 +153,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) Pdr_ManSetDefaultParams( pPars ); pPars->nTimeOut = nTimeOut; pPars->fSilent = 1; + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); RetValue = Pdr_ManSolve( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -115,6 +170,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) pPars->fUseGlucose = 1; pPars->nTimeOut = nTimeOut; pPars->fSilent = 1; + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); RetValue = Saig_ManBmcScalable( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -127,6 +187,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) pPars->fUseAbs = 1; pPars->nTimeOut = nTimeOut; pPars->fSilent = 1; + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); RetValue = Pdr_ManSolve( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -140,10 +205,17 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose ) pPars->nFramesAdd = 1; // the number of additional frames pPars->fNotVerbose = 1; // silent pPars->nTimeOut = nTimeOut; // timeout in seconds + if ( pThData && pThData->pShare ) + { + pPars->pFuncProgress = Cec_SProveCallback; + pPars->pProgress = (void *)pThData; + } RetValue = Bmcg_ManPerform( p, pPars ); } else assert( 0 ); //while ( Abc_Clock() < clkStop ); + if ( pThData && pThData->pShare && RetValue != -1 ) + Cec_SProveCallback( (void *)pThData, 1, (unsigned)RetValue ); if ( fVerbose ) { printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); @@ -183,16 +255,6 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -#define PAR_THR_MAX 8 -typedef struct Par_ThData_t_ -{ - Gia_Man_t * p; - int iEngine; - int fWorking; - int nTimeOut; - int Result; - int fVerbose; -} Par_ThData_t; void * Cec_GiaProveWorkerThread( void * pArg ) { Par_ThData_t * pThData = (Par_ThData_t *)pArg; @@ -207,13 +269,13 @@ void * Cec_GiaProveWorkerThread( void * pArg ) assert( 0 ); return NULL; } - pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose ); + pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData ); pThData->fWorking = 0; } assert( 0 ); return NULL; } -void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread ) +void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) { int i, status; assert( nProcs <= PAR_THR_MAX ); @@ -225,6 +287,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int n ThData[i].fWorking = 0; ThData[i].Result = -1; ThData[i].fVerbose = fVerbose; + ThData[i].pShare = pShare; if ( !WorkerThread ) continue; status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); @@ -254,7 +317,9 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in abctime clkScorr = 0, clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; + Par_Share_t Share; int i, RetValue = -1, RetEngine = -2; + memset( &Share, 0, sizeof(Par_Share_t) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); if ( !fSilent && fVerbose ) @@ -264,7 +329,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in fflush( stdout ); assert( nProcs == 3 || nProcs == 5 ); - Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread ); + Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread, &Share ); // meanwhile, perform scorr Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); @@ -280,7 +345,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(p), Gia_ManAndNum(pScorr) ); Abc_PrintTime( 1, "Time", clkScorr ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL ); + Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL, &Share ); // meanwhile, perform scorr if ( Gia_ManAndNum(pScorr) < 100000 ) @@ -297,7 +362,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); Abc_PrintTime( 1, "Time", clkScorr2 ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL ); + Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL, &Share ); RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); // do something else @@ -338,4 +403,3 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 01de9f858..618724685 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -81,6 +81,8 @@ struct Pdr_Par_t_ int RunId; // PDR id in this run int(*pFuncStop)(int); // callback to terminate int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode + int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback + void * pProgress; // progress callback data abctime timeLastSolved; // the time when the last output was solved Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) char * pInvFileName; // invariable file name @@ -108,4 +110,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 5c93addd9..8727282dd 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -81,6 +81,8 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->timeLastSolved = 0; // last one solved pPars->pInvFileName = NULL; // invariant file name pPars->fBlocking = 0; // clause pushing with blocking + pPars->pFuncProgress = NULL; // progress/termination callback + pPars->pProgress = NULL; // progress callback data } /**Function************************************************************* @@ -1812,6 +1814,8 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) for ( k = 0; k < Saig_ManPoNum(pAig); k++ ) if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec + if ( pPars->pFuncProgress && (RetValue == 0 || RetValue == 1) ) + pPars->pFuncProgress( pPars->pProgress, 1, (unsigned)RetValue ); if ( pPars->fUseBridge ) Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" ); return RetValue; diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index b1a5b66c4..cf4fafd6c 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -306,6 +306,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) return -1; + if ( p->pPars->pFuncProgress && p->pPars->pFuncProgress( p->pPars->pProgress, 0, (unsigned)k ) ) + return -1; } else // check relative containment in terms of next states { @@ -342,6 +344,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr else return -1; } + if ( p->pPars->pFuncProgress && p->pPars->pFuncProgress( p->pPars->pProgress, 0, (unsigned)k ) ) + return -1; } clk = Abc_Clock() - clk; p->tSat += clk; @@ -392,4 +396,3 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index bb4ff7594..e59c9d4f5 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -115,6 +115,8 @@ struct Ssw_RarPars_t_ int nSolved; Abc_Cex_t * pCex; int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode + int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback + void * pProgress; // progress callback data }; typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 679d30666..08bb14941 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -115,6 +115,8 @@ void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p ) p->fSetLastState = 0; p->fVerbose = 0; p->fNotVerbose = 0; + p->pFuncProgress = NULL; + p->pProgress = NULL; } /**Function************************************************************* @@ -1007,6 +1009,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) timeLastSolved = Abc_Clock(); for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ ) { + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)r ) ) + goto finish; clk = Abc_Clock(); if ( fTryBmc ) { @@ -1019,6 +1023,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) // simulate for ( f = 0; f < pPars->nFrames; f++ ) { + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)(r * pPars->nFrames + f) ) ) + goto finish; Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); if ( fMiter ) { diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 67b31ca7a..1e6d51a24 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -148,6 +148,8 @@ struct Saig_ParBmc_t_ int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode int RunId; // BMC id in this run int(*pFuncStop)(int); // callback to terminate + int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback + void * pProgress; // progress callback data }; @@ -173,7 +175,9 @@ struct Bmc_AndPar_t_ int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs - + + int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback + void * pProgress; // progress callback data void (*pFuncOnFrameDone)(int, int, int); // callback on each frame status (frame, po, statuss) }; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 6f4080479..7e0a6cfdc 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1353,6 +1353,8 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->nFailOuts = 0; // the number of failed outputs p->nDropOuts = 0; // the number of timed out outputs p->timeLastSolved = 0; // time when the last one was solved + p->pFuncProgress = NULL; // progress/termination callback + p->pProgress = NULL; // progress callback data } /**Function************************************************************* @@ -1528,6 +1530,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) pPars->timeLastSolved = Abc_Clock(); for ( f = 0; f < pPars->nFramesMax; f++ ) { + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)f ) ) + goto finish; // stop BMC after exploring all reachable states if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) { @@ -1632,6 +1636,8 @@ clkOther += Abc_Clock() - clk2; Abc_Print( 1, "Bmc3 got callbacks.\n" ); goto finish; } + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)((f<<16) | i) ) ) + goto finish; // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; @@ -1663,6 +1669,8 @@ clkSatRun = Abc_Clock() - clk2; fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d %8d\n", f, i, Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC), Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) ); + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)((f<<16) | i) ) ) + goto finish; if ( p->pTime4Outs ) { abctime timeSince = Abc_Clock() - clkOne; @@ -1894,4 +1902,3 @@ finish: ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index b9c2db2cc..23e98ea1d 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -960,6 +960,8 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Gia_Man_t * pTemp; int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2; abctime clk = Abc_Clock(); + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) ) + return -1; p = Bmc_MnaAlloc(); sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap ); @@ -993,6 +995,11 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) // sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); for ( f = 0; f < nFramesMax; f++ ) { + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)f ) ) + { + RetValue = -1; + break; + } if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) { // create another slice @@ -1000,6 +1007,11 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) // try solving the outputs for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) { + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)i ) ) + { + RetValue = -1; + break; + } Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i); if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) continue; @@ -1097,4 +1109,3 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c index e6205b19c..af2da1e2e 100644 --- a/src/sat/bmc/bmcBmcG.c +++ b/src/sat/bmc/bmcBmcG.c @@ -445,6 +445,8 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { pPars->nProcs = 1; + if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) ) + return -1; return Bmcg_ManPerformOne( pGia, pPars ); } @@ -454,4 +456,3 @@ int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ABC_NAMESPACE_IMPL_END - From c327b8312725bfb87d1e5c27cd7985549af4b6a2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 18 Dec 2025 23:07:11 -0800 Subject: [PATCH 10/11] Command "solver". --- src/base/cmd/cmd.c | 121 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 121 insertions(+) diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 20d0f0c38..a343c6789 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -66,6 +66,7 @@ static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int CmdCommandSolver ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -121,6 +122,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "capo", CmdCommandCapo, 0 ); Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 ); Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 ); + Cmd_CommandAdd( pAbc, "Various", "&solver", CmdCommandSolver, 0 ); Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 ); } @@ -2806,6 +2808,125 @@ usage: return 1; } +/**Function******************************************************************** + + Synopsis [Calls Capo internally.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int CmdCommandSolver( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine ); + FILE * pFile; + char Command[1000]; + char TempFileName[100]; + unsigned int RandomNum; + int i; + + // Check for help flags + if ( argc > 1 ) + { + if ( strcmp( argv[1], "-h" ) == 0 ) + goto usage; + if ( strcmp( argv[1], "-?" ) == 0 ) + goto usage; + } + + // Check if AIG is available + if ( pAbc->pGia == NULL ) + { + fprintf( pAbc->Err, "The current AIG is not available.\n" ); + goto usage; + } + + // Check if solver binary exists in current directory or PATH + char * pSolverName; + if ( (pFile = fopen( "./solver", "r" )) != NULL ) + { + pSolverName = "./solver"; + fclose( pFile ); + } + else + { + // Check if solver exists in PATH + char CheckCommand[100]; + sprintf( CheckCommand, "which solver > /dev/null 2>&1" ); + if ( system( CheckCommand ) == 0 ) + { + pSolverName = "solver"; + } + else + { + fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" ); + goto usage; + } + } + + // Generate random 8-hex-character temporary filename + RandomNum = (unsigned int)(ABC_PTRUINT_T)pAbc ^ + (unsigned int)(ABC_PTRUINT_T)pAbc->pGia ^ + (unsigned int)time(NULL) ^ + (unsigned int)getpid(); + sprintf( TempFileName, "%08X.aig", RandomNum ); + + // Write the current AIG to the temporary file + Gia_AigerWrite( pAbc->pGia, TempFileName, 0, 0, 1 ); + + // Verify the file was created successfully + if ( (pFile = fopen( TempFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Failed to create temporary AIG file \"%s\".\n", TempFileName ); + return 1; + } + fclose( pFile ); + + // Build the command string + sprintf( Command, "%s", pSolverName ); + + // Add all user arguments + for ( i = 1; i < argc; i++ ) + { + strcat( Command, " " ); + strcat( Command, argv[i] ); + } + + // Add the AIG filename at the end + strcat( Command, " " ); + strcat( Command, TempFileName ); + + // Debug: Show what command is being executed + fprintf( pAbc->Out, "Executing command: %s\n", Command ); + + // Execute the solver command + if ( system( Command ) == -1 ) + { + fprintf( pAbc->Err, "The following command has failed:\n" ); + fprintf( pAbc->Err, "\"%s\"\n", Command ); + unlink( TempFileName ); + return 1; + } + + // Clean up the temporary file + unlink( TempFileName ); + + return 0; + +usage: + fprintf( pAbc->Err, "\tusage: &solver \n"); + fprintf( pAbc->Err, "\t run the external solver binary on the current AIG\n" ); + fprintf( pAbc->Err, "\t-h : print the command usage\n" ); + fprintf( pAbc->Err, "\t : arguments to pass to the solver\n" ); + fprintf( pAbc->Err, "\t The current AIG will be written to a temporary file\n" ); + fprintf( pAbc->Err, "\t and passed as the last argument to the solver.\n" ); + fprintf( pAbc->Err, "\t Example: solver -h\n" ); + return 1; +} + /**Function******************************************************************** Synopsis [Print the version string.] From 64637b8395a94aa68e67b211d4ecc21840accde1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Dec 2025 20:32:11 -0800 Subject: [PATCH 11/11] Adding an option to &cec against a previous saved AIG. --- src/base/abci/abc.c | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2a96f7213..33323687f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34838,10 +34838,7 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } if ( fClear && pAbc->pGiaSaved != NULL ) - { Gia_ManStopP( &pAbc->pGiaSaved ); - return 0; - } if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) ) return 0; if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) ) @@ -42276,10 +42273,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pFile; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; char ** pArgvNew; - int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; + int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxytvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdbasxytvwh" ) ) != EOF ) { switch ( c ) { @@ -42314,6 +42311,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDualOutput ^= 1; break; + case 'b': + fSavedSpec ^= 1; + break; case 'a': fDumpMiter ^= 1; break; @@ -42444,6 +42444,16 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } } + else if ( fSavedSpec ) + { + if ( pAbc->pGiaSaved == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no saved specification.\n" ); + return 1; + } + pGias[0] = pAbc->pGia; + pGias[1] = pAbc->pGiaSaved; + } else { char * FileName, * pTemp; @@ -42565,17 +42575,19 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pGias[0] != pAbc->pGia ) Gia_ManStop( pGias[0] ); - Gia_ManStop( pGias[1] ); + if ( pGias[1] != pAbc->pGiaSaved ) + Gia_ManStop( pGias[1] ); return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxytvwh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-nmdbasxytvwh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); + Abc_Print( -2, "\t-b : toggle using saved specification [default = %s]\n", fSavedSpec? "yes":"no"); Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no"); Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNewX? "yes":"no");