1 /**CFile****************************************************************
2
3 FileName [ifTune.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [FPGA mapping based on priority cuts.]
8
9 Synopsis [Library tuning.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 21, 2006.]
16
17 Revision [$Id: ifTune.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "if.h"
22 #include "aig/gia/giaAig.h"
23 #include "sat/bsat/satStore.h"
24 #include "sat/cnf/cnf.h"
25 #include "misc/extra/extra.h"
26 #include "bool/kit/kit.h"
27
28 ABC_NAMESPACE_IMPL_START
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 #define IFN_INS 11
35 #define IFN_WRD (IFN_INS > 6 ? 1 << (IFN_INS-6) : 1)
36 #define IFN_PAR 1024
37
38 // network types
39 typedef enum {
40 IFN_DSD_NONE = 0, // 0: unknown
41 IFN_DSD_CONST0, // 1: constant
42 IFN_DSD_VAR, // 2: variable
43 IFN_DSD_AND, // 3: AND
44 IFN_DSD_XOR, // 4: XOR
45 IFN_DSD_MUX, // 5: MUX
46 IFN_DSD_PRIME // 6: PRIME
47 } Ifn_DsdType_t;
48
49 // object types
50 static char * Ifn_Symbs[16] = {
51 NULL, // 0: unknown
52 "const", // 1: constant
53 "var", // 2: variable
54 "()", // 3: AND
55 "[]", // 4: XOR
56 "<>", // 5: MUX
57 "{}" // 6: PRIME
58 };
59
60 typedef struct Ifn_Obj_t_ Ifn_Obj_t;
61 struct Ifn_Obj_t_
62 {
63 unsigned Type : 3; // node type
64 unsigned nFanins : 5; // fanin counter
65 unsigned iFirst : 8; // first parameter
66 unsigned Var : 16; // current variable
67 int Fanins[IFN_INS]; // fanin IDs
68 };
69 struct Ifn_Ntk_t_
70 {
71 // cell structure
72 int nInps; // inputs
73 int nObjs; // objects
74 Ifn_Obj_t Nodes[2*IFN_INS]; // nodes
75 // constraints
76 int pConstr[IFN_INS*IFN_INS]; // constraint pairs
77 int nConstr; // number of pairs
78 // user data
79 int nVars; // variables
80 int nWords; // truth table words
81 int nParsVNum; // selection parameters per variable
82 int nParsVIni; // first selection parameter
83 int nPars; // total parameters
84 word * pTruth; // user truth table
85 // matching procedures
86 int Values[IFN_PAR]; // variable values
87 word pTtElems[IFN_INS*IFN_WRD]; // elementary truth tables
88 word pTtObjs[2*IFN_INS*IFN_WRD]; // object truth tables
89 };
90
Ifn_ElemTruth(Ifn_Ntk_t * p,int i)91 static inline word * Ifn_ElemTruth( Ifn_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); }
Ifn_ObjTruth(Ifn_Ntk_t * p,int i)92 static inline word * Ifn_ObjTruth( Ifn_Ntk_t * p, int i ) { return p->pTtObjs + i * p->nWords; }
93
94 // variable ordering
95 // - primary inputs [0; p->nInps)
96 // - internal nodes [p->nInps; p->nObjs)
97 // - configuration params [p->nObjs; p->nParsVIni)
98 // - variable selection params [p->nParsVIni; p->nPars)
99
100 ////////////////////////////////////////////////////////////////////////
101 /// FUNCTION DEFINITIONS ///
102 ////////////////////////////////////////////////////////////////////////
103
104 /**Function*************************************************************
105
106 Synopsis [Prepare network to check the given function.]
107
108 Description []
109
110 SideEffects []
111
112 SeeAlso []
113
114 ***********************************************************************/
Ifn_Prepare(Ifn_Ntk_t * p,word * pTruth,int nVars)115 int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
116 {
117 int i, fVerbose = 0;
118 assert( nVars <= p->nInps );
119 p->pTruth = pTruth;
120 p->nVars = nVars;
121 p->nWords = Abc_TtWordNum(nVars);
122 p->nPars = p->nObjs;
123 for ( i = p->nInps; i < p->nObjs; i++ )
124 {
125 if ( p->Nodes[i].Type != IFN_DSD_PRIME )
126 continue;
127 p->Nodes[i].iFirst = p->nPars;
128 p->nPars += (1 << p->Nodes[i].nFanins);
129 if ( fVerbose )
130 printf( "Node %d Start %d Vars %d\n", i, p->Nodes[i].iFirst, (1 << p->Nodes[i].nFanins) );
131 }
132 if ( fVerbose )
133 printf( "Groups start %d\n", p->nPars );
134 p->nParsVIni = p->nPars;
135 p->nParsVNum = Abc_Base2Log(nVars);
136 p->nPars += p->nParsVNum * p->nInps;
137 assert( p->nPars <= IFN_PAR );
138 memset( p->Values, 0xFF, sizeof(int) * p->nPars );
139 return p->nPars;
140 }
Ifn_NtkPrint(Ifn_Ntk_t * p)141 void Ifn_NtkPrint( Ifn_Ntk_t * p )
142 {
143 int i, k;
144 if ( p == NULL )
145 printf( "String is empty.\n" );
146 if ( p == NULL )
147 return;
148 for ( i = p->nInps; i < p->nObjs; i++ )
149 {
150 printf( "%c=", 'a'+i );
151 printf( "%c", Ifn_Symbs[p->Nodes[i].Type][0] );
152 for ( k = 0; k < (int)p->Nodes[i].nFanins; k++ )
153 printf( "%c", 'a'+p->Nodes[i].Fanins[k] );
154 printf( "%c", Ifn_Symbs[p->Nodes[i].Type][1] );
155 printf( ";" );
156 }
157 printf( "\n" );
158 }
Ifn_NtkLutSizeMax(Ifn_Ntk_t * p)159 int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
160 {
161 int i, LutSize = 0;
162 for ( i = p->nInps; i < p->nObjs; i++ )
163 if ( p->Nodes[i].Type == IFN_DSD_PRIME )
164 LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
165 return LutSize;
166 }
Ifn_NtkInputNum(Ifn_Ntk_t * p)167 int Ifn_NtkInputNum( Ifn_Ntk_t * p )
168 {
169 return p->nInps;
170 }
171
172 /**Function*************************************************************
173
174 Synopsis []
175
176 Description []
177
178 SideEffects []
179
180 SeeAlso []
181
182 ***********************************************************************/
Ifn_ErrorMessage(const char * format,...)183 int Ifn_ErrorMessage( const char * format, ... )
184 {
185 char * pMessage;
186 va_list args;
187 va_start( args, format );
188 pMessage = vnsprintf( format, args );
189 va_end( args );
190 printf( "%s", pMessage );
191 ABC_FREE( pMessage );
192 return 0;
193 }
Inf_ManOpenSymb(char * pStr)194 int Inf_ManOpenSymb( char * pStr )
195 {
196 if ( pStr[0] == '(' )
197 return 3;
198 if ( pStr[0] == '[' )
199 return 4;
200 if ( pStr[0] == '<' )
201 return 5;
202 if ( pStr[0] == '{' )
203 return 6;
204 return 0;
205 }
Ifn_ManStrCheck(char * pStr,int * pnInps,int * pnObjs)206 int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
207 {
208 int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1;
209 for ( i = 0; pStr[i]; i++ )
210 {
211 if ( Inf_ManOpenSymb(pStr+i) )
212 nNodes++;
213 if ( pStr[i] == ';' ||
214 pStr[i] == '(' || pStr[i] == ')' ||
215 pStr[i] == '[' || pStr[i] == ']' ||
216 pStr[i] == '<' || pStr[i] == '>' ||
217 pStr[i] == '{' || pStr[i] == '}' )
218 continue;
219 if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
220 continue;
221 if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
222 {
223 MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') );
224 Marks[pStr[i] - 'a'] = 1;
225 continue;
226 }
227 return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
228 }
229 for ( i = 0; i <= MaxVar; i++ )
230 if ( Marks[i] == 0 )
231 return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
232 *pnInps = MaxVar + 1;
233 *pnObjs = MaxVar + 1 + nNodes;
234 return 1;
235 }
Ifn_NtkParseFindClosingParenthesis(char * pStr,char Open,char Close)236 static inline char * Ifn_NtkParseFindClosingParenthesis( char * pStr, char Open, char Close )
237 {
238 int Counter = 0;
239 assert( *pStr == Open );
240 for ( ; *pStr; pStr++ )
241 {
242 if ( *pStr == Open )
243 Counter++;
244 if ( *pStr == Close )
245 Counter--;
246 if ( Counter == 0 )
247 return pStr;
248 }
249 return NULL;
250 }
Ifn_NtkParseInt_rec(char * pStr,Ifn_Ntk_t * p,char ** ppFinal,int * piNode)251 int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode )
252 {
253 Ifn_Obj_t * pObj;
254 int nFanins = 0, pFanins[IFN_INS];
255 int Type = Inf_ManOpenSymb( pStr );
256 char * pLim = Ifn_NtkParseFindClosingParenthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
257 *ppFinal = NULL;
258 if ( pLim == NULL )
259 return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] );
260 while ( pStr < pLim )
261 {
262 assert( nFanins < IFN_INS );
263 if ( pStr[0] >= 'a' && pStr[0] <= 'z' )
264 pFanins[nFanins++] = pStr[0] - 'a', pStr++;
265 else if ( Inf_ManOpenSymb(pStr) )
266 {
267 if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) )
268 return 0;
269 pFanins[nFanins++] = *piNode - 1;
270 }
271 else
272 return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
273 }
274 assert( pStr == pLim );
275 pObj = p->Nodes + (*piNode)++;
276 pObj->Type = Type;
277 assert( pObj->nFanins == 0 );
278 pObj->nFanins = nFanins;
279 memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins );
280 *ppFinal = pLim + 1;
281 if ( Type == IFN_DSD_MUX && nFanins != 3 )
282 return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" );
283 return 1;
284 }
Ifn_NtkParseInt(char * pStr,Ifn_Ntk_t * p)285 int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
286 {
287 char * pFinal; int iNode;
288 if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
289 return 0;
290 if ( p->nInps > IFN_INS )
291 return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
292 assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
293 if ( !Inf_ManOpenSymb(pStr) )
294 return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" );
295 iNode = p->nInps;
296 if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) )
297 return 0;
298 if ( pFinal[0] && pFinal[0] != ';' )
299 return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" );
300 if ( iNode != p->nObjs )
301 return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" );
302 return 1;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis []
308
309 Description []
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Ifn_ManStrType2(char * pStr)316 int Ifn_ManStrType2( char * pStr )
317 {
318 int i;
319 for ( i = 0; pStr[i]; i++ )
320 if ( pStr[i] == '=' )
321 return 1;
322 return 0;
323 }
Ifn_ManStrCheck2(char * pStr,int * pnInps,int * pnObjs)324 int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs )
325 {
326 int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
327 for ( i = 0; pStr[i]; i++ )
328 {
329 if ( pStr[i] == '=' || pStr[i] == ';' ||
330 pStr[i] == '(' || pStr[i] == ')' ||
331 pStr[i] == '[' || pStr[i] == ']' ||
332 pStr[i] == '<' || pStr[i] == '>' ||
333 pStr[i] == '{' || pStr[i] == '}' )
334 continue;
335 if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
336 continue;
337 if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
338 {
339 if ( pStr[i+1] == '=' )
340 Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
341 continue;
342 }
343 return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
344 }
345 for ( i = 0; pStr[i]; i++ )
346 {
347 if ( pStr[i] == '=' || pStr[i] == ';' ||
348 pStr[i] == '(' || pStr[i] == ')' ||
349 pStr[i] == '[' || pStr[i] == ']' ||
350 pStr[i] == '<' || pStr[i] == '>' ||
351 pStr[i] == '{' || pStr[i] == '}' )
352 continue;
353 if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
354 continue;
355 if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
356 {
357 if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
358 Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
359 continue;
360 }
361 return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] );
362 }
363 MaxVar++;
364 MaxDef++;
365 for ( i = 0; i < MaxDef; i++ )
366 if ( Marks[i] == 0 )
367 return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i );
368 for ( i = 0; i < MaxVar; i++ )
369 if ( Marks[i] == 2 )
370 return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i );
371 for ( i = MaxVar; i < MaxDef; i++ )
372 if ( Marks[i] == 1 )
373 return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i );
374 *pnInps = MaxVar;
375 *pnObjs = MaxDef;
376 return 1;
377 }
Ifn_NtkParseInt2(char * pStr,Ifn_Ntk_t * p)378 int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
379 {
380 int i, k, n, f, nFans, iFan;
381 if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) )
382 return 0;
383 if ( p->nInps > IFN_INS )
384 return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
385 assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
386 for ( i = p->nInps; i < p->nObjs; i++ )
387 {
388 char Next = 0;
389 for ( k = 0; pStr[k]; k++ )
390 if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
391 break;
392 if ( pStr[k] == 0 )
393 return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i );
394 if ( pStr[k+2] == '(' )
395 p->Nodes[i].Type = IFN_DSD_AND, Next = ')';
396 else if ( pStr[k+2] == '[' )
397 p->Nodes[i].Type = IFN_DSD_XOR, Next = ']';
398 else if ( pStr[k+2] == '<' )
399 p->Nodes[i].Type = IFN_DSD_MUX, Next = '>';
400 else if ( pStr[k+2] == '{' )
401 p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
402 else
403 return Ifn_ErrorMessage( "Cannot find openning operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
404 for ( n = k + 3; pStr[n]; n++ )
405 if ( pStr[n] == Next )
406 break;
407 if ( pStr[n] == 0 )
408 return Ifn_ErrorMessage( "Cannot find closing operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
409 nFans = n - k - 3;
410 if ( nFans > 8 )
411 return Ifn_ErrorMessage( "Cannot find matching operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
412 for ( f = 0; f < nFans; f++ )
413 {
414 iFan = pStr[k + 3 + f] - 'a';
415 if ( iFan < 0 || iFan >= i )
416 return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
417 p->Nodes[i].Fanins[f] = iFan;
418 }
419 p->Nodes[i].nFanins = nFans;
420 }
421 return 1;
422 }
Ifn_NtkParseConstraints(char * pStr,Ifn_Ntk_t * p)423 void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p )
424 {
425 int i, k;
426 // parse constraints
427 p->nConstr = 0;
428 for ( i = 0; i < p->nInps; i++ )
429 for ( k = 0; pStr[k]; k++ )
430 if ( pStr[k] == 'A' + i && pStr[k-1] == ';' )
431 {
432 assert( p->nConstr < IFN_INS*IFN_INS );
433 p->pConstr[p->nConstr++] = ((int)(pStr[k] - 'A') << 16) | (int)(pStr[k+1] - 'A');
434 // printf( "Added constraint (%c < %c)\n", pStr[k], pStr[k+1] );
435 }
436 // if ( p->nConstr )
437 // printf( "Total constraints = %d\n", p->nConstr );
438 }
439
Ifn_NtkParse(char * pStr)440 Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
441 {
442 Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
443 if ( Ifn_ManStrType2(pStr) )
444 {
445 if ( !Ifn_NtkParseInt2( pStr, p ) )
446 {
447 ABC_FREE( p );
448 return NULL;
449 }
450 }
451 else
452 {
453 if ( !Ifn_NtkParseInt( pStr, p ) )
454 {
455 ABC_FREE( p );
456 return NULL;
457 }
458 }
459 Ifn_NtkParseConstraints( pStr, p );
460 Abc_TtElemInit2( p->pTtElems, p->nInps );
461 // printf( "Finished parsing: " ); Ifn_NtkPrint(p);
462 return p;
463 }
Ifn_NtkTtBits(char * pStr)464 int Ifn_NtkTtBits( char * pStr )
465 {
466 int i, Counter = 0;
467 Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStr );
468 for ( i = pNtk->nInps; i < pNtk->nObjs; i++ )
469 if ( pNtk->Nodes[i].Type == IFN_DSD_PRIME )
470 Counter += (1 << pNtk->Nodes[i].nFanins);
471 ABC_FREE( pNtk );
472 return Counter;
473 }
474
475
476
477 /**Function*************************************************************
478
479 Synopsis [Derive AIG.]
480
481 Description []
482
483 SideEffects []
484
485 SeeAlso []
486
487 ***********************************************************************/
Ifn_ManStrFindModel(Ifn_Ntk_t * p)488 Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
489 {
490 Gia_Man_t * pNew, * pTemp;
491 int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni );
492 pNew = Gia_ManStart( 1000 );
493 pNew->pName = Abc_UtilStrsav( "model" );
494 Gia_ManHashStart( pNew );
495 for ( i = 0; i < p->nInps; i++ )
496 pVarMap[i] = Gia_ManAppendCi(pNew);
497 for ( i = p->nObjs; i < p->nParsVIni; i++ )
498 pVarMap[i] = Gia_ManAppendCi(pNew);
499 for ( i = p->nInps; i < p->nObjs; i++ )
500 {
501 int Type = p->Nodes[i].Type;
502 int nFans = p->Nodes[i].nFanins;
503 int * pFans = p->Nodes[i].Fanins;
504 int iFanin = p->Nodes[i].iFirst;
505 if ( Type == IFN_DSD_AND )
506 {
507 iLit = 1;
508 for ( k = 0; k < nFans; k++ )
509 iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
510 pVarMap[i] = iLit;
511 }
512 else if ( Type == IFN_DSD_XOR )
513 {
514 iLit = 0;
515 for ( k = 0; k < nFans; k++ )
516 iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
517 pVarMap[i] = iLit;
518 }
519 else if ( Type == IFN_DSD_MUX )
520 {
521 assert( nFans == 3 );
522 pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
523 }
524 else if ( Type == IFN_DSD_PRIME )
525 {
526 int n, Step, pVarsData[256];
527 int nMints = (1 << nFans);
528 assert( nFans >= 0 && nFans <= 8 );
529 for ( k = 0; k < nMints; k++ )
530 pVarsData[k] = pVarMap[iFanin + k];
531 for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
532 for ( n = 0; n < nMints; n += Step << 1 )
533 pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] );
534 assert( Step == nMints );
535 pVarMap[i] = pVarsData[0];
536 }
537 else assert( 0 );
538 }
539 Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] );
540 ABC_FREE( pVarMap );
541 pNew = Gia_ManCleanup( pTemp = pNew );
542 Gia_ManStop( pTemp );
543 assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) );
544 assert( Gia_ManPoNum(pNew) == 1 );
545 return pNew;
546 }
547 // compute cofactors w.r.t. the first nIns variables
Ifn_ManStrFindCofactors(int nIns,Gia_Man_t * p)548 Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p )
549 {
550 Gia_Man_t * pNew, * pTemp;
551 Gia_Obj_t * pObj;
552 int i, m, nMints = 1 << nIns;
553 pNew = Gia_ManStart( Gia_ManObjNum(p) );
554 pNew->pName = Abc_UtilStrsav( p->pName );
555 Gia_ManHashAlloc( pNew );
556 Gia_ManConst0(p)->Value = 0;
557 Gia_ManForEachCi( p, pObj, i )
558 if ( i >= nIns )
559 pObj->Value = Gia_ManAppendCi( pNew );
560 for ( m = 0; m < nMints; m++ )
561 {
562 Gia_ManForEachCi( p, pObj, i )
563 if ( i < nIns )
564 pObj->Value = ((m >> i) & 1);
565 Gia_ManForEachAnd( p, pObj, i )
566 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
567 Gia_ManForEachPo( p, pObj, i )
568 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
569 }
570 pNew = Gia_ManCleanup( pTemp = pNew );
571 Gia_ManStop( pTemp );
572 return pNew;
573 }
574
575 /**Function*************************************************************
576
577 Synopsis [Derive SAT solver.]
578
579 Description []
580
581 SideEffects []
582
583 SeeAlso []
584
585 ***********************************************************************/
Cnf_DeriveGiaRemapped(Gia_Man_t * p)586 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
587 {
588 Cnf_Dat_t * pCnf;
589 Aig_Man_t * pAig = Gia_ManToAigSimple( p );
590 pAig->nRegs = 0;
591 pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
592 Aig_ManStop( pAig );
593 return pCnf;
594 }
Ifn_ManStrFindSolver(Gia_Man_t * p,Vec_Int_t ** pvPiVars,Vec_Int_t ** pvPoVars)595 sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
596 {
597 sat_solver * pSat;
598 Gia_Obj_t * pObj;
599 Cnf_Dat_t * pCnf;
600 int i;
601 pCnf = Cnf_DeriveGiaRemapped( p );
602 // start the SAT solver
603 pSat = sat_solver_new();
604 sat_solver_setnvars( pSat, pCnf->nVars );
605 // add timeframe clauses
606 for ( i = 0; i < pCnf->nClauses; i++ )
607 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
608 assert( 0 );
609 // inputs/outputs
610 *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
611 Gia_ManForEachCi( p, pObj, i )
612 Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
613 *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
614 Gia_ManForEachCo( p, pObj, i )
615 Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
616 Cnf_DataFree( pCnf );
617 return pSat;
618 }
Ifn_ManSatBuild(Ifn_Ntk_t * p,Vec_Int_t ** pvPiVars,Vec_Int_t ** pvPoVars)619 sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
620 {
621 Gia_Man_t * p1, * p2;
622 sat_solver * pSat = NULL;
623 *pvPiVars = *pvPoVars = NULL;
624 p1 = Ifn_ManStrFindModel( p );
625 // Gia_AigerWrite( p1, "satbuild.aig", 0, 0, 0 );
626 p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
627 Gia_ManStop( p1 );
628 // Gia_AigerWrite( p2, "satbuild2.aig", 0, 0, 0 );
629 pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
630 Gia_ManStop( p2 );
631 return pSat;
632 }
If_ManSatBuildFromCell(char * pStr,Vec_Int_t ** pvPiVars,Vec_Int_t ** pvPoVars,Ifn_Ntk_t ** ppNtk)633 void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk )
634 {
635 Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
636 Ifn_Prepare( p, NULL, p->nInps );
637 *ppNtk = p;
638 if ( p == NULL )
639 return NULL;
640 // Ifn_NtkPrint( p );
641 return Ifn_ManSatBuild( p, pvPiVars, pvPoVars );
642 }
643
644 /**Function*************************************************************
645
646 Synopsis []
647
648 Description []
649
650 SideEffects []
651
652 SeeAlso []
653
654 ***********************************************************************/
Ifn_ManSatPrintPerm(char * pPerms,int nVars)655 void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
656 {
657 int i;
658 for ( i = 0; i < nVars; i++ )
659 printf( "%c", 'a' + pPerms[i] );
660 printf( "\n" );
661 }
Ifn_ManSatCheckOne(sat_solver * pSat,Vec_Int_t * vPoVars,word * pTruth,int nVars,int * pPerm,int nInps,Vec_Int_t * vLits)662 int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
663 {
664 int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps);
665 assert( (1 << nInps) == Vec_IntSize(vPoVars) );
666 assert( nVars <= nInps );
667 // remap minterms
668 Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
669 for ( m = 0; m < nMints; m++ )
670 {
671 mNew = 0;
672 for ( v = 0; v < nInps; v++ )
673 {
674 assert( pPerm[v] < nVars );
675 if ( ((m >> pPerm[v]) & 1) )
676 mNew |= (1 << v);
677 }
678 assert( Vec_IntEntry(vLits, mNew) == -1 );
679 Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
680 }
681 // find assumptions
682 v = 0;
683 Vec_IntForEachEntry( vLits, Value, m )
684 if ( Value >= 0 )
685 Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
686 Vec_IntShrink( vLits, v );
687 // run SAT solver
688 Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
689 return (int)(Value == l_True);
690 }
Ifn_ManSatDeriveOne(sat_solver * pSat,Vec_Int_t * vPiVars,Vec_Int_t * vValues)691 void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
692 {
693 int i, iVar;
694 Vec_IntClear( vValues );
695 Vec_IntForEachEntry( vPiVars, iVar, i )
696 Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
697 }
If_ManSatFindCofigBits(void * pSat,Vec_Int_t * vPiVars,Vec_Int_t * vPoVars,word * pTruth,int nVars,word Perm,int nInps,Vec_Int_t * vValues)698 int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
699 {
700 // extract permutation
701 int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
702 assert( nInps <= IF_MAX_FUNC_LUTSIZE );
703 for ( i = 0; i < nInps; i++ )
704 {
705 pPerm[i] = Abc_TtGetHex( &Perm, i );
706 assert( pPerm[i] < nVars );
707 }
708 // perform SAT check
709 RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
710 Vec_IntClear( vValues );
711 if ( RetValue == 0 )
712 return 0;
713 Ifn_ManSatDeriveOne( (sat_solver*)pSat, vPiVars, vValues );
714 return 1;
715 }
Ifn_ManSatFindCofigBitsTest(Ifn_Ntk_t * p,word * pTruth,int nVars,word Perm)716 int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word Perm )
717 {
718 Vec_Int_t * vValues = Vec_IntAlloc( 100 );
719 Vec_Int_t * vPiVars, * vPoVars;
720 sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
721 int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
722 Vec_IntPrint( vValues );
723 // cleanup
724 sat_solver_delete( pSat );
725 Vec_IntFreeP( &vPiVars );
726 Vec_IntFreeP( &vPoVars );
727 Vec_IntFreeP( &vValues );
728 return RetValue;
729 }
730
731 /**Function*************************************************************
732
733 Synopsis [Derive GIA using programmable bits.]
734
735 Description []
736
737 SideEffects []
738
739 SeeAlso []
740
741 ***********************************************************************/
If_ManSatDeriveGiaFromBits(void * pGia,Ifn_Ntk_t * p,word * pConfigData,Vec_Int_t * vLeaves,Vec_Int_t * vCover)742 int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, word * pConfigData, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
743 {
744 Gia_Man_t * pNew = (Gia_Man_t *)pGia;
745 int i, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
746 int nTtBits = p->nParsVIni - p->nObjs;
747 int nPermBits = Abc_Base2Log(p->nInps + 1) + 1;
748 int fCompl = Abc_TtGetBit( pConfigData, nTtBits + nPermBits * p->nInps );
749 assert( Vec_IntSize(vLeaves) <= p->nInps && p->nParsVIni < 1000 );
750 for ( i = 0; i < p->nInps; i++ )
751 {
752 for ( iLit = k = 0; k < nPermBits; k++ )
753 if ( Abc_TtGetBit(pConfigData, nTtBits + i * nPermBits + k) )
754 iLit |= (1 << k);
755 assert( Abc_Lit2Var(iLit) < Vec_IntSize(vLeaves) );
756 pVarMap[i] = Abc_Lit2LitL( Vec_IntArray(vLeaves), iLit );
757 }
758 for ( i = p->nInps; i < p->nObjs; i++ )
759 {
760 int Type = p->Nodes[i].Type;
761 int nFans = p->Nodes[i].nFanins;
762 int * pFans = p->Nodes[i].Fanins;
763 //int iFanin = p->Nodes[i].iFirst;
764 assert( nFans <= 6 );
765 if ( Type == IFN_DSD_AND )
766 {
767 iLit = 1;
768 for ( k = 0; k < nFans; k++ )
769 iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
770 pVarMap[i] = iLit;
771 }
772 else if ( Type == IFN_DSD_XOR )
773 {
774 iLit = 0;
775 for ( k = 0; k < nFans; k++ )
776 iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
777 pVarMap[i] = iLit;
778 }
779 else if ( Type == IFN_DSD_MUX )
780 {
781 assert( nFans == 3 );
782 pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
783 }
784 else if ( Type == IFN_DSD_PRIME )
785 {
786 int pFaninLits[16];
787 // collect truth table
788 word uTruth = 0;
789 int nMints = (1 << nFans);
790 for ( k = 0; k < nMints; k++ )
791 if ( Abc_TtGetBit(pConfigData, iVar++) )
792 uTruth |= ((word)1 << k);
793 uTruth = Abc_Tt6Stretch( uTruth, nFans );
794 // collect function
795 for ( k = 0; k < nFans; k++ )
796 pFaninLits[k] = pVarMap[pFans[k]];
797 // implement the function
798 nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 );
799 if ( nVarsNew == 0 )
800 pVarMap[i] = (int)(uTruth & 1);
801 else
802 {
803 extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
804 Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits };
805 pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)&uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!!
806 }
807 }
808 else assert( 0 );
809 }
810 assert( iVar == nTtBits );
811 return Abc_LitNotCond( pVarMap[p->nObjs - 1], fCompl );
812 }
813
814 /**Function*************************************************************
815
816 Synopsis [Derive GIA using programmable bits.]
817
818 Description []
819
820 SideEffects []
821
822 SeeAlso []
823
824 ***********************************************************************/
If_ManDeriveGiaFromCells(void * pGia)825 void * If_ManDeriveGiaFromCells( void * pGia )
826 {
827 Gia_Man_t * p = (Gia_Man_t *)pGia;
828 Gia_Man_t * pNew, * pTemp;
829 Vec_Int_t * vCover, * vLeaves;
830 Ifn_Ntk_t * pNtkCell;
831 Gia_Obj_t * pObj;
832 word * pConfigData;
833 //word * pTruth;
834 int k, i, iLut, iVar;
835 int nConfigInts, Count = 0;
836 assert( p->vConfigs != NULL );
837 assert( p->pCellStr != NULL );
838 assert( Gia_ManHasMapping(p) );
839 // derive cell network
840 pNtkCell = Ifn_NtkParse( p->pCellStr );
841 Ifn_Prepare( pNtkCell, NULL, pNtkCell->nInps );
842 nConfigInts = Vec_IntEntry( p->vConfigs, 1 );
843 // create new manager
844 pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
845 pNew->pName = Abc_UtilStrsav( p->pName );
846 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
847 // map primary inputs
848 Gia_ManFillValue(p);
849 Gia_ManConst0(p)->Value = 0;
850 Gia_ManForEachCi( p, pObj, i )
851 pObj->Value = Gia_ManAppendCi(pNew);
852 // iterate through nodes used in the mapping
853 vLeaves = Vec_IntAlloc( 16 );
854 vCover = Vec_IntAlloc( 1 << 16 );
855 Gia_ManHashStart( pNew );
856 //Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
857 Gia_ManForEachAnd( p, pObj, iLut )
858 {
859 if ( Gia_ObjIsBuf(pObj) )
860 {
861 pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
862 continue;
863 }
864 if ( !Gia_ObjIsLut(p, iLut) )
865 continue;
866 // collect leaves
867 //Vec_IntClear( vLeaves );
868 //Gia_LutForEachFanin( p, iLut, iVar, k )
869 // Vec_IntPush( vLeaves, iVar );
870 //pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
871 // collect incoming literals
872 Vec_IntClear( vLeaves );
873 Gia_LutForEachFanin( p, iLut, iVar, k )
874 Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
875 pConfigData = (word *)Vec_IntEntryP( p->vConfigs, 2 + nConfigInts * Count++ );
876 Gia_ManObj(p, iLut)->Value = If_ManSatDeriveGiaFromBits( pNew, pNtkCell, pConfigData, vLeaves, vCover );
877 }
878 assert( Vec_IntEntry(p->vConfigs, 0) == Count );
879 assert( Vec_IntSize(p->vConfigs) == 2 + nConfigInts * Count );
880 //Gia_ObjComputeTruthTableStop( p );
881 Gia_ManForEachCo( p, pObj, i )
882 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
883 Gia_ManHashStop( pNew );
884 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
885 Vec_IntFree( vLeaves );
886 Vec_IntFree( vCover );
887 ABC_FREE( pNtkCell );
888 // perform cleanup
889 pNew = Gia_ManCleanup( pTemp = pNew );
890 Gia_ManStop( pTemp );
891 return pNew;
892
893 }
894
895 /**Function*************************************************************
896
897 Synopsis [Derive truth table given the configulation values.]
898
899 Description []
900
901 SideEffects []
902
903 SeeAlso []
904
905 ***********************************************************************/
Ifn_NtkDeriveTruth(Ifn_Ntk_t * p,int * pValues)906 word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
907 {
908 int i, v, f, iVar, iStart;
909 // elementary variables
910 for ( i = 0; i < p->nInps; i++ )
911 {
912 // find variable
913 iStart = p->nParsVIni + i * p->nParsVNum;
914 for ( v = iVar = 0; v < p->nParsVNum; v++ )
915 if ( p->Values[iStart+v] )
916 iVar += (1 << v);
917 // assign variable
918 Abc_TtCopy( Ifn_ObjTruth(p, i), Ifn_ElemTruth(p, iVar), p->nWords, 0 );
919 }
920 // internal variables
921 for ( i = p->nInps; i < p->nObjs; i++ )
922 {
923 int nFans = p->Nodes[i].nFanins;
924 int * pFans = p->Nodes[i].Fanins;
925 word * pTruth = Ifn_ObjTruth( p, i );
926 if ( p->Nodes[i].Type == IFN_DSD_AND )
927 {
928 Abc_TtFill( pTruth, p->nWords );
929 for ( f = 0; f < nFans; f++ )
930 Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
931 }
932 else if ( p->Nodes[i].Type == IFN_DSD_XOR )
933 {
934 Abc_TtClear( pTruth, p->nWords );
935 for ( f = 0; f < nFans; f++ )
936 Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
937 }
938 else if ( p->Nodes[i].Type == IFN_DSD_MUX )
939 {
940 assert( nFans == 3 );
941 Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
942 }
943 else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
944 {
945 int nValues = (1 << nFans);
946 word * pTemp = Ifn_ObjTruth(p, p->nObjs);
947 Abc_TtClear( pTruth, p->nWords );
948 for ( v = 0; v < nValues; v++ )
949 {
950 if ( pValues[p->Nodes[i].iFirst + v] == 0 )
951 continue;
952 Abc_TtFill( pTemp, p->nWords );
953 for ( f = 0; f < nFans; f++ )
954 if ( (v >> f) & 1 )
955 Abc_TtAnd( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
956 else
957 Abc_TtSharp( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords );
958 Abc_TtOr( pTruth, pTruth, pTemp, p->nWords );
959 }
960 }
961 else assert( 0 );
962 //Dau_DsdPrintFromTruth( pTruth, p->nVars );
963 }
964 return Ifn_ObjTruth(p, p->nObjs-1);
965 }
966
967 /**Function*************************************************************
968
969 Synopsis [Compute more or equal]
970
971 Description []
972
973 SideEffects []
974
975 SeeAlso []
976
977 ***********************************************************************/
Ifn_TtComparisonConstr(word * pTruth,int nVars,int fMore,int fEqual)978 void Ifn_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
979 {
980 word Cond[4], Equa[4], Temp[4];
981 word s_TtElems[8][4] = {
982 { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
983 { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
984 { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
985 { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
986 { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
987 { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
988 { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
989 { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
990 };
991 int i, nWords = Abc_TtWordNum(2*nVars);
992 assert( nVars > 0 && nVars <= 4 );
993 Abc_TtClear( pTruth, nWords );
994 Abc_TtFill( Equa, nWords );
995 for ( i = nVars - 1; i >= 0; i-- )
996 {
997 if ( fMore )
998 Abc_TtSharp( Cond, s_TtElems[2*i+1], s_TtElems[2*i+0], nWords );
999 else
1000 Abc_TtSharp( Cond, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords );
1001 Abc_TtAnd( Temp, Equa, Cond, nWords, 0 );
1002 Abc_TtOr( pTruth, pTruth, Temp, nWords );
1003 Abc_TtXor( Temp, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords, 1 );
1004 Abc_TtAnd( Equa, Equa, Temp, nWords, 0 );
1005 }
1006 if ( fEqual )
1007 Abc_TtNot( pTruth, nWords );
1008 }
1009
1010 /**Function*************************************************************
1011
1012 Synopsis [Adds parameter constraints.]
1013
1014 Description []
1015
1016 SideEffects []
1017
1018 SeeAlso []
1019
1020 ***********************************************************************/
Ifn_AddClause(sat_solver * pSat,int * pBeg,int * pEnd)1021 int Ifn_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
1022 {
1023 int fVerbose = 0;
1024 int RetValue = sat_solver_addclause( pSat, pBeg, pEnd );
1025 if ( fVerbose )
1026 {
1027 for ( ; pBeg < pEnd; pBeg++ )
1028 printf( "%c%d ", Abc_LitIsCompl(*pBeg) ? '-':'+', Abc_Lit2Var(*pBeg) );
1029 printf( "\n" );
1030 }
1031 return RetValue;
1032 }
Ifn_NtkAddConstrOne(sat_solver * pSat,Vec_Int_t * vCover,int * pVars,int nVars)1033 void Ifn_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars )
1034 {
1035 int RetValue, k, c, Cube, Literal, nLits, pLits[IFN_INS];
1036 Vec_IntForEachEntry( vCover, Cube, c )
1037 {
1038 nLits = 0;
1039 for ( k = 0; k < nVars; k++ )
1040 {
1041 Literal = 3 & (Cube >> (k << 1));
1042 if ( Literal == 1 ) // '0' -> pos lit
1043 pLits[nLits++] = Abc_Var2Lit(pVars[k], 0);
1044 else if ( Literal == 2 ) // '1' -> neg lit
1045 pLits[nLits++] = Abc_Var2Lit(pVars[k], 1);
1046 else if ( Literal != 0 )
1047 assert( 0 );
1048 }
1049 RetValue = Ifn_AddClause( pSat, pLits, pLits + nLits );
1050 assert( RetValue );
1051 }
1052 }
Ifn_NtkAddConstraints(Ifn_Ntk_t * p,sat_solver * pSat)1053 void Ifn_NtkAddConstraints( Ifn_Ntk_t * p, sat_solver * pSat )
1054 {
1055 int fAddConstr = 1;
1056 Vec_Int_t * vCover = Vec_IntAlloc( 0 );
1057 word uTruth = Abc_Tt6Stretch( ~Abc_Tt6Mask(p->nVars), p->nParsVNum );
1058 assert( p->nParsVNum <= 4 );
1059 if ( uTruth )
1060 {
1061 int i, k, pVars[IFN_INS];
1062 int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, p->nParsVNum, vCover, 0 );
1063 assert( RetValue == 0 );
1064 // Dau_DsdPrintFromTruth( &uTruth, p->nParsVNum );
1065 // add capacity constraints
1066 for ( i = 0; i < p->nInps; i++ )
1067 {
1068 for ( k = 0; k < p->nParsVNum; k++ )
1069 pVars[k] = p->nParsVIni + i * p->nParsVNum + k;
1070 Ifn_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum );
1071 }
1072 }
1073 // ordering constraints
1074 if ( fAddConstr && p->nConstr )
1075 {
1076 word pTruth[4];
1077 int i, k, RetValue, pVars[2*IFN_INS];
1078 int fForceDiff = (p->nVars == p->nInps);
1079 Ifn_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff );
1080 RetValue = Kit_TruthIsop( (unsigned *)pTruth, 2*p->nParsVNum, vCover, 0 );
1081 assert( RetValue == 0 );
1082 // Kit_TruthIsopPrintCover( vCover, 2*p->nParsVNum, 0 );
1083 for ( i = 0; i < p->nConstr; i++ )
1084 {
1085 int iVar1 = p->pConstr[i] >> 16;
1086 int iVar2 = p->pConstr[i] & 0xFFFF;
1087 for ( k = 0; k < p->nParsVNum; k++ )
1088 {
1089 pVars[2*k+0] = p->nParsVIni + iVar1 * p->nParsVNum + k;
1090 pVars[2*k+1] = p->nParsVIni + iVar2 * p->nParsVNum + k;
1091 }
1092 Ifn_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum );
1093 // printf( "added constraint with %d clauses for %d and %d\n", Vec_IntSize(vCover), iVar1, iVar2 );
1094 }
1095 }
1096 Vec_IntFree( vCover );
1097 }
1098
1099 /**Function*************************************************************
1100
1101 Synopsis [Derive clauses given variable assignment.]
1102
1103 Description []
1104
1105 SideEffects []
1106
1107 SeeAlso []
1108
1109 ***********************************************************************/
Ifn_NtkAddClauses(Ifn_Ntk_t * p,int * pValues,sat_solver * pSat)1110 int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
1111 {
1112 int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
1113 // assign new variables
1114 int nSatVars = sat_solver_nvars(pSat);
1115 // for ( i = 0; i < p->nObjs-1; i++ )
1116 for ( i = 0; i < p->nObjs; i++ )
1117 p->Nodes[i].Var = nSatVars++;
1118 //p->Nodes[p->nObjs-1].Var = 0xFFFF;
1119 sat_solver_setnvars( pSat, nSatVars );
1120 // verify variable values
1121 for ( i = 0; i < p->nVars; i++ )
1122 assert( pValues[i] != -1 );
1123 for ( i = p->nVars; i < p->nObjs-1; i++ )
1124 assert( pValues[i] == -1 );
1125 assert( pValues[p->nObjs-1] != -1 );
1126 // internal variables
1127 //printf( "\n" );
1128 for ( i = 0; i < p->nInps; i++ )
1129 {
1130 int iParStart = p->nParsVIni + i * p->nParsVNum;
1131 for ( v = 0; v < p->nVars; v++ )
1132 {
1133 // add output literal
1134 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, pValues[v]==0 );
1135 // add clause literals
1136 for ( f = 0; f < p->nParsVNum; f++ )
1137 pLits[f+1] = Abc_Var2Lit( iParStart + f, (v >> f) & 1 );
1138 if ( !Ifn_AddClause( pSat, pLits, pLits+p->nParsVNum+1 ) )
1139 return 0;
1140 }
1141 }
1142 //printf( "\n" );
1143 for ( i = p->nInps; i < p->nObjs; i++ )
1144 {
1145 int nFans = p->Nodes[i].nFanins;
1146 int * pFans = p->Nodes[i].Fanins;
1147 if ( p->Nodes[i].Type == IFN_DSD_AND )
1148 {
1149 nLits = 0;
1150 pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1151 for ( f = 0; f < nFans; f++ )
1152 {
1153 pLits[nLits++] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 1 );
1154 // add small clause
1155 pLits2[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1156 pLits2[1] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 0 );
1157 if ( !Ifn_AddClause( pSat, pLits2, pLits2 + 2 ) )
1158 return 0;
1159 }
1160 // add big clause
1161 if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
1162 return 0;
1163 }
1164 else if ( p->Nodes[i].Type == IFN_DSD_XOR )
1165 {
1166 int m, nMints = (1 << (nFans+1));
1167 for ( m = 0; m < nMints; m++ )
1168 {
1169 // skip even
1170 int Count = 0;
1171 for ( v = 0; v <= nFans; v++ )
1172 Count += ((m >> v) & 1);
1173 if ( (Count & 1) == 0 )
1174 continue;
1175 // generate minterm
1176 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, (m >> nFans) & 1 );
1177 for ( v = 0; v < nFans; v++ )
1178 pLits[v+1] = Abc_Var2Lit( p->Nodes[pFans[v]].Var, (m >> v) & 1 );
1179 if ( !Ifn_AddClause( pSat, pLits, pLits + nFans + 1 ) )
1180 return 0;
1181 }
1182 }
1183 else if ( p->Nodes[i].Type == IFN_DSD_MUX )
1184 {
1185 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1186 pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
1187 pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 1 );
1188 if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1189 return 0;
1190
1191 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1192 pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
1193 pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 0 );
1194 if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1195 return 0;
1196
1197 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1198 pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
1199 pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 1 );
1200 if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1201 return 0;
1202
1203 pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1204 pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
1205 pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 0 );
1206 if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) )
1207 return 0;
1208 }
1209 else if ( p->Nodes[i].Type == IFN_DSD_PRIME )
1210 {
1211 int nValues = (1 << nFans);
1212 int iParStart = p->Nodes[i].iFirst;
1213 for ( v = 0; v < nValues; v++ )
1214 {
1215 nLits = 0;
1216 if ( pValues[i] == -1 )
1217 {
1218 pLits[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
1219 pLits2[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
1220 nLits++;
1221 }
1222 for ( f = 0; f < nFans; f++, nLits++ )
1223 pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, (v >> f) & 1 );
1224 pLits[nLits] = Abc_Var2Lit( iParStart + v, 1 );
1225 pLits2[nLits] = Abc_Var2Lit( iParStart + v, 0 );
1226 nLits++;
1227 if ( pValues[i] != 0 )
1228 {
1229 if ( !Ifn_AddClause( pSat, pLits2, pLits2 + nLits ) )
1230 return 0;
1231 }
1232 if ( pValues[i] != 1 )
1233 {
1234 if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) )
1235 return 0;
1236 }
1237 }
1238 }
1239 else assert( 0 );
1240 //printf( "\n" );
1241 }
1242 // add last clause (not needed if the root node is IFN_DSD_PRIME)
1243 pLits[0] = Abc_Var2Lit( p->Nodes[p->nObjs-1].Var, pValues[p->nObjs-1]==0 );
1244 if ( !Ifn_AddClause( pSat, pLits, pLits + 1 ) )
1245 return 0;
1246 return 1;
1247 }
1248
1249 /**Function*************************************************************
1250
1251 Synopsis [Returns the minterm number for which there is a mismatch.]
1252
1253 Description []
1254
1255 SideEffects []
1256
1257 SeeAlso []
1258
1259 ***********************************************************************/
Ifn_NtkMatchPrintStatus(sat_solver * p,int Iter,int status,int iMint,int Value,abctime clk)1260 void Ifn_NtkMatchPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
1261 {
1262 printf( "Iter = %5d ", Iter );
1263 printf( "Mint = %5d ", iMint );
1264 printf( "Value = %2d ", Value );
1265 printf( "Var = %6d ", sat_solver_nvars(p) );
1266 printf( "Cla = %6d ", sat_solver_nclauses(p) );
1267 printf( "Conf = %6d ", sat_solver_nconflicts(p) );
1268 if ( status == l_False )
1269 printf( "status = unsat" );
1270 else if ( status == l_True )
1271 printf( "status = sat " );
1272 else
1273 printf( "status = undec" );
1274 Abc_PrintTime( 1, "Time", clk );
1275 }
Ifn_NtkMatchPrintConfig(Ifn_Ntk_t * p,sat_solver * pSat)1276 void Ifn_NtkMatchPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
1277 {
1278 int v, i;
1279 for ( v = p->nObjs; v < p->nPars; v++ )
1280 {
1281 for ( i = p->nInps; i < p->nObjs; i++ )
1282 if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
1283 break;
1284 if ( i < p->nObjs )
1285 printf( " " );
1286 else if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 )
1287 printf( " %d=", (v - p->nParsVIni) / p->nParsVNum );
1288 printf( "%d", sat_solver_var_value(pSat, v) );
1289 }
1290 }
Ifn_NtkMatchCollectPerm(Ifn_Ntk_t * p,sat_solver * pSat)1291 word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
1292 {
1293 word Perm = 0;
1294 int i, v, Mint;
1295 assert( p->nParsVNum <= 4 );
1296 for ( i = 0; i < p->nInps; i++ )
1297 {
1298 for ( Mint = v = 0; v < p->nParsVNum; v++ )
1299 if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
1300 Mint |= (1 << v);
1301 Abc_TtSetHex( &Perm, i, Mint );
1302 }
1303 return Perm;
1304 }
Ifn_NtkMatchCollectConfig(Ifn_Ntk_t * p,sat_solver * pSat,word * pConfig)1305 void Ifn_NtkMatchCollectConfig( Ifn_Ntk_t * p, sat_solver * pSat, word * pConfig )
1306 {
1307 int i, v, Mint;
1308 assert( p->nParsVNum <= 4 );
1309 for ( i = 0; i < p->nInps; i++ )
1310 {
1311 for ( Mint = v = 0; v < p->nParsVNum; v++ )
1312 if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
1313 Mint |= (1 << v);
1314 Abc_TtSetHex( pConfig, i, Mint );
1315 }
1316 for ( v = p->nObjs; v < p->nParsVIni; v++ )
1317 if ( sat_solver_var_value(pSat, v) )
1318 Abc_TtSetBit( pConfig + 1, v - p->nObjs );
1319 }
Ifn_NtkMatchPrintPerm(word Perm,int nInps)1320 void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
1321 {
1322 int i;
1323 assert( nInps <= 16 );
1324 for ( i = 0; i < nInps; i++ )
1325 printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
1326 printf( "\n" );
1327 }
Ifn_NtkMatch(Ifn_Ntk_t * p,word * pTruth,int nVars,int nConfls,int fVerbose,int fVeryVerbose,word * pConfig)1328 int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig )
1329 {
1330 word * pTruth1;
1331 int RetValue = 0;
1332 int nIterMax = (1<<nVars);
1333 int i, v, status, iMint = 0;
1334 abctime clk = Abc_Clock();
1335 // abctime clkTru = 0, clkSat = 0, clk2;
1336 sat_solver * pSat;
1337 if ( nVars == 0 )
1338 return 1;
1339 pSat = sat_solver_new();
1340 Ifn_Prepare( p, pTruth, nVars );
1341 sat_solver_setnvars( pSat, p->nPars );
1342 Ifn_NtkAddConstraints( p, pSat );
1343 if ( fVeryVerbose )
1344 Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
1345 if ( pConfig ) assert( *pConfig == 0 );
1346 for ( i = 0; i < nIterMax; i++ )
1347 {
1348 // get variable assignment
1349 for ( v = 0; v < p->nObjs; v++ )
1350 p->Values[v] = v < p->nVars ? (iMint >> v) & 1 : -1;
1351 p->Values[p->nObjs-1] = Abc_TtGetBit( pTruth, iMint );
1352 // derive clauses
1353 if ( !Ifn_NtkAddClauses( p, p->Values, pSat ) )
1354 break;
1355 // find assignment of parameters
1356 // clk2 = Abc_Clock();
1357 status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 );
1358 // clkSat += Abc_Clock() - clk2;
1359 if ( fVeryVerbose )
1360 Ifn_NtkMatchPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
1361 if ( status != l_True )
1362 break;
1363 // collect assignment
1364 for ( v = p->nObjs; v < p->nPars; v++ )
1365 p->Values[v] = sat_solver_var_value(pSat, v);
1366 // find truth table
1367 // clk2 = Abc_Clock();
1368 pTruth1 = Ifn_NtkDeriveTruth( p, p->Values );
1369 // clkTru += Abc_Clock() - clk2;
1370 Abc_TtXor( pTruth1, pTruth1, p->pTruth, p->nWords, 0 );
1371 // find mismatch if present
1372 iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
1373 if ( iMint == -1 )
1374 {
1375 if ( pConfig )
1376 Ifn_NtkMatchCollectConfig( p, pSat, pConfig );
1377 /*
1378 if ( pPerm )
1379 {
1380 int RetValue = Ifn_ManSatFindCofigBitsTest( p, pTruth, nVars, *pPerm );
1381 Ifn_NtkMatchPrintPerm( *pPerm, p->nInps );
1382 if ( RetValue == 0 )
1383 printf( "Verification failed.\n" );
1384 }
1385 */
1386 RetValue = 1;
1387 break;
1388 }
1389 }
1390 assert( i < nIterMax );
1391 if ( fVerbose )
1392 {
1393 printf( "%s Iter =%4d. Confl = %6d. ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) );
1394 if ( RetValue )
1395 Ifn_NtkMatchPrintConfig( p, pSat );
1396 printf( "\n" );
1397 }
1398 sat_solver_delete( pSat );
1399 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1400 // Abc_PrintTime( 1, "Sat", clkSat );
1401 // Abc_PrintTime( 1, "Tru", clkTru );
1402 return RetValue;
1403 }
1404
1405 /**Function*************************************************************
1406
1407 Synopsis []
1408
1409 Description []
1410
1411 SideEffects []
1412
1413 SeeAlso []
1414
1415 ***********************************************************************/
Ifn_NtkRead()1416 void Ifn_NtkRead()
1417 {
1418 int RetValue;
1419 int nVars = 8;
1420 // word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars );
1421 word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars );
1422 // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
1423 // word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars );
1424 // word * pTruth = Dau_DsdToTruth( "(abcd)", nVars );
1425 // word * pTruth = Dau_DsdToTruth( "(abc)", nVars );
1426 // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars );
1427 // char * pStr = "e={abc};f={ed};";
1428 // char * pStr = "d={ab};e={cd};";
1429 // char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
1430 // char * pStr = "i={abc};j={ide};k={ifg};l={jkh};";
1431 // char * pStr = "h={abcde};i={abcdf};j=<ghi>;";
1432 // char * pStr = "g=<abc>;h=<ade>;i={fgh};";
1433 // char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
1434 char * pStr = "{({(ab)cde}f)ghi};AB;CD;DE;GH;HI";
1435 Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
1436 word Perm = 0;
1437 if ( p == NULL )
1438 return;
1439 Ifn_NtkPrint( p );
1440 Dau_DsdPrintFromTruth( pTruth, nVars );
1441 // get the given function
1442 RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1, &Perm );
1443 ABC_FREE( p );
1444 }
1445
1446 ////////////////////////////////////////////////////////////////////////
1447 /// END OF FILE ///
1448 ////////////////////////////////////////////////////////////////////////
1449
1450
1451 ABC_NAMESPACE_IMPL_END
1452
1453