summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/cec/cecSimBack.c194
-rw-r--r--src/proof/pdr/pdrInv.c13
-rw-r--r--src/proof/pdr/pdrMan.c2
3 files changed, 206 insertions, 3 deletions
diff --git a/src/proof/cec/cecSimBack.c b/src/proof/cec/cecSimBack.c
new file mode 100644
index 00000000..c3d09ff5
--- /dev/null
+++ b/src/proof/cec/cecSimBack.c
@@ -0,0 +1,194 @@
+/**CFile****************************************************************
+
+ FileName [cecSimBack.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Combinational equivalence checking.]
+
+ Synopsis [Backward simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cecSimBack.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ObjSatVerify( Gia_Man_t * p, Gia_Obj_t * pRoot, int Value )
+{
+ Gia_Obj_t * pObj;
+ int i, RetValue = 1;
+ printf( "Obj = %4d Value = %d ", Gia_ObjId(p, pRoot), Value );
+ Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+ Gia_ManForEachCi( p, pObj, i )
+ if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
+ Gia_ObjTerSimSetX( pObj ), printf( "x" );
+ else if ( pObj->fMark0 )
+ Gia_ObjTerSimSet1( pObj ), printf( "1" );
+ else
+ Gia_ObjTerSimSet0( pObj ), printf( "0" );
+ printf( " " );
+ Gia_ManForEachAnd( p, pObj, i )
+ Gia_ObjTerSimAnd( pObj );
+ if ( Value ? Gia_ObjTerSimGet1(pRoot) : Gia_ObjTerSimGet0(pRoot) )
+ printf( "Verification successful.\n" );
+ else
+ printf( "Verification failed.\n" ), RetValue = 0;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Return 1 if pObj can have Value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+word Cec_ManCheckSat2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, word Value, Vec_Wrd_t * vValues )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return Value == (int)pObj->fMark0;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ pObj->fMark0 = Value;
+ if ( !Gia_ObjIsAnd(pObj) )
+ return 1;
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( Value )
+ {
+ return Cec_ManCheckSat2_rec( p, pFan0, !Gia_ObjFaninC0(pObj), vValues ) &&
+ Cec_ManCheckSat2_rec( p, pFan1, !Gia_ObjFaninC1(pObj), vValues );
+ }
+ if ( Gia_ObjIsTravIdCurrent(p, pFan0) ) // already assigned
+ {
+ if ( Gia_ObjFaninC0(pObj) == (int)pFan0->fMark0 ) // justified
+ return 1;
+ return Cec_ManCheckSat2_rec( p, pFan1, Gia_ObjFaninC1(pObj), vValues );
+ }
+ if ( Gia_ObjIsTravIdCurrent(p, pFan1) ) // already assigned
+ {
+ if ( Gia_ObjFaninC1(pObj) == (int)pFan1->fMark0 ) // justified
+ return 1;
+ return Cec_ManCheckSat2_rec( p, pFan0, Gia_ObjFaninC0(pObj), vValues );
+ }
+ return Cec_ManCheckSat2_rec( p, pFan0, Gia_ObjFaninC0(pObj), vValues );
+}
+word Cec_ManCheckSat2( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Vec_Wrd_t * vValues )
+{
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Return 1 if pObj can have Value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManCheckSat_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return Value == (int)pObj->fMark0;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ pObj->fMark0 = Value;
+ if ( !Gia_ObjIsAnd(pObj) )
+ return 1;
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( Value )
+ {
+ return Cec_ManCheckSat_rec( p, pFan0, !Gia_ObjFaninC0(pObj) ) &&
+ Cec_ManCheckSat_rec( p, pFan1, !Gia_ObjFaninC1(pObj) );
+ }
+ if ( Gia_ObjIsTravIdCurrent(p, pFan0) ) // already assigned
+ {
+ if ( Gia_ObjFaninC0(pObj) == (int)pFan0->fMark0 ) // justified
+ return 1;
+ return Cec_ManCheckSat_rec( p, pFan1, Gia_ObjFaninC1(pObj) );
+ }
+ if ( Gia_ObjIsTravIdCurrent(p, pFan1) ) // already assigned
+ {
+ if ( Gia_ObjFaninC1(pObj) == (int)pFan1->fMark0 ) // justified
+ return 1;
+ return Cec_ManCheckSat_rec( p, pFan0, Gia_ObjFaninC0(pObj) );
+ }
+ return Cec_ManCheckSat_rec( p, pFan0, Gia_ObjFaninC0(pObj) );
+}
+void Cec_ManSimBack( Gia_Man_t * p )
+{
+ abctime clk = Abc_Clock();
+ Vec_Wrd_t * vValues = Vec_WrdStart( Gia_ManObjNum(p) );
+ Gia_Obj_t * pObj;
+ int i, Count = 0;
+ word Res;
+ Gia_ManSetPhase( p );
+ //Gia_ManForEachAnd( p, pObj, i )
+ // printf( "%d", pObj->fPhase );
+ //printf( "\n" );
+ //return;
+
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ Gia_ManIncrementTravId(p);
+ //Gia_ManCleanMark0( p );
+ Res = Cec_ManCheckSat_rec( p, pObj, !pObj->fPhase );
+ //if ( Res )
+ // Cec_ObjSatVerify( p, pObj, !pObj->fPhase );
+
+ //Res = Cec_ManCheckSat2_rec( p, pObj, !pObj->fPhase ? ~(word)0 : 0, vValues );
+ //if ( Res )
+ // Cec_ObjSatVerify2( p, pObj, !pObj->fPhase, Res );
+
+ Count += (int)(Res > 0);
+ }
+ Vec_WrdFree( vValues );
+ printf( "Obj = %6d. SAT = %6d. ", Gia_ManAndNum(p), Count );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 554add9b..baade033 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
+ {
+ printf( "Frame " );
+ printf( "Clauses " );
+ printf( "Max Queue " );
+ printf( "Flops " );
+ printf( "Cex " );
+ printf( "Time" );
+ printf( "\n" );
return;
+ }
if ( Abc_FrameIsBatchMode() && !fClose )
return;
// count the total length of the printout
@@ -81,9 +90,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%5d", p->nQueMax );
- Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
+ Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
if ( p->pPars->fUseAbs )
- Abc_Print( 1, "%5d", p->nCexes );
+ Abc_Print( 1, "%4d", p->nCexes );
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index c19041ee..abe8c0a8 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -455,7 +455,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
int i, f, Lit, Flop, nFrames = 0;
int nPis = Saig_ManPiNum(p->pAig);
int nFfRefined = 0;
- if ( !p->pPars->fUseAbs )
+ if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
return Pdr_ManDeriveCex(p);
// restore previous map
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-10 05:22:49 +0000