1 /**CFile****************************************************************
2 
3   FileName    [ivyCanon.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [And-Inverter Graph package.]
8 
9   Synopsis    [Finding canonical form of objects.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - May 11, 2006.]
16 
17   Revision    [$Id: ivyCanon.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "ivy.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
31 
32 ////////////////////////////////////////////////////////////////////////
33 ///                     FUNCTION DEFINITIONS                         ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38   Synopsis    [Creates the canonical form of the node.]
39 
40   Description []
41 
42   SideEffects []
43 
44   SeeAlso     []
45 
46 ***********************************************************************/
Ivy_CanonPair_rec(Ivy_Man_t * p,Ivy_Obj_t * pGhost)47 Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
48 {
49     Ivy_Obj_t * pResult, * pLat0, * pLat1;
50     Ivy_Init_t Init, Init0, Init1;
51     int fCompl0, fCompl1;
52     Ivy_Type_t Type;
53     assert( Ivy_ObjIsNode(pGhost) );
54     assert( Ivy_ObjIsAnd(pGhost) || (!Ivy_ObjFaninC0(pGhost) && !Ivy_ObjFaninC1(pGhost)) );
55     assert( Ivy_ObjFaninId0(pGhost) != 0 && Ivy_ObjFaninId1(pGhost) != 0 );
56     // consider the case when the pair is canonical
57     if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) )
58     {
59         if ( (pResult = Ivy_TableLookup( p, pGhost )) )
60             return pResult;
61         return Ivy_ObjCreate( p, pGhost );
62     }
63     /// remember the latches
64     pLat0 = Ivy_ObjFanin0(pGhost);
65     pLat1 = Ivy_ObjFanin1(pGhost);
66     // remember type and compls
67     Type = Ivy_ObjType(pGhost);
68     fCompl0 = Ivy_ObjFaninC0(pGhost);
69     fCompl1 = Ivy_ObjFaninC1(pGhost);
70     // call recursively
71     pResult = Ivy_Oper( p, Ivy_NotCond(Ivy_ObjFanin0(pLat0), fCompl0), Ivy_NotCond(Ivy_ObjFanin0(pLat1), fCompl1), Type );
72     // build latch on top of this
73     Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 );
74     Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 );
75     Init  = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1);
76     return Ivy_Latch( p, pResult, Init );
77 }
78 
79 /**Function*************************************************************
80 
81   Synopsis    [Creates the canonical form of the node.]
82 
83   Description []
84 
85   SideEffects []
86 
87   SeeAlso     []
88 
89 ***********************************************************************/
Ivy_CanonAnd(Ivy_Man_t * p,Ivy_Obj_t * pObj0,Ivy_Obj_t * pObj1)90 Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
91 {
92     Ivy_Obj_t * pGhost, * pResult;
93     pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
94     pResult = Ivy_CanonPair_rec( p, pGhost );
95     return pResult;
96 }
97 
98 /**Function*************************************************************
99 
100   Synopsis    [Creates the canonical form of the node.]
101 
102   Description []
103 
104   SideEffects []
105 
106   SeeAlso     []
107 
108 ***********************************************************************/
Ivy_CanonExor(Ivy_Man_t * p,Ivy_Obj_t * pObj0,Ivy_Obj_t * pObj1)109 Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
110 {
111     Ivy_Obj_t * pGhost, * pResult;
112     int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1);
113     pObj0 = Ivy_Regular(pObj0);
114     pObj1 = Ivy_Regular(pObj1);
115     pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
116     pResult = Ivy_CanonPair_rec( p, pGhost );
117     return Ivy_NotCond( pResult, fCompl );
118 }
119 
120 /**Function*************************************************************
121 
122   Synopsis    [Creates the canonical form of the node.]
123 
124   Description []
125 
126   SideEffects []
127 
128   SeeAlso     []
129 
130 ***********************************************************************/
Ivy_CanonLatch(Ivy_Man_t * p,Ivy_Obj_t * pObj,Ivy_Init_t Init)131 Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init )
132 {
133     Ivy_Obj_t * pGhost, * pResult;
134     int fCompl = Ivy_IsComplement(pObj);
135     pObj = Ivy_Regular(pObj);
136     pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
137     pResult = Ivy_TableLookup( p, pGhost );
138     if ( pResult == NULL )
139         pResult = Ivy_ObjCreate( p, pGhost );
140     return Ivy_NotCond( pResult, fCompl );
141 }
142 
143 ////////////////////////////////////////////////////////////////////////
144 ///                       END OF FILE                                ///
145 ////////////////////////////////////////////////////////////////////////
146 
147 
148 ABC_NAMESPACE_IMPL_END
149 
150