Skip to content

A
abc
Commit 2140c5d9 by Alan Mishchenko
Options

Updating testcext to ignore the diff in register count and other things.

parent e4d0f471
Showing with 93 additions and 20 deletions
src/aig/cec/cecSeq.c
......@@ -242,8 +242,8 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex
Vec_PtrFree( vSimInfo );
if ( pPars->fVerbose )
ABC_PRT( "Time", clock() - clkTotal );
if ( RetValue && pPars->fCheckMiter )
Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
// if ( RetValue && pPars->fCheckMiter )
// Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
return RetValue;
}
......
src/aig/gia/giaUtil.c
......@@ -1191,9 +1191,11 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
assert( Gia_ManPiNum(pAig) == p->nPis );
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
// Gia_ManForEachRo( pAig, pObj, i )
// pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
......@@ -1207,7 +1209,7 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
// remember the number of failed output
// figure out the number of failed output
RetValue = -1;
for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
{
......
src/aig/saig/saig.h
......@@ -62,6 +62,7 @@ struct Saig_ParBmc_t_
int nFramesMax; // maximum number of timeframes
int nConfLimit; // maximum number of conflicts at a node
int nTimeOut; // approximate timeout in seconds
int nPisAbstract; // the number of PIs to abstract
int fSolveAll; // does not stop at the first SAT output
int fDropSatOuts; // replace sat outputs by constant 0
int fVerbose; // verbose
......
src/aig/saig/saigBmc3.c
......@@ -551,10 +551,6 @@ void Saig_ManBmcMappingTest( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Create manager.]
......@@ -613,6 +609,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
***********************************************************************/
void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
{
Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
assert( p->pAig->pSeqModelVec == NULL );
......@@ -1002,6 +999,58 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
/**Function*************************************************************
Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_NodeCompareRefsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
{
int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2);
if ( Diff > 0 )
return -1;
if ( Diff < 0 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Mark PIs to be skipped based on nPisAbstract.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract )
{
Vec_Ptr_t * vPis;
Aig_Obj_t * pObj;
int i;
if ( nPisAbstract < 1 )
return;
// sort PIs by the number of their fanouts
// Saig_ManForEachPi( pAig, pObj, i )
// printf( "%d=%d ", i, Aig_ObjRefs(pObj) );
// printf( "\n" );
vPis = Vec_PtrAlloc( 100 );
Saig_ManForEachPi( pAig, pObj, i )
Vec_PtrPush( vPis, pObj );
Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsDecrease );
Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i )
if ( i > Saig_ManPiNum(pAig) - nPisAbstract )
pObj->fMarkA = 1;
}
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
......@@ -1018,6 +1067,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->nFramesMax = 2000; // maximum number of timeframes
p->nConfLimit = 2000; // maximum number of conflicts at a node
p->nTimeOut = 0; // approximate timeout in seconds
p->nPisAbstract = 0; // the number of PIs to abstract
p->fSolveAll = 0; // stops on the first SAT instance
p->fDropSatOuts = 0; // replace sat outputs by constant 0
p->fVerbose = 0; // verbose
......@@ -1058,6 +1108,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
if ( p->pPars->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
// perform frames
// Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
for ( f = 0; f < pPars->nFramesMax; f++ )
{
pPars->iFrame = f;
......
src/base/abci/abc.c
......@@ -8544,7 +8544,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
// Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
// Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" );
Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
// Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
Ssm_ManExperiment( "m\\simp.ssim", "m\\simp_.ssim" );
}
*/
/*
{
Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" );
Gia_ManStop( pGia );
}
*/
return 0;
......@@ -18340,7 +18347,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCLsdrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCILsdrvh" ) ) != EOF )
{
switch ( c )
{
......@@ -18388,6 +18395,17 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPisAbstract = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPisAbstract < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
......@@ -18454,12 +18472,13 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTC num] [-L file] [-sdvh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-s : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-d : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
......@@ -19831,10 +19850,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
// else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
// Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
// else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
......@@ -19860,10 +19879,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "And AIG: There is no current network.\n");
else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis )
Abc_Print( 1, "And AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis );
else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
// else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
// Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
// else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
// Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
else
{
// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
......
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