luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master' into acd66

This commit is contained in:
aletempiac 2024-04-11 19:02:29 +02:00
parent 0c905f873b ca78f5e6e5
commit 045803dcb8
6 changed files with 312 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/aig/gia/giaEquiv.c
View File

@ -715,6 +715,30 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Obj_t * Gia_MakeRandomChoice( Gia_Man_t * p, int iRepr )
{
int iTemp, Rand, Count = 0;
Gia_ClassForEachObj( p, iRepr, iTemp )
Count++;
Rand = rand() % Count;
Count = 0;
Gia_ClassForEachObj( p, iRepr, iTemp )
if ( Count++ == Rand )
break;
return Gia_ManObj(p, iTemp);
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@ -735,7 +759,7 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) )
{
int iTemp, iRepr = Gia_ObjId(p, pRepr);
Gia_Obj_t * pRepr2 = Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) );
Gia_Obj_t * pRepr2 = vMap ? Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ) : Gia_MakeRandomChoice(p, iRepr);
Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 );
Gia_ClassForEachObj( p, iRepr, iTemp )
{
@ -751,12 +775,13 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p )
Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom )
{
Vec_Int_t * vMap;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
if ( fRandom ) srand(time(NULL));
if ( !p->pReprs && p->pSibls )
{
int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
@ -789,7 +814,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p )
break;
if ( i == Gia_ManObjNum(p) )
return Gia_ManDup( p );
vMap = Gia_ManChoiceMinLevel( p );
vMap = fRandom ? NULL : Gia_ManChoiceMinLevel( p );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
@ -805,7 +830,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Vec_IntFree( vMap );
Vec_IntFreeP( &vMap );
return pNew;
}

14
src/aig/gia/giaSupps.c
View File

@ -572,6 +572,10 @@ int Supp_FindNextDiv( Supp_Man_t * p, int Pair )
iDiv1 = iDiv1 == -1 ? ABC_INFINITY : iDiv1;
iDiv2 = iDiv2 == -1 ? ABC_INFINITY : iDiv2;
iDiv = Abc_MinInt( iDiv1, iDiv2 );
// return -1 if the pair cannot be distinguished by any divisor
// in this case the original resub problem has no solution
if ( iDiv == ABC_INFINITY )
return -1;
assert( iDiv >= 0 && iDiv < Vec_IntSize(p->vCands) );
return iDiv;
}
@ -582,6 +586,8 @@ int Supp_ManRandomSolution( Supp_Man_t * p, int iSet, int fVerbose )
{
int Pair = Supp_ComputePair( p, iSet );
int iDiv = Supp_FindNextDiv( p, Pair );
if ( iDiv == -1 )
return -1;
iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose );
if ( Supp_SetFuncNum(p, iSet) > 0 )
Vec_IntPush( p->vTempSets, iSet );
@ -883,6 +889,10 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t *
{
Supp_ManAddPatternsFunc( p, i );
iSet = Supp_ManRandomSolution( p, 0, fVeryVerbose );
if ( iSet == -1 ) {
Supp_ManDelete( p );
return NULL;
}
for ( r = 0; r < p->nRounds; r++ )
{
if ( fVeryVerbose )
@ -898,6 +908,10 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t *
iBest = iSet;
}
iSet = Supp_ManReconstruct( p, fVeryVerbose );
if ( iSet == -1 ) {
Supp_ManDelete( p );
return NULL;
}
}
if ( fVeryVerbose )
printf( "Matrix size %d.\n", Vec_PtrSize(p->vMatrix) );

2
src/base/abc/abc.h
View File

@ -841,7 +841,7 @@ extern ABC_DLL void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t
extern ABC_DLL void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
extern ABC_DLL void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose );
extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose );
extern ABC_DLL void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
extern ABC_DLL void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
extern ABC_DLL void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );

112
src/base/abci/abc.c
View File

@ -405,6 +405,7 @@ static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9WriteLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Pms ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MuxProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1183,6 +1184,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&wlut", Abc_CommandAbc9WriteLut, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&ps", Abc_CommandAbc9Ps, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&pfan", Abc_CommandAbc9PFan, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&pms", Abc_CommandAbc9Pms, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&profile", Abc_CommandAbc9MuxProfile, 0 );
@ -2022,14 +2024,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fListNodes;
int fProfile;
int fOutputs;
int fVerbose;
// set defaults
fListNodes = 0;
fProfile = 1;
fOutputs = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "npvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "npovh" ) ) != EOF )
{
switch ( c )
{
@ -2039,6 +2043,9 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fProfile ^= 1;
break;
case 'o':
fOutputs ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -2079,14 +2086,15 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// process all COs
Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fVerbose );
Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fOutputs, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: print_level [-npvh] <node>\n" );
Abc_Print( -2, "usage: print_level [-npovh] <node>\n" );
Abc_Print( -2, "\t prints information about node level and cone size\n" );
Abc_Print( -2, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
Abc_Print( -2, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
Abc_Print( -2, "\t-o : toggles printing output levels [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\tnode : (optional) one node to consider\n");
@ -9310,11 +9318,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars );
extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName );
int c, fKissat = 0, fKissat2 = 0;
extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize );
int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "INTadconugklvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklvh" ) ) != EOF )
{
switch ( c )
{
@ -9351,9 +9360,23 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->RuntimeLim < 0 )
goto usage;
break;
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
GateSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( GateSize < 0 )
goto usage;
break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
case 'b':
fUseNands ^= 1;
break;
case 'd':
pPars->fDynConstr ^= 1;
break;
@ -9401,7 +9424,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
if ( pPars->nVars >= 2 && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
@ -9416,7 +9439,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
return 1;
}
if ( fKissat )
if ( fUseNands )
Exa_ManExactSynthesis7( pPars, GateSize );
else if ( fKissat )
Exa_ManExactSynthesis4( pPars );
else if ( fKissat2 )
Exa_ManExactSynthesis5( pPars );
@ -9427,12 +9452,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: twoexact [-INT <num>] [-adconugklvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-abdconugklvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-G <num> : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize );
Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
@ -32499,6 +32526,57 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Pms( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Obj_t * pObj;
int c, nSat = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PFan(): There is no AIG.\n" );
return 1;
}
printf( "Status of %d outputs of the miter: ", Gia_ManPoNum(pAbc->pGia) );
Gia_ManForEachPo( pAbc->pGia, pObj, c )
{
printf( "%d", c );
if ( pAbc->pGia->vNamesOut )
printf( "(%s)", (char *)Vec_PtrEntry(pAbc->pGia->vNamesOut, c) );
printf( "=%s ", Gia_ObjFaninLit0p(pAbc->pGia, pObj) == 0 ? "unsat":"sat" );
nSat += Gia_ObjFaninLit0p(pAbc->pGia, pObj) != 0;
}
printf( "\n" );
printf( "Total sat = %d. Total unsat = %d.\n", nSat, Gia_ManPoNum(pAbc->pGia)-nSat );
return 0;
usage:
Abc_Print( -2, "usage: &pms [-h]\n" );
Abc_Print( -2, "\t prints miter status after SAT sweeping\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -44038,14 +44116,14 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom );
Gia_Man_t * pTemp;
Dch_Pars_t Pars, * pPars = &Pars;
int c, fMinLevel = 0, fEquiv = 0;
int c, fMinLevel = 0, fEquiv = 0, fRandom = 0;
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxyvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremngcxyvh" ) ) != EOF )
{
switch ( c )
{
@ -44103,6 +44181,9 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMinLevel ^= 1;
break;
case 'n':
fRandom ^= 1;
break;
case 'g':
pPars->fUseGia ^= 1;
break;
@ -44147,14 +44228,14 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
{
pTemp = Gia_ManPerformDch( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
if ( fMinLevel )
pTemp = Gia_ManEquivReduce2( pAbc->pGia );
if ( fMinLevel || fRandom )
pTemp = Gia_ManEquivReduce2( pAbc->pGia, fRandom );
}
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxyvh]\n" );
Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremngcxyvh]\n" );
Abc_Print( -2, "\t computes structural choices using a new approach\n" );
Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@ -44165,7 +44246,8 @@ usage:
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" );
Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fRandom? "yes": "no" );
Abc_Print( -2, "\t-n : toggle selecting random choices while merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );

12
src/base/abci/abcPrint.c
View File

@ -1228,11 +1228,19 @@ char * Abc_NodeGetPrintName( Abc_Obj_t * pObj )
}
return Abc_ObjName(nPos == 1 ? pFanout : pObj);
}
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose )
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose )
{
Abc_Obj_t * pNode;
int i, k, Length;
if ( fOutputs )
{
Abc_NtkLevel(pNtk);
printf( "Outputs by level: " );
Abc_NtkForEachCo( pNtk, pNode, k )
printf( "%d=%d ", k, Abc_ObjFanin0(pNode)->Level );
printf( "\n" );
return;
}
if ( fListNodes )
{
int nLevels;

162
src/sat/bmc/bmcMaj.c
View File

@ -3724,10 +3724,170 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
if ( pMini ) Mini_AigStop( pMini );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Exa7_AddClause( FILE * pFile, int * pLits, int nLits )
{
int i, k = 0;
for ( i = 0; i < nLits; i++ ) {
if ( pLits[i] == 1 )
return 0;
else if ( pLits[i] == 0 )
continue;
else
pLits[k++] = pLits[i];
}
nLits = k;
assert( nLits > 0 );
if ( pFile )
{
for ( i = 0; i < nLits; i++ )
fprintf( pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
fprintf( pFile, "0\n" );
}
if ( 0 )
{
for ( i = 0; i < nLits; i++ )
fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i])-1 );
fprintf( stdout, "\n" );
}
return 1;
}
static inline int Exa7_AddClause4( FILE * pFile, int Lit0, int Lit1, int Lit2, int Lit3 )
{
int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
return Exa7_AddClause( pFile, pLits, 4 );
}
int Exa7_GetVar( int n, int i, int j, int m )
{
return 1 + n*n*m + n*i + j;
}
int Exa7_ManGenCnf( char * pFileName, word * pTruth, int nVars, int nNodes, int GateSize )
{
int m, n, v, k, nV = nVars + nNodes, nMints = 1 << nVars, nClas = 0;
int pVars[32] = {0}; assert( nVars + nNodes + 1 < 32 );
FILE * pFile = fopen( pFileName, "wb" );
fputs( "p cnf \n", pFile );
for ( m = 0; m < nMints; m++ )
{
for ( v = 0; v < nVars; v++ )
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, v, v, m), ((m >> v)&1)==0), 0, 0, 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, nV-1, nV-1, m), ((pTruth[0] >> m)&1)==0), 0, 0, 0 );
for ( n = nVars; n < nV; n++ )
{
int iValNode = Exa7_GetVar(nV, n, n, m);
for ( v = 0; v < n; v++ )
{
int iParVar = Exa7_GetVar(nV, v, n, 0); // v < n
int iFanVar = Exa7_GetVar(nV, n, v, m);
int iValFan = Exa7_GetVar(nV, v, v, m);
// iFanVar = ~iParVar | iValFan
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 1), Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iParVar, 0), 0, 0 );
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iValFan, 1), 0, 0 );
// iParVar & ~iValFan => iValNode
nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), Abc_Var2Lit(iValNode, 0), 0 );
pVars[v] = Abc_Var2Lit(iFanVar, 1);
}
pVars[v] = Abc_Var2Lit(iValNode, 1);
// (iFanVar0 & iFanVar1 & iFanVar2) => ~iValNode
nClas += Exa7_AddClause( pFile, pVars, n+1 );
}
}
for ( n = nVars; n < nV; n++ ) {
for ( v = 0; v < n; v++ )
pVars[v] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 0); // v < n
nClas += Exa7_AddClause( pFile, pVars, n );
if ( GateSize ) {
int Total = 1 << n, Limit = GateSize + 1;
for ( m = 0; m < Total; m++ )
{
if ( Abc_TtCountOnes((word)m) != Limit )
continue;
for ( k = v = 0; v < n; v++ )
if ( (m >> v) & 1 )
pVars[k++] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 1);
assert( k == Limit );
nClas += Exa7_AddClause( pFile, pVars, Limit );
}
}
}
rewind( pFile );
fprintf( pFile, "p cnf %d %d", nMints * nV * nV, nClas );
fclose( pFile );
return nClas;
}
void Exa_ManDumpVerilog( Vec_Int_t * vValues, int nVars, int nNodes, int GateSize, word * pTruth )
{
FILE * pFile;
char Buffer[1000];
char FileName[1100];
int v, n, k, nV = nVars+nNodes;
Extra_PrintHexadecimalString( Buffer, (unsigned *)pTruth, nVars );
sprintf( FileName, "func%s_%d_%d.v", Buffer, GateSize, nNodes );
pFile = fopen( FileName, "wb" );
fprintf( pFile, "// Realization of the %d-input function %s using %d NAND gates:\n", nVars, Buffer, nNodes );
fprintf( pFile, "module func%s_%d_%d ( input", Buffer, GateSize, nNodes );
for ( v = 0; v < nVars; v++ )
fprintf( pFile, " %c,", 'a'+v );
fprintf( pFile, " output out );\n" );
for ( n = nVars; n < nV; n++ ) {
int nFans = 0;
for ( v = 0; v < n; v++ )
nFans += Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0));
fprintf( pFile, " wire %c = ~(", 'a'+n );
for ( k = v = 0; v < n; v++ )
if ( Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) )
fprintf( pFile, "%c%s", 'a'+v, ++k < nFans ? " & ":"" );
fprintf( pFile, ");\n" );
}
fprintf( pFile, " assign out = %c;\n", 'a'+nV-1 );
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
printf( "Solution was dumped into file \"%s\".\n", FileName );
}
void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize )
{
abctime clkTotal = Abc_Clock();
int v, n, nMints = 1 << pPars->nVars;
int nV = pPars->nVars + pPars->nNodes;
word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
Vec_Int_t * vValues = NULL;
char * pFileNameIn = "_temp_.cnf";
char * pFileNameOut = "_temp_out.cnf";
int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize );
if ( pPars->fVerbose )
printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );
vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, pPars->RuntimeLim, pPars->fVerbose );
if ( pPars->fVerbose && vValues ) {
printf( " " );
for ( n = 0; n < nV; n++ )
printf( "%2d ", n );
printf( "\n" );
for ( n = pPars->nVars; n < nV; n++, printf("\n") ) {
printf( "%2d : ", n );
for ( v = 0; v < n; v++ )
printf( " %c ", Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ? '1':'.' ); // v < n
}
}
if ( vValues )
Exa_ManDumpVerilog( vValues, pPars->nVars, pPars->nNodes, GateSize, pTruth );
Vec_IntFreeP( &vValues );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END