Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into acd66
Browse files Browse the repository at this point in the history
  • Loading branch information
@aletempiac
aletempiac committed Apr 11, 2024
2 parents 0c905f8 + ca78f5e commit 045803d
Show file tree
Hide file tree
Showing 6 changed files with 312 additions and 23 deletions.
33 changes: 29 additions & 4 deletions src/aig/gia/giaEquiv.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.]
Expand All @@ -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 )
{
Expand All @@ -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) );
Expand Down Expand Up @@ -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 );
Expand All @@ -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;
}

Expand Down
14 changes: 14 additions & 0 deletions src/aig/gia/giaSupps.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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 );
Expand Down Expand Up @@ -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 )
Expand All @@ -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) );
Expand Down
2 changes: 1 addition & 1 deletion src/base/abc/abc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
Expand Down
112 changes: 97 additions & 15 deletions src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
Expand Down Expand Up @@ -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 );
Expand Down Expand Up @@ -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 )
{
Expand All @@ -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;
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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 )
{
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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 );
Expand All @@ -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" );
Expand Down Expand Up @@ -32499,6 +32526,57 @@ int Abc_CommandAbc9PFan( Abc_Frame_t * pAbc, int argc, char ** argv )
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 []
Expand Down Expand Up @@ -44038,14 +44116,14 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
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 )
{
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 );
Expand All @@ -44165,7 +44246,8 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
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" );
Expand Down
12 changes: 10 additions & 2 deletions src/base/abci/abcPrint.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading

0 comments on commit 045803d

Please sign in to comment.