mirror of https://github.com/YosysHQ/abc.git
Experiments with exact synthesis.
This commit is contained in:
Alan Mishchenko
parent
38c2bec1ff
commit
3bd528c0bf
|
|
@ -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<<iCtrl));
|
||||
return Gia_ManAppendMux( pNew, Vec_IntEntry(vCtrls, iCtrl), iLit1, iLit0 );
|
||||
}
|
||||
Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
|
||||
Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
|
||||
{
|
||||
srand(Seed);
|
||||
char * pPerm = Gia_LutCasPerm( nVars, nLuts, LutSize );
|
||||
if ( Seed )
|
||||
srand(Seed);
|
||||
else {
|
||||
struct timespec ts;
|
||||
clock_gettime(CLOCK_REALTIME, &ts);
|
||||
unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec);
|
||||
srand(seed);
|
||||
}
|
||||
int fOwnPerm = (pPermStr == NULL);
|
||||
char * pPerm = fOwnPerm ? Gia_LutCasPerm( nVars, nLuts, LutSize ) : pPermStr;
|
||||
int nParams = nLuts * (1 << LutSize);
|
||||
printf( "Generating AIG with %d parameters and %d inputs using fanin assignment %s.\n", nParams, nVars, pPerm );
|
||||
if ( fVerbose )
|
||||
printf( "Generating AIG with %d parameters and %d inputs using fanin assignment %s.\n", nParams, nVars, pPerm );
|
||||
Gia_Man_t * pNew = Gia_ManStart( nParams + nVars );
|
||||
pNew->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
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Reference in New Issue