summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/saig.h4
-rw-r--r--src/aig/saig/saigAbs.c53
-rw-r--r--src/aig/saig/saigBmc.c21
3 files changed, 59 insertions, 19 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 85d2d191..b77a4292 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -90,10 +90,10 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
+extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
+extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 3da92fc0..844d6f24 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -25,6 +25,7 @@
#include "satStore.h"
#include "ssw.h"
#include "ioa.h"
+#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -694,17 +695,38 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
+Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int * pnUseStart, int fVerbose )
{
- extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
+ extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
+ extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
Vec_Int_t * vFlopsNew, * vPiToReg;
Aig_Obj_t * pObj;
int i, Entry, iFlop;
- Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
+ if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
+ {
+ Fra_Sec_t SecPar, * pSecPar = &SecPar;
+ int RetValue;
+ Fra_SecSetDefaultParams( pSecPar );
+ pSecPar->fVerbose = fVerbose;
+ RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
+ }
+ else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
+ {
+ int nBddMax = 1000000;
+ int nIterMax = nFrames;
+ int fPartition = 1;
+ int fReorder = 1;
+ int fReorderImage = 1;
+ Aig_ManVerifyUsingBdds( pAbs, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
+ }
+ else
+ Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 20, nConfMaxOne, 1000000, fVerbose, 0 );
if ( pAbs->pSeqModel == NULL )
return NULL;
+ if ( pnUseStart )
+ *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame;
// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
if ( Vec_IntSize(vFlopsNew) == 0 )
@@ -766,7 +788,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
{
Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf;
@@ -845,13 +867,14 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
Saig_AbsExtendOneStep( p, vFlops );
if ( fVerbose )
printf( " %d flops.\n", Vec_IntSize(vFlops) );
- }
+ }
*/
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
if ( fExtend )
{
+ int nUseStart = 0;
if ( !fVerbose )
{
printf( "Init : " );
@@ -860,21 +883,19 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
- char FileName[100];
- pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
+ pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose );
if ( pTemp == NULL )
break;
Aig_ManStop( pResult );
pResult = pTemp;
- printf( "%4d : ", Iter );
+ printf( "ITER %4d : ", Iter );
if ( !fVerbose )
Aig_ManPrintStats( pResult );
- else
- printf( " -----------------------------------------------------\n" );
+// else
+// printf( " -----------------------------------------------------\n" );
// output the intermediate result of abstraction
- sprintf( FileName, "gabs%02d.aig", Iter );
- Ioa_WriteAiger( pResult, FileName, 0, 0 );
- printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
+ Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
+// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
// check if the ratio is reached
if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
{
@@ -886,6 +907,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
}
}
Vec_IntFree( vFlops );
+ // write the final result
+ if ( pResult )
+ {
+ Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
+ printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
+ }
return pResult;
}
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 57759594..a37be3ad 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -508,7 +508,7 @@ Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
-int Saig_BmcSolveTargets( Saig_Bmc_t * p )
+int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
{
Aig_Obj_t * pObj;
int i, VarNum, Lit, RetValue;
@@ -520,6 +520,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
}
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
+ if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
+ continue;
if ( p->pSat->stats.conflicts > p->nConfMaxAll )
return l_Undef;
VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
@@ -575,11 +577,12 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
-void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
+void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite )
{
Saig_Bmc_t * p;
Aig_Man_t * pNew;
Cnf_Dat_t * pCnf;
+ int nOutsSolved = 0;
int Iter, RetValue, clk = clock(), clk2;
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
if ( fVerbose )
@@ -609,7 +612,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
Cnf_DataFree( pCnf );
Aig_ManStop( pNew );
// solve the targets
- RetValue = Saig_BmcSolveTargets( p );
+ RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
if ( fVerbose )
{
printf( "%3d : F = %3d. O =%4d. And = %7d. Var = %7d. Conf = %7d. ",
@@ -620,11 +623,21 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
break;
}
if ( RetValue == l_True )
+ {
+ assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
p->iOutputFail, p->iFrameFail );
+ }
else // if ( RetValue == l_False || RetValue == l_Undef )
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
- ABC_PRT( "Time", clock() - clk );
+ if ( fVerbOverwrite )
+ {
+ ABC_PRTr( "Time", clock() - clk );
+ }
+ else
+ {
+ ABC_PRT( "Time", clock() - clk );
+ }
if ( RetValue != l_True )
{
if ( p->iFrameLast >= p->nFramesMax )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 00:15:56 +0000