summaryrefslogtreecommitdiffstats
path: root/src/proof/abs/absUtil.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/abs/absUtil.c')
-rw-r--r--src/proof/abs/absUtil.c257
1 files changed, 257 insertions, 0 deletions
diff --git a/src/proof/abs/absUtil.c b/src/proof/abs/absUtil.c
new file mode 100644
index 00000000..60429496
--- /dev/null
+++ b/src/proof/abs/absUtil.c
@@ -0,0 +1,257 @@
+/**CFile****************************************************************
+
+ FileName [absUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Abstraction package.]
+
+ Synopsis [Interface to pthreads.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: absUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abs.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abs_ParSetDefaults( Abs_Par_t * p )
+{
+ memset( p, 0, sizeof(Abs_Par_t) );
+ p->nFramesMax = 0; // maximum frames
+ p->nFramesStart = 0; // starting frame
+ p->nFramesPast = 4; // overlap frames
+ p->nConfLimit = 0; // conflict limit
+ p->nLearnedMax = 1000; // max number of learned clauses
+ p->nLearnedStart = 1000; // max number of learned clauses
+ p->nLearnedDelta = 200; // max number of learned clauses
+ p->nLearnedPerce = 70; // max number of learned clauses
+ p->nTimeOut = 0; // timeout in seconds
+ p->nRatioMin = 0; // stop when less than this % of object is abstracted
+ p->nRatioMax = 30; // restart when more than this % of object is abstracted
+ p->fUseTermVars = 0; // use terminal variables
+ p->fUseRollback = 0; // use rollback to the starting number of frames
+ p->fPropFanout = 1; // propagate fanouts during refinement
+ p->fVerbose = 0; // verbose flag
+ p->iFrame = -1; // the number of frames covered
+ p->iFrameProved = -1; // the number of frames proved
+ p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converting VTA vector to GLA vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
+{
+ Gia_Obj_t * pObj;
+ Vec_Int_t * vGla;
+ int nObjMask, nObjs = Gia_ManObjNum(p);
+ int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
+ assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+ // get the bitmask
+ nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+ assert( nObjs <= nObjMask );
+ // go through objects
+ vGla = Vec_IntStart( nObjs );
+ Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
+ {
+ pObj = Gia_ManObj( p, (Entry & nObjMask) );
+ assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
+ Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 );
+ }
+ Vec_IntWriteEntry( vGla, 0, nFrames );
+ return vGla;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converting GLA vector to VTA vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
+{
+ Vec_Int_t * vVta;
+ int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
+ int i, k, j, Entry, Counter, nGlaSize;
+ //. get the GLA size
+ nGlaSize = Vec_IntSum(vGla);
+ // get the bitmask
+ nObjBits = Abc_Base2Log(nObjs);
+ nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+ assert( nObjs <= nObjMask );
+ // go through objects
+ vVta = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vVta, nFrames );
+ Counter = nFrames + 2;
+ for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
+ Vec_IntPush( vVta, Counter );
+ for ( i = 0; i < nFrames; i++ )
+ for ( k = 0; k <= i; k++ )
+ Vec_IntForEachEntry( vGla, Entry, j )
+ if ( Entry )
+ Vec_IntPush( vVta, (k << nObjBits) | j );
+ Counter = Vec_IntEntry(vVta, nFrames+1);
+ assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+ return vVta;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converting GLA vector to FLA vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
+ if ( Gia_ObjIsRo(p, pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+ Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converting FLA vector to GLA vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
+{
+ Vec_Int_t * vGla;
+ Gia_Obj_t * pObj;
+ int i;
+ // mark const0 and relevant CI objects
+ Gia_ManIncrementTravId( p );
+ Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
+ Gia_ManForEachPi( p, pObj, i )
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ Gia_ManForEachRo( p, pObj, i )
+ if ( !Vec_IntEntry(vFla, i) )
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ // label all objects reachable from the PO and selected flops
+ vGla = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_IntWriteEntry( vGla, 0, 1 );
+ Gia_ManForEachPo( p, pObj, i )
+ Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+ Gia_ManForEachRi( p, pObj, i )
+ if ( Vec_IntEntry(vFla, i) )
+ Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+ return vGla;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converting GLA vector to FLA vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
+{
+ Vec_Int_t * vFla;
+ Gia_Obj_t * pObj;
+ int i;
+ vFla = Vec_IntStart( Gia_ManRegNum(p) );
+ Gia_ManForEachRo( p, pObj, i )
+ if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
+ Vec_IntWriteEntry( vFla, i, 1 );
+ return vFla;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla )
+{
+ Gia_Obj_t * pObj;
+ int i, Count = 0;
+ Gia_ManForEachRo( p, pObj, i )
+ if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
+ Count++;
+ return Count;
+}
+int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
+{
+ Gia_Obj_t * pObj;
+ int i, Count = 0;
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
+ Count++;
+ return Count;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 04:03:20 +0000