ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
plaMan.c
Go to the documentation of this file.
1
20
21#include "pla.h"
22
24
28
32
44void Pla_GenSorter( int nVars )
45{
46 int i, k, Count, nMints = ( 1 << nVars );
47 char Buffer[20];
48 FILE * pFile;
49 sprintf( Buffer, "sorter%02d.pla", nVars );
50 pFile = fopen( Buffer, "wb" );
51 fprintf( pFile, "# This file was generated by ABC on %s.\n", Extra_TimeStamp() );
52 fprintf( pFile, ".i %d\n", nVars );
53 fprintf( pFile, ".o %d\n", nVars );
54 fprintf( pFile, ".p %d\n", nMints-1 );
55 for ( i = 1; i < nMints; i++ )
56 {
57 Count = 0;
58 for ( k = nVars-1; k >= 0; k-- )
59 {
60 Count += ((i >> k) & 1);
61 fprintf( pFile, "%d", (i >> k) & 1 );
62 }
63 fprintf( pFile, " " );
64 for ( k = 0; k < Count; k++ )
65 fprintf( pFile, "1" );
66 for ( ; k < nVars; k++ )
67 fprintf( pFile, "0" );
68 fprintf( pFile, "\n" );
69 }
70 fprintf( pFile, ".end\n" );
71 fclose( pFile );
72}
73
86{
87 int i, n, nBits = 1 << nVars;
88 Vec_Bit_t * vMap = Vec_BitStartFull( Abc_MaxInt(64, nBits) );
89 for ( i = nBits; i < 64; i++ )
90 Vec_BitWriteEntry( vMap, i, 0 );
91 Vec_BitShrink( vMap, nBits );
92 Vec_BitWriteEntry( vMap, 0, 0 );
93 Vec_BitWriteEntry( vMap, 1, 0 );
94 for ( n = 2; n < nBits; n++ )
95 if ( Vec_BitEntry(vMap, n) )
96 for ( i = 2*n; i < nBits; i += n )
97 Vec_BitWriteEntry( vMap, i, 0 );
98 return vMap;
99}
101{
102 int n, nBits = ( 1 << nVars );
103 Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 );
104 Vec_Bit_t * vMap = Pla_ManPrimesTable( nVars );
105 for ( n = 2; n < nBits; n++ )
106 if ( Vec_BitEntry(vMap, n) )
107 Vec_IntPush( vPrimes, n );
108 printf( "Primes up to 2^%d = %d\n", nVars, Vec_IntSize(vPrimes) );
109// Abc_GenCountHits1( vMap, vPrimes, nVars );
110 Vec_BitFree( vMap );
111 return vPrimes;
112}
113Pla_Man_t * Pla_GenFromMinterms( char * pName, Vec_Int_t * vMints, int nVars )
114{
115 Pla_Man_t * p = Pla_ManAlloc( pName, nVars, 1, Vec_IntSize(vMints) );
116 int i, k, Lit, Mint;
117 word * pCube;
118 Pla_ForEachCubeIn( p, pCube, i )
119 {
120 Mint = Vec_IntEntry(vMints, i);
121 Pla_CubeForEachLitIn( p, pCube, Lit, k )
122 Pla_CubeSetLit( pCube, k, ((Mint >> k) & 1) ? PLA_LIT_ONE : PLA_LIT_ZERO );
123 }
124 Pla_ForEachCubeOut( p, pCube, i )
125 Pla_CubeSetLit( pCube, 0, PLA_LIT_ONE );
126 return p;
127}
129{
130 char pName[1000];
131 Pla_Man_t * p;
132 Vec_Int_t * vMints = Pla_GenPrimes( nVars );
133 sprintf( pName, "primes%02d", nVars );
134 p = Pla_GenFromMinterms( pName, vMints, nVars );
135 Vec_IntFree( vMints );
136 return p;
137}
138
150Vec_Bit_t * Pla_GenRandom( int nVars, int nNums, int fNonZero )
151{
152 int Mint, Count = 0;
153 Vec_Bit_t * vBits = Vec_BitStart( 1 << nVars );
154 assert( nVars > 0 && nVars <= 30 );
155 assert( nNums > 0 && nNums < (1 << (nVars - 1)) );
156 while ( Count < nNums )
157 {
158 Mint = Gia_ManRandom(0) & ((1 << nVars) - 1);
159 if ( fNonZero && Mint == 0 )
160 continue;
161 if ( Vec_BitEntry(vBits, Mint) )
162 continue;
163 Vec_BitWriteEntry( vBits, Mint, 1 );
164 Count++;
165 }
166 return vBits;
167}
168Pla_Man_t * Pla_ManGenerate( int nInputs, int nOutputs, int nCubes, int fVerbose )
169{
170 Pla_Man_t * p;
171 Vec_Bit_t * vBits;
172 int i, k, Count;
173 word * pCube;
174 char Buffer[1000];
175 sprintf( Buffer, "%s_%d_%d_%d", "rand", nInputs, nOutputs, nCubes );
176 p = Pla_ManAlloc( Buffer, nInputs, nOutputs, nCubes );
177 // generate nCube random input minterms
178 vBits = Pla_GenRandom( nInputs, nCubes, 0 );
179 for ( i = Count = 0; i < Vec_BitSize(vBits); i++ )
180 if ( Vec_BitEntry(vBits, i) )
181 {
182 pCube = Pla_CubeIn( p, Count++ );
183 for ( k = 0; k < nInputs; k++ )
184 Pla_CubeSetLit( pCube, k, ((i >> k) & 1) ? PLA_LIT_ONE : PLA_LIT_ZERO );
185 }
186 assert( Count == nCubes );
187 Vec_BitFree( vBits );
188 // generate nCube random output minterms
189 if ( nOutputs > 1 )
190 {
191 vBits = Pla_GenRandom( nOutputs, nCubes, 1 );
192 for ( i = Count = 0; i < Vec_BitSize(vBits); i++ )
193 if ( Vec_BitEntry(vBits, i) )
194 {
195 pCube = Pla_CubeOut( p, Count++ );
196 for ( k = 0; k < nOutputs; k++ )
197 Pla_CubeSetLit( pCube, k, ((i >> k) & 1) ? PLA_LIT_ONE : PLA_LIT_ZERO );
198 }
199 assert( Count == nCubes );
200 Vec_BitFree( vBits );
201 }
202 else
203 {
204 Pla_ForEachCubeOut( p, pCube, i )
205 Pla_CubeSetLit( pCube, 0, PLA_LIT_ONE );
206 }
207 return p;
208}
209
222{
223 Vec_Int_t * vCube;
224 word * pCube; int i, k, Lit, Count;
225 Vec_WecClear( &p->vCubeLits );
226 Vec_WecClear( &p->vOccurs );
227 Vec_WecInit( &p->vCubeLits, Pla_ManCubeNum(p) );
228 Vec_WecInit( &p->vOccurs, 2*Pla_ManInNum(p) );
229 Pla_ForEachCubeIn( p, pCube, i )
230 {
231 vCube = Vec_WecEntry( &p->vCubeLits, i );
232
233 Count = 0;
234 Pla_CubeForEachLitIn( p, pCube, Lit, k )
235 if ( Lit != PLA_LIT_DASH )
236 Count++;
237 Vec_IntGrow( vCube, Count );
238
239 Count = 0;
240 Pla_CubeForEachLitIn( p, pCube, Lit, k )
241 if ( Lit != PLA_LIT_DASH )
242 {
243 Lit = Abc_Var2Lit( k, Lit == PLA_LIT_ZERO );
244 Vec_WecPush( &p->vCubeLits, i, Lit );
245// Vec_WecPush( &p->vOccurs, Lit, Pla_CubeHandle(i, Count++) );
246 Vec_WecPush( &p->vOccurs, Lit, i );
247 }
248 assert( Vec_IntSize(vCube) == Vec_IntCap(vCube) );
249 }
250}
252{
253 Vec_Int_t * vCube; int i, k, Lit;
254 Vec_IntFillNatural( &p->vCubes, Vec_WecSize(&p->vCubeLits) );
255 Vec_WrdFill( &p->vInBits, Pla_ManCubeNum(p) * p->nInWords, 0 );
256 Vec_WecForEachLevel( &p->vCubeLits, vCube, i )
257 Vec_IntForEachEntry( vCube, Lit, k )
258 Pla_CubeSetLit( Pla_CubeIn(p, i), Abc_Lit2Var(Lit), Abc_LitIsCompl(Lit) ? PLA_LIT_ZERO : PLA_LIT_ONE );
259}
260
273{
274 word * pCube1, * pCube2;
275 int i, k, Dist, Count = 0;
276 Pla_ForEachCubeIn( p, pCube1, i )
277 Pla_ForEachCubeInStart( p, pCube2, k, i+1 )
278 {
279 Dist = Pla_CubesAreDistance1( pCube1, pCube2, p->nInWords );
280// Dist = Pla_CubesAreConsensus( pCube1, pCube2, p->nInWords, NULL );
281 Count += (Dist == 1);
282 }
283 return Count;
284}
286{
287 abctime clk = Abc_Clock();
288 int Count = Pla_ManDist1Num( p );
289 printf( "Found %d pairs among %d cubes using cube pair enumeration. ", Count, Pla_ManCubeNum(p) );
290 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
291 return 1;
292}
293
297
298
300
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
cubedist Dist
Definition exorList.c:1012
char * Extra_TimeStamp()
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition giaUtil.c:49
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
void Pla_ManConvertToBits(Pla_Man_t *p)
Definition plaMan.c:251
void Pla_ManConvertFromBits(Pla_Man_t *p)
Definition plaMan.c:221
Pla_Man_t * Pla_GenFromMinterms(char *pName, Vec_Int_t *vMints, int nVars)
Definition plaMan.c:113
ABC_NAMESPACE_IMPL_START void Pla_GenSorter(int nVars)
DECLARATIONS ///.
Definition plaMan.c:44
Vec_Bit_t * Pla_GenRandom(int nVars, int nNums, int fNonZero)
Definition plaMan.c:150
Pla_Man_t * Pla_ManGenerate(int nInputs, int nOutputs, int nCubes, int fVerbose)
Definition plaMan.c:168
int Pla_ManDist1Num(Pla_Man_t *p)
Definition plaMan.c:272
Vec_Int_t * Pla_GenPrimes(int nVars)
Definition plaMan.c:100
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
#define Pla_ForEachCubeIn(p, pCube, i)
MACRO DEFINITIONS ///.
Definition pla.h:114
#define Pla_CubeForEachLitIn(p, pCube, Lit, i)
Definition pla.h:126
#define Pla_ForEachCubeOut(p, pCube, i)
Definition pla.h:119
#define Pla_ForEachCubeInStart(p, pCube, i, Start)
Definition pla.h:116
struct Pla_Man_t_ Pla_Man_t
Definition pla.h:63
@ PLA_LIT_ONE
Definition pla.h:58
@ PLA_LIT_ZERO
Definition pla.h:57
@ PLA_LIT_DASH
Definition pla.h:56
#define assert(ex)
Definition util_old.h:213
char * sprintf()
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
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55