From 655a50101e18176f1163ccfc67cf69d86623d1f2 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 18 Sep 2008 08:01:00 -0700
Subject: Version abc80918

---
 src/aig/ssw/ssw.h      |  1 +
 src/aig/ssw/sswPairs.c | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)

(limited to 'src/aig/ssw')

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 14c10f6a..91c2165a 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -85,6 +85,7 @@ extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t
 /*=== sswPairs.c ===================================================*/
 extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
+extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index 92d3d91d..a11bdf98 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -430,6 +430,39 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Runs inductive SEC for the miter of two AIGs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
+{
+    Aig_Man_t * pAigRes;
+    int RetValue, clk = clock();
+    // try the new AIGs
+//    printf( "Performing general verification without node pairs.\n" );
+    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
+    // report the results
+    RetValue = Ssw_MiterStatus( pAigRes, 1 );
+    if ( RetValue == 1 )
+        printf( "Verification successful.  " );
+    else if ( RetValue == 0 )
+        printf( "Verification failed with a counter-example.  " );
+    else
+        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
+            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
+    PRT( "Time", clock() - clk );
+    // cleanup
+    Aig_ManStop( pAigRes );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3