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