1 /**CFile****************************************************************
2 
3   FileName    [amapRule.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Technology mapper for standard cells.]
8 
9   Synopsis    [Matching rules.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: amapRule.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "amapInt.h"
22 #include "bool/kit/kit.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 extern int Amap_LibDeriveGatePerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, char * pArray );
32 
33 ////////////////////////////////////////////////////////////////////////
34 ///                     FUNCTION DEFINITIONS                         ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39   Synopsis    [Checks if the three-argument rule exist.]
40 
41   Description []
42 
43   SideEffects []
44 
45   SeeAlso     []
46 
47 ***********************************************************************/
Amap_CreateRulesPrime(Amap_Lib_t * p,Vec_Int_t * vNods0,Vec_Int_t * vNods1,Vec_Int_t * vNods2)48 Vec_Int_t * Amap_CreateRulesPrime( Amap_Lib_t * p, Vec_Int_t * vNods0, Vec_Int_t * vNods1, Vec_Int_t * vNods2 )
49 {
50     Vec_Int_t * vRes;
51     int i, k, j, iNod, iNod0, iNod1, iNod2;
52     if ( p->vRules3 == NULL )
53         p->vRules3 = Vec_IntAlloc( 100 );
54     vRes = Vec_IntAlloc( 10 );
55     Vec_IntForEachEntry( vNods0, iNod0, i )
56     Vec_IntForEachEntry( vNods1, iNod1, k )
57     Vec_IntForEachEntry( vNods2, iNod2, j )
58     {
59         iNod = Amap_LibFindMux( p, iNod0, iNod1, iNod2 );
60         if ( iNod == -1 )
61             iNod = Amap_LibCreateMux( p, iNod0, iNod1, iNod2 );
62         Vec_IntPush( vRes, Abc_Var2Lit(iNod, 0) );
63     }
64     return vRes;
65 }
66 
67 /**Function*************************************************************
68 
69   Synopsis    []
70 
71   Description []
72 
73   SideEffects []
74 
75   SeeAlso     []
76 
77 ***********************************************************************/
Amap_CreateRulesTwo(Amap_Lib_t * p,Vec_Int_t * vNods,Vec_Int_t * vNods0,Vec_Int_t * vNods1,int fXor)78 void Amap_CreateRulesTwo( Amap_Lib_t * p, Vec_Int_t * vNods, Vec_Int_t * vNods0, Vec_Int_t * vNods1, int fXor )
79 {
80     int i, k, iNod, iNod0, iNod1;
81     Vec_IntForEachEntry( vNods0, iNod0, i )
82     Vec_IntForEachEntry( vNods1, iNod1, k )
83     {
84         iNod = Amap_LibFindNode( p, iNod0, iNod1, fXor );
85         if ( iNod == -1 )
86             iNod = Amap_LibCreateNode( p, iNod0, iNod1, fXor );
87         Vec_IntPushUnique( vNods, Abc_Var2Lit(iNod, 0) );
88     }
89 }
90 
91 /**Function*************************************************************
92 
93   Synopsis    []
94 
95   Description []
96 
97   SideEffects []
98 
99   SeeAlso     []
100 
101 ***********************************************************************/
Amap_CreateCheckAllZero(Vec_Ptr_t * vVecNods)102 int Amap_CreateCheckAllZero( Vec_Ptr_t * vVecNods )
103 {
104     Vec_Int_t * vNods;
105     int i;
106     Vec_PtrForEachEntryReverse( Vec_Int_t *, vVecNods, vNods, i )
107         if ( Vec_IntSize(vNods) != 1 || Vec_IntEntry(vNods,0) != 0 )
108             return 0;
109     return 1;
110 }
111 
112 /**Function*************************************************************
113 
114   Synopsis    []
115 
116   Description []
117 
118   SideEffects []
119 
120   SeeAlso     []
121 
122 ***********************************************************************/
Amap_CreateRulesVector_rec(Amap_Lib_t * p,Vec_Ptr_t * vVecNods,int fXor)123 Vec_Int_t * Amap_CreateRulesVector_rec( Amap_Lib_t * p, Vec_Ptr_t * vVecNods, int fXor )
124 {
125     Vec_Ptr_t * vVecNods0, * vVecNods1;
126     Vec_Int_t * vRes, * vNods, * vNods0, * vNods1;
127     int i, k;
128     if ( Vec_PtrSize(vVecNods) == 1 )
129         return Vec_IntDup( (Vec_Int_t *)Vec_PtrEntry(vVecNods, 0) );
130     vRes = Vec_IntAlloc( 10 );
131     vVecNods0 = Vec_PtrAlloc( Vec_PtrSize(vVecNods) );
132     vVecNods1 = Vec_PtrAlloc( Vec_PtrSize(vVecNods) );
133     if ( Amap_CreateCheckAllZero(vVecNods) )
134     {
135         for ( i = Vec_PtrSize(vVecNods)-1; i > 0; i-- )
136         {
137             Vec_PtrClear( vVecNods0 );
138             Vec_PtrClear( vVecNods1 );
139             Vec_PtrForEachEntryStop( Vec_Int_t *, vVecNods, vNods, k, i )
140                 Vec_PtrPush( vVecNods0, vNods );
141             Vec_PtrForEachEntryStart( Vec_Int_t *, vVecNods, vNods, k, i )
142                 Vec_PtrPush( vVecNods1, vNods );
143             vNods0 = Amap_CreateRulesVector_rec( p, vVecNods0, fXor );
144             vNods1 = Amap_CreateRulesVector_rec( p, vVecNods1, fXor );
145             Amap_CreateRulesTwo( p, vRes, vNods0, vNods1, fXor );
146             Vec_IntFree( vNods0 );
147             Vec_IntFree( vNods1 );
148         }
149     }
150     else
151     {
152         int Limit = (1 << Vec_PtrSize(vVecNods))-2;
153         for ( i = 1; i < Limit; i++ )
154         {
155             Vec_PtrClear( vVecNods0 );
156             Vec_PtrClear( vVecNods1 );
157             Vec_PtrForEachEntryReverse( Vec_Int_t *, vVecNods, vNods, k )
158             {
159                 if ( i & (1 << k) )
160                     Vec_PtrPush( vVecNods1, vNods );
161                 else
162                     Vec_PtrPush( vVecNods0, vNods );
163             }
164             assert( Vec_PtrSize(vVecNods0) > 0 );
165             assert( Vec_PtrSize(vVecNods1) > 0 );
166             assert( Vec_PtrSize(vVecNods0) < Vec_PtrSize(vVecNods) );
167             assert( Vec_PtrSize(vVecNods1) < Vec_PtrSize(vVecNods) );
168             vNods0 = Amap_CreateRulesVector_rec( p, vVecNods0, fXor );
169             vNods1 = Amap_CreateRulesVector_rec( p, vVecNods1, fXor );
170             Amap_CreateRulesTwo( p, vRes, vNods0, vNods1, fXor );
171             Vec_IntFree( vNods0 );
172             Vec_IntFree( vNods1 );
173         }
174     }
175     Vec_PtrFree( vVecNods0 );
176     Vec_PtrFree( vVecNods1 );
177     return vRes;
178 }
179 
180 /**Function*************************************************************
181 
182   Synopsis    []
183 
184   Description []
185 
186   SideEffects []
187 
188   SeeAlso     []
189 
190 ***********************************************************************/
Amap_CreateRulesFromDsd_rec(Amap_Lib_t * pLib,Kit_DsdNtk_t * p,int iLit)191 Vec_Int_t * Amap_CreateRulesFromDsd_rec( Amap_Lib_t * pLib, Kit_DsdNtk_t * p, int iLit )
192 {
193     Vec_Int_t * vRes = NULL;
194     Vec_Ptr_t * vVecNods;
195     Vec_Int_t * vNodsFanin;
196     Kit_DsdObj_t * pObj;
197     unsigned i;
198     int iFanin, iNod, k;
199     assert( !Abc_LitIsCompl(iLit) );
200     pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
201     if ( pObj == NULL )
202         return Vec_IntStartNatural( 1 );
203     // solve for the inputs
204     vVecNods = Vec_PtrAlloc( pObj->nFans );
205     Kit_DsdObjForEachFanin( p, pObj, iFanin, i )
206     {
207         vNodsFanin = Amap_CreateRulesFromDsd_rec( pLib, p, Abc_LitRegular(iFanin) );
208         if ( Abc_LitIsCompl(iFanin) )
209         {
210             Vec_IntForEachEntry( vNodsFanin, iNod, k )
211                 if ( iNod > 0 )
212                     Vec_IntWriteEntry( vNodsFanin, k, Abc_LitNot(iNod) );
213         }
214         Vec_PtrPush( vVecNods, vNodsFanin );
215     }
216     if ( pObj->Type == KIT_DSD_AND )
217         vRes = Amap_CreateRulesVector_rec( pLib, vVecNods, 0 );
218     else if ( pObj->Type == KIT_DSD_XOR )
219         vRes = Amap_CreateRulesVector_rec( pLib, vVecNods, 1 );
220     else if ( pObj->Type == KIT_DSD_PRIME )
221     {
222         assert( pObj->nFans == 3 );
223         assert( Kit_DsdObjTruth(pObj)[0] == 0xCACACACA );
224         vRes = Amap_CreateRulesPrime( pLib, (Vec_Int_t *)Vec_PtrEntry(vVecNods, 0),
225             (Vec_Int_t *)Vec_PtrEntry(vVecNods, 1), (Vec_Int_t *)Vec_PtrEntry(vVecNods, 2) );
226     }
227     else assert( 0 );
228     Vec_PtrForEachEntry( Vec_Int_t *, vVecNods, vNodsFanin, k )
229         Vec_IntFree( vNodsFanin );
230     Vec_PtrFree( vVecNods );
231     return vRes;
232 }
Amap_CreateRulesFromDsd(Amap_Lib_t * pLib,Kit_DsdNtk_t * p)233 Vec_Int_t * Amap_CreateRulesFromDsd( Amap_Lib_t * pLib, Kit_DsdNtk_t * p )
234 {
235     Vec_Int_t * vNods;
236     int iNod, i;
237     assert( p->nVars >= 2 );
238     vNods = Amap_CreateRulesFromDsd_rec( pLib, p, Abc_LitRegular(p->Root) );
239     if ( vNods == NULL )
240         return NULL;
241     if ( Abc_LitIsCompl(p->Root) )
242     {
243         Vec_IntForEachEntry( vNods, iNod, i )
244             Vec_IntWriteEntry( vNods, i, Abc_LitNot(iNod) );
245     }
246     return vNods;
247 }
248 
249 /**Function*************************************************************
250 
251   Synopsis    [Returns 1 if DSD network contains asymentry due to complements.]
252 
253   Description []
254 
255   SideEffects []
256 
257   SeeAlso     []
258 
259 ***********************************************************************/
Amap_CreateCheckEqual_rec(Kit_DsdNtk_t * p,int iLit0,int iLit1)260 int Amap_CreateCheckEqual_rec( Kit_DsdNtk_t * p, int iLit0, int iLit1 )
261 {
262     Kit_DsdObj_t * pObj0, * pObj1;
263     int i;
264     assert( !Abc_LitIsCompl(iLit0) );
265     assert( !Abc_LitIsCompl(iLit1) );
266     pObj0 = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit0) );
267     pObj1 = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit1) );
268     if ( pObj0 == NULL && pObj1 == NULL )
269         return 1;
270     if ( pObj0 == NULL || pObj1 == NULL )
271         return 0;
272     if ( pObj0->Type != pObj1->Type )
273         return 0;
274     if ( pObj0->nFans != pObj1->nFans )
275         return 0;
276     if ( pObj0->Type == KIT_DSD_PRIME )
277         return 0;
278     assert( pObj0->Type == KIT_DSD_AND || pObj0->Type == KIT_DSD_XOR );
279     for ( i = 0; i < (int)pObj0->nFans; i++ )
280     {
281         if ( Abc_LitIsCompl(pObj0->pFans[i]) != Abc_LitIsCompl(pObj1->pFans[i]) )
282             return 0;
283         if ( !Amap_CreateCheckEqual_rec( p, Abc_LitRegular(pObj0->pFans[i]), Abc_LitRegular(pObj1->pFans[i]) ) )
284             return 0;
285     }
286     return 1;
287 }
Amap_CreateCheckAsym_rec(Kit_DsdNtk_t * p,int iLit,Vec_Int_t ** pvSyms)288 void Amap_CreateCheckAsym_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t ** pvSyms )
289 {
290     Kit_DsdObj_t * pObj;
291     int i, k, iFanin;
292     assert( !Abc_LitIsCompl(iLit) );
293     pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
294     if ( pObj == NULL )
295         return;
296     Kit_DsdObjForEachFanin( p, pObj, iFanin, i )
297         Amap_CreateCheckAsym_rec( p, Abc_LitRegular(iFanin), pvSyms );
298     if ( pObj->Type == KIT_DSD_PRIME )
299         return;
300     assert( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR );
301     for ( i = 0; i < (int)pObj->nFans; i++ )
302     for ( k = i+1; k < (int)pObj->nFans; k++ )
303     {
304         if ( Abc_LitIsCompl(pObj->pFans[i]) != Abc_LitIsCompl(pObj->pFans[k]) &&
305              Kit_DsdNtkObj(p, Abc_Lit2Var(pObj->pFans[i])) == NULL &&
306              Kit_DsdNtkObj(p, Abc_Lit2Var(pObj->pFans[k])) == NULL )
307         {
308             if ( *pvSyms == NULL )
309                 *pvSyms = Vec_IntAlloc( 16 );
310             Vec_IntPush( *pvSyms, (Abc_Lit2Var(pObj->pFans[i]) << 8) | Abc_Lit2Var(pObj->pFans[k]) );
311         }
312     }
313 }
Amap_CreateCheckAsym(Kit_DsdNtk_t * p,Vec_Int_t ** pvSyms)314 void Amap_CreateCheckAsym( Kit_DsdNtk_t * p, Vec_Int_t ** pvSyms )
315 {
316     Amap_CreateCheckAsym_rec( p, Abc_LitRegular(p->Root), pvSyms );
317 }
318 
319 /**Function*************************************************************
320 
321   Synopsis    [Creates rules for the given gate]
322 
323   Description []
324 
325   SideEffects []
326 
327   SeeAlso     []
328 
329 ***********************************************************************/
Amap_CreateRulesForGate(Amap_Lib_t * pLib,Amap_Gat_t * pGate)330 void Amap_CreateRulesForGate( Amap_Lib_t * pLib, Amap_Gat_t * pGate )
331 {
332     Kit_DsdNtk_t * pNtk, * pTemp;
333     Vec_Int_t * vSyms = NULL;
334     Vec_Int_t * vNods;
335     Amap_Nod_t * pNod;
336     Amap_Set_t * pSet, * pSet2;
337     int iNod, i, k, Entry;
338 //    if ( pGate->nPins > 4 )
339 //        return;
340     pNtk = Kit_DsdDecomposeMux( pGate->pFunc, pGate->nPins, 2 );
341     if ( pGate->nPins == 2 && (pGate->pFunc[0] == 0x66666666 || pGate->pFunc[0] == ~0x66666666) )
342          pLib->fHasXor = 1;
343     if ( Kit_DsdNonDsdSizeMax(pNtk) == 3 )
344         pLib->fHasMux = pGate->fMux = 1;
345     pNtk = Kit_DsdExpand( pTemp = pNtk );
346     Kit_DsdNtkFree( pTemp );
347     Kit_DsdVerify( pNtk, pGate->pFunc, pGate->nPins );
348     // check symmetries
349     Amap_CreateCheckAsym( pNtk, &vSyms );
350 //    if ( vSyms )
351 //        Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
352 
353 if ( pLib->fVerbose )
354 //if ( pGate->fMux )
355 {
356 printf( "\nProcessing library gate %4d: %10s ", pGate->Id, pGate->pName );
357 Kit_DsdPrint( stdout, pNtk );
358 }
359     vNods = Amap_CreateRulesFromDsd( pLib, pNtk );
360     if ( vNods )
361     {
362         Vec_IntForEachEntry( vNods, iNod, i )
363         {
364             assert( iNod > 1 );
365             pNod = Amap_LibNod( pLib, Abc_Lit2Var(iNod) );
366 //            assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
367             pSet = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) );
368             memset( pSet, 0, sizeof(Amap_Set_t) );
369             pSet->iGate = pGate->Id;
370             pSet->fInv  = Abc_LitIsCompl(iNod);
371             pSet->nIns  = pGate->nPins;
372             if ( Amap_LibDeriveGatePerm( pLib, pGate, pNtk, pNod, pSet->Ins ) == 0 )
373             {
374 if ( pLib->fVerbose )
375 {
376                 printf( "Cound not prepare gate \"%s\": ", pGate->pName );
377                 Kit_DsdPrint( stdout, pNtk );
378 }
379                 continue;
380             }
381             pSet->pNext = pNod->pSets;
382             pNod->pSets = pSet;
383             pLib->nSets++;
384             if ( vSyms == NULL )
385                 continue;
386 //            continue;
387             // add sets equivalent due to symmetry
388             Vec_IntForEachEntry( vSyms, Entry, k )
389             {
390                 int iThis = Entry & 0xff;
391                 int iThat = Entry >> 8;
392 //                printf( "%d %d\n", iThis, iThat );
393                 // create new set
394                 pSet2 = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) );
395                 memset( pSet2, 0, sizeof(Amap_Set_t) );
396                 pSet2->iGate = pGate->Id;
397                 pSet2->fInv  = Abc_LitIsCompl(iNod);
398                 pSet2->nIns  = pGate->nPins;
399                 memcpy( pSet2->Ins, pSet->Ins, (size_t)pGate->nPins );
400                 // update inputs
401                 pSet2->Ins[iThis] = Abc_Var2Lit( Abc_Lit2Var(pSet->Ins[iThat]), Abc_LitIsCompl(pSet->Ins[iThis]) );
402                 pSet2->Ins[iThat] = Abc_Var2Lit( Abc_Lit2Var(pSet->Ins[iThis]), Abc_LitIsCompl(pSet->Ins[iThat]) );
403                 // add set to collection
404                 pSet2->pNext = pNod->pSets;
405                 pNod->pSets  = pSet2;
406                 pLib->nSets++;
407             }
408         }
409         Vec_IntFree( vNods );
410     }
411     Kit_DsdNtkFree( pNtk );
412     Vec_IntFreeP( &vSyms );
413 }
414 
415 /**Function*************************************************************
416 
417   Synopsis    [Creates rules for the given gate]
418 
419   Description []
420 
421   SideEffects []
422 
423   SeeAlso     []
424 
425 ***********************************************************************/
Amap_LibCreateRules(Amap_Lib_t * pLib,int fVeryVerbose)426 void Amap_LibCreateRules( Amap_Lib_t * pLib, int fVeryVerbose )
427 {
428     Amap_Gat_t * pGate;
429     int i, nGates = 0;
430 //    abctime clk = Abc_Clock();
431     pLib->fVerbose = fVeryVerbose;
432     pLib->vRules   = Vec_PtrAlloc( 100 );
433     pLib->vRulesX  = Vec_PtrAlloc( 100 );
434     pLib->vRules3  = Vec_IntAlloc( 100 );
435     Amap_LibCreateVar( pLib );
436     Vec_PtrForEachEntry( Amap_Gat_t *, pLib->vSelect, pGate, i )
437     {
438         if ( pGate->nPins < 2 )
439             continue;
440         if ( pGate->pFunc == NULL )
441         {
442             printf( "Amap_LibCreateRules(): Skipping gate %s (%s).\n", pGate->pName, pGate->pForm );
443             continue;
444         }
445         Amap_CreateRulesForGate( pLib, pGate );
446         nGates++;
447     }
448     assert( Vec_PtrSize(pLib->vRules)  == 2*pLib->nNodes );
449     assert( Vec_PtrSize(pLib->vRulesX) == 2*pLib->nNodes );
450     pLib->pRules  = Amap_LibLookupTableAlloc( pLib->vRules, 0 );
451     pLib->pRulesX = Amap_LibLookupTableAlloc( pLib->vRulesX, 0 );
452     Vec_VecFree( (Vec_Vec_t *)pLib->vRules );  pLib->vRules  = NULL;
453     Vec_VecFree( (Vec_Vec_t *)pLib->vRulesX ); pLib->vRulesX = NULL;
454 }
455 
456 ////////////////////////////////////////////////////////////////////////
457 ///                       END OF FILE                                ///
458 ////////////////////////////////////////////////////////////////////////
459 
460 
461 ABC_NAMESPACE_IMPL_END
462 
463