ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sscClass.c File Reference
#include "sscInt.h"
Include dependency graph for sscClass.c:

Go to the source code of this file.

Functions

void Ssc_GiaSimClassCreate (Gia_Man_t *p, Vec_Int_t *vClass)
 
int Ssc_GiaSimClassRefineOneBit (Gia_Man_t *p, int i)
 
int Ssc_GiaSimClassRefineOne (Gia_Man_t *p, int i)
 
void Ssc_GiaSimProcessRefined (Gia_Man_t *p, Vec_Int_t *vRefined)
 
void Ssc_GiaClassesInit (Gia_Man_t *p)
 FUNCTION DECLARATIONS ///.
 
int Ssc_GiaClassesRefine (Gia_Man_t *p)
 
void Ssc_GiaClassesCheckPairs (Gia_Man_t *p, Vec_Int_t *vDisPairs)
 

Function Documentation

◆ Ssc_GiaClassesCheckPairs()

void Ssc_GiaClassesCheckPairs ( Gia_Man_t * p,
Vec_Int_t * vDisPairs )

Function*************************************************************

Synopsis [Check if the pairs have been disproved.]

Description []

SideEffects []

SeeAlso []

Definition at line 309 of file sscClass.c.

310{
311 int i, iRepr, iObj, Result = 1;
312 Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i )
313 if ( iRepr == Gia_ObjRepr(p, iObj) )
314 printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0;
315// if ( Result )
316// printf( "Classes are refined correctly.\n" );
317}
Cube * p
Definition exorList.c:222
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Here is the caller graph for this function:

◆ Ssc_GiaClassesInit()

void Ssc_GiaClassesInit ( Gia_Man_t * p)

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Refines equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file sscClass.c.

266{
267 Gia_Obj_t * pObj;
268 int i;
269 assert( p->pReprs == NULL );
270 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
271 p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
272 Gia_ManForEachObj( p, pObj, i )
273 Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
274 if ( p->vClassOld == NULL )
275 p->vClassOld = Vec_IntAlloc( 100 );
276 if ( p->vClassNew == NULL )
277 p->vClassNew = Vec_IntAlloc( 100 );
278}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
#define GIA_VOID
Definition gia.h:46
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Ssc_GiaClassesRefine()

int Ssc_GiaClassesRefine ( Gia_Man_t * p)

Definition at line 279 of file sscClass.c.

280{
281 Vec_Int_t * vRefinedC;
282 Gia_Obj_t * pObj;
283 int i, Counter = 0;
284 assert( p->pReprs != NULL );
285 vRefinedC = Vec_IntAlloc( 100 );
286 Gia_ManForEachCand( p, pObj, i )
287 if ( Gia_ObjIsTail(p, i) )
288 Counter += Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
289 else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
290 Vec_IntPush( vRefinedC, i );
291 Ssc_GiaSimProcessRefined( p, vRefinedC );
292 Counter += Vec_IntSize( vRefinedC );
293 Vec_IntFree( vRefinedC );
294 return Counter;
295}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
#define Gia_ManForEachCand(p, pObj, i)
Definition gia.h:1220
void Ssc_GiaSimProcessRefined(Gia_Man_t *p, Vec_Int_t *vRefined)
Definition sscClass.c:221
int Ssc_GiaSimClassRefineOne(Gia_Man_t *p, int i)
Definition sscClass.c:197
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssc_GiaSimClassCreate()

void Ssc_GiaSimClassCreate ( Gia_Man_t * p,
Vec_Int_t * vClass )

Function*************************************************************

Synopsis [Refines one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file sscClass.c.

129{
130 int Repr = GIA_VOID, EntPrev = -1, Ent, i;
131 assert( Vec_IntSize(vClass) > 0 );
132 Vec_IntForEachEntry( vClass, Ent, i )
133 {
134 if ( i == 0 )
135 {
136 Repr = Ent;
137 Gia_ObjSetRepr( p, Ent, GIA_VOID );
138 EntPrev = Ent;
139 }
140 else
141 {
142 assert( Repr < Ent );
143 Gia_ObjSetRepr( p, Ent, Repr );
144 Gia_ObjSetNext( p, EntPrev, Ent );
145 EntPrev = Ent;
146 }
147 }
148 Gia_ObjSetNext( p, EntPrev, 0 );
149}
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Ssc_GiaSimClassRefineOne()

int Ssc_GiaSimClassRefineOne ( Gia_Man_t * p,
int i )

Function*************************************************************

Synopsis [Refines one class using simulation patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file sscClass.c.

198{
199 Gia_Obj_t * pObj;
200 int Ent;
201 assert( Gia_ObjIsHead( p, i ) );
202 Vec_IntClear( p->vClassOld );
203 Vec_IntClear( p->vClassNew );
204 Vec_IntPush( p->vClassOld, i );
205 pObj = Gia_ManObj(p, i);
206 Gia_ClassForEachObj1( p, i, Ent )
207 {
208 if ( Ssc_GiaSimAreEqual( p, i, Ent ) )
209 Vec_IntPush( p->vClassOld, Ent );
210 else
211 Vec_IntPush( p->vClassNew, Ent );
212 }
213 if ( Vec_IntSize( p->vClassNew ) == 0 )
214 return 0;
215 Ssc_GiaSimClassCreate( p, p->vClassOld );
216 Ssc_GiaSimClassCreate( p, p->vClassNew );
217 if ( Vec_IntSize(p->vClassNew) > 1 )
218 return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
219 return 1;
220}
#define Gia_ClassForEachObj1(p, i, iObj)
Definition gia.h:1109
void Ssc_GiaSimClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition sscClass.c:128
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssc_GiaSimClassRefineOneBit()

int Ssc_GiaSimClassRefineOneBit ( Gia_Man_t * p,
int i )

Function*************************************************************

Synopsis [Refines one equivalence class using individual bit-pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file sscClass.c.

163{
164 Gia_Obj_t * pObj;
165 int Ent;
166 assert( Gia_ObjIsHead( p, i ) );
167 Vec_IntClear( p->vClassOld );
168 Vec_IntClear( p->vClassNew );
169 Vec_IntPush( p->vClassOld, i );
170 pObj = Gia_ManObj(p, i);
171 Gia_ClassForEachObj1( p, i, Ent )
172 {
173 if ( Ssc_GiaSimAreEqualBit( p, i, Ent ) )
174 Vec_IntPush( p->vClassOld, Ent );
175 else
176 Vec_IntPush( p->vClassNew, Ent );
177 }
178 if ( Vec_IntSize( p->vClassNew ) == 0 )
179 return 0;
180 Ssc_GiaSimClassCreate( p, p->vClassOld );
181 Ssc_GiaSimClassCreate( p, p->vClassNew );
182 return 1;
183}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssc_GiaSimProcessRefined()

void Ssc_GiaSimProcessRefined ( Gia_Man_t * p,
Vec_Int_t * vRefined )

Definition at line 221 of file sscClass.c.

222{
223 int * pTable, nTableSize, i, k, Key;
224 if ( Vec_IntSize(vRefined) == 0 )
225 return;
226 nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
227 pTable = ABC_CALLOC( int, nTableSize );
228 Vec_IntForEachEntry( vRefined, i, k )
229 {
230 assert( !Ssc_GiaSimIsConst0( p, i ) );
231 Key = Ssc_GiaSimHashKey( p, i, nTableSize );
232 if ( pTable[Key] == 0 )
233 {
234 assert( Gia_ObjRepr(p, i) == 0 );
235 assert( Gia_ObjNext(p, i) == 0 );
236 Gia_ObjSetRepr( p, i, GIA_VOID );
237 }
238 else
239 {
240 Gia_ObjSetNext( p, pTable[Key], i );
241 Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) );
242 if ( Gia_ObjRepr(p, i) == GIA_VOID )
243 Gia_ObjSetRepr( p, i, pTable[Key] );
244 assert( Gia_ObjRepr(p, i) > 0 );
245 }
246 pTable[Key] = i;
247 }
248 Vec_IntForEachEntry( vRefined, i, k )
249 if ( Gia_ObjIsHead( p, i ) )
251 ABC_FREE( pTable );
252}
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the call graph for this function:
Here is the caller graph for this function: