ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acecPa.c
Go to the documentation of this file.
1
20
21#include "acecInt.h"
22#include "misc/vec/vecWec.h"
23#include "misc/extra/extra.h"
24
26
30
31
35
48{
49 int Truth0, Truth1;
50 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
51 return pObj->Value;
52 Gia_ObjSetTravIdCurrent(p, pObj);
53 assert( Gia_ObjIsAnd(pObj) );
54 assert( !Gia_ObjIsXor(pObj) );
55 Truth0 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
56 Truth1 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
57 Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
58 Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
59 return (pObj->Value = Truth0 & Truth1);
60}
61void Pas_ManVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
62{
63 Gia_Obj_t * pObj;
64 unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
65 int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
66
67 if ( !fFadd )
68 return;
69
71 for ( k = 0; k < 3; k++ )
72 {
73 iObj = Vec_IntEntry( vAdds, 6*iBox+k );
74 if ( iObj == 0 )
75 continue;
76 pObj = Gia_ManObj( p, iObj );
77 pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
78 Gia_ObjSetTravIdCurrent( p, pObj );
79 }
80
81 iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
82 TruthXor = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
83 TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
84
85 iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
86 TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
87 TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
88
89 if ( fFadd ) // FADD
90 {
91 if ( TruthXor != 0x96 )
92 printf( "Fadd %d sum is wrong.\n", iBox );
93 if ( TruthMaj != 0xE8 )
94 printf( "Fadd %d carry is wrong.\n", iBox );
95 }
96 else
97 {
98 if ( TruthXor != 0x66 )
99 printf( "Hadd %d sum is wrong.\n", iBox );
100 if ( TruthMaj != 0x88 )
101 printf( "Hadd %d carry is wrong.\n", iBox );
102 }
103}
104void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase )
105{
106 int k, iBox;
107 Vec_IntForEachEntry( vOrder, iBox, k )
108 Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase );
109}
110
122void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase )
123{
124 int k, iBox, iXor, Sign, fXorPhase;
125 assert( pObj != Gia_ManConst0(p) );
126 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
127 return;
128 Gia_ObjSetTravIdCurrent(p, pObj);
129 if ( fPhase )
130 Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase );
131 if ( !Gia_ObjIsAnd(pObj) )
132 return;
133 iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) );
134 if ( iBox == -1 )
135 return;
136 iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
137 Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
138 fXorPhase = ((Sign >> 3) & 1);
139 // remember complemented HADD
140 if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase )
141 Vec_BitWriteEntry( vConstPhase, iBox, 1 );
142 for ( k = 0; k < 3; k++ )
143 {
144 int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
145 int fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
146 fXorPhase ^= fPhaseThis;
147 if ( iObj == 0 )
148 continue;
149 Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase );
150 }
151 Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
152}
153Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase )
154{
155 Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) );
156 Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 );
157 int i, iRoot;
159 Vec_IntForEachEntry( vRoots, iRoot, i )
160 Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase );
161 *pvConstPhase = vConstPhase;
162 return vPhase;
163}
164
176int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts )
177{
178 Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) );
179 Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
180 Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
181 Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
182 Vec_Bit_t * vPhase, * vConstPhase;
183 int i, k, Entry, nTrees;
184
185 // map carries into adder indexes and mark driven nodes
186 Vec_IntForEachEntry( vOrder, i, k )
187 {
188 int Carry = Vec_IntEntry(vAdds, 6*i+4);
189 if ( Vec_BitEntry(vUnique, Carry) )
190 printf( "Carry %d participates more than once.\n", Carry );
191 Vec_BitWriteEntry( vUnique, Carry, 1 );
192 Vec_IntWriteEntry( vMap, Carry, i );
193 // mark driven
194 Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 );
195 Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 );
196 Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 );
197 }
198 // collect carries that do not drive other adders
199 for ( i = 0; i < Gia_ManObjNum(p); i++ )
200 if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) )
201 Vec_IntPush( vRoots, i );
202 nTrees = Vec_IntSize( vRoots );
203
204 Vec_IntPrint( vRoots );
205
206 // compute phases
207 if ( Vec_IntSize(vRoots) > 0 )
208 {
209 int nCompls = 0;
210
211 vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase );
212 Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase );
213
214 printf( "Outputs: " );
215 Vec_IntForEachEntry( vOuts, Entry, i )
216 printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
217 printf( "\n" );
218
219 printf( "Inputs: " );
220 Vec_IntForEachEntry( vIns, Entry, i )
221 {
222 printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
223 nCompls += Vec_BitEntry(vPhase, Entry);
224 }
225 printf( " Compl = %d\n", nCompls );
226
227 Vec_BitFreeP( &vPhase );
228 Vec_BitFreeP( &vConstPhase );
229 }
230
231 Vec_IntFree( vRoots );
232 Vec_IntFree( vMap );
233 Vec_BitFree( vUnique );
234 Vec_BitFree( vUsed );
235 return nTrees;
236}
237
250{
251 abctime clk = Abc_Clock();
252 Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
253 Vec_Int_t * vIns, * vOuts;
254 Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts );
255 int nTrees, nFadds = Ree_ManCountFadds( vAdds );
256 //Ree_ManPrintAdders( vAdds, 1 );
257 printf( "Detected %d FAs and %d HAs. Collected %d adders. ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) );
258 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
259 // detect trees
260 clk = Abc_Clock();
261 nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts );
262 Vec_IntFree( vAdds );
263 Vec_IntFree( vOrder );
264 Vec_IntFree( vIns );
265 Vec_IntFree( vOuts );
266
267 printf( "Detected %d adder trees. ", nTrees );
268 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
269}
270
274
275
277
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Vec_Int_t * Gia_PolynCoreOrder(Gia_Man_t *pGia, Vec_Int_t *vAdds, Vec_Int_t *vAddCos, Vec_Int_t **pvIns, Vec_Int_t **pvOuts)
ITERATORS ///.
Definition acecCo.c:163
void Pas_ManVerifyPhaseOne(Gia_Man_t *p, Vec_Int_t *vAdds, int iBox, Vec_Bit_t *vPhase)
Definition acecPa.c:61
Vec_Bit_t * Pas_ManPhase(Gia_Man_t *p, Vec_Int_t *vAdds, Vec_Int_t *vMap, Vec_Int_t *vRoots, Vec_Bit_t **pvConstPhase)
Definition acecPa.c:153
void Pas_ManVerifyPhase(Gia_Man_t *p, Vec_Int_t *vAdds, Vec_Int_t *vOrder, Vec_Bit_t *vPhase)
Definition acecPa.c:104
void Pas_ManPhase_rec(Gia_Man_t *p, Vec_Int_t *vAdds, Vec_Int_t *vMap, Gia_Obj_t *pObj, int fPhase, Vec_Bit_t *vPhase, Vec_Bit_t *vConstPhase)
Definition acecPa.c:122
int Pas_ManComputeCuts(Gia_Man_t *p, Vec_Int_t *vAdds, Vec_Int_t *vOrder, Vec_Int_t *vIns, Vec_Int_t *vOuts)
Definition acecPa.c:176
void Pas_ManComputeCutsTest(Gia_Man_t *p)
Definition acecPa.c:249
ABC_NAMESPACE_IMPL_START int Pas_ManVerifyPhaseOne_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
DECLARATIONS ///.
Definition acecPa.c:47
Vec_Int_t * Ree_ManComputeCuts(Gia_Man_t *p, Vec_Int_t **pvXors, int fVerbose)
Definition acecRe.c:408
int Ree_ManCountFadds(Vec_Int_t *vAdds)
Definition acecRe.c:556
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
unsigned Value
Definition gia.h:89
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54