From 362661f00d0ee8b8f15feb6dd2d14c10c4c03640 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 10 Dec 2025 14:12:22 -0800 Subject: [PATCH] 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; }