ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
amapPerm.c File Reference
#include "amapInt.h"
#include "bool/kit/kit.h"
Include dependency graph for amapPerm.c:

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 ///.
 
Vec_Int_tAmap_LibCollectFanins (Amap_Lib_t *pLib, Amap_Nod_t *pNod)
 
Vec_Int_tAmap_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 ///.
 

Function Documentation

◆ Amap_LibCollectFanins()

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}
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
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Amap_LibCollectFanins_rec()

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}
struct Amap_Nod_t_ Amap_Nod_t
Definition amapInt.h:67
unsigned Type
Definition amapInt.h:177
short iFan0
Definition amapInt.h:178
short iFan1
Definition amapInt.h:179
unsigned Id
Definition amapInt.h:175
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Amap_LibDeriveGatePerm()

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 * Amap_LibDeriveGatePerm_rec(Amap_Lib_t *pLib, Kit_DsdNtk_t *pNtk, int iLit, Amap_Nod_t *pNod)
Definition amapPerm.c:95
if(last==0)
Definition sparse_int.h:34
unsigned nSuppSize
Definition amapInt.h:176
unsigned short Root
Definition kit.h:130
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Amap_LibDeriveGatePerm_rec()

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}
@ AMAP_OBJ_XOR
Definition amapInt.h:56
@ AMAP_OBJ_AND
Definition amapInt.h:55
@ AMAP_OBJ_MUX
Definition amapInt.h:57
Vec_Int_t * Amap_LibCollectFanins(Amap_Lib_t *pLib, Amap_Nod_t *pNod)
Definition amapPerm.c:77
@ KIT_DSD_XOR
Definition kit.h:106
@ KIT_DSD_PRIME
Definition kit.h:107
@ KIT_DSD_AND
Definition kit.h:105
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
#define Kit_DsdObjForEachFaninReverse(pNtk, pObj, iLit, i)
Definition kit.h:162
short iFan2
Definition amapInt.h:180
unsigned Type
Definition kit.h:115
unsigned nFans
Definition kit.h:119
unsigned short pFans[0]
Definition kit.h:120
unsigned fMark
Definition kit.h:116
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Amap_LibVerifyPerm()

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}
int nWords
Definition abcNpn.c:127
#define AMAP_MAXINS
INCLUDES ///.
Definition amapInt.h:44
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
char * pForm
Definition amapInt.h:158
unsigned nPins
Definition amapInt.h:162
unsigned * pFunc
Definition amapInt.h:159
unsigned Id
Definition amapInt.h:160
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:

◆ 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 )

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}
Here is the call graph for this function:
Here is the caller graph for this function: