Skip to content

A
abc
Commit 3f2b1233 by Alan Mishchenko
Options

Adding silent mode to &cec -m.

parent 1451e455
Showing with 41 additions and 15 deletions
src/base/abci/abc.c
......@@ -30862,7 +30862,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasvh" ) ) != EOF )
{
switch ( c )
{
......@@ -30900,6 +30900,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
fDumpMiter ^= 1;
break;
case 's':
pPars->fSilent ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -30918,12 +30921,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
return 1;
}
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars );
}
else
{
Gia_Man_t * pTemp;
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
pTemp = Gia_ManTransformToDual( pAbc->pGia );
pAbc->Status = Cec_ManVerify( pTemp, pPars );
......@@ -30982,7 +30987,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &cec [-CT num] [-nmdavh]\n" );
Abc_Print( -2, "usage: &cec [-CT num] [-nmdasvh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
......@@ -30990,6 +30995,7 @@ usage:
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
src/proof/cec/cec.h
......@@ -123,6 +123,7 @@ struct Cec_ParCec_t_
int fUseSmartCnf; // use smart CNF computation
int fRewriting; // enables AIG rewriting
int fNaive; // performs naive SAT-based checking
int fSilent; // print no messages
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the number of failed output
......
src/proof/cec/cecCec.c
......@@ -68,7 +68,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
SeeAlso []
***********************************************************************/
int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal )
int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal, int fSilent )
{
// extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
......@@ -83,13 +83,19 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
// report the miter
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
if ( !fSilent )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
if ( !fSilent )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
if ( pMiterCec->pData == NULL )
Abc_Print( 1, "Counter-example is not available.\n" );
else
......@@ -99,19 +105,20 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
Abc_Print( 1, "Counter-example verification has failed.\n" );
else
{
// Aig_Obj_t * pObj = Aig_ManCo(pMiterCec, iOut);
// Aig_Obj_t * pFan = Aig_ObjFanin0(pObj);
Abc_Print( 1, "Primary output %d has failed", iOut );
if ( nOuts-1 >= 0 )
Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 );
Abc_Print( 1, ".\n" );
if ( !fSilent )
{
Abc_Print( 1, "Primary output %d has failed", iOut );
if ( nOuts-1 >= 0 )
Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 );
Abc_Print( 1, ".\n" );
}
if ( piOutFail )
*piOutFail = iOut;
}
Cec_ManTransformPattern( pMiter, iOut, (int *)pMiterCec->pData );
}
}
else
else if ( !fSilent )
{
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
......@@ -146,8 +153,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
// (for example, when they have the same driver but complemented)
if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) )
{
if ( !pPars->fSilent )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different phase). ", i/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
return 0;
......@@ -158,8 +168,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
// drivers are different PIs
if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 )
{
if ( !pPars->fSilent )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different PIs). ", i/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
// if their compl attributes are the same - one should be complemented
......@@ -171,8 +184,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) ||
(Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) )
{
if ( !pPars->fSilent )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (PI vs. constant). ", i/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
// the compl attributes are the same - the PI should be complemented
......@@ -186,8 +202,11 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
}
if ( Gia_ManAndNum(p) == 0 )
{
if ( !pPars->fSilent )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return 1;
}
return -1;
......@@ -383,7 +402,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
if ( pPars->fVerbose )
Abc_Print( 1, "Calling the old CEC engine.\n" );
fflush( stdout );
RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal );
RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal, pPars->fSilent );
p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
Abc_Print( 1, "Counter-example simulation has failed.\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment