pla.h 11.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
/**CFile****************************************************************

  FileName    [pla.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SOP manager.]

  Synopsis    [Scalable SOP transformations.]

  Author      [Alan Mishchenko]
12

13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - March 18, 2015.]

  Revision    [$Id: pla.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $]

***********************************************************************/

#ifndef ABC__base__wlc__wlc_h
#define ABC__base__wlc__wlc_h

////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "aig/gia/gia.h"
#include "misc/extra/extra.h"
#include "base/main/mainInt.h"
//#include "misc/util/utilTruth.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

37
ABC_NAMESPACE_HEADER_START
38 39 40 41 42 43 44 45

#define MASK55 ABC_CONST(0x5555555555555555)

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

// file types
46 47 48 49 50 51 52
typedef enum {
    PLA_FILE_FD = 0,
    PLA_FILE_F,
    PLA_FILE_FR,
    PLA_FILE_FDR,
    PLA_FILE_NONE
} Pla_File_t;
53 54

// literal types
55 56 57 58 59 60
typedef enum {
    PLA_LIT_DASH = 0,
    PLA_LIT_ZERO,
    PLA_LIT_ONE,
    PLA_LIT_FULL
} Pla_Lit_t;
61 62 63


typedef struct Pla_Man_t_ Pla_Man_t;
64
struct Pla_Man_t_
65 66 67 68 69 70 71 72 73 74 75 76
{
    char *           pName;      // model name
    char *           pSpec;      // input file
    Pla_File_t       Type;       // file type
    int              nIns;       // inputs
    int              nOuts;      // outputs
    int              nInWords;   // words of input data
    int              nOutWords;  // words of output data
    Vec_Int_t        vCubes;     // cubes
    Vec_Int_t        vHashes;    // hash values
    Vec_Wrd_t        vInBits;    // input bits
    Vec_Wrd_t        vOutBits;   // output bits
77 78 79
    Vec_Wec_t        vCubeLits;  // cubes as interger arrays
    Vec_Wec_t        vOccurs;    // occurence counters for the literals
    Vec_Int_t        vDivs;      // divisor definitions
80 81
};

82
static inline char * Pla_ManName( Pla_Man_t * p )                    { return p->pName;                   }
83 84 85
static inline int    Pla_ManInNum( Pla_Man_t * p )                   { return p->nIns;                    }
static inline int    Pla_ManOutNum( Pla_Man_t * p )                  { return p->nOuts;                   }
static inline int    Pla_ManCubeNum( Pla_Man_t * p )                 { return Vec_IntSize( &p->vCubes );  }
86
static inline int    Pla_ManDivNum( Pla_Man_t * p )                  { return Vec_IntSize( &p->vDivs );   }
87 88 89 90

static inline word * Pla_CubeIn( Pla_Man_t * p, int i )              { return Vec_WrdEntryP(&p->vInBits,  i * p->nInWords);  }
static inline word * Pla_CubeOut( Pla_Man_t * p, int i )             { return Vec_WrdEntryP(&p->vOutBits, i * p->nOutWords); }

91 92 93 94 95 96 97 98 99 100 101 102 103
static inline int    Pla_CubeNum( int hCube )                        { return hCube >> 8;    }
static inline int    Pla_CubeLit( int hCube )                        { return hCube & 0xFF;  }
static inline int    Pla_CubeHandle( int iCube, int iLit )           { assert( !(iCube >> 24) && !(iLit >> 8) ); return iCube << 8 | iLit; }

// read/write/flip i-th bit of a bit string table
static inline int    Pla_TtGetBit( word * p, int i )                 { return (int)(p[i>>6] >> (i & 63)) & 1;      }
static inline void   Pla_TtSetBit( word * p, int i )                 { p[i>>6] |= (((word)1)<<(i & 63));           }
static inline void   Pla_TtXorBit( word * p, int i )                 { p[i>>6] ^= (((word)1)<<(i & 63));           }

// read/write/flip i-th literal in a cube
static inline int    Pla_CubeGetLit( word * p, int i )               { return (int)(p[i>>5] >> ((i<<1) & 63)) & 3; }
static inline void   Pla_CubeSetLit( word * p, int i, Pla_Lit_t d )  { p[i>>5] |= (((word)d)<<((i<<1) & 63));      }
static inline void   Pla_CubeXorLit( word * p, int i, Pla_Lit_t d )  { p[i>>5] ^= (((word)d)<<((i<<1) & 63));      }
104 105 106 107 108 109 110 111 112 113 114


////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                             ITERATORS                            ///
////////////////////////////////////////////////////////////////////////

#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 127 128 129 130 131 132 133 134 135 136 137 138 139 140
#define Pla_CubeForEachLitIn( p, pCube, Lit, i )                    \
    Pla_CubeForEachLit( Pla_ManInNum(p), pCube, Lit, i )
#define Pla_CubeForEachLitOut( p, pCube, Lit, i )                   \
    Pla_CubeForEachLit( Pla_ManOutNum(p), pCube, Lit, i )


////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Checks if cubes are distance-1.]

  Description []
141

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Pla_OnlyOneOne( word t )
{
    return t ? ((t & (t-1)) == 0) : 0;
}
static inline int Pla_CubesAreDistance1( word * p, word * q, int nWords )
{
    word Test; int c, fFound = 0;
    for ( c = 0; c < nWords; c++ )
    {
        if ( p[c] == q[c] )
            continue;
        if ( fFound )
            return 0;
        // check if the number of 1s is one, which means exactly one different literal (0/1, -/1, -/0)
        Test = ((p[c] ^ q[c]) | ((p[c] ^ q[c]) >> 1)) & MASK55;
        if ( !Pla_OnlyOneOne(Test) )
            return 0;
        fFound = 1;
    }
    return fFound;
}
static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * piVar )
{
    word Test; int c, fFound = 0;
    for ( c = 0; c < nWords; c++ )
    {
        if ( p[c] == q[c] )
            continue;
        if ( fFound )
            return 0;
        // 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 180 181 182 183 184 185
        if ( !Pla_OnlyOneOne(Test) )
            return 0;
        fFound = 1;
        if ( piVar ) *piVar = c * 32 + Abc_Tt6FirstBit(Test)/2;
    }
    return fFound;
}
186 187
static inline int Pla_TtCountOnesOne( word x )
{
188 189 190
    x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
    x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
    x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
191 192
    x = x + (x >> 8);
    x = x + (x >> 16);
193
    x = x + (x >> 32);
194 195 196 197 198 199 200 201 202
    return (int)(x & 0xFF);
}
static inline int Pla_TtCountOnes( word * p, int nWords )
{
    int i, Count = 0;
    for ( i = 0; i < nWords; i++ )
        Count += Pla_TtCountOnesOne( p[i] );
    return Count;
}
203

204 205 206 207 208
/**Function*************************************************************

  Synopsis    [Manager APIs.]

  Description []
209

210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Pla_Man_t * Pla_ManAlloc( char * pFileName, int nIns, int nOuts, int nCubes )
{
    Pla_Man_t * p = ABC_CALLOC( Pla_Man_t, 1 );
    p->pName = Extra_FileDesignName( pFileName );
    p->pSpec = Abc_UtilStrsav( pFileName );
    p->nIns  = nIns;
    p->nOuts = nOuts;
    p->nInWords  = Abc_Bit6WordNum( 2*nIns );
    p->nOutWords = Abc_Bit6WordNum( 2*nOuts );
    Vec_IntFillNatural( &p->vCubes, nCubes );
    Vec_WrdFill( &p->vInBits,  Pla_ManCubeNum(p) * p->nInWords,  0 );
    Vec_WrdFill( &p->vOutBits, Pla_ManCubeNum(p) * p->nOutWords, 0 );
    return p;
}
static inline void Pla_ManFree( Pla_Man_t * p )
{
    Vec_IntErase( &p->vCubes );
    Vec_IntErase( &p->vHashes );
    Vec_WrdErase( &p->vInBits );
    Vec_WrdErase( &p->vOutBits );
235
    Vec_WecErase( &p->vCubeLits );
236
    Vec_WecErase( &p->vOccurs );
237
    Vec_IntErase( &p->vDivs );
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
    ABC_FREE( p->pName );
    ABC_FREE( p->pSpec );
    ABC_FREE( p );
}
static inline int Pla_ManLitInNum( Pla_Man_t * p )
{
    word * pCube; int i, k, Lit, Count = 0;
    Pla_ForEachCubeIn( p, pCube, i )
        Pla_CubeForEachLitIn( p, pCube, Lit, k )
            Count += Lit != PLA_LIT_DASH;
    return Count;
}
static inline int Pla_ManLitOutNum( Pla_Man_t * p )
{
    word * pCube; int i, k, Lit, Count = 0;
    Pla_ForEachCubeOut( p, pCube, i )
        Pla_CubeForEachLitOut( p, pCube, Lit, k )
            Count += Lit == PLA_LIT_ONE;
    return Count;
}
static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose )
{
260
    printf( "%-16s :  ",     Pla_ManName(p) );
261 262 263 264 265
    printf( "In =%4d  ",     Pla_ManInNum(p) );
    printf( "Out =%4d  ",    Pla_ManOutNum(p) );
    printf( "Cube =%8d  ",   Pla_ManCubeNum(p) );
    printf( "LitIn =%8d  ",  Pla_ManLitInNum(p) );
    printf( "LitOut =%8d  ", Pla_ManLitOutNum(p) );
266
    printf( "Div =%6d  ",    Pla_ManDivNum(p) );
Alan Mishchenko committed
267
    printf( "\n" );
268 269 270
}


271

272 273
/*=== plaHash.c ========================================================*/
extern int                 Pla_ManHashDist1NumTest( Pla_Man_t * p );
274
extern void                Pla_ManComputeDist1Test( Pla_Man_t * p );
275
/*=== plaMan.c ========================================================*/
276 277
extern Vec_Bit_t *         Pla_ManPrimesTable( int nVars );
extern Pla_Man_t *         Pla_ManPrimesDetector( int nVars );
278 279 280 281 282 283
extern Pla_Man_t *         Pla_ManGenerate( int nIns, int nOuts, int nCubes, int fVerbose );
extern void                Pla_ManConvertFromBits( Pla_Man_t * p );
extern void                Pla_ManConvertToBits( Pla_Man_t * p );
extern int                 Pla_ManDist1NumTest( Pla_Man_t * p );
/*=== plaMerge.c ========================================================*/
extern int                 Pla_ManDist1Merge( Pla_Man_t * p );
284 285
/*=== plaSimple.c ========================================================*/
extern int                 Pla_ManFxPerformSimple( int nVars );
286 287 288 289 290 291 292 293 294 295 296 297
/*=== plaRead.c ========================================================*/
extern Pla_Man_t *         Pla_ReadPla( char * pFileName );
/*=== plaWrite.c ========================================================*/
extern void                Pla_WritePla( Pla_Man_t * p, char * pFileName );

ABC_NAMESPACE_HEADER_END

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////