ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sbdSim.c
Go to the documentation of this file.
1
20
21#include "sbdInt.h"
22
24
25
29
30static inline word * Sbd_ObjSims( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims, p->iPatsPi * i ); }
31static inline word * Sbd_ObjCtrl( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSimsPi, p->iPatsPi * i ); }
32
36
49{
50 int nWords = p->iPatsPi;
51 Gia_Obj_t * pObj;
52 int w, i, Id;
53 // init primary outputs
54 Gia_ManForEachCoId( p, Id, i )
55 for ( w = 0; w < nWords; w++ )
56 Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0);
57 // transfer to nodes
58 Gia_ManForEachCo( p, pObj, i )
59 {
60 word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
61 Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) );
62 }
63 // simulate nodes
64 Gia_ManForEachAndReverse( p, pObj, i )
65 {
66 word * pSims = Sbd_ObjSims(p, i);
67 word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i));
68 word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i));
69 word Rand = Gia_ManRandomW(0);
70 for ( w = 0; w < nWords; w++ )
71 {
72 pSims0[w] = pSims[w] | Rand;
73 pSims1[w] = pSims[w] | ~Rand;
74 }
75 if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords );
76 if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords );
77 }
78 // primary inputs are initialized
79}
80
81
93int Sbd_GiaSatOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, int fFirst, int iPat )
94{
95 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
96 return (int)pObj->fMark0 == Value;
97 Gia_ObjSetTravIdCurrent(p, pObj);
98 pObj->fMark0 = Value;
99 if ( Gia_ObjIsCi(pObj) )
100 {
101 word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
102 if ( Abc_TtGetBit( pSims, iPat ) != Value )
103 Abc_TtXorBit( pSims, iPat );
104 return 1;
105 }
106 assert( Gia_ObjIsAnd(pObj) );
107 assert( !Gia_ObjIsXor(pObj) );
108 if ( Value )
109 return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) &&
110 Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat );
111 if ( fFirst )
112 return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat );
113 else
114 return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat );
115}
117{
118 int k, n, Var1, Var2, iPat = 0;
119 //Gia_ManSetPhase( p );
120 Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k )
121 {
122 Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 );
123 Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 );
124 assert( Var2 > 0 );
125 if ( Var1 == 0 )
126 {
127 for ( n = 0; n < 2; n++ )
128 {
130 if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
131 {
132 iPat++;
133 break;
134 }
135 }
136 printf( "%c", n == 2 ? '.' : 'c' );
137 }
138 else
139 {
140 for ( n = 0; n < 2; n++ )
141 {
143 if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) )
144 {
145 iPat++;
146 break;
147 }
149 if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
150 {
151 iPat++;
152 break;
153 }
154 }
155 printf( "%c", n == 2 ? '.' : 'e' );
156 }
157 if ( iPat == 64 * p->iPatsPi - 1 )
158 break;
159 }
160 printf( "\n" );
161 return iPat;
162}
163
176{
177 extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap );
178 Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) );
179 Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
180 Vec_Int_t * vMap; // maps each node into its class
181 int i, nConsts = 0, nClasses = 0, nPats;
182 Sbd_GiaSimRound( p, 0, &vMap );
184 {
185 if ( Vec_IntEntry(vMap, i) == 0 )
186 Vec_IntPushTwo( vPairs, 0, i ), nConsts++;
187 else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 )
188 Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i );
189 else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 )
190 {
191 Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i );
192 Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 );
193 nClasses++;
194 }
195 }
196 Vec_IntFree( vMap );
197 Vec_IntFree( vReprs );
198 printf( "Constants = %d. Classes = %d.\n", nConsts, nClasses );
199
200 nPats = Sbd_GiaSatOne( p, vPairs );
201 Vec_IntFree( vPairs );
202
203 printf( "Generated %d patterns.\n", nPats );
204}
205
217void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap )
218{
219 int nWords = p->iPatsPi;
220 Vec_Mem_t * vStore;
221 Gia_Obj_t * pObj;
222 Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) );
223 int w, i, Id, fCompl, RetValue;
224 // init primary inputs
225 if ( fTry )
226 {
228 Gia_ManForEachCiId( p, Id, i )
229 Sbd_ObjSims(p, Id)[0] <<= 1;
230 }
231 else
232 {
233 Gia_ManForEachCiId( p, Id, i )
234 for ( w = 0; w < nWords; w++ )
235 Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w;
236 }
237 // simulate internal nodes
238 vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page
239 Vec_MemHashAlloc( vStore, 1 << 16 );
240 RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero
241 assert( RetValue == 0 );
242 Gia_ManForEachAnd( p, pObj, i )
243 {
244 word * pSims = Sbd_ObjSims(p, i);
245 if ( Gia_ObjIsXor(pObj) )
246 Abc_TtXor( pSims,
247 Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)),
248 Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)),
249 nWords,
250 Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
251 else
252 Abc_TtAndCompl( pSims,
253 Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj),
254 Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj),
255 nWords );
256 // hash sim info
257 fCompl = (int)(pSims[0] & 1);
258 if ( fCompl ) Abc_TtNot( pSims, nWords );
259 Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) );
260 if ( fCompl ) Abc_TtNot( pSims, nWords );
261 }
262 Gia_ManForEachCo( p, pObj, i )
263 {
264 word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
265 Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) );
266// printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) );
267 assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) );
268 }
269// printf( "\n" );
270 Vec_MemHashFree( vStore );
271 Vec_MemFree( vStore );
272 printf( "Objects = %6d. Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) );
273 if ( pvMap )
274 *pvMap = vMap;
275 else
276 Vec_IntFree( vMap );
277}
279{
280 Gia_ManSetPhase( pGia );
281
282 // allocate simulation info
283 pGia->iPatsPi = 32;
284 pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
285 pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
286
287 Gia_ManRandom( 1 );
288
289 Sbd_GiaSimRound( pGia, 0, NULL );
290 Sbd_GiaSimRound( pGia, 0, NULL );
291 Sbd_GiaSimRound( pGia, 0, NULL );
292
293 printf( "\n" );
294 Sbd_GiaSimRound( pGia, 1, NULL );
295 printf( "\n" );
296 Sbd_GiaSimRound( pGia, 1, NULL );
297 printf( "\n" );
298 Sbd_GiaSimRound( pGia, 1, NULL );
299
300 Vec_WrdFreeP( &pGia->vSims );
301 Vec_WrdFreeP( &pGia->vSimsPi );
302}
303
307
308
310
int nWords
Definition abcNpn.c:127
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
#define Gia_ManForEachCoId(p, Id, i)
Definition gia.h:1240
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
word Gia_ManRandomW(int fReset)
Definition giaUtil.c:67
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
#define Gia_ManForEachAndId(p, i)
Definition gia.h:1216
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition giaUtil.c:49
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
void Sbd_GiaSimRoundBack2(Gia_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition sbdSim.c:48
void Sbd_GiaSimRound(Gia_Man_t *p, int fTry, Vec_Int_t **pvMap)
Definition sbdSim.c:217
int Sbd_GiaSatOne(Gia_Man_t *p, Vec_Int_t *vPairs)
Definition sbdSim.c:116
void Sbd_GiaSimRoundBack(Gia_Man_t *p)
Definition sbdSim.c:175
void Sbd_GiaSimTest(Gia_Man_t *pGia)
Definition sbdSim.c:278
int Sbd_GiaSatOne_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int Value, int fFirst, int iPat)
Definition sbdSim.c:93
Vec_Wrd_t * vSims
Definition gia.h:213
Vec_Wrd_t * vSimsPi
Definition gia.h:215
int iPatsPi
Definition gia.h:208
unsigned fPhase
Definition gia.h:87
unsigned fMark0
Definition gia.h:81
typedefABC_NAMESPACE_IMPL_START struct Vec_Mem_t_ Vec_Mem_t
DECLARATIONS ///.
Definition utilMem.c:35
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
@ Var1
Definition xsatSolver.h:56