ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
lpkMux.c File Reference
#include "lpkInt.h"
Include dependency graph for lpkMux.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Lpk_MapTreeBestCofVar (Lpk_Man_t *p, unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
 DECLARATIONS ///.
 
If_Obj_t * Lpk_MapTreeMux_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
If_Obj_t * Lpk_MapSuppRedDec_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
void Lpk_TryDec (word *pTruth, int nVars)
 
void Lpk_TryDecTest ()
 

Function Documentation

◆ Lpk_MapSuppRedDec_rec()

If_Obj_t * Lpk_MapSuppRedDec_rec ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )

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

Synopsis [Implements support-reducing decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file lpkMux.c.

134{
135 Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
136 If_Obj_t * pObjNew;
137 unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
138 unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
139 unsigned * pDec0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 2 );
140 unsigned * pDec1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 3 );
141 unsigned * pDec = (unsigned *)Vec_PtrEntry( p->vTtNodes, 4 );
142 unsigned * pCo00 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 5 );
143 unsigned * pCo01 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 6 );
144 unsigned * pCo10 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 7 );
145 unsigned * pCo11 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 8 );
146 unsigned * pCo0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 9 );
147 unsigned * pCo1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 10 );
148 unsigned * pCo = (unsigned *)Vec_PtrEntry( p->vTtNodes, 11 );
149 int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
150 int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
151
152 // determine if supp-red decomposition exists
153 uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
154 if ( uSubsets == 0 )
155 return NULL;
156 p->nCalledSRed++;
157
158 // get the cofactors
159 Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
160 Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
161
162 // get the bound sets
163 uSubset0 = uSubsets & 0xFFFF;
164 uSubset1 = uSubsets >> 16;
165
166 // compute the decomposed functions
167 ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
168 ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
169 ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
170 ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
171 Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
172 Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
173// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 );
174// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 );
175 Kit_DsdNtkFree( ppNtks[0] );
176 Kit_DsdNtkFree( ppNtks[1] );
177//Kit_DsdPrintFromTruth( pDec0, nVars );
178//Kit_DsdPrintFromTruth( pDec1, nVars );
179 // get the decomposed function
180 Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
181
182 // find any true assignments of the decomposed functions
183 TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
184 TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
185 assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
186 // find any false assignments of the decomposed functions
187 FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
188 FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
189 assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
190
191 // cofactor the cofactors according to these minterms
192 Kit_TruthCopy( pCo00, pCof0, nVars );
193 Kit_TruthCopy( pCo01, pCof0, nVars );
194 for ( i = 0; i < nVars; i++ )
195 if ( uSubset0 & (1 << i) )
196 {
197 if ( FalseMint0 & (1 << i) )
198 Kit_TruthCofactor1( pCo00, nVars, i );
199 else
200 Kit_TruthCofactor0( pCo00, nVars, i );
201 if ( TrueMint0 & (1 << i) )
202 Kit_TruthCofactor1( pCo01, nVars, i );
203 else
204 Kit_TruthCofactor0( pCo01, nVars, i );
205 }
206 Kit_TruthCopy( pCo10, pCof1, nVars );
207 Kit_TruthCopy( pCo11, pCof1, nVars );
208 for ( i = 0; i < nVars; i++ )
209 if ( uSubset1 & (1 << i) )
210 {
211 if ( FalseMint1 & (1 << i) )
212 Kit_TruthCofactor1( pCo10, nVars, i );
213 else
214 Kit_TruthCofactor0( pCo10, nVars, i );
215 if ( TrueMint1 & (1 << i) )
216 Kit_TruthCofactor1( pCo11, nVars, i );
217 else
218 Kit_TruthCofactor0( pCo11, nVars, i );
219 }
220
221 // derive the functions by composing them with the new variable (iVarReused)
222 Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
223 Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
224//Kit_DsdPrintFromTruth( pCo0, nVars );
225//Kit_DsdPrintFromTruth( pCo1, nVars );
226
227 // derive the composition function
228 Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
229
230 // process the decomposed function
231 pNtkDec = Kit_DsdDecompose( pDec, nVars );
232 pNtkComp = Kit_DsdDecompose( pCo, nVars );
233//Kit_DsdPrint( stdout, pNtkDec );
234//Kit_DsdPrint( stdout, pNtkComp );
235//printf( "cofactored variable %c\n", 'a' + iVar );
236//printf( "reused variable %c\n", 'a' + iVarReused );
237
238 ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
239 pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
240
241 Kit_DsdNtkFree( pNtkDec );
242 Kit_DsdNtkFree( pNtkComp );
243 return pObjNew;
244}
p
Cube * p
Definition exorList.c:222
If_Obj_t
struct If_Obj_t_ If_Obj_t
Definition if.h:79
Kit_DsdDecompose
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition kitDsd.c:2315
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:368
Kit_TruthMuxVar
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition kitTruth.c:1069
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
Kit_DsdNtkFree
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:164
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:470
Kit_DsdNtk_t
struct Kit_DsdNtk_t_ Kit_DsdNtk_t
Definition kit.h:124
Kit_DsdExpand
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition kitDsd.c:1452
Kit_DsdTruthPartial
void Kit_DsdTruthPartial(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
Definition kitDsd.c:1108
Lpk_MapSuppRedDecSelect
unsigned Lpk_MapSuppRedDecSelect(Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)
Definition lpkSets.c:323
Lpk_MapTree_rec
If_Obj_t * Lpk_MapTree_rec(Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
Definition lpkMap.c:110
Kit_DsdNtk_t_::Root
unsigned short Root
Definition kit.h:130
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapTreeBestCofVar()

ABC_NAMESPACE_IMPL_START int Lpk_MapTreeBestCofVar ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
unsigned * pCof0,
unsigned * pCof1 )

DECLARATIONS ///.

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

FileName [lpkMux.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkMux.c.

46{
47 int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
48 // iterate through variables
49 iBestVar = -1;
50 nSuppSizeMin = KIT_INFINITY;
51 for ( i = 0; i < nVars; i++ )
52 {
53 // cofactor the functiona and get support sizes
54 Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
55 Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
56 nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
57 nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
58 nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
59 // skip cofactoring that goes above the limit
60 if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
61 continue;
62 // compare this variable with other variables
63 if ( nSuppSizeMin > nSuppSizeCur )
64 {
65 nSuppSizeMin = nSuppSizeCur;
66 iBestVar = i;
67 }
68 }
69 // cofactor w.r.t. this variable
70 if ( iBestVar != -1 )
71 {
72 Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
73 Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
74 }
75 return iBestVar;
76}
Kit_TruthSupportSize
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
KIT_INFINITY
#define KIT_INFINITY
Definition kit.h:176
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapTreeMux_rec()

If_Obj_t * Lpk_MapTreeMux_rec ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )

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

Synopsis [Maps the function by the best cofactoring.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file lpkMux.c.

90{
91 unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
92 unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
93 If_Obj_t * pObj0, * pObj1;
94 Kit_DsdNtk_t * ppNtks[2];
95 int iBestVar;
96 assert( nVars > 3 );
97 p->fCalledOnce = 1;
98 // cofactor w.r.t. the best variable
99 iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
100 if ( iBestVar == -1 )
101 return NULL;
102 // decompose the functions
103 ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
104 ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
105 if ( p->pPars->fVeryVerbose )
106 {
107 printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n",
108 'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
109 Kit_DsdPrintExpanded( ppNtks[0] );
110 Kit_DsdPrintExpanded( ppNtks[1] );
111 }
112 // map the DSD structures
113 pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
114 pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
115 Kit_DsdNtkFree( ppNtks[0] );
116 Kit_DsdNtkFree( ppNtks[1] );
117 return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
118}
If_ManCreateMux
If_Obj_t * If_ManCreateMux(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1, If_Obj_t *pCtrl)
Definition ifMan.c:441
Kit_DsdPrintExpanded
void Kit_DsdPrintExpanded(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:472
Lpk_MapTreeBestCofVar
ABC_NAMESPACE_IMPL_START int Lpk_MapTreeBestCofVar(Lpk_Man_t *p, unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
DECLARATIONS ///.
Definition lpkMux.c:45
Here is the call graph for this function:

◆ Lpk_TryDec()

void Lpk_TryDec ( word * pTruth,
int nVars )

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

Synopsis [Evaluates 4-LUT decompositions of larger functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file lpkMux.c.

258{
259 extern word If_Dec6Perform( word t, int fDerive );
260 extern void If_Dec6Verify( word t, word z );
261 //int nWords = Abc_Truth6WordNum( nVars );
262 assert( nVars == 8 );
263 printf( "%d", If_Dec6Perform(pTruth[0], 1) > 0 );
264 printf( "%d", If_Dec6Perform(pTruth[1], 1) > 0 );
265 printf( "%d", If_Dec6Perform(pTruth[2], 1) > 0 );
266 printf( "%d", If_Dec6Perform(pTruth[3], 1) > 0 );
267 printf( "\n" );
268}
If_Dec6Perform
word If_Dec6Perform(word t, int fDerive)
Definition ifDec07.c:409
If_Dec6Verify
void If_Dec6Verify(word t, word z)
Definition ifDec07.c:131
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_TryDecTest()

void Lpk_TryDecTest ( )

Definition at line 269 of file lpkMux.c.

270{
271 word t0 = ABC_CONST(0x4f1ead396f247a04);
272 word t1 = ABC_CONST(0x10bdb210c006eab5);
273 word t2 = ABC_CONST(0x68ab4bfa8acb7a13);
274 word t3 = ABC_CONST(0xb14ede67096c6eed);
275 word Truth[4] = {t0, t1, t2, t3};
276 Lpk_TryDec( Truth, 8 );
277
278}
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
Lpk_TryDec
void Lpk_TryDec(word *pTruth, int nVars)
Definition lpkMux.c:257
Here is the call graph for this function: