summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp4
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/aig/gia/giaUtil.c2
-rw-r--r--src/base/abci/abc.c62
-rw-r--r--src/base/abci/abcDar.c82
-rw-r--r--src/proof/ssw/ssw.h1
-rw-r--r--src/proof/ssw/sswRarity.c12
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c3
-rw-r--r--src/sat/bmc/module.make1
11 files changed, 126 insertions, 45 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 4d2239c7..ca334c98 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1447,6 +1447,10 @@ SOURCE=.\src\sat\bmc\bmcLoad.c
# End Source File
# Begin Source File
+SOURCE=.\src\sat\bmc\bmcMulti.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\sat\bmc\bmcUnroll.c
# End Source File
# End Group
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 122e5025..8d953273 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -133,6 +133,7 @@ struct Gia_Man_t_
Vec_Int_t * vLutConfigs; // LUT configurations
Abc_Cex_t * pCexComb; // combinational counter-example
Abc_Cex_t * pCexSeq; // sequential counter-example
+ Vec_Ptr_t * vSeqModelVec; // sequential counter-examples
int * pCopies; // intermediate copies
Vec_Int_t * vTruths; // used for truth table computation
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 2eaf8eee..eb728cd0 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -72,6 +72,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
***********************************************************************/
void Gia_ManStop( Gia_Man_t * p )
{
+ if ( p->vSeqModelVec )
+ Vec_PtrFreeFree( p->vSeqModelVec );
Gia_ManStaticFanoutStop( p );
Tim_ManStopP( (Tim_Man_t **)&p->pManTime );
assert( p->pManTime == NULL );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 08136e7d..f3edca36 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1716,7 +1716,7 @@ int Gia_ManHasChoices_very_old( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
+Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
{
Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
Gia_Man_t * p = Gia_ManDup( pInit );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 21ace6d8..5c66958f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -398,6 +398,7 @@ static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Slice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -961,6 +962,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&slice", Abc_CommandAbc9Slice, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
@@ -32259,9 +32261,9 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
+ extern Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
Vec_Int_t * vStatus;
char * pCommLine = NULL;
int c, nGroupSize = 1, fVerbose = 0;
@@ -32300,15 +32302,15 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
- Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
+ Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" );
return 1;
}
- vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
+ vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
Vec_IntFree( vStatus );
return 0;
usage:
- Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" );
+ Abc_Print( -2, "usage: &gprove [-GS num] [-vh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by splitting outputs into groups\n" );
Abc_Print( -2, "\t (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" );
Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize );
@@ -32329,6 +32331,56 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose );
+ Vec_Int_t * vStatuses;
+ char * pCommLine = NULL;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
+ return 1;
+ }
+ pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose );
+ vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
+ Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
+ Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &mprove [-vh]\n" );
+ Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4fbf7c70..d662f376 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
- if ( RetValue == 1 )
- {
- Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
- }
- else if ( RetValue == -1 )
+ if ( !pPars->fSilent )
{
- if ( pPars->nFailOuts == 0 )
+ if ( RetValue == 1 )
{
- Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
- if ( nTimeOut && Abc_Clock() > nTimeOut )
- Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
- else
- Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+ Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
}
- else
+ else if ( RetValue == -1 )
{
- Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
- if ( Abc_Clock() > nTimeOut )
- Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+ if ( pPars->nFailOuts == 0 )
+ {
+ Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
+ if ( nTimeOut && Abc_Clock() > nTimeOut )
+ Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+ else
+ Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+ }
else
- Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
- }
- }
- else // if ( RetValue == 0 )
- {
- if ( !pPars->fSolveAll )
- {
- Abc_Cex_t * pCex = pNtk->pSeqModel;
- Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+ {
+ Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
+ if ( Abc_Clock() > nTimeOut )
+ Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+ else
+ Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+ }
}
- else
+ else // if ( RetValue == 0 )
{
- int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
- if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
- Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
- else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
- Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
+ if ( !pPars->fSolveAll )
+ {
+ Abc_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+ }
else
{
- Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
- if ( pPars->nDropOuts )
- Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
- Abc_Print( 1, ". " );
+ int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
+ if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
+ Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
+ else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
+ Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
+ else
+ {
+ Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+ if ( pPars->nDropOuts )
+ Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
+ Abc_Print( 1, ". " );
+ }
}
- if ( pNtk->vSeqModelVec )
- Vec_PtrFreeFree( pNtk->vSeqModelVec );
- pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
+ ABC_PRT( "Time", Abc_Clock() - clk );
+ }
+ if ( RetValue == 0 && pPars->fSolveAll )
+ {
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
+ pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
- ABC_PRT( "Time", Abc_Clock() - clk );
if ( pNtk->pSeqModel )
{
status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index 57bd91bf..cd65fc67 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -101,6 +101,7 @@ struct Ssw_RarPars_t_
int fSetLastState;
int fVerbose;
int fNotVerbose;
+ int fSilent;
int fDropSatOuts;
int fMiter;
int fUseCex;
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index e5640f6a..cd93d28b 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1051,16 +1051,22 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
// check timeout
if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
+ if ( !pPars->fSilent )
+ {
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
+ }
goto finish;
}
if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
{
+ if ( !pPars->fSilent )
+ {
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
+ }
goto finish;
}
// check if all outputs are solved by now
@@ -1106,15 +1112,21 @@ finish:
}
if ( pPars->nSolved )
{
+ if ( !pPars->fSilent )
+ {
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+ }
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
{
+ if ( !pPars->fSilent )
+ {
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+ }
}
// cleanup
Ssw_RarManStop( p );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 65c24e93..ff1e005b 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
+ int fSilent; // completely silent
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ed8f089a..ea08c1e4 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1397,7 +1397,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
- Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
+ if ( !pPars->fSilent )
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
goto finish;
}
// skip solved outputs
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index e567e92b..82d18fde 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -8,4 +8,5 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcLoad.c \
+ src/sat/bmc/bmcMulti.c \
src/sat/bmc/bmcUnroll.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 00:22:56 +0000