From 3bd528c0bff8c4d48e003c677bfae5881dbb7c33 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 11 Nov 2025 22:41:26 -0800 Subject: [PATCH] Experiments with exact synthesis. --- src/aig/gia/giaLutCas.c | 77 +++++++++++++++++++++++++++++++++++++---- src/aig/gia/giaQbf.c | 21 +++++++---- src/base/abci/abc.c | 51 +++++++++++++++++++++------ 3 files changed, 125 insertions(+), 24 deletions(-) diff --git a/src/aig/gia/giaLutCas.c b/src/aig/gia/giaLutCas.c index 1d1721ab0..7465ad18c 100644 --- a/src/aig/gia/giaLutCas.c +++ b/src/aig/gia/giaLutCas.c @@ -109,12 +109,21 @@ int Gia_ManLutCasGen_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_I int iLit1 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<pName = Abc_UtilStrsav( pPerm ); Vec_Int_t * vDatas = Vec_IntAlloc( nParams ); @@ -132,18 +141,72 @@ Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int f Vec_IntWriteEntry( vLits, k, Vec_IntEntry(vCtrls, (int)(*pCur++ - 'a')) ); Vec_IntWriteEntry( vLits, 0, Gia_ManLutCasGen_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize)) ); } - Gia_ManAppendCo( pNew, Vec_IntEntry(vLits, 0) ); + // if the AIG is given, create a miter + int iLit = Vec_IntEntry(vLits, 0); + if ( p ) { + assert( Gia_ManCiNum(p) == nVars ); + assert( Gia_ManCoNum(p) == 1 ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_Obj_t * pObj; int i; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Vec_IntEntry(vCtrls, i); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + iLit = Gia_ManAppendXor( pNew, iLit, Gia_ObjFanin0Copy(Gia_ManCo(p, 0)) ); + iLit = Abc_LitNot(iLit); + } + Gia_ManAppendCo( pNew, iLit ); Vec_IntFree( vDatas ); Vec_IntFree( vCtrls ); Vec_IntFree( vLits ); - ABC_FREE( pPerm ); + if ( fOwnPerm ) + ABC_FREE( pPerm ); return pNew; } +/* +int Gia_ManLutCasGenSolve( int nVars, int nLuts, int LutSize, char * pTtStr, int fVerbose ) +{ + extern Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll ); + assert( strlen(pTtStr) <= 1024 ); + word pTruth[64] = {0}; + int i, Id, nVars = Abc_TtReadHex( pTruth, pTtStr ); + assert( nVars <= 12 ); + int nParams = nLuts * (1 << LutSize); + Gia_Man_t * pCas = Gia_ManLutCasGen( NULL, NULL, nVars, nLuts, LutSize, 0, fVerbose ); + Gia_Man_t * pCofs = Gia_QbfQuantifyAll( pCas, nParams, 0, 0 ); + Gia_ManFree( pCas ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCofs, 8, 0, 0, 0, 0 ); + cadical_solver* pSat = cadical_solver_new(void); + cadical_solver_setnvars( pSat, pCnf->nVars ); + // add output literals + assert( Gia_ManCoNum(pCofs) == (1 << nVars) ); + Gia_ManForEachCoId( pCofs, Id, i ) { + int Lit = Abc_Var2Lit(pCnf->pVarNums[Id], Abc_TtGetBit(pTruth, i)); + int status = cadical_solver_addclause( pSat, &Lit, &Lit+1 ); + } + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !cadical_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) { + Cnf_DataFree( pCnf ); + return 0; + } + Cnf_DataFree( pCnf ); + Gia_ManFree( pCofs ); + int status = cadical_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + for ( i = 0; i < nLuts; i++, printf(" ") ) + for ( k = 0; k < (1 << LutSize); k++ ) { + int Value = cadical_solver_get_var_value(pSat, i*(1 << LutSize) + k); + printf( "%d", Value ); + } + cadical_solver_delete( pSat ); + return 1; +} +*/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 8af8c6c6f..08bc0bf5f 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -893,7 +893,7 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues ) SeeAlso [] ***********************************************************************/ -int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose ) +int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fSilent, int fVerbose ) { Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fCadical, fVerbose ); Gia_Man_t * pCof; @@ -939,9 +939,18 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i if ( RetValue == 0 ) { int nZeros = Vec_IntCountZero( p->vValues ); - printf( "Parameters: " ); + printf( "Parameters (%d): 0x", nPars ); assert( Vec_IntSize(p->vValues) == nPars ); - Vec_IntPrintBinary( p->vValues ); + //Vec_IntPrintBinary( p->vValues ); + while ( Vec_IntSize(p->vValues) % 4 ) + Vec_IntPush(p->vValues, 0); + for ( int i = Vec_IntSize(p->vValues)/4 - 1; i >= 0; i-- ) { + int Digit = Vec_IntEntry(p->vValues, 4*i+0); + Digit |= Vec_IntEntry(p->vValues, 4*i+1) << 1; + Digit |= Vec_IntEntry(p->vValues, 4*i+2) << 2; + Digit |= Vec_IntEntry(p->vValues, 4*i+3) << 3; + printf( "%x", Digit ); + } printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(p->vValues) - nZeros ); if ( nEncVars ) { @@ -956,9 +965,9 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i printf( "The problem aborted after %d conflicts. ", nConfLimit ); else if ( RetValue == -1 && nIterLimit ) printf( "The problem aborted after %d iterations. ", nIterLimit ); - else if ( RetValue == 1 ) + else if ( RetValue == 1 && !fSilent ) printf( "The problem is UNSAT after %d iterations. ", i ); - else + else if ( !fSilent ) printf( "The problem is SAT after %d iterations. ", i ); if ( fVerbose ) { @@ -967,7 +976,7 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat ); Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart ); } - else + else if ( !fSilent ) Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); Gia_QbfFree( p ); return RetValue; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4c712e94b..1d2ad8a1a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10924,7 +10924,7 @@ usage: Abc_Print( -2, "\t-r : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" ); Abc_Print( -2, "\t-f : toggle fixing LUT inputs in cascade mapping [default = %s]\n", pPars->fLutInFixed ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); - Abc_Print( -2, "\t-c : toggle using CaDiCal 2.2.0-rc1 by Armin Biere [default = %s]\n", pPars->fCadical ? "yes" : "no" ); + Abc_Print( -2, "\t-c : toggle using CaDiCal 2.2.0-rc1 by Armin Biere et al [default = %s]\n", pPars->fCadical ? "yes" : "no" ); Abc_Print( -2, "\t-k : toggle using Kissat 4.0.2 by Armin Biere [default = %s]\n", pPars->fKissat ? "yes" : "no" ); Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" ); Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" ); @@ -51340,7 +51340,7 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); extern void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ); - extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose ); + extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fSilent, int fVerbose ); int c, nPars = -1; int nIterLimit = 0; int nConfLimit = 0; @@ -51350,9 +51350,10 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) int fDumpCnf2 = 0; int fGlucose = 0; int fCadical = 0; + int fSilent = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegcsvh" ) ) != EOF ) { switch ( c ) { @@ -51423,6 +51424,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fCadical ^= 1; break; + case 's': + fSilent ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -51457,11 +51461,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) else if ( fDumpCnf2 ) Gia_QbfDumpFileInv( pAbc->pGia, nPars ); else - Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fCadical, fVerbose ); + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fCadical, fSilent, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICTK num] [-degcvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICTK num] [-degcsvh]\n" ); Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" ); Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars ); Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit ); @@ -51472,6 +51476,7 @@ usage: Abc_Print( -2, "\t-e : toggle dumping QDIMACS file instead of solving (original QBF) [default = %s]\n", fDumpCnf2? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere [default = %s]\n", fCadical? "yes": "no" ); + Abc_Print( -2, "\t-s : no printout except when a solution is found [default = %s]\n", fSilent? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n\n"); Abc_Print( -2, "\t As an example of using this command, consider specification (the three-input AND-gate) and implementation\n"); @@ -51721,16 +51726,17 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int fVerbose ); - int nVars = 8; + extern Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose ); + int nVars = 0; int nLuts = 2; int LutSize = 6; int Seed = 0; int fVerbose = 0; int c; + char * pPermStr = NULL; Gia_Man_t * pTemp; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NMKSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NMKSPvh" ) ) != EOF ) { switch ( c ) { @@ -51778,6 +51784,15 @@ int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Seed < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a string.\n" ); + goto usage; + } + pPermStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'v': fVerbose ^= 1; break; @@ -51787,6 +51802,19 @@ int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( pAbc->pGia == NULL && nVars == 0 ) + { + Abc_Print( -1, "The number of inputs (%d) should be specified on the command line.\n", nVars ); + return 1; + } + if ( pAbc->pGia ) + nVars = Gia_ManCiNum(pAbc->pGia); + if ( pPermStr && (nLuts * LutSize != (int)strlen(pPermStr)) ) + { + Abc_Print( -1, "Permutation \"%s\" has %d symbols instead of expected %d = %d * %d symbols (LutSize * nLuts).\n", + pPermStr, (int)strlen(pPermStr), LutSize * nLuts, LutSize, nLuts ); + return 1; + } if ( nVars <= LutSize ) { Abc_Print( -1, "The number of inputs (%d) should be more than LUT size (%d).\n", nVars, LutSize ); @@ -51812,17 +51840,18 @@ int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function with %d variables is too large for a cascade composed of %d connected %d-LUTs.\n", nVars, nLuts, LutSize ); return 1; } - pTemp = Gia_ManLutCasGen( nVars, nLuts, LutSize, Seed, fVerbose ); + pTemp = Gia_ManLutCasGen( pAbc->pGia, pPermStr, nVars, nLuts, LutSize, Seed, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &genlutcas[-NMKS num] [-vh]\n" ); - Abc_Print( -2, "\t generates single-rail LUT cascade\n" ); + Abc_Print( -2, "usage: &genlutcas[-NMKS num] [-P str] [-vh]\n" ); + Abc_Print( -2, "\t generates a miter for synthesizing the LUT cascade\n" ); Abc_Print( -2, "\t-N num : the number of primary inputs [default = %d]\n", nVars ); Abc_Print( -2, "\t-M num : the number of LUTs [default = %d]\n", nLuts ); Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", LutSize ); Abc_Print( -2, "\t-S num : the random seed [default = %d]\n", Seed ); + Abc_Print( -2, "\t-P str : variable permutation (for example, \"abcd_aef\" for S44) [default = %s]\n", pPermStr ? pPermStr : "unused" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1;