abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
amapPerm.c File Reference
#include "amapInt.h"
#include "bool/kit/kit.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Amap_LibCollectFanins_rec (Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Int_t *vFanins)
 DECLARATIONS ///. More...
 
Vec_Int_t * Amap_LibCollectFanins (Amap_Lib_t *pLib, Amap_Nod_t *pNod)
 
Vec_Int_t * Amap_LibDeriveGatePerm_rec (Amap_Lib_t *pLib, Kit_DsdNtk_t *pNtk, int iLit, Amap_Nod_t *pNod)
 
unsigned * Amap_LibVerifyPerm_rec (Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Ptr_t *vTtElems, Vec_Int_t *vTruth, int nWords, int *piInput)
 
void Amap_LibVerifyPerm (Amap_Lib_t *pLib, Amap_Gat_t *pGate, Kit_DsdNtk_t *pNtk, Amap_Nod_t *pNod, int *pArray)
 
int Amap_LibDeriveGatePerm (Amap_Lib_t *pLib, Amap_Gat_t *pGate, Kit_DsdNtk_t *pNtk, Amap_Nod_t *pNod, char *pArray)
 DECLARATIONS ///. More...
 

Function Documentation

Vec_Int_t* Amap_LibCollectFanins ( Amap_Lib_t *  pLib,
Amap_Nod_t *  pNod 
)

Function*************************************************************

Synopsis [Collects fanins of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file amapPerm.c.

78 {
79  Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
80  Amap_LibCollectFanins_rec( pLib, pNod, vFanins );
81  return vFanins;
82 }
Amap_LibCollectFanins_rec
ABC_NAMESPACE_IMPL_START void Amap_LibCollectFanins_rec(Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Int_t *vFanins)
DECLARATIONS ///.
Definition: amapPerm.c:46
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
ABC_NAMESPACE_IMPL_START void Amap_LibCollectFanins_rec ( Amap_Lib_t *  pLib,
Amap_Nod_t *  pNod,
Vec_Int_t *  vFanins 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [amapPerm.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Technology mapper for standard cells.]

Synopsis [Deriving permutation for the gate.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
amapPerm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Collects fanins of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file amapPerm.c.

47 {
48  Amap_Nod_t * pFan0, * pFan1;
49  if ( pNod->Id == 0 )
50  {
51  Vec_IntPush( vFanins, 0 );
52  return;
53  }
54  pFan0 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
55  if ( Abc_LitIsCompl(pNod->iFan0) || pFan0->Type != pNod->Type )
56  Vec_IntPush( vFanins, pNod->iFan0 );
57  else
58  Amap_LibCollectFanins_rec( pLib, pFan0, vFanins );
59  pFan1 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
60  if ( Abc_LitIsCompl(pNod->iFan1) || pFan1->Type != pNod->Type )
61  Vec_IntPush( vFanins, pNod->iFan1 );
62  else
63  Amap_LibCollectFanins_rec( pLib, pFan1, vFanins );
64 }
Amap_LibCollectFanins_rec
ABC_NAMESPACE_IMPL_START void Amap_LibCollectFanins_rec(Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Int_t *vFanins)
DECLARATIONS ///.
Definition: amapPerm.c:46
Amap_Nod_t_::iFan0
short iFan0
Definition: amapInt.h:177
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Amap_Nod_t_::Type
unsigned Type
Definition: amapInt.h:176
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Amap_Nod_t_
Definition: amapInt.h:172
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Amap_Nod_t_::Id
unsigned Id
Definition: amapInt.h:174
Amap_Nod_t_::iFan1
short iFan1
Definition: amapInt.h:178
Amap_LibNod
static Amap_Nod_t * Amap_LibNod(Amap_Lib_t *p, int i)
Definition: amapInt.h:264
int Amap_LibDeriveGatePerm ( Amap_Lib_t *  pLib,
Amap_Gat_t *  pGate,
Kit_DsdNtk_t *  pNtk,
Amap_Nod_t *  pNod,
char *  pArray 
)

DECLARATIONS ///.

Function*************************************************************

Synopsis [Matches the node with the DSD of a gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file amapPerm.c.

332 {
333  int fVerbose = 0;
334  Vec_Int_t * vPerm;
335  int Entry, Entry2, i, k;
336 // Kit_DsdPrint( stdout, pNtk );
337 
338  vPerm = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Abc_LitRegular(pNtk->Root), pNod );
339  if ( vPerm == NULL )
340  return 0;
341  // check that the permutation is valid
342  assert( Vec_IntSize(vPerm) == (int)pNod->nSuppSize );
343  Vec_IntForEachEntry( vPerm, Entry, i )
344  Vec_IntForEachEntryStart( vPerm, Entry2, k, i+1 )
345  if ( Abc_Lit2Var(Entry) == Abc_Lit2Var(Entry2) )
346  {
347  Vec_IntFree( vPerm );
348  return 0;
349  }
350 
351  // reverse the permutation
352  Vec_IntForEachEntry( vPerm, Entry, i )
353  {
354  assert( Entry < 2 * (int)pNod->nSuppSize );
355  pArray[Abc_Lit2Var(Entry)] = Abc_Var2Lit( i, Abc_LitIsCompl(Entry) );
356 // pArray[i] = Entry;
357 //printf( "%d=%d%c ", Abc_Lit2Var(Entry), i, Abc_LitIsCompl(Entry)?'-':'+' );
358  }
359 //printf( "\n" );
360 // if ( Kit_DsdNonDsdSizeMax(pNtk) < 3 )
361 // Amap_LibVerifyPerm( pLib, pGate, pNtk, pNod, Vec_IntArray(vPerm) );
362  Vec_IntFree( vPerm );
363  // print the result
364  if ( fVerbose )
365  {
366  printf( "node %4d : ", pNod->Id );
367  for ( i = 0; i < (int)pNod->nSuppSize; i++ )
368  printf( "%d=%d%c ", i, Abc_Lit2Var(pArray[i]), Abc_LitIsCompl(pArray[i])?'-':'+' );
369  printf( "\n" );
370  }
371  return 1;
372 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Kit_DsdNtk_t_::Root
unsigned short Root
Definition: kit.h:127
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
if
if(last==0)
Definition: sparse_int.h:34
Amap_Nod_t_::nSuppSize
unsigned nSuppSize
Definition: amapInt.h:175
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Amap_LibDeriveGatePerm_rec
Vec_Int_t * Amap_LibDeriveGatePerm_rec(Amap_Lib_t *pLib, Kit_DsdNtk_t *pNtk, int iLit, Amap_Nod_t *pNod)
Definition: amapPerm.c:95
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Amap_Nod_t_::Id
unsigned Id
Definition: amapInt.h:174
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Amap_LibDeriveGatePerm_rec ( Amap_Lib_t *  pLib,
Kit_DsdNtk_t *  pNtk,
int  iLit,
Amap_Nod_t *  pNod 
)

Function*************************************************************

Synopsis [Matches the node with the DSD node.]

Description [Returns perm if the node can be matched.]

SideEffects []

SeeAlso []

Definition at line 95 of file amapPerm.c.

96 {
97  Vec_Int_t * vPerm, * vPermFanin, * vNodFanin, * vDsdLits;
98  Kit_DsdObj_t * pDsdObj, * pDsdFanin;
99  Amap_Nod_t * pNodFanin;
100  int iDsdFanin, iNodFanin, Value, iDsdLit, i, k, j;
101 // assert( !Abc_LitIsCompl(iLit) );
102  pDsdObj = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iLit) );
103  if ( pDsdObj == NULL )
104  {
105  vPerm = Vec_IntAlloc( 1 );
106  Vec_IntPush( vPerm, iLit );
107  return vPerm;
108  }
109  if ( pDsdObj->Type == KIT_DSD_PRIME && pNod->Type == AMAP_OBJ_MUX )
110  {
111  vPerm = Vec_IntAlloc( 10 );
112 
113  iDsdFanin = pDsdObj->pFans[0];
114  pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
115  vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
116  if ( vPermFanin == NULL )
117  {
118  Vec_IntFree( vPerm );
119  return NULL;
120  }
121  Vec_IntForEachEntry( vPermFanin, Value, k )
122  Vec_IntPush( vPerm, Value );
123  Vec_IntFree( vPermFanin );
124 
125  iDsdFanin = pDsdObj->pFans[1];
126  pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
127  vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
128  if ( vPermFanin == NULL )
129  {
130  Vec_IntFree( vPerm );
131  return NULL;
132  }
133  Vec_IntForEachEntry( vPermFanin, Value, k )
134  Vec_IntPush( vPerm, Value );
135  Vec_IntFree( vPermFanin );
136 
137  iDsdFanin = pDsdObj->pFans[2];
138  pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan2) );
139  vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
140  if ( vPermFanin == NULL )
141  {
142  Vec_IntFree( vPerm );
143  return NULL;
144  }
145  Vec_IntForEachEntry( vPermFanin, Value, k )
146  Vec_IntPush( vPerm, Value );
147  Vec_IntFree( vPermFanin );
148 
149  return vPerm;
150  }
151  // return if wrong types
152  if ( pDsdObj->Type == KIT_DSD_PRIME || pNod->Type == AMAP_OBJ_MUX )
153  return NULL;
154  // return if sizes do not agree
155  vNodFanin = Amap_LibCollectFanins( pLib, pNod );
156  if ( Vec_IntSize(vNodFanin) != (int)pDsdObj->nFans )
157  {
158  Vec_IntFree( vNodFanin );
159  return NULL;
160  }
161  // match fanins of DSD with fanins of nodes
162  // clean the mark and save variable literals
163  vPerm = Vec_IntAlloc( 10 );
164  vDsdLits = Vec_IntAlloc( 10 );
165  Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
166  {
167  pDsdFanin = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iDsdFanin) );
168  if ( pDsdFanin )
169  pDsdFanin->fMark = 0;
170  else
171  Vec_IntPush( vDsdLits, iDsdFanin );
172  }
173  // match each fanins of the node
174  iDsdLit = 0;
175  Vec_IntForEachEntry( vNodFanin, iNodFanin, k )
176  {
177  if ( iNodFanin == 0 )
178  {
179  if ( iDsdLit >= Vec_IntSize(vDsdLits) )
180  {
181  Vec_IntFree( vPerm );
182  Vec_IntFree( vDsdLits );
183  Vec_IntFree( vNodFanin );
184  return NULL;
185  }
186  iDsdFanin = Vec_IntEntry( vDsdLits, iDsdLit++ );
187  Vec_IntPush( vPerm, iDsdFanin );
188  continue;
189  }
190  // find a matching component
191  pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(iNodFanin) );
192  Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
193  {
194  pDsdFanin = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iDsdFanin) );
195  if ( pDsdFanin == NULL )
196  continue;
197  if ( pDsdFanin->fMark == 1 )
198  continue;
199  if ( !((pDsdFanin->Type == KIT_DSD_AND && pNodFanin->Type == AMAP_OBJ_AND) ||
200  (pDsdFanin->Type == KIT_DSD_XOR && pNodFanin->Type == AMAP_OBJ_XOR) ||
201  (pDsdFanin->Type == KIT_DSD_PRIME && pNodFanin->Type == AMAP_OBJ_MUX)) )
202  continue;
203  vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Abc_LitRegular(iDsdFanin), pNodFanin );
204  if ( vPermFanin == NULL )
205  {
206  Vec_IntFree( vNodFanin );
207  Vec_IntFree( vDsdLits );
208  Vec_IntFree( vPerm );
209  return NULL;
210  }
211  pDsdFanin->fMark = 1;
212  Vec_IntForEachEntry( vPermFanin, Value, j )
213  Vec_IntPush( vPerm, Value );
214  Vec_IntFree( vPermFanin );
215  break;
216  }
217  }
218 // assert( iDsdLit == Vec_IntSize(vDsdLits) );
219  if ( iDsdLit != Vec_IntSize(vDsdLits) )
220  Vec_IntFreeP( &vPerm );
221  Vec_IntFree( vNodFanin );
222  Vec_IntFree( vDsdLits );
223  return vPerm;
224 }
Kit_DsdObj_t_::Type
unsigned Type
Definition: kit.h:112
Kit_DsdObj_t_::fMark
unsigned fMark
Definition: kit.h:113
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Amap_Nod_t_::iFan0
short iFan0
Definition: amapInt.h:177
Kit_DsdNtkObj
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
Amap_LibCollectFanins
Vec_Int_t * Amap_LibCollectFanins(Amap_Lib_t *pLib, Amap_Nod_t *pNod)
Definition: amapPerm.c:77
Kit_DsdObj_t_
Definition: kit.h:109
Amap_Nod_t_::Type
unsigned Type
Definition: amapInt.h:176
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if
if(last==0)
Definition: sparse_int.h:34
Kit_DsdObjForEachFaninReverse
#define Kit_DsdObjForEachFaninReverse(pNtk, pObj, iLit, i)
Definition: kit.h:159
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Kit_DsdObj_t_::pFans
unsigned short pFans[0]
Definition: kit.h:117
Amap_LibDeriveGatePerm_rec
Vec_Int_t * Amap_LibDeriveGatePerm_rec(Amap_Lib_t *pLib, Kit_DsdNtk_t *pNtk, int iLit, Amap_Nod_t *pNod)
Definition: amapPerm.c:95
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Amap_Nod_t_
Definition: amapInt.h:172
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
Amap_LibNod
static Amap_Nod_t * Amap_LibNod(Amap_Lib_t *p, int i)
Definition: amapInt.h:264
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Amap_LibVerifyPerm ( Amap_Lib_t *  pLib,
Amap_Gat_t *  pGate,
Kit_DsdNtk_t *  pNtk,
Amap_Nod_t *  pNod,
int *  pArray 
)

Function*************************************************************

Synopsis [Performs verification of one gate and one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file amapPerm.c.

281 {
282  Vec_Ptr_t * vTtElems;
283  Vec_Ptr_t * vTtElemsPol;
284  Vec_Int_t * vTruth;
285  unsigned * pTruth;
286  int i, nWords;
287  int iInput = 0;
288 
289  // allocate storage for truth tables
290  assert( pGate->nPins > 1 );
291  nWords = Kit_TruthWordNum( pGate->nPins );
292  vTruth = Vec_IntAlloc( nWords * AMAP_MAXINS );
293  vTtElems = Vec_PtrAllocTruthTables( pGate->nPins );
294  vTtElemsPol = Vec_PtrAlloc( pGate->nPins );
295  for ( i = 0; i < (int)pGate->nPins; i++ )
296  {
297  pTruth = (unsigned *)Vec_PtrEntry( vTtElems, Abc_Lit2Var(pArray[i]) );
298  if ( Abc_LitIsCompl( pArray[i] ) )
299  Kit_TruthNot( pTruth, pTruth, pGate->nPins );
300  Vec_PtrPush( vTtElemsPol, pTruth );
301  }
302 //Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 0), 4 ); printf("\n" );
303 //Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 1), 4 ); printf("\n" );
304  // compute the truth table recursively
305  pTruth = Amap_LibVerifyPerm_rec( pLib, pNod, vTtElemsPol, vTruth, nWords, &iInput );
306  assert( iInput == (int)pGate->nPins );
307  if ( Abc_LitIsCompl(pNtk->Root) )
308  Kit_TruthNot( pTruth, pTruth, pGate->nPins );
309 //Extra_PrintBinary( stdout, pTruth, 4 ); printf("\n" );
310 //Extra_PrintBinary( stdout, pGate->pFunc, 4 ); printf("\n" );
311  // compare
312  if ( !Kit_TruthIsEqual(pGate->pFunc, pTruth, pGate->nPins) )
313  printf( "Verification failed for gate %d (%s) and node %d.\n",
314  pGate->Id, pGate->pForm, pNod->Id );
315  Vec_IntFree( vTruth );
316  Vec_PtrFree( vTtElems );
317  Vec_PtrFree( vTtElemsPol );
318 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Amap_Gat_t_::pForm
char * pForm
Definition: amapInt.h:157
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Kit_DsdNtk_t_::Root
unsigned short Root
Definition: kit.h:127
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
nWords
int nWords
Definition: abcNpn.c:127
Vec_PtrAllocTruthTables
static Vec_Ptr_t * Vec_PtrAllocTruthTables(int nVars)
Definition: vecPtr.h:1065
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
AMAP_MAXINS
#define AMAP_MAXINS
INCLUDES ///.
Definition: amapInt.h:44
Amap_Gat_t_::pFunc
unsigned * pFunc
Definition: amapInt.h:158
Amap_Gat_t_::nPins
unsigned nPins
Definition: amapInt.h:161
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Amap_LibVerifyPerm_rec
unsigned * Amap_LibVerifyPerm_rec(Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Ptr_t *vTtElems, Vec_Int_t *vTruth, int nWords, int *piInput)
Definition: amapPerm.c:237
Amap_Nod_t_::Id
unsigned Id
Definition: amapInt.h:174
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Amap_Gat_t_::Id
unsigned Id
Definition: amapInt.h:159
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
unsigned* Amap_LibVerifyPerm_rec ( Amap_Lib_t *  pLib,
Amap_Nod_t *  pNod,
Vec_Ptr_t *  vTtElems,
Vec_Int_t *  vTruth,
int  nWords,
int *  piInput 
)

Function*************************************************************

Synopsis [Performs verification of one gate and one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file amapPerm.c.

239 {
240  Amap_Nod_t * pFan0, * pFan1;
241  unsigned * pTruth0, * pTruth1, * pTruth;
242  int i;
243  assert( pNod->Type != AMAP_OBJ_MUX );
244  if ( pNod->Id == 0 )
245  return (unsigned *)Vec_PtrEntry( vTtElems, (*piInput)++ );
246  pFan0 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
247  pTruth0 = Amap_LibVerifyPerm_rec( pLib, pFan0, vTtElems, vTruth, nWords, piInput );
248  pFan1 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
249  pTruth1 = Amap_LibVerifyPerm_rec( pLib, pFan1, vTtElems, vTruth, nWords, piInput );
250  pTruth = Vec_IntFetch( vTruth, nWords );
251  if ( pNod->Type == AMAP_OBJ_XOR )
252  for ( i = 0; i < nWords; i++ )
253  pTruth[i] = pTruth0[i] ^ pTruth1[i];
254  else if ( !Abc_LitIsCompl(pNod->iFan0) && !Abc_LitIsCompl(pNod->iFan1) )
255  for ( i = 0; i < nWords; i++ )
256  pTruth[i] = pTruth0[i] & pTruth1[i];
257  else if ( !Abc_LitIsCompl(pNod->iFan0) && Abc_LitIsCompl(pNod->iFan1) )
258  for ( i = 0; i < nWords; i++ )
259  pTruth[i] = pTruth0[i] & ~pTruth1[i];
260  else if ( Abc_LitIsCompl(pNod->iFan0) && !Abc_LitIsCompl(pNod->iFan1) )
261  for ( i = 0; i < nWords; i++ )
262  pTruth[i] = ~pTruth0[i] & pTruth1[i];
263  else // if ( Abc_LitIsCompl(pNod->iFan0) && Hop_ObjFaninC1(pObj) )
264  for ( i = 0; i < nWords; i++ )
265  pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
266  return pTruth;
267 }
Amap_Nod_t_::iFan0
short iFan0
Definition: amapInt.h:177
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
nWords
int nWords
Definition: abcNpn.c:127
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Amap_Nod_t_::Type
unsigned Type
Definition: amapInt.h:176
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Amap_Nod_t_
Definition: amapInt.h:172
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Amap_LibVerifyPerm_rec
unsigned * Amap_LibVerifyPerm_rec(Amap_Lib_t *pLib, Amap_Nod_t *pNod, Vec_Ptr_t *vTtElems, Vec_Int_t *vTruth, int nWords, int *piInput)
Definition: amapPerm.c:237
Amap_Nod_t_::Id
unsigned Id
Definition: amapInt.h:174
Amap_Nod_t_::iFan1
short iFan1
Definition: amapInt.h:178
assert
#define assert(ex)
Definition: util_old.h:213
Amap_LibNod
static Amap_Nod_t * Amap_LibNod(Amap_Lib_t *p, int i)
Definition: amapInt.h:264