Added switch 'write_counter -f' to output flop values in each time frame.

2 files changed, 53 insertions, 0 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 99928a66..64bb3b02 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -168,6 +168,7 @@ extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
 extern Aig_Man_t *       Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
 extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern Abc_Cex_t *       Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern Aig_Man_t *       Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
 /*=== saigHaig.c ==========================================================*/
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 45c37c3b..ca06398c 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -315,6 +315,58 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Abc_Cex_t * pNew;
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    // create new counter-example
+    pNew = Abc_CexAlloc( 0, Aig_ManPiNum(pAig), p->iFrame + 1 );
+    pNew->iPo = p->iPo;
+    pNew->iFrame = p->iFrame;
+    // simulate the AIG
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        ///////// write PI+LO values ////////////
+        Aig_ManForEachPi( pAig, pObj, k )
+            if ( pObj->fMarkB )
+                Aig_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k);
+        /////////////////////////////////////////
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
+    Aig_ManCleanMarkB(pAig);
+    if ( RetValue == 0 )
+        printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
 {
     Aig_Obj_t * pObj, * pObjRi, * pObjRo;