summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAbs.c7
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigAbs.c6
-rw-r--r--src/aig/saig/saigAbsCba.c6
-rw-r--r--src/aig/saig/saigAbsPba.c77
-rw-r--r--src/aig/saig/saigAbsStart.c2
-rw-r--r--src/aig/saig/saigBmc3.c3
-rw-r--r--src/base/abci/abc.c14
9 files changed, 86 insertions, 33 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3beed711..2f07e0e9 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -600,7 +600,7 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars );
Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
-extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose );
+extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 673d45e8..e08d63fc 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -268,8 +268,9 @@ void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAd
SeeAlso []
***********************************************************************/
-int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
+int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
{
+ Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vAbsFfsToAdd;
@@ -315,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
SeeAlso []
***********************************************************************/
-int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
+int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
@@ -331,7 +332,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
- vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose );
+ vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose, piFrame );
// derive new classes
if ( pAig->pSeqModel == NULL )
{
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f20641a5..505fd6ee 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
/*=== sswAbsPba.c ==========================================================*/
-extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose );
+extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
/*=== sswAbsStart.c ==========================================================*/
extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 19dbe0fd..01b1e6a6 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -91,9 +91,9 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
Aig_Obj_t * pObj;
int i, f;
if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
- printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
- else
- printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
+ printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
+// else
+// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
// start the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 78a77ecb..02d01852 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -180,6 +180,8 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsConst1(pObj) )
+ return;
if ( Aig_ObjIsPi(pObj) )
{
Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) );
@@ -267,7 +269,7 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
Aig_ManIncrementTravId( p->pFrames );
Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
Vec_IntFree( vPrios );
- assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
+// assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
return vReasons;
}
@@ -630,7 +632,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
if ( pPars->fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
- Abc_PrintTime( 0, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", clock() - clk );
}
return vAbsFfsToAdd;
}
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 21d92f57..edc9b6fd 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -171,19 +171,63 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap )
{
Abc_Cex_t * pCex;
- int i, f, Entry;
- pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
+ Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+ int i, f, Entry, iBit = 0;
+ pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
+ pCex->iPo = -1;
+ pCex->iFrame = -1;
Vec_IntForEachEntry( vPiVarMap, Entry, i )
+ {
if ( Entry >= 0 )
{
int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ];
if ( sat_solver_var_value( pSat, iSatVar ) )
Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i );
}
+ }
// check what frame has failed
+ Aig_ManCleanMarkB(pAig);
+ Aig_ManConst1(pAig)->fMarkB = 1;
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
for ( f = 0; f < nFrames; f++ )
{
-// Aig_ManForEach
+ // compute new state
+ Saig_ManForEachPi( pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
+ (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+ Aig_ManForEachPo( pAig, pObj, i )
+ pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+ Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
+ pObjRo->fMarkB = pObjRi->fMarkB;
+ // check the outputs
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( pObj->fMarkB )
+ {
+ pCex->iPo = i;
+ pCex->iFrame = f;
+ pCex->nBits = pCex->nRegs + pCex->nPis * (f+1);
+ break;
+ }
+ }
+ if ( i < Saig_ManPoNum(pAig) )
+ break;
+ }
+ Aig_ManCleanMarkB(pAig);
+ if ( f == nFrames )
+ {
+ Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" );
+ Abc_CexFree( pCex );
+ pCex = NULL;
+ }
+ if ( !Saig_ManVerifyCex( pAig, pCex ) )
+ {
+ Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" );
+ Abc_CexFree( pCex );
+ pCex = NULL;
}
return pCex;
}
@@ -199,7 +243,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t
SeeAlso []
***********************************************************************/
-Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose )
+Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
@@ -248,46 +292,40 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
{
if ( RetValue == l_True )
{
- printf( "Saig_ManPerformPba(): The eproblem is SAT. Abstraction refinement is still not enabled.\n" );
-/*
Vec_Int_t * vAbsFfsToAdd;
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
+ printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame );
+ *piFrame = pAig->pSeqModel->iFrame;
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
{
Vec_IntFree( vAbsFfsToAdd );
- return NULL;
+ goto finish;
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
- Abc_PrintTime( 0, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", clock() - clk );
}
vFlops = vAbsFfsToAdd;
-*/
}
else
{
- printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" );
+ printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" );
}
- Vec_IntFree( vPiVarMap );
- Vec_IntFree( vAssumps );
- Vec_IntFree( vMapVar2FF );
- sat_solver_delete( pSat );
- Aig_ManStop( pFrames );
- Cnf_DataFree( pCnf );
- return NULL;
+ goto finish;
}
assert( RetValue == l_False ); // UNSAT
+ *piFrame = nFrames;
// get relevant SAT literals
nCoreLits = sat_solver_final( pSat, &pCoreLits );
assert( nCoreLits > 0 );
if ( fVerbose )
- printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n",
- nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
+ printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n",
+ nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
// collect flops
vFlops = Vec_IntAlloc( nCoreLits );
@@ -300,6 +338,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
Vec_IntSort( vFlops, 0 );
// cleanup
+finish:
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index ff813c98..ec933512 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -196,7 +196,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vFlopsNew) );
- Abc_PrintTime( 0, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", clock() - clk );
}
// vFlopsNew contains PI number that should be kept in pAbs
// add to the abstraction
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 4dc0c714..a4567446 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1292,6 +1292,9 @@ clkOther += clock() - clk2;
fflush( stdout );
}
}
+ // consider the next timeframe
+ if ( RetValue == -1 && pPars->nStart == 0 )
+ pPars->iFrame = f;
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
{
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f680144..637d0cd4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -881,6 +881,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
void For_ManFileExperiment();
// For_ManFileExperiment();
}
+ {
+ void Bdc_SpfdDecomposeTest();
+ Bdc_SpfdDecomposeTest();
+ }
/*
{
int i1, i2, i3, i4, i5, i6, N, Counter = 0;
@@ -28437,6 +28441,7 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
int nConfMax = 100000;
int fVerbose = 0;
+ int iFrame = -1;
int c;
Extra_UtilGetoptReset();
@@ -28490,8 +28495,10 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The flop map is not given.\n" );
return 0;
}
- Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose );
-// Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+ Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose, &iFrame );
+ if ( iFrame >= 0 )
+ pAbc->nFrames = iFrame;
+ Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
@@ -28591,7 +28598,8 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
- pAbc->nFrames = pPars->iFrame;
+ if ( pPars->nStart == 0 )
+ pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-16 02:22:08 +0000