summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abc.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r--src/base/abci/abc.c264
1 files changed, 246 insertions, 18 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 264b1df4..b8a9cefe 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -200,6 +200,7 @@ static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -218,6 +219,7 @@ static int Abc_CommandAbc8Write ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8ReadLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8PrintLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Check ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Pfan ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -458,6 +460,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
@@ -473,6 +476,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*wlogic", Abc_CommandAbc8WriteLogic, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*rlut", Abc_CommandAbc8ReadLut, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*plut", Abc_CommandAbc8PrintLut, 0 );
+ Cmd_CommandAdd( pAbc, "ABC8", "*check", Abc_CommandAbc8Check, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*ps", Abc_CommandAbc8Ps, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*pfan", Abc_CommandAbc8Pfan, 0 );
@@ -6357,7 +6361,7 @@ int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: topand [-h]\n" );
- fprintf( pErr, "\t AND-decomposition of single-output combinational miter\n" );
+ fprintf( pErr, "\t performs AND-decomposition of single-output combinational miter\n" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tname : the node name\n");
return 1;
@@ -14196,7 +14200,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fPartition;
int fMiter;
- extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -14850,14 +14854,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int RetValue;
- int fFlipBits;
+ int fAlignPol;
int fAndOuts;
int fVerbose;
int nConfLimit;
int nInsLimit;
int clk;
- extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -14865,13 +14869,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fFlipBits = 0;
+ fAlignPol = 0;
fAndOuts = 0;
fVerbose = 0;
nConfLimit = 100000;
nInsLimit = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
{
switch ( c )
{
@@ -14897,8 +14901,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInsLimit < 0 )
goto usage;
break;
- case 'f':
- fFlipBits ^= 1;
+ case 'p':
+ fAlignPol ^= 1;
break;
case 'a':
fAndOuts ^= 1;
@@ -14937,7 +14941,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
clk = clock();
- RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose );
+ RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fAlignPol, fAndOuts, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
{
@@ -14970,13 +14974,177 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" );
+ fprintf( pErr, "usage: dsat [-C num] [-I num] [-pavh]\n" );
fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
- fprintf( pErr, "\t-f : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" );
- fprintf( pErr, "\t-a : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" );
+ fprintf( pErr, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
+ fprintf( pErr, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int RetValue;
+ int c, clk;
+ int nAlgo;
+ int nPartSize;
+ int nConfPart;
+ int nConfTotal;
+ int fAlignPol;
+ int fSynthesize;
+ int fVerbose;
+
+ extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nAlgo = 0;
+ nPartSize = 10000;
+ nConfPart = 0;
+ nConfTotal = 1000000;
+ fAlignPol = 1;
+ fSynthesize = 0;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "APCpsvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nAlgo = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nAlgo < 0 )
+ goto usage;
+ break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nPartSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nPartSize < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfTotal = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfTotal < 0 )
+ goto usage;
+ break;
+ case 'p':
+ fAlignPol ^= 1;
+ break;
+ case 's':
+ fSynthesize ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ {
+ fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+
+ clk = clock();
+ RetValue = Abc_NtkPartitionedSat( pNtk, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
+ // verify that the pattern is correct
+ if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
+ {
+ //int i;
+ //Abc_Obj_t * pObj;
+ int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
+ if ( pSimInfo[0] != 1 )
+ printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+ free( pSimInfo );
+ /*
+ // print model
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ printf( "%d", (int)(pNtk->pModel[i] > 0) );
+ if ( i == 70 )
+ break;
+ }
+ printf( "\n" );
+ */
+ }
+
+ if ( RetValue == -1 )
+ printf( "UNDECIDED " );
+ else if ( RetValue == 0 )
+ printf( "SATISFIABLE " );
+ else
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+ PRT( "Time", clock() - clk );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: psat [-APC num] [-psvh]\n" );
+ fprintf( pErr, "\t solves the combinational miter using partitioning\n" );
+ fprintf( pErr, "\t (derives CNF from the current network and leave it unchanged)\n" );
+ fprintf( pErr, "\t for multi-output miters, tries to prove that the AND of POs is always 0\n" );
+ fprintf( pErr, "\t (if POs should be ORed instead of ANDed, use command \"orpos\")\n" );
+ fprintf( pErr, "\t-A num : partitioning algorithm [default = %d]\n", nAlgo );
+ fprintf( pErr, "\t 0 : no partitioning\n" );
+ fprintf( pErr, "\t 1 : partitioning by level\n" );
+ fprintf( pErr, "\t 2 : DFS post-order\n" );
+ fprintf( pErr, "\t 3 : DFS pre-order\n" );
+ fprintf( pErr, "\t 4 : bit-slicing\n" );
+ fprintf( pErr, "\t partitions are ordered by level (high level first)\n" );
+ fprintf( pErr, "\t-P num : limit on the partition size [default = %d]\n", nPartSize );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfTotal );
+ fprintf( pErr, "\t-p : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
+ fprintf( pErr, "\t-s : apply logic synthesis to each partition [default = %s]\n", fSynthesize? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -15347,11 +15515,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
int fRewrite;
int fTransLoop;
int fUsePudlak;
+ int fUseOther;
+ int fUseMiniSat;
int fCheckInd;
int fCheckKstep;
int fVerbose;
- extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose );
+ extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -15363,11 +15533,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
fRewrite = 0;
fTransLoop = 1;
fUsePudlak = 0;
+ fUseOther = 0;
+ fUseMiniSat= 0;
fCheckInd = 0;
fCheckKstep= 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF )
{
switch ( c )
{
@@ -15402,6 +15574,12 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fUsePudlak ^= 1;
break;
+ case 'o':
+ fUseOther ^= 1;
+ break;
+ case 'm':
+ fUseMiniSat ^= 1;
+ break;
case 'i':
fCheckInd ^= 1;
break;
@@ -15437,18 +15615,19 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
return 0;
}
- Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose );
+ Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" );
+ fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" );
fprintf( pErr, "\t uses interpolation to prove the property\n" );
fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
-// fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
- fprintf( pErr, "\t-p : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+ fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" );
+ fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" );
fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -16364,6 +16543,55 @@ usage:
return 1; /* error exit */
}
+/**Function*************************************************************
+
+ Synopsis [Command procedure to read LUT libraries.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc8Check( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ int c;
+ extern int Nwk_ManCheck( void * p );
+
+ // set the defaults
+ Extra_UtilGetoptReset();
+ while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF )
+ {
+ switch (c)
+ {
+ case 'h':
+ goto usage;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != globalUtilOptind )
+ {
+ goto usage;
+ }
+
+ // set the new network
+ if ( pAbc->pAbc8Nwk == NULL )
+ printf( "Abc_CommandAbc8Check(): There is no mapped network.\n" );
+ else
+ Nwk_ManCheck( pAbc->pAbc8Nwk );
+ return 0;
+
+usage:
+ fprintf( stdout, "\nusage: *check [-h]\n");
+ fprintf( stdout, "\t checks if the current mapped network has duplicated fanins\n" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1; /* error exit */
+}
+
/**Function*************************************************************