1 /**CFile****************************************************************
2
3 FileName [sscSim.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT sweeping under constraints.]
8
9 Synopsis [Simulation procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 29, 2008.]
16
17 Revision [$Id: sscSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sscInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
Ssc_Random()30 static inline word Ssc_Random() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 0); }
Ssc_Random1(int Bit)31 static inline word Ssc_Random1( int Bit ) { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 1) | (word)Bit; }
Ssc_Random2()32 static inline word Ssc_Random2() { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 2) | (word)2; }
33
Ssc_SimAnd(word * pSim,word * pSim0,word * pSim1,int nWords,int fComp0,int fComp1)34 static inline void Ssc_SimAnd( word * pSim, word * pSim0, word * pSim1, int nWords, int fComp0, int fComp1 )
35 {
36 int w;
37 if ( fComp0 && fComp1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]);
38 else if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w] & pSim1[w];
39 else if ( fComp1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] &~pSim1[w];
40 else for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w];
41 }
42
Ssc_SimDup(word * pSim,word * pSim0,int nWords,int fComp0)43 static inline void Ssc_SimDup( word * pSim, word * pSim0, int nWords, int fComp0 )
44 {
45 int w;
46 if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w];
47 else for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w];
48 }
49
Ssc_SimConst(word * pSim,int nWords,int fComp0)50 static inline void Ssc_SimConst( word * pSim, int nWords, int fComp0 )
51 {
52 int w;
53 if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(word)0;
54 else for ( w = 0; w < nWords; w++ ) pSim[w] = 0;
55 }
56
Ssc_SimOr(word * pSim,word * pSim0,int nWords,int fComp0)57 static inline void Ssc_SimOr( word * pSim, word * pSim0, int nWords, int fComp0 )
58 {
59 int w;
60 if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] |= ~pSim0[w];
61 else for ( w = 0; w < nWords; w++ ) pSim[w] |= pSim0[w];
62 }
63
Ssc_SimFindBitWord(word t)64 static inline int Ssc_SimFindBitWord( word t )
65 {
66 int n = 0;
67 if ( t == 0 ) return -1;
68 if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; }
69 if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; }
70 if ( (t & 0x00000000000000FF) == 0 ) { n += 8; t >>= 8; }
71 if ( (t & 0x000000000000000F) == 0 ) { n += 4; t >>= 4; }
72 if ( (t & 0x0000000000000003) == 0 ) { n += 2; t >>= 2; }
73 if ( (t & 0x0000000000000001) == 0 ) { n++; }
74 return n;
75 }
Ssc_SimFindBit(word * pSim,int nWords)76 static inline int Ssc_SimFindBit( word * pSim, int nWords )
77 {
78 int w;
79 for ( w = 0; w < nWords; w++ )
80 if ( pSim[w] )
81 return 64*w + Ssc_SimFindBitWord(pSim[w]);
82 return -1;
83 }
84
Ssc_SimCountBitsWord(word x)85 static inline int Ssc_SimCountBitsWord( word x )
86 {
87 x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
88 x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
89 x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
90 x = x + (x >> 8);
91 x = x + (x >> 16);
92 x = x + (x >> 32);
93 return (int)(x & 0xFF);
94 }
Ssc_SimCountBits(word * pSim,int nWords)95 static inline int Ssc_SimCountBits( word * pSim, int nWords )
96 {
97 int w, Counter = 0;
98 for ( w = 0; w < nWords; w++ )
99 Counter += Ssc_SimCountBitsWord(pSim[w]);
100 return Counter;
101 }
102
103
104 ////////////////////////////////////////////////////////////////////////
105 /// FUNCTION DEFINITIONS ///
106 ////////////////////////////////////////////////////////////////////////
107
108 /**Function*************************************************************
109
110 Synopsis []
111
112 Description []
113
114 SideEffects []
115
116 SeeAlso []
117
118 ***********************************************************************/
Vec_WrdDoubleSimInfo(Vec_Wrd_t * p,int nObjs)119 void Vec_WrdDoubleSimInfo( Vec_Wrd_t * p, int nObjs )
120 {
121 word * pArray = ABC_CALLOC( word, 2 * Vec_WrdSize(p) );
122 int i, nWords = Vec_WrdSize(p) / nObjs;
123 assert( Vec_WrdSize(p) % nObjs == 0 );
124 for ( i = 0; i < nObjs; i++ )
125 memcpy( pArray + 2*i*nWords, p->pArray + i*nWords, sizeof(word) * nWords );
126 ABC_FREE( p->pArray ); p->pArray = pArray;
127 p->nSize = p->nCap = 2*nWords*nObjs;
128 }
129
130 /**Function*************************************************************
131
132 Synopsis []
133
134 Description []
135
136 SideEffects []
137
138 SeeAlso []
139
140 ***********************************************************************/
Ssc_GiaResetPiPattern(Gia_Man_t * p,int nWords)141 void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords )
142 {
143 p->iPatsPi = 0;
144 if ( p->vSimsPi == NULL )
145 p->vSimsPi = Vec_WrdStart(0);
146 Vec_WrdFill( p->vSimsPi, nWords * Gia_ManCiNum(p), 0 );
147 assert( nWords == Gia_ObjSimWords( p ) );
148 }
Ssc_GiaSavePiPattern(Gia_Man_t * p,Vec_Int_t * vPat)149 void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
150 {
151 word * pSimPi;
152 int i;
153 assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
154 if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
155 Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManCiNum(p) );
156 assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
157 pSimPi = Gia_ObjSimPi( p, 0 );
158 for ( i = 0; i < Gia_ManCiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
159 if ( Vec_IntEntry(vPat, i) )
160 Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
161 p->iPatsPi++;
162 }
Ssc_GiaRandomPiPattern(Gia_Man_t * p,int nWords,Vec_Int_t * vPivot)163 void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
164 {
165 word * pSimPi;
166 int i, w;
167 Ssc_GiaResetPiPattern( p, nWords );
168 pSimPi = Gia_ObjSimPi( p, 0 );
169 for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += nWords )
170 {
171 pSimPi[0] = vPivot ? Ssc_Random1(Vec_IntEntry(vPivot, i)) : Ssc_Random2();
172 for ( w = 1; w < nWords; w++ )
173 pSimPi[w] = Ssc_Random();
174 // if ( i < 10 )
175 // Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
176 }
177 }
Ssc_GiaPrintPiPatterns(Gia_Man_t * p)178 void Ssc_GiaPrintPiPatterns( Gia_Man_t * p )
179 {
180 Gia_Obj_t * pObj;
181 word * pSimAig;
182 int i;//, nWords = Gia_ObjSimWords( p );
183 Gia_ManForEachCi( p, pObj, i )
184 {
185 pSimAig = Gia_ObjSimObj( p, pObj );
186 // Extra_PrintBinary( stdout, pSimAig, 64 * nWords );
187 }
188 }
189
190 /**Function*************************************************************
191
192 Synopsis [Transfer the simulation pattern from pCare to pAig.]
193
194 Description []
195
196 SideEffects []
197
198 SeeAlso []
199
200 ***********************************************************************/
Ssc_GiaTransferPiPattern(Gia_Man_t * pAig,Gia_Man_t * pCare,Vec_Int_t * vPivot)201 int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot )
202 {
203 extern word * Ssc_GiaGetCareMask( Gia_Man_t * p );
204 Gia_Obj_t * pObj;
205 int i, w, nWords = Gia_ObjSimWords( pCare );
206 word * pCareMask = Ssc_GiaGetCareMask( pCare );
207 int Count = Ssc_SimCountBits( pCareMask, nWords );
208 word * pSimPiCare, * pSimPiAig;
209 if ( Count == 0 )
210 {
211 ABC_FREE( pCareMask );
212 return 0;
213 }
214 Ssc_GiaResetPiPattern( pAig, nWords );
215 Gia_ManForEachCi( pCare, pObj, i )
216 {
217 pSimPiAig = Gia_ObjSimPi( pAig, i );
218 pSimPiCare = Gia_ObjSimObj( pCare, pObj );
219 for ( w = 0; w < nWords; w++ )
220 if ( Vec_IntEntry(vPivot, i) )
221 pSimPiAig[w] = pSimPiCare[w] | ~pCareMask[w];
222 else
223 pSimPiAig[w] = pSimPiCare[w] & pCareMask[w];
224 }
225 ABC_FREE( pCareMask );
226 return Count;
227 }
228
229 /**Function*************************************************************
230
231 Synopsis []
232
233 Description []
234
235 SideEffects []
236
237 SeeAlso []
238
239 ***********************************************************************/
Ssc_GiaResetSimInfo(Gia_Man_t * p)240 void Ssc_GiaResetSimInfo( Gia_Man_t * p )
241 {
242 assert( Vec_WrdSize(p->vSimsPi) % Gia_ManCiNum(p) == 0 );
243 if ( p->vSims == NULL )
244 p->vSims = Vec_WrdAlloc(0);
245 Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 );
246 }
Ssc_GiaSimRound(Gia_Man_t * p)247 void Ssc_GiaSimRound( Gia_Man_t * p )
248 {
249 Gia_Obj_t * pObj;
250 word * pSim, * pSim0, * pSim1;
251 int i, nWords = Gia_ObjSimWords(p);
252 Ssc_GiaResetSimInfo( p );
253 assert( nWords == Vec_WrdSize(p->vSims) / Gia_ManObjNum(p) );
254 // constant node
255 Ssc_SimConst( Gia_ObjSim(p, 0), nWords, 0 );
256 // primary inputs
257 pSim = Gia_ObjSim( p, 1 );
258 pSim0 = Gia_ObjSimPi( p, 0 );
259 Gia_ManForEachCi( p, pObj, i )
260 {
261 assert( pSim == Gia_ObjSimObj( p, pObj ) );
262 Ssc_SimDup( pSim, pSim0, nWords, 0 );
263 pSim += nWords;
264 pSim0 += nWords;
265 }
266 // intermediate nodes
267 pSim = Gia_ObjSim( p, 1+Gia_ManCiNum(p) );
268 Gia_ManForEachAnd( p, pObj, i )
269 {
270 assert( pSim == Gia_ObjSim( p, i ) );
271 pSim0 = pSim - pObj->iDiff0 * nWords;
272 pSim1 = pSim - pObj->iDiff1 * nWords;
273 Ssc_SimAnd( pSim, pSim0, pSim1, nWords, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
274 pSim += nWords;
275 }
276 // primary outputs
277 pSim = Gia_ObjSim( p, Gia_ManObjNum(p) - Gia_ManPoNum(p) );
278 Gia_ManForEachPo( p, pObj, i )
279 {
280 assert( pSim == Gia_ObjSimObj( p, pObj ) );
281 pSim0 = pSim - pObj->iDiff0 * nWords;
282 Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) );
283 // Extra_PrintBinary( stdout, pSim, 64 ), printf( "\n" );
284 pSim += nWords;
285 }
286 }
287
288 /**Function*************************************************************
289
290 Synopsis [Returns one SAT assignment of the PIs.]
291
292 Description []
293
294 SideEffects []
295
296 SeeAlso []
297
298 ***********************************************************************/
Ssc_GiaGetCareMask(Gia_Man_t * p)299 word * Ssc_GiaGetCareMask( Gia_Man_t * p )
300 {
301 Gia_Obj_t * pObj;
302 int i, nWords = Gia_ObjSimWords( p );
303 word * pRes = ABC_FALLOC( word, nWords );
304 Gia_ManForEachPo( p, pObj, i )
305 Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
306 return pRes;
307 }
Ssc_GiaGetOneSim(Gia_Man_t * p)308 Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
309 {
310 Vec_Int_t * vInit;
311 Gia_Obj_t * pObj;
312 int i, iBit, nWords = Gia_ObjSimWords( p );
313 word * pRes = Ssc_GiaGetCareMask( p );
314 iBit = Ssc_SimFindBit( pRes, nWords );
315 ABC_FREE( pRes );
316 if ( iBit == -1 )
317 return NULL;
318 vInit = Vec_IntAlloc( 100 );
319 Gia_ManForEachCi( p, pObj, i )
320 Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
321 return vInit;
322 }
Ssc_GiaFindPivotSim(Gia_Man_t * p)323 Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
324 {
325 Vec_Int_t * vInit;
326 Ssc_GiaRandomPiPattern( p, 1, NULL );
327 Ssc_GiaSimRound( p );
328 vInit = Ssc_GiaGetOneSim( p );
329 return vInit;
330 }
331
332 /**Function*************************************************************
333
334 Synopsis []
335
336 Description []
337
338 SideEffects []
339
340 SeeAlso []
341
342 ***********************************************************************/
Ssc_GiaCountCaresSim(Gia_Man_t * p)343 int Ssc_GiaCountCaresSim( Gia_Man_t * p )
344 {
345 word * pRes = Ssc_GiaGetCareMask( p );
346 int nWords = Gia_ObjSimWords( p );
347 int Count = Ssc_SimCountBits( pRes, nWords );
348 ABC_FREE( pRes );
349 return Count;
350 }
Ssc_GiaEstimateCare(Gia_Man_t * p,int nWords)351 int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords )
352 {
353 Ssc_GiaRandomPiPattern( p, nWords, NULL );
354 Ssc_GiaSimRound( p );
355 return Ssc_GiaCountCaresSim( p );
356 }
357
358 ////////////////////////////////////////////////////////////////////////
359 /// END OF FILE ///
360 ////////////////////////////////////////////////////////////////////////
361
362
363 ABC_NAMESPACE_IMPL_END
364
365