summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/sswSemi.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw/sswSemi.c')
-rw-r--r--src/proof/ssw/sswSemi.c322
1 files changed, 322 insertions, 0 deletions
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
new file mode 100644
index 00000000..74305adf
--- /dev/null
+++ b/src/proof/ssw/sswSemi.c
@@ -0,0 +1,322 @@
+/**CFile****************************************************************
+
+ FileName [sswSemi.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Semiformal for equivalence clases.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager
+
+struct Ssw_Sem_t_
+{
+ // parameters
+ int nConfMaxStart; // the starting conflict limit
+ int nConfMax; // the intermediate conflict limit
+ int nFramesSweep; // the number of frames to sweep
+ int fVerbose; // prints output statistics
+ // equivalences considered
+ Ssw_Man_t * pMan; // SAT sweeping manager
+ Vec_Ptr_t * vTargets; // the nodes that are watched
+ // storage for patterns
+ int nPatternsAlloc; // the max number of interesting states
+ int nPatterns; // the number of patterns
+ Vec_Ptr_t * vPatterns; // storage for the interesting states
+ Vec_Int_t * vHistory; // what state and how many steps
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
+{
+ Ssw_Sem_t * p;
+ Aig_Obj_t * pObj;
+ int i;
+ // create interpolation manager
+ p = ABC_ALLOC( Ssw_Sem_t, 1 );
+ memset( p, 0, sizeof(Ssw_Sem_t) );
+ p->nConfMaxStart = nConfMax;
+ p->nConfMax = nConfMax;
+ p->nFramesSweep = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
+ p->fVerbose = fVerbose;
+ // equivalences considered
+ p->pMan = pMan;
+ p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
+ Saig_ManForEachPo( p->pMan->pAig, pObj, i )
+ Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
+ // storage for patterns
+ p->nPatternsAlloc = 512;
+ p->nPatterns = 1;
+ p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) );
+ Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) );
+ p->vHistory = Vec_IntAlloc( 100 );
+ Vec_IntPush( p->vHistory, 0 );
+ // update arrays of the manager
+ assert( 0 );
+/*
+ ABC_FREE( p->pMan->pNodeToFrames );
+ Vec_IntFree( p->pMan->vSatVars );
+ p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
+ p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
+*/
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SemManStop( Ssw_Sem_t * p )
+{
+ Vec_PtrFree( p->vTargets );
+ Vec_PtrFree( p->vPatterns );
+ Vec_IntFree( p->vHistory );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SemCheckTargets( Ssw_Sem_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
+ if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
+{
+ unsigned * pInfo;
+ Aig_Obj_t * pObj;
+ int i;
+ if ( p->nPatterns >= p->nPatternsAlloc )
+ return;
+ Saig_ManForEachLo( p->pMan->pAig, pObj, i )
+ {
+ pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
+ if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
+ Abc_InfoSetBit( pInfo, p->nPatterns );
+ }
+ p->nPatterns++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
+{
+ Ssw_Man_t * p = pBmc->pMan;
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
+ unsigned * pInfo;
+ int i, f, clk, RetValue, fFirst = 0;
+clk = clock();
+
+ // start initialized timeframes
+ p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ {
+ pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
+ pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) );
+ Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
+ }
+
+ // sweep internal nodes
+ RetValue = pBmc->nFramesSweep;
+ for ( f = 0; f < pBmc->nFramesSweep; f++ )
+ {
+ // map constants and PIs
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ // sweep internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+ if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
+ {
+ Ssw_ManFilterBmcSavePattern( pBmc );
+ if ( fFirst == 0 )
+ {
+ fFirst = 1;
+ pBmc->nConfMax *= 10;
+ }
+ }
+ if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
+ {
+ RetValue = -1;
+ break;
+ }
+ }
+ // quit if this is the last timeframe
+ if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
+ {
+ RetValue += f + 1;
+ break;
+ }
+ if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
+ break;
+ // transfer latch input to the latch outputs
+ // build logic cones for register outputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ {
+ pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
+ Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
+ }
+//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
+ }
+ if ( fFirst )
+ pBmc->nConfMax /= 10;
+
+ // cleanup
+ Ssw_ClassesCheck( p->ppClasses );
+p->timeBmc += clock() - clk;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if one of the targets has failed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
+{
+ Ssw_Sem_t * p;
+ int RetValue, Frames, Iter, clk = clock();
+ p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
+ if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
+ {
+ assert( 0 );
+ Ssw_SemManStop( p );
+ return 1;
+ }
+ if ( fVerbose )
+ {
+ printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
+ Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
+ }
+ RetValue = 0;
+ for ( Iter = 0; Iter < p->nPatterns; Iter++ )
+ {
+clk = clock();
+ pMan->pMSat = Ssw_SatStart( 0 );
+ Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
+ if ( fVerbose )
+ {
+ printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
+ Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
+ Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
+ p->pMan->nSatFailsReal? "f" : " " );
+ ABC_PRT( "T", clock() - clk );
+ }
+ Ssw_ManCleanup( p->pMan );
+ if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
+ {
+ printf( "Target is hit!!!\n" );
+ RetValue = 1;
+ }
+ if ( p->nPatterns >= p->nPatternsAlloc )
+ break;
+ }
+ Ssw_SemManStop( p );
+
+ pMan->nStrangers = 0;
+ pMan->nSatCalls = 0;
+ pMan->nSatProof = 0;
+ pMan->nSatFailsReal = 0;
+ pMan->nSatCallsUnsat = 0;
+ pMan->nSatCallsSat = 0;
+ pMan->timeSimSat = 0;
+ pMan->timeSat = 0;
+ pMan->timeSatSat = 0;
+ pMan->timeSatUnsat = 0;
+ pMan->timeSatUndec = 0;
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:04:52 +0000