summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswSimSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw/sswSimSat.c')
-rw-r--r--src/aig/ssw/sswSimSat.c123
1 files changed, 0 insertions, 123 deletions
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
deleted file mode 100644
index 6b18a3a6..00000000
--- a/src/aig/ssw/sswSimSat.c
+++ /dev/null
@@ -1,123 +0,0 @@
-/**CFile****************************************************************
-
- FileName [sswSimSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Inductive prover with constraints.]
-
- Synopsis [Performs resimulation using counter-examples.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - September 1, 2008.]
-
- Revision [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sswInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
-{
- Aig_Obj_t * pObj;
- int i, RetValue1, RetValue2, clk = clock();
- // set the PI simulation information
- Aig_ManConst1(p->pAig)->fMarkB = 1;
- Aig_ManForEachPi( p->pAig, pObj, i )
- pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
- // simulate internal nodes
- Aig_ManForEachNode( p->pAig, pObj, i )
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
- // if repr is given, perform refinement
- if ( pRepr )
- {
- // check equivalence classes
- RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
- RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
- // make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
- {
- assert( RetValue1 );
- if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
- }
- else
- {
- assert( RetValue2 );
- if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
- }
- }
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
-{
- int RetValue1, RetValue2, clk = clock();
- // set the PI simulation information
- Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
- // simulate internal nodes
- Ssw_SmlSimulateOne( p->pSml );
- // check equivalence classes
- RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
- RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
- // make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
- {
- assert( RetValue1 );
- if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
- }
- else
- {
- assert( RetValue2 );
- if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
- }
-p->timeSimSat += clock() - clk;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-