ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bmcMesh.c
Go to the documentation of this file.
1
20
21#include "bmc.h"
22#include "sat/satoko/satoko.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
31#define NCPARS 16
32
33static inline int Bmc_MeshTVar( int Me[102][102], int x, int y ) { return Me[x][y]; }
34static inline int Bmc_MeshGVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100]; }
35static inline int Bmc_MeshCVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100] + Me[101][101]; }
36static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100] + Me[101][101] + NCPARS; }
37
41
53static inline int Bmc_MeshVarValue( satoko_t * p, int v )
54{
55// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v);
56// return value == SATOKO_LIT_TRUE;
57 return satoko_var_polarity(p, v) == SATOKO_LIT_TRUE;
58}
59
71int Bmc_MeshAddOneHotness( satoko_t * pSat, int iFirst, int iLast )
72{
73 int i, j, v, pVars[100], nVars = 0, nCount = 0;
74 assert( iFirst < iLast && iFirst + 110 > iLast );
75 for ( v = iFirst; v < iLast; v++ )
76 if ( Bmc_MeshVarValue(pSat, v) ) // v = 1
77 {
78 assert( nVars < 100 );
79 pVars[ nVars++ ] = v;
80 }
81 if ( nVars <= 1 )
82 return 0;
83 for ( i = 0; i < nVars; i++ )
84 for ( j = i+1; j < nVars; j++ )
85 {
86 int pLits[2], RetValue;
87 pLits[0] = Abc_Var2Lit( pVars[i], 1 );
88 pLits[1] = Abc_Var2Lit( pVars[j], 1 );
89 RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue );
90 nCount++;
91 }
92 return nCount;
93}
94
106void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
107{
108 abctime clk = Abc_Clock();
109 satoko_t * pSat = satoko_create();
110 Gia_Obj_t * pObj;
111 int Me[102][102] = {{0}};
112 int pN[102][2] = {{0}};
113 int I = Gia_ManPiNum(p);
114 int G = I + Gia_ManAndNum(p);
115 int i, x, y, t, g, c, status, RetValue, Lit, iVar, nClauses = 0;
116
117 assert( X <= 100 && Y <= 100 && T <= 100 && G <= 100 );
118
119 // init the graph
120 for ( i = 0; i < I; i++ )
121 pN[i][0] = pN[i][1] = -1;
122 Gia_ManForEachAnd( p, pObj, i )
123 {
124 pN[i-1][0] = Gia_ObjFaninId0(pObj, i)-1;
125 pN[i-1][1] = Gia_ObjFaninId1(pObj, i)-1;
126 }
127 if ( fVerbose )
128 {
129 printf( "The graph has %d inputs: ", Gia_ManPiNum(p) );
130 for ( i = 0; i < I; i++ )
131 printf( "%c ", 'a' + i );
132 printf( " and %d nodes: ", Gia_ManAndNum(p) );
133 for ( i = I; i < G; i++ )
134 printf( "%c=%c%c ", 'a' + i, 'a' + pN[i][0] , 'a' + pN[i][1] );
135 printf( "\n" );
136 }
137
138 // init SAT variables (time vars + graph vars + config vars)
139 // config variables: 16 = 4 buff vars + 12 node vars
140 iVar = 0;
141 for ( y = 0; y < Y; y++ )
142 for ( x = 0; x < X; x++ )
143 {
144 //printf( "%3d %3d %3d %s", iVar, iVar+T, iVar+T+G, x == X-1 ? "\n":"" );
145 Me[x][y] = iVar;
146 iVar += T + G + NCPARS + 1;
147 }
148 Me[101][100] = T;
149 Me[101][101] = G;
150 if ( fVerbose )
151 printf( "SAT variable count is %d (%d time vars + %d graph vars + %d config vars + %d aux vars)\n", iVar, X*Y*T, X*Y*G, X*Y*NCPARS, X*Y );
152
153 // add constraints
154
155 // time 0 and primary inputs only on the boundary
156 for ( x = 0; x < X; x++ )
157 for ( y = 0; y < Y; y++ )
158 {
159 int iTVar = Bmc_MeshTVar( Me, x, y );
160 int iGVar = Bmc_MeshGVar( Me, x, y );
161
162 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
163 {
164 // time 0 is required
165 for ( t = 0; t < T; t++ )
166 {
167 Lit = Abc_Var2Lit( iTVar+t, (int)(t > 0) );
168 RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue );
169 }
170 // internal nodes are not allowed
171 for ( g = I; g < G; g++ )
172 {
173 Lit = Abc_Var2Lit( iGVar+g, 1 );
174 RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue );
175 }
176 }
177 else // not a boundary
178 {
179 Lit = Abc_Var2Lit( iTVar, 1 ); // cannot have time 0
180 RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue );
181 }
182 }
183 for ( x = 1; x < X-1; x++ )
184 for ( y = 1; y < Y-1; y++ )
185 {
186 int pLits[100], nLits;
187
188 int iTVar = Bmc_MeshTVar( Me, x, y );
189 int iGVar = Bmc_MeshGVar( Me, x, y );
190 int iCVar = Bmc_MeshCVar( Me, x, y );
191 int iUVar = Bmc_MeshUVar( Me, x, y );
192
193 // 0=left 1=up 2=right 3=down
194 int iTVars[4];
195 int iGVars[4];
196
197 iTVars[0] = Bmc_MeshTVar( Me, x-1, y );
198 iGVars[0] = Bmc_MeshGVar( Me, x-1, y );
199
200 iTVars[1] = Bmc_MeshTVar( Me, x, y-1 );
201 iGVars[1] = Bmc_MeshGVar( Me, x, y-1 );
202
203 iTVars[2] = Bmc_MeshTVar( Me, x+1, y );
204 iGVars[2] = Bmc_MeshGVar( Me, x+1, y );
205
206 iTVars[3] = Bmc_MeshTVar( Me, x, y+1 );
207 iGVars[3] = Bmc_MeshGVar( Me, x, y+1 );
208
209 // condition when cell is used
210 for ( g = 0; g < G; g++ )
211 {
212 pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
213 pLits[1] = Abc_Var2Lit( iUVar, 0 );
214 RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue );
215 nClauses++;
216 }
217
218 // at least one time is used
219 pLits[0] = Abc_Var2Lit( iUVar, 1 );
220 for ( t = 1; t < T; t++ )
221 pLits[t] = Abc_Var2Lit( iTVar+t, 0 );
222 RetValue = satoko_add_clause( pSat, pLits, T ); assert( RetValue );
223 nClauses++;
224
225 // at least one config is used
226 pLits[0] = Abc_Var2Lit( iUVar, 1 );
227 for ( c = 0; c < NCPARS; c++ )
228 pLits[c+1] = Abc_Var2Lit( iCVar+c, 0 );
229 RetValue = satoko_add_clause( pSat, pLits, NCPARS+1 ); assert( RetValue );
230 nClauses++;
231
232 // constraints for each time
233 for ( t = 1; t < T; t++ )
234 {
235 int Conf[12][2] = {{0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 3}, {2, 3}, {1, 0}, {2, 0}, {3, 0}, {2, 1}, {3, 1}, {3, 2}};
236 // buffer
237 for ( g = 0; g < G; g++ )
238 for ( c = 0; c < 4; c++ )
239 {
240 nLits = 0;
241 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
242 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
243 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 );
244 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[c]+t-1, 0 );
245 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
246
247 nLits = 0;
248 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
249 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
250 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 );
251 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[c]+g, 0 );
252 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
253
254 nClauses += 2;
255 }
256 for ( g = 0; g < I; g++ )
257 for ( c = 4; c < NCPARS; c++ )
258 {
259 pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
260 pLits[1] = Abc_Var2Lit( iCVar+c, 1 );
261 RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue );
262 nClauses++;
263 }
264 // node
265 for ( g = I; g < G; g++ )
266 for ( c = 0; c < 12; c++ )
267 {
268 assert( pN[g][0] >= 0 && pN[g][1] >= 0 );
269
270 nLits = 0;
271 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
272 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
273 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
274 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][0]]+t-1, 0 );
275 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
276
277 nLits = 0;
278 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
279 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
280 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
281 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][1]]+t-1, 0 );
282 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
283
284
285 nLits = 0;
286 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
287 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
288 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
289 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][0]]+pN[g][0], 0 );
290 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
291
292 nLits = 0;
293 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
294 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
295 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
296 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][1]]+pN[g][1], 0 );
297 RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue );
298
299 nClauses += 4;
300 }
301 }
302 }
303
304 // final condition
305 {
306 int iGVar = Bmc_MeshGVar( Me, 1, 1 ) + G-1;
307 Lit = Abc_Var2Lit( iGVar, 0 );
308 RetValue = satoko_add_clause( pSat, &Lit, 1 );
309 if ( RetValue == 0 )
310 {
311 printf( "Problem has no solution. " );
312 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
313 satoko_destroy( pSat );
314 return;
315 }
316 }
317
318 if ( fVerbose )
319 printf( "Finished adding %d clauses. Started solving...\n", nClauses );
320
321 while ( 1 )
322 {
323 int nAddClauses = 0;
324 status = satoko_solve( pSat );
325 if ( status == SATOKO_UNSAT )
326 {
327 printf( "Problem has no solution. " );
328 break;
329 }
330 if ( status == SATOKO_UNDEC )
331 {
332 printf( "Computation timed out. " );
333 break;
334 }
335 assert( status == SATOKO_SAT );
336 // check if the solution is valid and add constraints
337 for ( x = 0; x < X; x++ )
338 for ( y = 0; y < Y; y++ )
339 {
340 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
341 {
342 int iGVar = Bmc_MeshGVar( Me, x, y );
343 nAddClauses += Bmc_MeshAddOneHotness( pSat, iGVar, iGVar + G );
344 }
345 else
346 {
347 int iTVar = Bmc_MeshTVar( Me, x, y );
348 int iGVar = Bmc_MeshGVar( Me, x, y );
349 int iCVar = Bmc_MeshCVar( Me, x, y );
350 nAddClauses += Bmc_MeshAddOneHotness( pSat, iTVar, iTVar + T );
351 nAddClauses += Bmc_MeshAddOneHotness( pSat, iGVar, iGVar + G );
352 nAddClauses += Bmc_MeshAddOneHotness( pSat, iCVar, iCVar + NCPARS );
353 }
354 }
355 if ( nAddClauses > 0 )
356 {
357 printf( "Adding %d one-hotness clauses.\n", nAddClauses );
358 continue;
359 }
360 printf( "Satisfying solution found. " );
361/*
362 iVar = satoko_varnum(pSat);
363 for ( i = 0; i < iVar; i++ )
364 if ( Bmc_MeshVarValue(pSat, i) )
365 printf( "%d ", i );
366 printf( "\n" );
367*/
368 break;
369 }
370 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
371 if ( status == SATOKO_SAT )
372 {
373 // count the number of nodes and buffers
374 int nBuffs = 0, nNodes = 0;
375 for ( y = 1; y < Y-1; y++ )
376 for ( x = 1; x < X-1; x++ )
377 {
378 int iCVar = Bmc_MeshCVar( Me, x, y );
379 for ( c = 0; c < 4; c++ )
380 if ( Bmc_MeshVarValue(pSat, iCVar+c) )
381 {
382 //printf( "Buffer y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c );
383 nBuffs++;
384 }
385 for ( c = 4; c < NCPARS; c++ )
386 if ( Bmc_MeshVarValue(pSat, iCVar+c) )
387 {
388 //printf( "Node y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c );
389 nNodes++;
390 }
391 }
392 printf( "The %d x %d mesh with latency %d with %d active cells (%d nodes and %d buffers):\n", X, Y, T, nNodes+nBuffs, nNodes, nBuffs );
393 // print mesh
394 printf( " Y\\X " );
395 for ( x = 0; x < X; x++ )
396 printf( " %-2d ", x );
397 printf( "\n" );
398 for ( y = 0; y < Y; y++ )
399 {
400 printf( " %-2d ", y );
401 for ( x = 0; x < X; x++ )
402 {
403 int iTVar = Bmc_MeshTVar( Me, x, y );
404 int iGVar = Bmc_MeshGVar( Me, x, y );
405
406 int fFound = 0; ;
407 for ( t = 0; t < T; t++ )
408 for ( g = 0; g < G; g++ )
409 if ( Bmc_MeshVarValue(pSat, iTVar+t) && Bmc_MeshVarValue(pSat, iGVar+g) )
410 {
411 printf( " %c%-2d ", 'a' + g, t );
412 fFound = 1;
413 }
414 if ( fFound )
415 continue;
416 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
417 printf( " * " );
418 else
419 printf( " " );
420 }
421 printf( "\n" );
422 }
423 }
424 satoko_destroy( pSat );
425}
426
430
431
432ABC_NAMESPACE_IMPL_END
433
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
NCPARS
#define NCPARS
DECLARATIONS ///.
Definition bmcMesh.c:31
Bmc_MeshAddOneHotness
int Bmc_MeshAddOneHotness(satoko_t *pSat, int iFirst, int iLast)
Definition bmcMesh.c:71
Bmc_MeshTest
void Bmc_MeshTest(Gia_Man_t *p, int X, int Y, int T, int fVerbose)
Definition bmcMesh.c:106
p
Cube * p
Definition exorList.c:222
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
satoko_solve
int satoko_solve(satoko_t *)
Definition solver_api.c:314
SATOKO_UNSAT
@ SATOKO_UNSAT
Definition satoko.h:25
SATOKO_SAT
@ SATOKO_SAT
Definition satoko.h:24
SATOKO_UNDEC
@ SATOKO_UNDEC
Definition satoko.h:23
satoko_var_polarity
char satoko_var_polarity(satoko_t *, unsigned)
Definition solver_api.c:672
SATOKO_LIT_TRUE
@ SATOKO_LIT_TRUE
Definition satoko.h:30
satoko_add_clause
int satoko_add_clause(satoko_t *, int *, int)
Definition solver_api.c:255
satoko_t
struct solver_t_ satoko_t
Definition satoko.h:35
satoko_destroy
void satoko_destroy(satoko_t *)
Definition solver_api.c:132
satoko_create
satoko_t * satoko_create(void)
Definition solver_api.c:88
assert
#define assert(ex)
Definition util_old.h:213