ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
bmcMesh2.c File Reference
#include "bmc.h"
#include "sat/bsat/satSolver.h"
Include dependency graph for bmcMesh2.c:

Go to the source code of this file.

Macros

#define NCPARS   16
 DECLARATIONS ///.
 

Functions

int Bmc_MeshAddOneHotness2 (sat_solver *pSat, int iFirst, int iLast)
 
void Bmc_MeshTest2 (Gia_Man_t *p, int X, int Y, int T, int fVerbose)
 

Macro Definition Documentation

◆ NCPARS

#define NCPARS   16

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcMesh.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Synthesis for mesh of LUTs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
bmcMesh.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 32 of file bmcMesh2.c.

Function Documentation

◆ Bmc_MeshAddOneHotness2()

int Bmc_MeshAddOneHotness2 ( sat_solver * pSat,
int iFirst,
int iLast )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file bmcMesh2.c.

75{
76 int i, j, v, pVars[100], nVars = 0, nCount = 0;
77 assert( iFirst < iLast && iFirst + 110 > iLast );
78 for ( v = iFirst; v < iLast; v++ )
79 if ( Bmc_MeshVarValue2(pSat, v) ) // v = 1
80 {
81 assert( nVars < 100 );
82 pVars[ nVars++ ] = v;
83 }
84 if ( nVars <= 1 )
85 return 0;
86 for ( i = 0; i < nVars; i++ )
87 for ( j = i+1; j < nVars; j++ )
88 {
89 int pLits[2], RetValue;
90 pLits[0] = Abc_Var2Lit( pVars[i], 1 );
91 pLits[1] = Abc_Var2Lit( pVars[j], 1 );
92 RetValue = sat_solver_addclause( pSat, pLits, pLits+2 ); assert( RetValue );
93 nCount++;
94 }
95 return nCount;
96}
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Bmc_MeshTest2()

void Bmc_MeshTest2 ( Gia_Man_t * p,
int X,
int Y,
int T,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file bmcMesh2.c.

110{
111 abctime clk = Abc_Clock();
112// sat_solver * pSat = satoko_create();
113 sat_solver * pSat = sat_solver_new();
114 Gia_Obj_t * pObj;
115 int Me[102][102] = {{0}};
116 int pN[102][2] = {{0}};
117 int I = Gia_ManPiNum(p);
118 int G = I + Gia_ManAndNum(p);
119 int i, x, y, t, g, c, status, RetValue, Lit, iVar, nClauses = 0;
120
121 assert( X <= 100 && Y <= 100 && T <= 100 && G <= 100 );
122
123 // init the graph
124 for ( i = 0; i < I; i++ )
125 pN[i][0] = pN[i][1] = -1;
126 Gia_ManForEachAnd( p, pObj, i )
127 {
128 pN[i-1][0] = Gia_ObjFaninId0(pObj, i)-1;
129 pN[i-1][1] = Gia_ObjFaninId1(pObj, i)-1;
130 }
131 if ( fVerbose )
132 {
133 printf( "The graph has %d inputs: ", Gia_ManPiNum(p) );
134 for ( i = 0; i < I; i++ )
135 printf( "%c ", 'a' + i );
136 printf( " and %d nodes: ", Gia_ManAndNum(p) );
137 for ( i = I; i < G; i++ )
138 printf( "%c=%c%c ", 'a' + i, 'a' + pN[i][0] , 'a' + pN[i][1] );
139 printf( "\n" );
140 }
141
142 // init SAT variables (time vars + graph vars + config vars)
143 // config variables: 16 = 4 buff vars + 12 node vars
144 iVar = 0;
145 for ( y = 0; y < Y; y++ )
146 for ( x = 0; x < X; x++ )
147 {
148 //printf( "%3d %3d %3d %s", iVar, iVar+T, iVar+T+G, x == X-1 ? "\n":"" );
149 Me[x][y] = iVar;
150 iVar += T + G + NCPARS + 1;
151 }
152 Me[101][100] = T;
153 Me[101][101] = G;
154 if ( fVerbose )
155 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 );
156
157 // add constraints
158
159 // time 0 and primary inputs only on the boundary
160 for ( x = 0; x < X; x++ )
161 for ( y = 0; y < Y; y++ )
162 {
163 int iTVar = Bmc_MeshTVar( Me, x, y );
164 int iGVar = Bmc_MeshGVar( Me, x, y );
165
166 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
167 {
168 // time 0 is required
169 for ( t = 0; t < T; t++ )
170 {
171 Lit = Abc_Var2Lit( iTVar+t, (int)(t > 0) );
172 RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 ); assert( RetValue );
173 }
174 // internal nodes are not allowed
175 for ( g = I; g < G; g++ )
176 {
177 Lit = Abc_Var2Lit( iGVar+g, 1 );
178 RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 ); assert( RetValue );
179 }
180 }
181 else // not a boundary
182 {
183 Lit = Abc_Var2Lit( iTVar, 1 ); // cannot have time 0
184 RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 ); assert( RetValue );
185 }
186 }
187 for ( x = 1; x < X-1; x++ )
188 for ( y = 1; y < Y-1; y++ )
189 {
190 int pLits[100], nLits;
191
192 int iTVar = Bmc_MeshTVar( Me, x, y );
193 int iGVar = Bmc_MeshGVar( Me, x, y );
194 int iCVar = Bmc_MeshCVar( Me, x, y );
195 int iUVar = Bmc_MeshUVar( Me, x, y );
196
197 // 0=left 1=up 2=right 3=down
198 int iTVars[4];
199 int iGVars[4];
200
201 iTVars[0] = Bmc_MeshTVar( Me, x-1, y );
202 iGVars[0] = Bmc_MeshGVar( Me, x-1, y );
203
204 iTVars[1] = Bmc_MeshTVar( Me, x, y-1 );
205 iGVars[1] = Bmc_MeshGVar( Me, x, y-1 );
206
207 iTVars[2] = Bmc_MeshTVar( Me, x+1, y );
208 iGVars[2] = Bmc_MeshGVar( Me, x+1, y );
209
210 iTVars[3] = Bmc_MeshTVar( Me, x, y+1 );
211 iGVars[3] = Bmc_MeshGVar( Me, x, y+1 );
212
213 // condition when cell is used
214 for ( g = 0; g < G; g++ )
215 {
216 pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
217 pLits[1] = Abc_Var2Lit( iUVar, 0 );
218 RetValue = sat_solver_addclause( pSat, pLits, pLits+2 ); assert( RetValue );
219 nClauses++;
220 }
221
222 // at least one time is used
223 pLits[0] = Abc_Var2Lit( iUVar, 1 );
224 for ( t = 1; t < T; t++ )
225 pLits[t] = Abc_Var2Lit( iTVar+t, 0 );
226 RetValue = sat_solver_addclause( pSat, pLits, pLits+T ); assert( RetValue );
227 nClauses++;
228
229 // at least one config is used
230 pLits[0] = Abc_Var2Lit( iUVar, 1 );
231 for ( c = 0; c < NCPARS; c++ )
232 pLits[c+1] = Abc_Var2Lit( iCVar+c, 0 );
233 RetValue = sat_solver_addclause( pSat, pLits, pLits+NCPARS+1 ); assert( RetValue );
234 nClauses++;
235
236 // constraints for each time
237 for ( t = 1; t < T; t++ )
238 {
239 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}};
240 // buffer
241 for ( g = 0; g < G; g++ )
242 for ( c = 0; c < 4; c++ )
243 {
244 nLits = 0;
245 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
246 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
247 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 );
248 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[c]+t-1, 0 );
249 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
250
251 nLits = 0;
252 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
253 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
254 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 );
255 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[c]+g, 0 );
256 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
257
258 nClauses += 2;
259 }
260 for ( g = 0; g < I; g++ )
261 for ( c = 4; c < NCPARS; c++ )
262 {
263 pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
264 pLits[1] = Abc_Var2Lit( iCVar+c, 1 );
265 RetValue = sat_solver_addclause( pSat, pLits, pLits+2 ); assert( RetValue );
266 nClauses++;
267 }
268 // node
269 for ( g = I; g < G; g++ )
270 for ( c = 0; c < 12; c++ )
271 {
272 assert( pN[g][0] >= 0 && pN[g][1] >= 0 );
273 assert( pN[g][0] < g && pN[g][1] < g );
274
275 nLits = 0;
276 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
277 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
278 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
279 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][0]]+t-1, 0 );
280 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
281
282 nLits = 0;
283 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
284 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
285 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
286 pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][1]]+t-1, 0 );
287 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
288
289
290 nLits = 0;
291 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
292 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
293 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
294 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][0]]+pN[g][0], 0 );
295 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
296
297 nLits = 0;
298 pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 );
299 pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 );
300 pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 );
301 pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][1]]+pN[g][1], 0 );
302 RetValue = sat_solver_addclause( pSat, pLits, pLits+nLits ); assert( RetValue );
303
304 nClauses += 4;
305 }
306 }
307 }
308
309 // final condition
310 {
311 int iGVar = Bmc_MeshGVar( Me, 1, 1 ) + G-1;
312 Lit = Abc_Var2Lit( iGVar, 0 );
313 RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
314 if ( RetValue == 0 )
315 {
316 printf( "Problem has no solution. " );
317 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
318// satoko_destroy( pSat );
319 sat_solver_delete( pSat );
320 return;
321 }
322 }
323
324 if ( fVerbose )
325 printf( "Finished adding %d clauses. Started solving...\n", nClauses );
326
327 while ( 1 )
328 {
329 int nAddClauses = 0;
330// status = satoko_solve( pSat );
331 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
332// if ( status == SATOKO_UNSAT )
333 if ( status == l_False )
334 {
335 printf( "Problem has no solution. " );
336 break;
337 }
338// if ( status == SATOKO_UNDEC )
339 if ( status == l_Undef )
340 {
341 printf( "Computation timed out. " );
342 break;
343 }
344// assert( status == SATOKO_SAT );
345 assert( status == l_True );
346 // check if the solution is valid and add constraints
347 for ( x = 0; x < X; x++ )
348 for ( y = 0; y < Y; y++ )
349 {
350 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
351 {
352 int iGVar = Bmc_MeshGVar( Me, x, y );
353 nAddClauses += Bmc_MeshAddOneHotness2( pSat, iGVar, iGVar + G );
354 }
355 else
356 {
357 int iTVar = Bmc_MeshTVar( Me, x, y );
358 int iGVar = Bmc_MeshGVar( Me, x, y );
359 int iCVar = Bmc_MeshCVar( Me, x, y );
360 nAddClauses += Bmc_MeshAddOneHotness2( pSat, iTVar, iTVar + T );
361 nAddClauses += Bmc_MeshAddOneHotness2( pSat, iGVar, iGVar + G );
362 nAddClauses += Bmc_MeshAddOneHotness2( pSat, iCVar, iCVar + NCPARS );
363 }
364 }
365 if ( nAddClauses > 0 )
366 {
367 printf( "Adding %d one-hotness clauses.\n", nAddClauses );
368 continue;
369 }
370 printf( "Satisfying solution found. " );
371/*
372// iVar = satoko_varnum(pSat);
373 iVar = sat_solver_nvars(pSat);
374 for ( i = 0; i < iVar; i++ )
375 if ( Bmc_MeshVarValue2(pSat, i) )
376 printf( "%d ", i );
377 printf( "\n" );
378*/
379 break;
380 }
381 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
382// if ( status == SATOKO_SAT )
383 if ( status == l_True )
384 {
385 // count the number of nodes and buffers
386 int nBuffs = 0, nNodes = 0;
387 for ( y = 1; y < Y-1; y++ )
388 for ( x = 1; x < X-1; x++ )
389 {
390 int iCVar = Bmc_MeshCVar( Me, x, y );
391 for ( c = 0; c < 4; c++ )
392 if ( Bmc_MeshVarValue2(pSat, iCVar+c) )
393 {
394 //printf( "Buffer y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c );
395 nBuffs++;
396 }
397 for ( c = 4; c < NCPARS; c++ )
398 if ( Bmc_MeshVarValue2(pSat, iCVar+c) )
399 {
400 //printf( "Node y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c );
401 nNodes++;
402 }
403 }
404 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 );
405 // print mesh
406 printf( " Y\\X " );
407 for ( x = 0; x < X; x++ )
408 printf( " %-2d ", x );
409 printf( "\n" );
410 for ( y = 0; y < Y; y++ )
411 {
412 printf( " %-2d ", y );
413 for ( x = 0; x < X; x++ )
414 {
415 int iTVar = Bmc_MeshTVar( Me, x, y );
416 int iGVar = Bmc_MeshGVar( Me, x, y );
417
418 int fFound = 0; ;
419 for ( t = 0; t < T; t++ )
420 for ( g = 0; g < G; g++ )
421 if ( Bmc_MeshVarValue2(pSat, iTVar+t) && Bmc_MeshVarValue2(pSat, iGVar+g) )
422 {
423 printf( " %c%-2d ", 'a' + g, t );
424 fFound = 1;
425 }
426 if ( fFound )
427 continue;
428 if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
429 printf( " * " );
430 else
431 printf( " " );
432 }
433 printf( "\n" );
434 }
435 }
436 //satoko_destroy( pSat );
437 sat_solver_delete( pSat );
438}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Bmc_MeshAddOneHotness2
int Bmc_MeshAddOneHotness2(sat_solver *pSat, int iFirst, int iLast)
Definition bmcMesh2.c:74
NCPARS
#define NCPARS
DECLARATIONS ///.
Definition bmcMesh.c:31
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
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
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Here is the call graph for this function: