1 /**CFile****************************************************************
2
3 FileName [bmcInse.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "aig/gia/giaAig.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
Gia_ParTestAlloc(Gia_Man_t * p,int nWords)33 static inline void Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, 2*nWords*Gia_ManObjNum(p)); p->iData = nWords; }
Gia_ParTestFree(Gia_Man_t * p)34 static inline void Gia_ParTestFree( Gia_Man_t * p ) { ABC_FREE( p->pData ); p->iData = 0; }
Gia_ParTestObj(Gia_Man_t * p,int Id)35 static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (word *)p->pData + Id*(p->iData << 1); }
36
37 ////////////////////////////////////////////////////////////////////////
38 /// FUNCTION DEFINITIONS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 /**Function*************************************************************
42
43 Synopsis []
44
45 Description []
46
47 SideEffects []
48
49 SeeAlso []
50
51 ***********************************************************************/
Gia_ManInseInit(Gia_Man_t * p,Vec_Int_t * vInit)52 void Gia_ManInseInit( Gia_Man_t * p, Vec_Int_t * vInit )
53 {
54 Gia_Obj_t * pObj;
55 word * pData1, * pData0;
56 int i, k;
57 Gia_ManForEachRi( p, pObj, k )
58 {
59 pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
60 pData1 = pData0 + p->iData;
61 if ( Vec_IntEntry(vInit, k) == 0 ) // 0
62 for ( i = 0; i < p->iData; i++ )
63 pData0[i] = ~(word)0, pData1[i] = 0;
64 else if ( Vec_IntEntry(vInit, k) == 1 ) // 1
65 for ( i = 0; i < p->iData; i++ )
66 pData0[i] = 0, pData1[i] = ~(word)0;
67 else // if ( Vec_IntEntry(vInit, k) > 1 ) // X
68 for ( i = 0; i < p->iData; i++ )
69 pData0[i] = pData1[i] = 0;
70 }
71 }
Gia_ManInseSimulateObj(Gia_Man_t * p,int Id)72 void Gia_ManInseSimulateObj( Gia_Man_t * p, int Id )
73 {
74 Gia_Obj_t * pObj = Gia_ManObj( p, Id );
75 word * pData0, * pDataA0, * pDataB0;
76 word * pData1, * pDataA1, * pDataB1;
77 int i;
78 if ( Gia_ObjIsAnd(pObj) )
79 {
80 pData0 = Gia_ParTestObj( p, Id );
81 pData1 = pData0 + p->iData;
82 if ( Gia_ObjFaninC0(pObj) )
83 {
84 pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
85 pDataA0 = pDataA1 + p->iData;
86 if ( Gia_ObjFaninC1(pObj) )
87 {
88 pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
89 pDataB0 = pDataB1 + p->iData;
90 }
91 else
92 {
93 pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
94 pDataB1 = pDataB0 + p->iData;
95 }
96 }
97 else
98 {
99 pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
100 pDataA1 = pDataA0 + p->iData;
101 if ( Gia_ObjFaninC1(pObj) )
102 {
103 pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
104 pDataB0 = pDataB1 + p->iData;
105 }
106 else
107 {
108 pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
109 pDataB1 = pDataB0 + p->iData;
110 }
111 }
112 for ( i = 0; i < p->iData; i++ )
113 pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i];
114 }
115 else if ( Gia_ObjIsCo(pObj) )
116 {
117 pData0 = Gia_ParTestObj( p, Id );
118 pData1 = pData0 + p->iData;
119 if ( Gia_ObjFaninC0(pObj) )
120 {
121 pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
122 pDataA0 = pDataA1 + p->iData;
123 }
124 else
125 {
126 pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
127 pDataA1 = pDataA0 + p->iData;
128 }
129 for ( i = 0; i < p->iData; i++ )
130 pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
131 }
132 else if ( Gia_ObjIsCi(pObj) )
133 {
134 if ( Gia_ObjIsPi(p, pObj) )
135 {
136 pData0 = Gia_ParTestObj( p, Id );
137 pData1 = pData0 + p->iData;
138 for ( i = 0; i < p->iData; i++ )
139 pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i];
140 }
141 else
142 {
143 int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj));
144 pData0 = Gia_ParTestObj( p, Id );
145 pData1 = pData0 + p->iData;
146 pDataA0 = Gia_ParTestObj( p, Id2 );
147 pDataA1 = pDataA0 + p->iData;
148 for ( i = 0; i < p->iData; i++ )
149 pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
150 }
151 }
152 else if ( Gia_ObjIsConst0(pObj) )
153 {
154 pData0 = Gia_ParTestObj( p, Id );
155 pData1 = pData0 + p->iData;
156 for ( i = 0; i < p->iData; i++ )
157 pData0[i] = ~(word)0, pData1[i] = 0;
158 }
159 else assert( 0 );
160 }
161
162 /**Function*************************************************************
163
164 Synopsis []
165
166 Description []
167
168 SideEffects []
169
170 SeeAlso []
171
172 ***********************************************************************/
Gia_ManInseHighestScore(Gia_Man_t * p,int * pCost)173 int Gia_ManInseHighestScore( Gia_Man_t * p, int * pCost )
174 {
175 Gia_Obj_t * pObj;
176 word * pData0, * pData1;
177 int * pCounts, CountBest;
178 int i, k, b, nPats, iPat;
179 nPats = 64 * p->iData;
180 pCounts = ABC_CALLOC( int, nPats );
181 Gia_ManForEachRi( p, pObj, k )
182 {
183 pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
184 pData1 = pData0 + p->iData;
185 for ( i = 0; i < p->iData; i++ )
186 for ( b = 0; b < 64; b++ )
187 pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary
188 }
189 iPat = 0;
190 CountBest = pCounts[0];
191 for ( k = 1; k < nPats; k++ )
192 if ( CountBest < pCounts[k] )
193 CountBest = pCounts[k], iPat = k;
194 *pCost = Gia_ManRegNum(p) - CountBest; // ternary
195 ABC_FREE( pCounts );
196 return iPat;
197 }
Gia_ManInseFindStarting(Gia_Man_t * p,int iPat,Vec_Int_t * vInit,Vec_Int_t * vInputs)198 void Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs )
199 {
200 Gia_Obj_t * pObj;
201 word * pData0, * pData1;
202 int i, k;
203 Vec_IntClear( vInit );
204 Gia_ManForEachRi( p, pObj, k )
205 {
206 pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
207 pData1 = pData0 + p->iData;
208 for ( i = 0; i < p->iData; i++ )
209 assert( (pData0[i] & pData1[i]) == 0 );
210 if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
211 Vec_IntPush( vInit, 0 );
212 else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
213 Vec_IntPush( vInit, 1 );
214 else
215 Vec_IntPush( vInit, 2 );
216 }
217 Gia_ManForEachPi( p, pObj, k )
218 {
219 pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
220 pData1 = pData0 + p->iData;
221 for ( i = 0; i < p->iData; i++ )
222 assert( (pData0[i] & pData1[i]) == 0 );
223 if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
224 Vec_IntPush( vInputs, 0 );
225 else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
226 Vec_IntPush( vInputs, 1 );
227 else
228 Vec_IntPush( vInputs, 2 );
229 }
230 }
Gia_ManInseSimulate(Gia_Man_t * p,Vec_Int_t * vInit0,Vec_Int_t * vInputs,Vec_Int_t * vInit)231 Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit )
232 {
233 Vec_Int_t * vRes;
234 Gia_Obj_t * pObj, * pObjRo, * pObjRi;
235 int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
236 int i, f, iBit = 0;
237 assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
238 assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
239 assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
240 Gia_ManConst0(p)->fMark0 = 0;
241 Gia_ManForEachRi( p, pObj, i )
242 pObj->fMark0 = Vec_IntEntry(vInit0, i);
243 for ( f = 0; f < nFrames; f++ )
244 {
245 Gia_ManForEachPi( p, pObj, i )
246 pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
247 Gia_ManForEachAnd( p, pObj, i )
248 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
249 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
250 Gia_ManForEachRi( p, pObj, i )
251 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
252 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
253 pObjRo->fMark0 = pObjRi->fMark0;
254 }
255 assert( iBit == Vec_IntSize(vInputs) );
256 vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
257 Gia_ManForEachRo( p, pObj, i )
258 assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
259 Gia_ManForEachRo( p, pObj, i )
260 Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
261 Gia_ManForEachObj( p, pObj, i )
262 pObj->fMark0 = 0;
263 return vRes;
264 }
265
266 /**Function*************************************************************
267
268 Synopsis []
269
270 Description []
271
272 SideEffects []
273
274 SeeAlso []
275
276 ***********************************************************************/
Gia_ManInsePerform(Gia_Man_t * p,Vec_Int_t * vInit0,int nFrames,int nWords,int fVerbose)277 Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
278 {
279 Vec_Int_t * vRes, * vInit, * vInputs;
280 Gia_Obj_t * pObj;
281 int i, f, iPat, Cost, Cost0;
282 abctime clk, clkTotal = Abc_Clock();
283 Gia_ManRandomW( 1 );
284 if ( fVerbose )
285 printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
286 vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
287 vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
288 Gia_ParTestAlloc( p, nWords );
289 Gia_ManInseInit( p, vInit );
290 Cost0 = 0;
291 Vec_IntForEachEntry( vInit, iPat, i )
292 Cost0 += ((iPat >> 1) & 1);
293 if ( fVerbose )
294 printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 );
295 for ( f = 0; f < nFrames; f++ )
296 {
297 clk = Abc_Clock();
298 Gia_ManForEachObj( p, pObj, i )
299 Gia_ManInseSimulateObj( p, i );
300 iPat = Gia_ManInseHighestScore( p, &Cost );
301 Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
302 Gia_ManInseInit( p, vInit );
303 if ( fVerbose )
304 printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 );
305 if ( fVerbose )
306 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
307 }
308 Gia_ParTestFree( p );
309 vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
310 Vec_IntFreeP( &vInit );
311 Vec_IntFreeP( &vInputs );
312 printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) );
313 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
314 return vRes;
315 }
316
317 /**Function*************************************************************
318
319 Synopsis []
320
321 Description []
322
323 SideEffects []
324
325 SeeAlso []
326
327 ***********************************************************************/
Gia_ManInseTest(Gia_Man_t * p,Vec_Int_t * vInit0,int nFrames,int nWords,int nTimeOut,int fSim,int fVerbose)328 Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
329 {
330 Vec_Int_t * vRes, * vInit;
331 vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
332 vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
333 if ( vInit != vInit0 )
334 Vec_IntFree( vInit );
335 return vRes;
336 }
337
338
339 ////////////////////////////////////////////////////////////////////////
340 /// END OF FILE ///
341 ////////////////////////////////////////////////////////////////////////
342
343
344 ABC_NAMESPACE_IMPL_END
345
346