ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
pla.h
Go to the documentation of this file.
1
20
21#ifndef ABC__base__wlc__wlc_h
22#define ABC__base__wlc__wlc_h
23
27
28#include "aig/gia/gia.h"
29#include "misc/extra/extra.h"
30#include "base/main/mainInt.h"
31//#include "misc/util/utilTruth.h"
32
36
38
39#define MASK55 ABC_CONST(0x5555555555555555)
40
44
45// file types
53
54// literal types
61
62
63typedef struct Pla_Man_t_ Pla_Man_t;
65{
66 char * pName; // model name
67 char * pSpec; // input file
68 Pla_File_t Type; // file type
69 int nIns; // inputs
70 int nOuts; // outputs
71 int nInWords; // words of input data
72 int nOutWords; // words of output data
73 Vec_Int_t vCubes; // cubes
74 Vec_Int_t vHashes; // hash values
75 Vec_Wrd_t vInBits; // input bits
76 Vec_Wrd_t vOutBits; // output bits
77 Vec_Wec_t vCubeLits; // cubes as interger arrays
78 Vec_Wec_t vOccurs; // occurence counters for the literals
79 Vec_Int_t vDivs; // divisor definitions
80};
81
82static inline char * Pla_ManName( Pla_Man_t * p ) { return p->pName; }
83static inline int Pla_ManInNum( Pla_Man_t * p ) { return p->nIns; }
84static inline int Pla_ManOutNum( Pla_Man_t * p ) { return p->nOuts; }
85static inline int Pla_ManCubeNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vCubes ); }
86static inline int Pla_ManDivNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vDivs ); }
87
88static inline word * Pla_CubeIn( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vInBits, i * p->nInWords); }
89static inline word * Pla_CubeOut( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vOutBits, i * p->nOutWords); }
90
91static inline int Pla_CubeNum( int hCube ) { return hCube >> 8; }
92static inline int Pla_CubeLit( int hCube ) { return hCube & 0xFF; }
93static inline int Pla_CubeHandle( int iCube, int iLit ) { assert( !(iCube >> 24) && !(iLit >> 8) ); return iCube << 8 | iLit; }
94
95// read/write/flip i-th bit of a bit string table
96static inline int Pla_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; }
97static inline void Pla_TtSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); }
98static inline void Pla_TtXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); }
99
100// read/write/flip i-th literal in a cube
101static inline int Pla_CubeGetLit( word * p, int i ) { return (int)(p[i>>5] >> ((i<<1) & 63)) & 3; }
102static inline void Pla_CubeSetLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] |= (((word)d)<<((i<<1) & 63)); }
103static inline void Pla_CubeXorLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] ^= (((word)d)<<((i<<1) & 63)); }
104
105
109
113
114#define Pla_ForEachCubeIn( p, pCube, i ) \
115 for ( i = 0; (i < Pla_ManCubeNum(p)) && (((pCube) = Pla_CubeIn(p, i)), 1); i++ )
116#define Pla_ForEachCubeInStart( p, pCube, i, Start ) \
117 for ( i = Start; (i < Pla_ManCubeNum(p)) && (((pCube) = Pla_CubeIn(p, i)), 1); i++ )
118
119#define Pla_ForEachCubeOut( p, pCube, i ) \
120 for ( i = 0; (i < Pla_ManCubeNum(p)) && (((pCube) = Pla_CubeOut(p, i)), 1); i++ )
121#define Pla_ForEachCubeInOut( p, pCubeIn, pCubeOut, i ) \
122 for ( i = 0; (i < Pla_ManCubeNum(p)) && (((pCubeIn) = Pla_CubeIn(p, i)), 1) && (((pCubeOut) = Pla_CubeOut(p, i)), 1); i++ )
123
124#define Pla_CubeForEachLit( nVars, pCube, Lit, i ) \
125 for ( i = 0; (i < nVars) && (((Lit) = Pla_CubeGetLit(pCube, i)), 1); i++ )
126#define Pla_CubeForEachLitIn( p, pCube, Lit, i ) \
127 Pla_CubeForEachLit( Pla_ManInNum(p), pCube, Lit, i )
128#define Pla_CubeForEachLitOut( p, pCube, Lit, i ) \
129 Pla_CubeForEachLit( Pla_ManOutNum(p), pCube, Lit, i )
130
131
135
147static inline int Pla_OnlyOneOne( word t )
148{
149 return t ? ((t & (t-1)) == 0) : 0;
150}
151static inline int Pla_CubesAreDistance1( word * p, word * q, int nWords )
152{
153 word Test; int c, fFound = 0;
154 for ( c = 0; c < nWords; c++ )
155 {
156 if ( p[c] == q[c] )
157 continue;
158 if ( fFound )
159 return 0;
160 // check if the number of 1s is one, which means exactly one different literal (0/1, -/1, -/0)
161 Test = ((p[c] ^ q[c]) | ((p[c] ^ q[c]) >> 1)) & MASK55;
162 if ( !Pla_OnlyOneOne(Test) )
163 return 0;
164 fFound = 1;
165 }
166 return fFound;
167}
168static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * piVar )
169{
170 word Test; int c, fFound = 0;
171 for ( c = 0; c < nWords; c++ )
172 {
173 if ( p[c] == q[c] )
174 continue;
175 if ( fFound )
176 return 0;
177 // check if the number of 1s is one, which means exactly one opposite literal (0/1) but may have other diffs (-/0 or -/1)
178 Test = ((p[c] ^ q[c]) & ((p[c] ^ q[c]) >> 1)) & MASK55;
179 if ( !Pla_OnlyOneOne(Test) )
180 return 0;
181 fFound = 1;
182 if ( piVar ) *piVar = c * 32 + Abc_Tt6FirstBit(Test)/2;
183 }
184 return fFound;
185}
186static inline int Pla_TtCountOnesOne( word x )
187{
188 x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
189 x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
190 x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
191 x = x + (x >> 8);
192 x = x + (x >> 16);
193 x = x + (x >> 32);
194 return (int)(x & 0xFF);
195}
196static inline int Pla_TtCountOnes( word * p, int nWords )
197{
198 int i, Count = 0;
199 for ( i = 0; i < nWords; i++ )
200 Count += Pla_TtCountOnesOne( p[i] );
201 return Count;
202}
203
215static inline Pla_Man_t * Pla_ManAlloc( char * pFileName, int nIns, int nOuts, int nCubes )
216{
218 p->pName = Extra_FileDesignName( pFileName );
219 p->pSpec = Abc_UtilStrsav( pFileName );
220 p->nIns = nIns;
221 p->nOuts = nOuts;
222 p->nInWords = Abc_Bit6WordNum( 2*nIns );
223 p->nOutWords = Abc_Bit6WordNum( 2*nOuts );
224 Vec_IntFillNatural( &p->vCubes, nCubes );
225 Vec_WrdFill( &p->vInBits, Pla_ManCubeNum(p) * p->nInWords, 0 );
226 Vec_WrdFill( &p->vOutBits, Pla_ManCubeNum(p) * p->nOutWords, 0 );
227 return p;
228}
229static inline void Pla_ManFree( Pla_Man_t * p )
230{
231 Vec_IntErase( &p->vCubes );
232 Vec_IntErase( &p->vHashes );
233 Vec_WrdErase( &p->vInBits );
234 Vec_WrdErase( &p->vOutBits );
235 Vec_WecErase( &p->vCubeLits );
236 Vec_WecErase( &p->vOccurs );
237 Vec_IntErase( &p->vDivs );
238 ABC_FREE( p->pName );
239 ABC_FREE( p->pSpec );
240 ABC_FREE( p );
241}
242static inline int Pla_ManLitInNum( Pla_Man_t * p )
243{
244 word * pCube; int i, k, Lit, Count = 0;
245 Pla_ForEachCubeIn( p, pCube, i )
246 Pla_CubeForEachLitIn( p, pCube, Lit, k )
247 Count += Lit != PLA_LIT_DASH;
248 return Count;
249}
250static inline int Pla_ManLitOutNum( Pla_Man_t * p )
251{
252 word * pCube; int i, k, Lit, Count = 0;
253 Pla_ForEachCubeOut( p, pCube, i )
254 Pla_CubeForEachLitOut( p, pCube, Lit, k )
255 Count += Lit == PLA_LIT_ONE;
256 return Count;
257}
258static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose )
259{
260 printf( "%-16s : ", Pla_ManName(p) );
261 printf( "In =%4d ", Pla_ManInNum(p) );
262 printf( "Out =%4d ", Pla_ManOutNum(p) );
263 printf( "Cube =%8d ", Pla_ManCubeNum(p) );
264 printf( "LitIn =%8d ", Pla_ManLitInNum(p) );
265 printf( "LitOut =%8d ", Pla_ManLitOutNum(p) );
266 printf( "Div =%6d ", Pla_ManDivNum(p) );
267 printf( "\n" );
268}
269
270
271
272/*=== plaHash.c ========================================================*/
273extern int Pla_ManHashDist1NumTest( Pla_Man_t * p );
274extern void Pla_ManComputeDist1Test( Pla_Man_t * p );
275/*=== plaMan.c ========================================================*/
276extern Vec_Bit_t * Pla_ManPrimesTable( int nVars );
277extern Pla_Man_t * Pla_ManPrimesDetector( int nVars );
278extern Pla_Man_t * Pla_ManGenerate( int nIns, int nOuts, int nCubes, int fVerbose );
279extern void Pla_ManConvertFromBits( Pla_Man_t * p );
280extern void Pla_ManConvertToBits( Pla_Man_t * p );
281extern int Pla_ManDist1NumTest( Pla_Man_t * p );
282/*=== plaMerge.c ========================================================*/
283extern int Pla_ManDist1Merge( Pla_Man_t * p );
284/*=== plaSimple.c ========================================================*/
285extern int Pla_ManFxPerformSimple( int nVars );
286/*=== plaRead.c ========================================================*/
287extern Pla_Man_t * Pla_ReadPla( char * pFileName );
288/*=== plaWrite.c ========================================================*/
289extern void Pla_WritePla( Pla_Man_t * p, char * pFileName );
290
292
293#endif
294
int nWords
Definition abcNpn.c:127
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
#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
char * Extra_FileDesignName(char *pFileName)
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
int Pla_ManDist1Merge(Pla_Man_t *p)
DECLARATIONS ///.
Definition plaMerge.c:44
#define Pla_ForEachCubeIn(p, pCube, i)
MACRO DEFINITIONS ///.
Definition pla.h:114
#define MASK55
INCLUDES ///.
Definition pla.h:39
Pla_File_t
BASIC TYPES ///.
Definition pla.h:46
@ PLA_FILE_FR
Definition pla.h:49
@ PLA_FILE_FDR
Definition pla.h:50
@ PLA_FILE_NONE
Definition pla.h:51
@ PLA_FILE_F
Definition pla.h:48
@ PLA_FILE_FD
Definition pla.h:47
void Pla_ManComputeDist1Test(Pla_Man_t *p)
Definition plaHash.c:333
#define Pla_CubeForEachLitIn(p, pCube, Lit, i)
Definition pla.h:126
#define Pla_CubeForEachLitOut(p, pCube, Lit, i)
Definition pla.h:128
void Pla_ManConvertToBits(Pla_Man_t *p)
Definition plaMan.c:251
void Pla_ManConvertFromBits(Pla_Man_t *p)
Definition plaMan.c:221
#define Pla_ForEachCubeOut(p, pCube, i)
Definition pla.h:119
int Pla_ManFxPerformSimple(int nVars)
Definition plaSimple.c:323
Pla_Man_t * Pla_ReadPla(char *pFileName)
Definition plaRead.c:186
struct Pla_Man_t_ Pla_Man_t
Definition pla.h:63
void Pla_WritePla(Pla_Man_t *p, char *pFileName)
Definition plaWrite.c:88
Pla_Man_t * Pla_ManGenerate(int nIns, int nOuts, int nCubes, int fVerbose)
Definition plaMan.c:168
Pla_Man_t * Pla_ManPrimesDetector(int nVars)
Definition plaMan.c:128
Vec_Bit_t * Pla_ManPrimesTable(int nVars)
Definition plaMan.c:85
int Pla_ManDist1NumTest(Pla_Man_t *p)
Definition plaMan.c:285
int Pla_ManHashDist1NumTest(Pla_Man_t *p)
Definition plaHash.c:212
Pla_Lit_t
Definition pla.h:55
@ PLA_LIT_ONE
Definition pla.h:58
@ PLA_LIT_FULL
Definition pla.h:59
@ PLA_LIT_ZERO
Definition pla.h:57
@ PLA_LIT_DASH
Definition pla.h:56
Vec_Wec_t vCubeLits
Definition pla.h:77
int nOutWords
Definition pla.h:72
Vec_Int_t vHashes
Definition pla.h:74
char * pSpec
Definition pla.h:67
char * pName
Definition pla.h:66
Vec_Int_t vCubes
Definition pla.h:73
Pla_File_t Type
Definition pla.h:68
int nOuts
Definition pla.h:70
int nInWords
Definition pla.h:71
Vec_Int_t vDivs
Definition pla.h:79
Vec_Wec_t vOccurs
Definition pla.h:78
Vec_Wrd_t vOutBits
Definition pla.h:76
Vec_Wrd_t vInBits
Definition pla.h:75
int nIns
Definition pla.h:69
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42