ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ioResub.h
Go to the documentation of this file.
1
20
21#ifndef ABC__base__io__ioResub_h
22#define ABC__base__io__ioResub_h
23
24
26
27
31
35
39
42{
43 int nIns; // the number of inputs
44 int nOuts; // the number of outputs
45 int nPats; // the number of patterns
46 int nSimWords; // the number of words needed to store the patterns
47 Vec_Wrd_t * vSimsIn; // input simulation signatures
48 Vec_Wrd_t * vSimsOut; // output simulation signatures
49 Vec_Int_t * vDivs; // divisors
50 Vec_Int_t * vSol; // solution
51};
52
56
57static inline int Abc_RDataGetIn ( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); }
58static inline int Abc_RDataGetOut( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); }
59
60static inline void Abc_RDataSetIn ( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); }
61static inline void Abc_RDataSetOut( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); }
62
66
67extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
68
80static inline Abc_RData_t * Abc_RDataStart( int nIns, int nOuts, int nPats )
81{
83 p->nIns = nIns;
84 p->nOuts = nOuts;
85 p->nPats = nPats;
86 p->nSimWords = Abc_Bit6WordNum(nPats);
87 p->vSimsIn = Vec_WrdStart( p->nIns * p->nSimWords );
88 p->vSimsOut = Vec_WrdStart( 2*p->nOuts * p->nSimWords );
89 p->vDivs = Vec_IntAlloc( 16 );
90 p->vSol = Vec_IntAlloc( 16 );
91 return p;
92}
93static inline void Abc_RDataStop( Abc_RData_t * p )
94{
95 Vec_IntFree( p->vSol );
96 Vec_IntFree( p->vDivs );
97 Vec_WrdFree( p->vSimsIn );
98 Vec_WrdFree( p->vSimsOut );
99 ABC_FREE( p );
100}
101static inline int Abc_ReadPlaResubParams( char * pFileName, int * pnIns, int * pnOuts, int * pnPats )
102{
103 FILE * pFile = fopen( pFileName, "rb" );
104 if ( pFile == NULL ) {
105 printf( "Cannot open file \"%s\" for reading.\n", pFileName );
106 return 0;
107 }
108 int nLineSize = 1000000, iLine = 0;
109 char * pBuffer = ABC_ALLOC( char, nLineSize );
110 *pnIns = *pnOuts = *pnPats = 0;
111 while ( fgets( pBuffer, nLineSize, pFile ) != NULL ) {
112 iLine += (pBuffer[0] == '0' || pBuffer[0] == '1' || pBuffer[0] == '-');
113 if ( pBuffer[0] != '.' )
114 continue;
115 if ( pBuffer[1] == 'i' )
116 *pnIns = atoi(pBuffer+2);
117 else if ( pBuffer[1] == 'o' )
118 *pnOuts = atoi(pBuffer+2);
119 else if ( pBuffer[1] == 'p' )
120 *pnPats = atoi(pBuffer+2);
121 else if ( pBuffer[1] == 'e' )
122 break;
123 }
124 if ( *pnPats == 0 )
125 *pnPats = iLine;
126 else if ( *pnPats != iLine )
127 printf( "The number of lines in the file (%d) does not match the number listed in .p (%d).\n", iLine, *pnPats );
128 fclose(pFile);
129 free( pBuffer );
130 return 1;
131}
132static inline int Abc_ReadPlaResubData( Abc_RData_t * p, char * pFileName )
133{
134 FILE * pFile = fopen( pFileName, "rb" );
135 if ( pFile == NULL ) {
136 printf( "Cannot open file \"%s\" for reading.\n", pFileName );
137 return 0;
138 }
139 int i, iLine = 0, nDashes = 0, MaxLineSize = p->nIns+p->nOuts+10000;
140 char * pTemp, * pBuffer = ABC_ALLOC( char, MaxLineSize );
141 while ( fgets( pBuffer, MaxLineSize, pFile ) != NULL ) {
142 if ( pBuffer[0] == '0' || pBuffer[0] == '1' || pBuffer[0] == '-' ) {
143 for ( pTemp = pBuffer, i = 0; *pTemp; pTemp++ ) {
144 if ( i < p->nIns ) { // input part
145 nDashes += (*pTemp == '-');
146 if ( *pTemp == '1' )
147 Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), iLine );
148 }
149 else { // output part
150 if ( *pTemp == '0' )
151 Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine );
152 else if ( *pTemp == '1' )
153 Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine );
154 //else if ( *pTemp == '-' ) {
155 // Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine );
156 // Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine );
157 //}
158 }
159 i += (*pTemp == '0' || *pTemp == '1' || *pTemp == '-');
160 }
161 assert( i == p->nIns + p->nOuts );
162 iLine++;
163 }
164 if ( pBuffer[0] == '.' && (pBuffer[1] == 's' || pBuffer[1] == 'a') ) {
165 Vec_Int_t * vArray = pBuffer[1] == 'a' ? p->vSol : p->vDivs;
166 if ( Vec_IntSize(vArray) > 0 )
167 continue;
168 char * pTemp = strtok( pBuffer+2, " \r\n\t" );
169 do Vec_IntPush( vArray, atoi(pTemp) );
170 while ( (pTemp = strtok( NULL, " \r\n\t" )) );
171 }
172 }
173 if ( nDashes )
174 printf( "Several (%d) don't-care literals in the input part are replaced by zeros \"%s\" \n", nDashes, pFileName );
175 assert ( iLine == p->nPats );
176 ABC_FREE(pBuffer);
177 fclose(pFile);
178 return 1;
179}
180static inline Abc_RData_t * Abc_ReadPla( char * pFileName )
181{
182 int nIns, nOuts, nPats;
183 int RetValue = Abc_ReadPlaResubParams( pFileName, &nIns, &nOuts, &nPats );
184 if ( !RetValue ) return NULL;
185 Abc_RData_t * p = Abc_RDataStart( nIns, nOuts, nPats );
186 RetValue = Abc_ReadPlaResubData( p, pFileName );
187 return p;
188}
189static inline void Abc_WritePla( Abc_RData_t * p, char * pFileName, int fRel )
190{
191 FILE * pFile = fopen( pFileName, "wb" ); int i, k;
192 if ( pFile == NULL ) {
193 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
194 return;
195 }
196 assert( fRel || Vec_WrdSize(p->vSimsOut) == 2*p->nOuts*p->nSimWords );
197 assert( !fRel || Vec_WrdSize(p->vSimsOut) == (1 << p->nOuts)*p->nSimWords );
198 fprintf( pFile, ".i %d\n", p->nIns );
199 fprintf( pFile, ".o %d\n", p->nOuts );
200 if ( fRel == 2 ) {
201 int n, iLine = 0, Count = 0; word Entry;
202 Vec_WrdForEachEntry( p->vSimsOut, Entry, i )
203 Count += Abc_TtCountOnes(Entry);
204 fprintf( pFile, ".p %d\n", Count );
205 for ( i = 0; i < p->nPats; i++ )
206 for ( n = 0; n < (1 << p->nOuts); n++ ) {
207 if ( !Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, n*p->nSimWords), i) )
208 continue;
209 for ( k = 0; k < p->nIns; k++ )
210 fprintf( pFile, "%d", Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, k*p->nSimWords), i) );
211 fprintf( pFile, " ");
212 for ( k = 0; k < p->nOuts; k++ )
213 fprintf( pFile, "%d", (n >> k) & 1 );
214 fprintf( pFile, "\n");
215 iLine++;
216 }
217 assert( iLine == Count );
218 }
219 else {
220 fprintf( pFile, ".p %d\n", p->nPats );
221 for ( i = 0; i < p->nPats; i++ ) {
222 for ( k = 0; k < p->nIns; k++ )
223 fprintf( pFile, "%d", Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, k*p->nSimWords), i) );
224 fprintf( pFile, " ");
225 if ( !fRel ) { // multi-output function
226 for ( k = 0; k < p->nOuts; k++ ) {
227 int Val0 = Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*k+0)*p->nSimWords), i);
228 int Val1 = Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*k+1)*p->nSimWords), i);
229 char Val = (Val0 && Val1) ? '-' : Val1 ? '1' : '0';
230 fprintf( pFile, "%c", Val );
231 }
232 }
233 else { // relation
234 for ( k = 0; k < (1 << p->nOuts); k++ )
235 fprintf( pFile, "%d", Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, k*p->nSimWords), i) );
236 }
237 fprintf( pFile, "\n");
238 }
239 }
240 fprintf( pFile, ".e\n" );
241 fclose(pFile);
242}
243
255static inline int Abc_RDataIsRel( Abc_RData_t * p )
256{
257 assert( p->nIns < 64 );
258 Vec_Wrd_t * vTransIn = Vec_WrdStart( 64*p->nSimWords );
259 Extra_BitMatrixTransposeP( p->vSimsIn, p->nSimWords, vTransIn, 64*p->nSimWords );
260 Vec_WrdShrink( vTransIn, p->nPats );
261 Vec_WrdUniqify( vTransIn );
262 int Value = Vec_WrdSize(vTransIn) < p->nPats;
263 Vec_WrdFree( vTransIn );
264 return Value;
265}
266static inline Abc_RData_t * Abc_RData2Rel( Abc_RData_t * p )
267{
268 assert( p->nIns < 64 );
269 assert( p->nOuts < 32 );
270 int w;
271 Vec_Wrd_t * vSimsIn2 = Vec_WrdStart( 64*p->nSimWords );
272 Vec_Wrd_t * vSimsOut2 = Vec_WrdStart( 64*p->nSimWords );
273 for ( w = 0; w < p->nIns; w++ )
274 Abc_TtCopy( Vec_WrdEntryP(vSimsIn2, w*p->nSimWords), Vec_WrdEntryP(p->vSimsIn, w*p->nSimWords), p->nSimWords, 0 );
275 for ( w = 0; w < p->nOuts; w++ )
276 Abc_TtCopy( Vec_WrdEntryP(vSimsOut2, w*p->nSimWords), Vec_WrdEntryP(p->vSimsOut, (2*w+1)*p->nSimWords), p->nSimWords, 0 );
277 Vec_Wrd_t * vTransIn = Vec_WrdStart( 64*p->nSimWords );
278 Vec_Wrd_t * vTransOut = Vec_WrdStart( 64*p->nSimWords );
279 Extra_BitMatrixTransposeP( vSimsIn2, p->nSimWords, vTransIn, 1 );
280 Extra_BitMatrixTransposeP( vSimsOut2, p->nSimWords, vTransOut, 1 );
281 Vec_WrdShrink( vTransIn, p->nPats );
282 Vec_WrdShrink( vTransOut, p->nPats );
283 Vec_Wrd_t * vTransInCopy = Vec_WrdDup(vTransIn);
284 Vec_WrdUniqify( vTransInCopy );
285// if ( Vec_WrdSize(vTransInCopy) == p->nPats )
286// printf( "This resub problem is not a relation.\n" );
287 // create the relation
288 Abc_RData_t * pNew = Abc_RDataStart( p->nIns, 1 << (p->nOuts-1), Vec_WrdSize(vTransInCopy) );
289 pNew->nOuts = p->nOuts;
290 int i, k, n, iLine = 0; word Entry, Entry2;
291 Vec_WrdForEachEntry( vTransInCopy, Entry, i ) {
292 for ( n = 0; n < p->nIns; n++ )
293 if ( (Entry >> n) & 1 )
294 Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsIn, n*pNew->nSimWords), iLine );
295 Vec_WrdForEachEntry( vTransIn, Entry2, k ) {
296 if ( Entry != Entry2 )
297 continue;
298 Entry2 = Vec_WrdEntry( vTransOut, k );
299 assert( Entry2 < (1 << p->nOuts) );
300 Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(pNew->vSimsOut, Entry2*pNew->nSimWords), iLine );
301 }
302 iLine++;
303 }
304 assert( iLine == pNew->nPats );
305 Vec_WrdFree( vTransOut );
306 Vec_WrdFree( vTransInCopy );
307 Vec_WrdFree( vTransIn );
308 Vec_WrdFree( vSimsIn2 );
309 Vec_WrdFree( vSimsOut2 );
310 return pNew;
311}
312
324/*
325void Abc_ReadPlaTest( char * pFileName )
326{
327 Abc_RData_t * p = Abc_ReadPla( pFileName );
328 Abc_WritePla( p, "resub_out.pla", 0 );
329 Abc_RData_t * p2 = Abc_RData2Rel( p );
330 Abc_WritePla( p2, "resub_out1.pla", 1 );
331 Abc_WritePla( p2, "resub_out2.pla", 2 );
332 Abc_RDataStop( p2 );
333 Abc_RDataStop( p );
334}
335*/
336
338
339#endif
340
344
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
typedefABC_NAMESPACE_HEADER_START struct Abc_RData_t_ Abc_RData_t
INCLUDES ///.
Definition ioResub.h:40
void Extra_BitMatrixTransposeP(Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
FUNCTION DECLARATIONS ///.
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Vec_Wrd_t * vSimsOut
Definition ioResub.h:48
Vec_Wrd_t * vSimsIn
Definition ioResub.h:47
int nSimWords
Definition ioResub.h:46
Vec_Int_t * vDivs
Definition ioResub.h:49
Vec_Int_t * vSol
Definition ioResub.h:50
#define assert(ex)
Definition util_old.h:213
char * strtok()
VOID_HACK free()
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42