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

Go to the source code of this file.

Functions

int Cec_ManSimCompareConst (unsigned *p, int nWords)
 FUNCTION DEFINITIONS ///.
 
int Cec_ManSimCompareEqual (unsigned *p0, unsigned *p1, int nWords)
 
int Cec_ManSimCompareConstFirstBit (unsigned *p, int nWords)
 
int Cec_ManSimCompareEqualFirstBit (unsigned *p0, unsigned *p1, int nWords)
 
void Cec_ManSimCompareConstScore (unsigned *p, int nWords, int *pScores)
 
void Cec_ManSimCompareEqualScore (unsigned *p0, unsigned *p1, int nWords, int *pScores)
 
void Cec_ManSimClassCreate (Gia_Man_t *p, Vec_Int_t *vClass)
 
int Cec_ManSimClassRefineOne_rec (Cec_ManSim_t *p, int i)
 
int Cec_ManSimClassRefineOne_ (Cec_ManSim_t *p, int i)
 
int Cec_ManSimClassRefineOne (Cec_ManSim_t *p, int i)
 
int Cec_ManSimClassRemoveOne (Cec_ManSim_t *p, int i)
 
int Cec_ManSimHashKey (unsigned *pSim, int nWords, int nTableSize)
 
void Cec_ManSimMemRelink (Cec_ManSim_t *p)
 
unsigned * Cec_ManSimSimRef (Cec_ManSim_t *p, int i)
 
unsigned * Cec_ManSimSimDeref (Cec_ManSim_t *p, int i)
 
void Cec_ManSimProcessRefined (Cec_ManSim_t *p, Vec_Int_t *vRefined)
 
void Cec_ManSimSavePattern (Cec_ManSim_t *p, int iPat)
 
void Cec_ManSimFindBestPattern (Cec_ManSim_t *p)
 
int Cec_ManSimAnalyzeOutputs (Cec_ManSim_t *p)
 
int Cec_ManSimSimulateRound (Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
 
void Cec_ManSimCreateInfo (Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
 
int Cec_ManSimClassesPrepare (Cec_ManSim_t *p, int LevelMax)
 
int Cec_ManSimClassesRefine (Cec_ManSim_t *p)
 

Function Documentation

◆ Cec_ManSimAnalyzeOutputs()

int Cec_ManSimAnalyzeOutputs ( Cec_ManSim_t * p)

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

Synopsis [Returns 1 if computation should stop.]

Description []

SideEffects []

SeeAlso []

Definition at line 600 of file cecClass.c.

601{
602 unsigned * pInfo, * pInfo2;
603 int i;
604 if ( !p->pPars->fCheckMiter )
605 return 0;
606 assert( p->vCoSimInfo != NULL );
607 // compare outputs with 0
608 if ( p->pPars->fDualOut )
609 {
610 assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
611 for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
612 {
613 pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
614 pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i );
615 if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
616 {
617 if ( p->iOut == -1 )
618 {
619 p->iOut = i/2;
620 Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
621 }
622 if ( p->pCexes == NULL )
623 p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
624 if ( p->pCexes[i/2] == NULL )
625 {
626 p->nOuts++;
627 p->pCexes[i/2] = (void *)1;
628 }
629 }
630 }
631 }
632 else
633 {
634 for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
635 {
636 pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
637 if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
638 {
639 if ( p->iOut == -1 )
640 {
641 p->iOut = i;
643 }
644 if ( p->pCexes == NULL )
645 p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
646 if ( p->pCexes[i] == NULL )
647 {
648 p->nOuts++;
649 p->pCexes[i] = (void *)1;
650 }
651 }
652 }
653 }
654 return p->pCexes != NULL;
655}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
int Cec_ManSimCompareEqual(unsigned *p0, unsigned *p1, int nWords)
Definition cecClass.c:80
int Cec_ManSimCompareConstFirstBit(unsigned *p, int nWords)
Definition cecClass.c:110
void Cec_ManSimSavePattern(Cec_ManSim_t *p, int iPat)
Definition cecClass.c:534
int Cec_ManSimCompareEqualFirstBit(unsigned *p0, unsigned *p1, int nWords)
Definition cecClass.c:140
int Cec_ManSimCompareConst(unsigned *p, int nWords)
FUNCTION DEFINITIONS ///.
Definition cecClass.c:50
Cube * p
Definition exorList.c:222
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimClassCreate()

void Cec_ManSimClassCreate ( Gia_Man_t * p,
Vec_Int_t * vClass )

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

Synopsis [Creates equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file cecClass.c.

235{
236 int Repr = GIA_VOID, EntPrev = -1, Ent, i;
237 assert( Vec_IntSize(vClass) > 0 );
238 Vec_IntForEachEntry( vClass, Ent, i )
239 {
240 if ( i == 0 )
241 {
242 Repr = Ent;
243 Gia_ObjSetRepr( p, Ent, GIA_VOID );
244 EntPrev = Ent;
245 }
246 else
247 {
248 assert( Repr < Ent );
249 Gia_ObjSetRepr( p, Ent, Repr );
250 Gia_ObjSetNext( p, EntPrev, Ent );
251 EntPrev = Ent;
252 }
253 }
254 Gia_ObjSetNext( p, EntPrev, 0 );
255}
#define GIA_VOID
Definition gia.h:46
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Cec_ManSimClassesPrepare()

int Cec_ManSimClassesPrepare ( Cec_ManSim_t * p,
int LevelMax )

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

Synopsis [Returns 1 if the bug is found.]

Description []

SideEffects []

SeeAlso []

Definition at line 867 of file cecClass.c.

868{
869 Gia_Obj_t * pObj;
870 int i;
871 assert( p->pAig->pReprs == NULL );
872 // allocate representation
873 p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
874 p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
875 // create references
876 Gia_ManCreateValueRefs( p->pAig );
877 // set starting representative of internal nodes to be constant 0
878 if ( p->pPars->fLatchCorr )
879 Gia_ManForEachObj( p->pAig, pObj, i )
880 Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
881 else if ( LevelMax == -1 )
882 Gia_ManForEachObj( p->pAig, pObj, i )
883 Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
884 else
885 {
886 Gia_ManLevelNum( p->pAig );
887 Gia_ManForEachObj( p->pAig, pObj, i )
888 Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID );
889 Vec_IntFreeP( &p->pAig->vLevels );
890 }
891 // if sequential simulation, set starting representative of ROs to be constant 0
892 if ( p->pPars->fSeqSimulate )
893 Gia_ManForEachRo( p->pAig, pObj, i )
894 if ( pObj->Value )
895 Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
896 // perform simulation
897 if ( p->pAig->nSimWords )
898 {
899 p->nWords = 2*p->pAig->nSimWords;
900 assert( Vec_WrdSize(p->pAig->vSimsPi) == Gia_ManCiNum(p->pAig) * p->pAig->nSimWords );
901 //Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
902 for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
903 memmove( Vec_PtrEntry(p->vCiSimInfo, i), Vec_WrdEntryP(p->pAig->vSimsPi, i*p->pAig->nSimWords), sizeof(word)*p->pAig->nSimWords );
904 if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
905 return 1;
906 if ( p->pPars->fVerbose )
907 Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
908 }
909 else
910 {
911 p->nWords = 1;
912 do {
913 if ( p->pPars->fVerbose )
914 Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
915 for ( i = 0; i < 4; i++ )
916 {
917 Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
918 if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
919 return 1;
920 }
921 p->nWords = 2 * p->nWords + 1;
922 }
923 while ( p->nWords <= p->pPars->nWords );
924 }
925 return 0;
926}
void Cec_ManSimCreateInfo(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition cecClass.c:824
int Cec_ManSimSimulateRound(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition cecClass.c:668
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition giaUtil.c:750
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition giaEquiv.c:501
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
unsigned Value
Definition gia.h:89
char * memmove()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimClassesRefine()

int Cec_ManSimClassesRefine ( Cec_ManSim_t * p)

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

Synopsis [Returns 1 if the bug is found.]

Description []

SideEffects []

SeeAlso []

Definition at line 939 of file cecClass.c.

940{
941 int i;
942 Gia_ManCreateValueRefs( p->pAig );
943 p->nWords = p->pPars->nWords;
944 for ( i = 0; i < p->pPars->nRounds; i++ )
945 {
946 if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
947 Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
948 Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
949 if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
950 return 1;
951 }
952 if ( p->pPars->fVerbose )
953 Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
954 return 0;
955}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimClassRefineOne()

int Cec_ManSimClassRefineOne ( Cec_ManSim_t * p,
int i )

Definition at line 308 of file cecClass.c.

309{
310 return Cec_ManSimClassRefineOne_rec( p, i );
311}
int Cec_ManSimClassRefineOne_rec(Cec_ManSim_t *p, int i)
Definition cecClass.c:270
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimClassRefineOne_()

int Cec_ManSimClassRefineOne_ ( Cec_ManSim_t * p,
int i )

Definition at line 299 of file cecClass.c.

300{
301 int Res;
302 s_Count = 0;
304 if ( s_Count > 10 )
305 printf( "%d ", s_Count );
306 return Res;
307}
Here is the call graph for this function:

◆ Cec_ManSimClassRefineOne_rec()

int Cec_ManSimClassRefineOne_rec ( Cec_ManSim_t * p,
int i )

Definition at line 270 of file cecClass.c.

271{
272 unsigned * pSim0, * pSim1;
273 int Ent;
274 s_Count++;
275 Vec_IntClear( p->vClassOld );
276 Vec_IntClear( p->vClassNew );
277 Vec_IntPush( p->vClassOld, i );
278 pSim0 = Cec_ObjSim(p, i);
279 Gia_ClassForEachObj1( p->pAig, i, Ent )
280 {
281 pSim1 = Cec_ObjSim(p, Ent);
282 if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
283 Vec_IntPush( p->vClassOld, Ent );
284 else
285 {
286 Vec_IntPush( p->vClassNew, Ent );
287 if ( p->pBestState )
288 Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores );
289 }
290 }
291 if ( Vec_IntSize( p->vClassNew ) == 0 )
292 return 0;
293 Cec_ManSimClassCreate( p->pAig, p->vClassOld );
294 Cec_ManSimClassCreate( p->pAig, p->vClassNew );
295 if ( Vec_IntSize(p->vClassNew) > 1 )
296 return 1 + Cec_ManSimClassRefineOne_rec( p, Vec_IntEntry(p->vClassNew,0) );
297 return 1;
298}
void Cec_ManSimCompareEqualScore(unsigned *p0, unsigned *p1, int nWords, int *pScores)
Definition cecClass.c:202
void Cec_ManSimClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition cecClass.c:234
#define Gia_ClassForEachObj1(p, i, iObj)
Definition gia.h:1109
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimClassRemoveOne()

int Cec_ManSimClassRemoveOne ( Cec_ManSim_t * p,
int i )

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

Synopsis [Refines one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 324 of file cecClass.c.

325{
326 int iRepr, Ent;
327 if ( Gia_ObjIsConst(p->pAig, i) )
328 {
329 Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
330 return 1;
331 }
332 if ( !Gia_ObjIsClass(p->pAig, i) )
333 return 0;
334 assert( Gia_ObjIsClass(p->pAig, i) );
335 iRepr = Gia_ObjRepr( p->pAig, i );
336 if ( iRepr == GIA_VOID )
337 iRepr = i;
338 // collect nodes
339 Vec_IntClear( p->vClassOld );
340 Vec_IntClear( p->vClassNew );
341 Gia_ClassForEachObj( p->pAig, iRepr, Ent )
342 {
343 if ( Ent == i )
344 Vec_IntPush( p->vClassNew, Ent );
345 else
346 Vec_IntPush( p->vClassOld, Ent );
347 }
348 assert( Vec_IntSize( p->vClassNew ) == 1 );
349 Cec_ManSimClassCreate( p->pAig, p->vClassOld );
350 Cec_ManSimClassCreate( p->pAig, p->vClassNew );
351 assert( !Gia_ObjIsClass(p->pAig, i) );
352 return 1;
353}
#define Gia_ClassForEachObj(p, i, iObj)
Definition gia.h:1107
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimCompareConst()

int Cec_ManSimCompareConst ( unsigned * p,
int nWords )

FUNCTION DEFINITIONS ///.

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

Synopsis [Compares simulation info of one node with constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file cecClass.c.

51{
52 int w;
53 if ( p[0] & 1 )
54 {
55 for ( w = 0; w < nWords; w++ )
56 if ( p[w] != ~0 )
57 return 0;
58 return 1;
59 }
60 else
61 {
62 for ( w = 0; w < nWords; w++ )
63 if ( p[w] != 0 )
64 return 0;
65 return 1;
66 }
67}
int nWords
Definition abcNpn.c:127
Here is the caller graph for this function:

◆ Cec_ManSimCompareConstFirstBit()

int Cec_ManSimCompareConstFirstBit ( unsigned * p,
int nWords )

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

Synopsis [Returns the number of the first non-equal bit.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file cecClass.c.

111{
112 int w;
113 if ( p[0] & 1 )
114 {
115 for ( w = 0; w < nWords; w++ )
116 if ( p[w] != ~0 )
117 return 32*w + Gia_WordFindFirstBit( ~p[w] );
118 return -1;
119 }
120 else
121 {
122 for ( w = 0; w < nWords; w++ )
123 if ( p[w] != 0 )
124 return 32*w + Gia_WordFindFirstBit( p[w] );
125 return -1;
126 }
127}
Here is the caller graph for this function:

◆ Cec_ManSimCompareConstScore()

void Cec_ManSimCompareConstScore ( unsigned * p,
int nWords,
int * pScores )

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

Synopsis [Returns the number of the first non-equal bit.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file cecClass.c.

171{
172 int w, b;
173 if ( p[0] & 1 )
174 {
175 for ( w = 0; w < nWords; w++ )
176 if ( p[w] != ~0 )
177 for ( b = 0; b < 32; b++ )
178 if ( ((~p[w]) >> b ) & 1 )
179 pScores[32*w + b]++;
180 }
181 else
182 {
183 for ( w = 0; w < nWords; w++ )
184 if ( p[w] != 0 )
185 for ( b = 0; b < 32; b++ )
186 if ( ((p[w]) >> b ) & 1 )
187 pScores[32*w + b]++;
188 }
189}
Here is the caller graph for this function:

◆ Cec_ManSimCompareEqual()

int Cec_ManSimCompareEqual ( unsigned * p0,
unsigned * p1,
int nWords )

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

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file cecClass.c.

81{
82 int w;
83 if ( (p0[0] & 1) == (p1[0] & 1) )
84 {
85 for ( w = 0; w < nWords; w++ )
86 if ( p0[w] != p1[w] )
87 return 0;
88 return 1;
89 }
90 else
91 {
92 for ( w = 0; w < nWords; w++ )
93 if ( p0[w] != ~p1[w] )
94 return 0;
95 return 1;
96 }
97}
Here is the caller graph for this function:

◆ Cec_ManSimCompareEqualFirstBit()

int Cec_ManSimCompareEqualFirstBit ( unsigned * p0,
unsigned * p1,
int nWords )

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

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file cecClass.c.

141{
142 int w;
143 if ( (p0[0] & 1) == (p1[0] & 1) )
144 {
145 for ( w = 0; w < nWords; w++ )
146 if ( p0[w] != p1[w] )
147 return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
148 return -1;
149 }
150 else
151 {
152 for ( w = 0; w < nWords; w++ )
153 if ( p0[w] != ~p1[w] )
154 return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
155 return -1;
156 }
157}
Here is the caller graph for this function:

◆ Cec_ManSimCompareEqualScore()

void Cec_ManSimCompareEqualScore ( unsigned * p0,
unsigned * p1,
int nWords,
int * pScores )

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

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file cecClass.c.

203{
204 int w, b;
205 if ( (p0[0] & 1) == (p1[0] & 1) )
206 {
207 for ( w = 0; w < nWords; w++ )
208 if ( p0[w] != p1[w] )
209 for ( b = 0; b < 32; b++ )
210 if ( ((p0[w] ^ p1[w]) >> b ) & 1 )
211 pScores[32*w + b]++;
212 }
213 else
214 {
215 for ( w = 0; w < nWords; w++ )
216 if ( p0[w] != ~p1[w] )
217 for ( b = 0; b < 32; b++ )
218 if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 )
219 pScores[32*w + b]++;
220 }
221}
Here is the caller graph for this function:

◆ Cec_ManSimCreateInfo()

void Cec_ManSimCreateInfo ( Cec_ManSim_t * p,
Vec_Ptr_t * vInfoCis,
Vec_Ptr_t * vInfoCos )

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

Synopsis [Creates simulation info for this round.]

Description []

SideEffects []

SeeAlso []

Definition at line 824 of file cecClass.c.

825{
826 unsigned * pRes0, * pRes1;
827 int i, w;
828 if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 )
829 {
830 assert( vInfoCis && vInfoCos );
831 for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
832 {
833 pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
834 for ( w = 0; w < p->nWords; w++ )
835 pRes0[w] = Gia_ManRandom( 0 );
836 }
837 for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
838 {
839 pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
840 pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
841 for ( w = 0; w < p->nWords; w++ )
842 pRes0[w] = pRes1[w];
843 }
844 }
845 else
846 {
847 for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
848 {
849 pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
850 for ( w = 0; w < p->nWords; w++ )
851 pRes0[w] = Gia_ManRandom( 0 );
852 }
853 }
854}
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition giaUtil.c:49
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimFindBestPattern()

void Cec_ManSimFindBestPattern ( Cec_ManSim_t * p)

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

Synopsis [Find the best pattern using the scores.]

Description []

SideEffects []

SeeAlso []

Definition at line 564 of file cecClass.c.

565{
566 unsigned * pInfo;
567 int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
568 // find the best pattern
569 for ( i = 0; i < 32 * p->nWords; i++ )
570 if ( ScoreBest < p->pScores[i] )
571 {
572 ScoreBest = p->pScores[i];
573 iPatBest = i;
574 }
575 // compare this with the available patterns - and save
576 if ( p->pBestState->iPo <= ScoreBest )
577 {
578 assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) );
579 for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
580 {
581 pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
582 if ( Abc_InfoHasBit(p->pBestState->pData, i) != Abc_InfoHasBit(pInfo, iPatBest) )
583 Abc_InfoXorBit( p->pBestState->pData, i );
584 }
585 p->pBestState->iPo = ScoreBest;
586 }
587}
Here is the caller graph for this function:

◆ Cec_ManSimHashKey()

int Cec_ManSimHashKey ( unsigned * pSim,
int nWords,
int nTableSize )

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

Synopsis [Computes hash key of the simuation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 366 of file cecClass.c.

367{
368 static int s_Primes[16] = {
369 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
370 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
371 unsigned uHash = 0;
372 int i;
373 if ( pSim[0] & 1 )
374 for ( i = 0; i < nWords; i++ )
375 uHash ^= ~pSim[i] * s_Primes[i & 0xf];
376 else
377 for ( i = 0; i < nWords; i++ )
378 uHash ^= pSim[i] * s_Primes[i & 0xf];
379 return (int)(uHash % nTableSize);
380
381}
Here is the caller graph for this function:

◆ Cec_ManSimMemRelink()

void Cec_ManSimMemRelink ( Cec_ManSim_t * p)

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

Synopsis [Resets pointers to the simulation memory.]

Description []

SideEffects []

SeeAlso []

Definition at line 394 of file cecClass.c.

395{
396 unsigned * pPlace, Ent;
397 pPlace = (unsigned *)&p->MemFree;
398 for ( Ent = p->nMems * (p->nWords + 1);
399 Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
400 Ent += p->nWords + 1 )
401 {
402 *pPlace = Ent;
403 pPlace = p->pMems + Ent;
404 }
405 *pPlace = 0;
406 p->nWordsOld = p->nWords;
407}
Here is the caller graph for this function:

◆ Cec_ManSimProcessRefined()

void Cec_ManSimProcessRefined ( Cec_ManSim_t * p,
Vec_Int_t * vRefined )

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

Synopsis [Refines nodes belonging to candidate constant class.]

Description []

SideEffects []

SeeAlso []

Definition at line 483 of file cecClass.c.

484{
485 unsigned * pSim;
486 int * pTable, nTableSize, i, k, Key;
487 if ( Vec_IntSize(vRefined) == 0 )
488 return;
489 nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
490 pTable = ABC_CALLOC( int, nTableSize );
491 Vec_IntForEachEntry( vRefined, i, k )
492 {
493 pSim = Cec_ObjSim( p, i );
494 assert( !Cec_ManSimCompareConst( pSim, p->nWords ) );
495 Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize );
496 if ( pTable[Key] == 0 )
497 {
498 assert( Gia_ObjRepr(p->pAig, i) == 0 );
499 assert( Gia_ObjNext(p->pAig, i) == 0 );
500 Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
501 }
502 else
503 {
504 Gia_ObjSetNext( p->pAig, pTable[Key], i );
505 Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
506 if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
507 Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
508 assert( Gia_ObjRepr(p->pAig, i) > 0 );
509 }
510 pTable[Key] = i;
511 }
512 Vec_IntForEachEntry( vRefined, i, k )
513 {
514 if ( Gia_ObjIsHead( p->pAig, i ) )
516 }
517 Vec_IntForEachEntry( vRefined, i, k )
518 Cec_ManSimSimDeref( p, i );
519 ABC_FREE( pTable );
520}
#define ABC_FREE(obj)
Definition abc_global.h:267
unsigned * Cec_ManSimSimDeref(Cec_ManSim_t *p, int i)
Definition cecClass.c:457
int Cec_ManSimHashKey(unsigned *pSim, int nWords, int nTableSize)
Definition cecClass.c:366
int Cec_ManSimClassRefineOne(Cec_ManSim_t *p, int i)
Definition cecClass.c:308
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimSavePattern()

void Cec_ManSimSavePattern ( Cec_ManSim_t * p,
int iPat )

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

Synopsis [Saves the input pattern with the given number.]

Description []

SideEffects []

SeeAlso []

Definition at line 534 of file cecClass.c.

535{
536 unsigned * pInfo;
537 int i;
538 assert( p->pCexComb == NULL );
539 assert( iPat >= 0 && iPat < 32 * p->nWords );
540 p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char,
541 sizeof(Abc_Cex_t) + sizeof(unsigned) * Abc_BitWordNum(Gia_ManCiNum(p->pAig)) );
542 p->pCexComb->iPo = p->iOut;
543 p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
544 p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
545 for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
546 {
547 pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
548 if ( Abc_InfoHasBit( pInfo, iPat ) )
549 Abc_InfoSetBit( p->pCexComb->pData, i );
550 }
551}
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the caller graph for this function:

◆ Cec_ManSimSimDeref()

unsigned * Cec_ManSimSimDeref ( Cec_ManSim_t * p,
int i )

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

Synopsis [Dereferences simulaton info.]

Description []

SideEffects []

SeeAlso []

Definition at line 457 of file cecClass.c.

458{
459 unsigned * pSim;
460 assert( p->pSimInfo[i] > 0 );
461 pSim = p->pMems + p->pSimInfo[i];
462 if ( --pSim[0] == 0 )
463 {
464 pSim[0] = p->MemFree;
465 p->MemFree = p->pSimInfo[i];
466 p->pSimInfo[i] = 0;
467 p->nMems--;
468 }
469 return pSim;
470}
Here is the caller graph for this function:

◆ Cec_ManSimSimRef()

unsigned * Cec_ManSimSimRef ( Cec_ManSim_t * p,
int i )

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

Synopsis [References simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 420 of file cecClass.c.

421{
422 unsigned * pSim;
423 assert( p->pSimInfo[i] == 0 );
424 if ( p->MemFree == 0 )
425 {
426 if ( p->nWordsAlloc == 0 )
427 {
428 assert( p->pMems == NULL );
429 p->nWordsAlloc = (1<<17); // -> 1Mb
430 p->nMems = 1;
431 }
432 p->nWordsAlloc *= 2;
433 p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
435 }
436 p->pSimInfo[i] = p->MemFree;
437 pSim = p->pMems + p->MemFree;
438 p->MemFree = pSim[0];
439 pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
440 p->nMems++;
441 if ( p->nMemsMax < p->nMems )
442 p->nMemsMax = p->nMems;
443 return pSim;
444}
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
void Cec_ManSimMemRelink(Cec_ManSim_t *p)
Definition cecClass.c:394
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManSimSimulateRound()

int Cec_ManSimSimulateRound ( Cec_ManSim_t * p,
Vec_Ptr_t * vInfoCis,
Vec_Ptr_t * vInfoCos )

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

Synopsis [Simulates one round.]

Description [Returns the number of PO entry if failed; 0 otherwise.]

SideEffects []

SeeAlso []

Definition at line 668 of file cecClass.c.

669{
670 Gia_Obj_t * pObj;
671 unsigned * pRes0, * pRes1, * pRes;
672 int i, k, w, Ent, iCiId = 0, iCoId = 0;
673 // prepare internal storage
674 if ( p->nWordsOld != p->nWords )
676 p->nMemsMax = 0;
677 // allocate score counters
678 ABC_FREE( p->pScores );
679 if ( p->pBestState )
680 p->pScores = ABC_CALLOC( int, 32 * p->nWords );
681 // simulate nodes
682 Vec_IntClear( p->vRefinedC );
683 if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
684 {
685 pRes = Cec_ManSimSimRef( p, 0 );
686 for ( w = 1; w <= p->nWords; w++ )
687 pRes[w] = 0;
688 }
689 Gia_ManForEachObj1( p->pAig, pObj, i )
690 {
691 if ( Gia_ObjIsCi(pObj) )
692 {
693 if ( Gia_ObjValue(pObj) == 0 )
694 {
695 iCiId++;
696 continue;
697 }
698 pRes = Cec_ManSimSimRef( p, i );
699 if ( vInfoCis )
700 {
701 pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ );
702 for ( w = 1; w <= p->nWords; w++ )
703 pRes[w] = pRes0[w-1];
704 }
705 else
706 {
707 for ( w = 1; w <= p->nWords; w++ )
708 pRes[w] = Gia_ManRandom( 0 );
709 }
710 // make sure the first pattern is always zero
711 pRes[1] ^= (pRes[1] & 1);
712 goto references;
713 }
714 if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
715 {
716 pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
717 if ( vInfoCos )
718 {
719 pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ );
720 if ( Gia_ObjFaninC0(pObj) )
721 for ( w = 1; w <= p->nWords; w++ )
722 pRes[w-1] = ~pRes0[w];
723 else
724 for ( w = 1; w <= p->nWords; w++ )
725 pRes[w-1] = pRes0[w];
726 }
727 continue;
728 }
729 assert( Gia_ObjValue(pObj) );
730 pRes = Cec_ManSimSimRef( p, i );
731 pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
732 pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
733
734// Abc_Print( 1, "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
735
736 if ( Gia_ObjFaninC0(pObj) )
737 {
738 if ( Gia_ObjFaninC1(pObj) )
739 for ( w = 1; w <= p->nWords; w++ )
740 pRes[w] = ~(pRes0[w] | pRes1[w]);
741 else
742 for ( w = 1; w <= p->nWords; w++ )
743 pRes[w] = ~pRes0[w] & pRes1[w];
744 }
745 else
746 {
747 if ( Gia_ObjFaninC1(pObj) )
748 for ( w = 1; w <= p->nWords; w++ )
749 pRes[w] = pRes0[w] & ~pRes1[w];
750 else
751 for ( w = 1; w <= p->nWords; w++ )
752 pRes[w] = pRes0[w] & pRes1[w];
753 }
754
755references:
756 // if this node is candidate constant, collect it
757 if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
758 {
759 pRes[0]++;
760 Vec_IntPush( p->vRefinedC, i );
761 if ( p->pBestState )
762 Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
763 }
764 // if the node belongs to a class, save it
765 if ( Gia_ObjIsClass(p->pAig, i) )
766 pRes[0]++;
767 // if this is the last node of the class, process it
768 if ( Gia_ObjIsTail(p->pAig, i) )
769 {
770 Vec_IntClear( p->vClassTemp );
771 Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
772 Vec_IntPush( p->vClassTemp, Ent );
773 Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
774 Vec_IntForEachEntry( p->vClassTemp, Ent, k )
775 Cec_ManSimSimDeref( p, Ent );
776 }
777 }
778
779 if ( p->pPars->fConstCorr )
780 {
781 Vec_IntForEachEntry( p->vRefinedC, i, k )
782 {
783 Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
784 Cec_ManSimSimDeref( p, i );
785 }
786 Vec_IntClear( p->vRefinedC );
787 }
788
789 if ( Vec_IntSize(p->vRefinedC) > 0 )
790 Cec_ManSimProcessRefined( p, p->vRefinedC );
791 assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
792 assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
793 assert( p->nMems == 1 );
794 if ( p->nMems != 1 )
795 Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" );
796 if ( p->pPars->fVeryVerbose )
797 Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
798 if ( p->pBestState )
800/*
801 if ( p->nMems > 1 ) {
802 for ( i = 1; i < p->nObjs; i++ )
803 if ( p->pSims[i] ) {
804 int x = 0;
805 }
806 }
807*/
808 return Cec_ManSimAnalyzeOutputs( p );
809}
unsigned * Cec_ManSimSimRef(Cec_ManSim_t *p, int i)
Definition cecClass.c:420
int Cec_ManSimAnalyzeOutputs(Cec_ManSim_t *p)
Definition cecClass.c:600
void Cec_ManSimProcessRefined(Cec_ManSim_t *p, Vec_Int_t *vRefined)
Definition cecClass.c:483
void Cec_ManSimFindBestPattern(Cec_ManSim_t *p)
Definition cecClass.c:564
void Cec_ManSimCompareConstScore(unsigned *p, int nWords, int *pScores)
Definition cecClass.c:170
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
Here is the call graph for this function:
Here is the caller graph for this function: