ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ivyCanon.c
Go to the documentation of this file.
1
20
21#include "ivy.h"
22
24
25
29
30static 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
35
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 }
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
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
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
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
146
147
149
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
Ivy_Obj_t * Ivy_CanonAnd(Ivy_Man_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
Definition ivyCanon.c:90
Ivy_Obj_t * Ivy_CanonLatch(Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Init_t Init)
Definition ivyCanon.c:131
Ivy_Obj_t * Ivy_CanonPair_rec(Ivy_Man_t *p, Ivy_Obj_t *pGhost)
FUNCTION DEFINITIONS ///.
Definition ivyCanon.c:47
Ivy_Obj_t * Ivy_CanonExor(Ivy_Man_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
Definition ivyCanon.c:109
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition ivy.h:46
Ivy_Init_t
Definition ivy.h:65
@ IVY_INIT_NONE
Definition ivy.h:66
Ivy_Obj_t * Ivy_Latch(Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Init_t Init)
Definition ivyOper.c:287
Ivy_Obj_t * Ivy_TableLookup(Ivy_Man_t *p, Ivy_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition ivyTable.c:71
Ivy_Obj_t * Ivy_ObjCreate(Ivy_Man_t *p, Ivy_Obj_t *pGhost)
Definition ivyObj.c:77
Ivy_Obj_t * Ivy_Oper(Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1, Ivy_Type_t Type)
FUNCTION DEFINITIONS ///.
Definition ivyOper.c:63
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
Ivy_Type_t
Definition ivy.h:52
@ IVY_AND
Definition ivy.h:58
@ IVY_LATCH
Definition ivy.h:57
@ IVY_EXOR
Definition ivy.h:59
#define assert(ex)
Definition util_old.h:213