Skip to content

Commit

Permalink
Merge pull request #316 from YosysHQ/povik/yosyshq-commands
Browse files Browse the repository at this point in the history 
Pull command changes from YosysHQ fork
  • Loading branch information
@alanminko
alanminko authored Aug 8, 2024
2 parents e6b36cb + 5444cf2 commit 0129b4c
Show file tree
Hide file tree
Showing 19 changed files with 1,045 additions and 132 deletions.
2 changes: 1 addition & 1 deletion src/aig/saig/saig.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ extern Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * v
extern int Saig_ManDetectConstrTest( Aig_Man_t * p );
extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigConstr2.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
// -- jlong -- begin
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );
Expand Down
5 changes: 3 additions & 2 deletions src/aig/saig/saigConstr2.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -939,7 +939,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nCo
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
Expand Down Expand Up @@ -1000,7 +1000,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo

// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
if ( fSeqCleanup )
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}

Expand Down
61 changes: 52 additions & 9 deletions src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29343,31 +29343,35 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtkRes;
int c;
int nFrames;
int nConfs;
int nProps;
int fRemove;
int fPurge;
int fStruct;
int fInvert;
int fOldAlgo;
int fVerbose;
int nConstrs;
extern void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose );
extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange );

pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
nFrames = 1;
nConfs = 1000;
nProps = 1000;
fRemove = 0;
fPurge = 0;
fStruct = 0;
fInvert = 0;
fOldAlgo = 0;
fVerbose = 0;
nConstrs = -1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrpsiavh" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -29418,6 +29422,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRemove ^= 1;
break;
case 'p':
fPurge ^= 1;
break;
case 's':
fStruct ^= 1;
break;
Expand Down Expand Up @@ -29453,7 +29460,22 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Constraints are not defined.\n" );
return 0;
}
Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );

if ( fPurge )
{
Abc_Print( 1, "Constraints are removed.\n" );
pNtkRes = Abc_NtkMakeOnePo( pNtk, 0, Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) );
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
pNtk = Abc_FrameReadNtk(pAbc);
}
else
Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );
pNtk->nConstrs = 0;
return 0;
}
Expand Down Expand Up @@ -29498,7 +29520,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" );
Abc_Print( -2, "usage: constr [-FCPN num] [-rpisavh]\n" );
Abc_Print( -2, "\t a toolkit for constraint manipulation\n" );
Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" );
Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" );
Expand All @@ -29507,7 +29529,8 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
Abc_Print( -2, "\t-N num : manually set the last <num> POs to be constraints [default = %d]\n", nConstrs );
Abc_Print( -2, "\t-r : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" );
Abc_Print( -2, "\t-r : manually remove the constraints, converting them to POs [default = %s]\n", fRemove? "yes": "no" );
Abc_Print( -2, "\t-p : remove constraints instead of converting them to POs [default = %s]\n", fPurge? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" );
Abc_Print( -2, "\t-a : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" );
Expand Down Expand Up @@ -29687,14 +29710,16 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int fCompl;
int fVerbose;
int fSeqCleanup;
int c;
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fCompl = 0;
fVerbose = 0;
fSeqCleanup = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cvsh" ) ) != EOF )
{
switch ( c )
{
Expand All @@ -29704,6 +29729,9 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 's':
fSeqCleanup ^= 1;
break;
case 'h':
goto usage;
default:
Expand Down Expand Up @@ -29733,7 +29761,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsComb(pNtk) )
Abc_Print( 0, "The network is combinational.\n" );
// modify the current network
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose );
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose, fSeqCleanup );
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
Expand All @@ -29748,6 +29776,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" );
Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-s : toggle performing sequential cleanup [default = %s]\n", fSeqCleanup? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
Expand Down Expand Up @@ -30218,7 +30247,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -30339,9 +30368,21 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pInvFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" );
goto usage;
}
pPars->pCexFilePrefix = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'a':
pPars->fSolveAll ^= 1;
break;
case 'l':
pPars->fAnytime ^= 1;
break;
case 'x':
pPars->fStoreCex ^= 1;
break;
Expand Down Expand Up @@ -30446,7 +30487,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;

usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-X <prefix>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
Expand All @@ -30461,7 +30502,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" );
Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as <pref>*.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled");
Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-l : toggle anytime schedule when solving all outputs [default = %s]\n", pPars->fAnytime? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Expand Down
4 changes: 2 additions & 2 deletions src/base/abci/abcDar.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4682,15 +4682,15 @@ Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nPr
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose, fSeqCleanup );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
Expand Down
Loading

0 comments on commit 0129b4c

Please sign in to comment.