Sweeper internal verification.

4 files changed, 77 insertions, 24 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c3e0d033..a6e36e6c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1008,7 +1008,7 @@ extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
-extern Gia_Man_t *         Gia_ManDupAnd( Gia_Man_t * p, int fCompl );
+extern Gia_Man_t *         Gia_ManDupAndOr( Gia_Man_t * p, int fUseOr, int fCompl );
 extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 92076573..657aa2bb 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2027,9 +2027,40 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl )
+Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int fUseOr, int fCompl )
 {
-    return NULL;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, iResult;
+    assert( Gia_ManRegNum(p) == 0 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    if ( fUseOr ) // construct OR of all POs
+    {
+        iResult = 0;
+        Gia_ManForEachPo( p, pObj, i )
+            iResult = Gia_ManHashOr( pNew, iResult, Gia_ObjFanin0Copy(pObj) );
+    }
+    else // construct AND of all POs
+    {
+        iResult = 1;
+        Gia_ManForEachPo( p, pObj, i )
+            iResult = Gia_ManHashAnd( pNew, iResult, Gia_ObjFanin0Copy(pObj) );
+    }
+    iResult = Abc_LitNotCond( iResult, (int)(fCompl > 0) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, iResult );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 2da162d1..3c91c467 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -969,27 +969,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Verification of the sweeper.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
-{
-    Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
-    Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 );
-
-    Gia_ManStop( pConstr );
-    Gia_ManStop( pMiter );
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Performs conditional sweeping of the cone.]
 
   Description [Returns the result as a new GIA manager with as many inputs 
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index aba5c80f..bb89d936 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sscInt.h"
+#include "proof/cec/cec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -210,6 +211,47 @@ int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Perform verification of conditional sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
+{
+    int Status;
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    // derive the OR of constraint outputs
+    Gia_Man_t * pCond = Gia_ManDupAndOr( pC, 1, 0 );
+    // derive F = F & !OR(c0, c1, c2, ...)
+    Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 );
+    // derive F = F & !OR(c0, c1, c2, ...)
+    Gia_Man_t * p1c = Gia_ManMiter( p1, pCond, 0, 0, 0, 1, 0 );
+    // derive dual-output miter
+    Gia_Man_t * pMiter = Gia_ManMiter( p0c, p1c, 0, 1, 0, 0, 0 );
+    Gia_ManStop( p0c );
+    Gia_ManStop( p1c );
+    Gia_ManStop( pCond );
+    // run equivalence checking
+    Cec_ManCecSetDefaultParams( pPars );
+    Status = Cec_ManVerify( pMiter, pPars );
+    Gia_ManStop( pMiter );
+    // report the results
+    if ( Status == 1 )
+        printf( "Verification succeeded.\n" );
+    else if ( Status == 0 )
+        printf( "Verification failed.\n" );
+    else if ( Status == -1 )
+        printf( "Verification undecided.\n" );
+    else assert( 0 );
+    return Status;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -401,6 +443,7 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
     pAig = Gia_ManDupLevelized( pResult = pAig );
     Gia_ManStop( pResult );
     pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
+    Ssc_PerformVerification( pAig, pResult, pCare );
     if ( pPars->fAppend )
     {
         Gia_ManDupAppendShare( pResult, pCare );