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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START If_Obj_tLpk_MapPrimeInternal (If_Man_t *pIfMan, Kit_Graph_t *pGraph)
 DECLARATIONS ///.
 
If_Obj_tLpk_MapPrime (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
If_Obj_tLpk_MapTree_rec (Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
 

Function Documentation

◆ Lpk_MapPrime()

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

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

Synopsis [Strashes one logic node using its SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file lpkMap.c.

80{
81 Kit_Graph_t * pGraph;
82 Kit_Node_t * pNode;
83 If_Obj_t * pRes;
84 int i;
85 // derive the factored form
86 pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
87 if ( pGraph == NULL )
88 return NULL;
89 // collect the fanins
90 Kit_GraphForEachLeaf( pGraph, pNode, i )
91 pNode->pFunc = ppLeaves[i];
92 // perform strashing
93 pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
94 pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
95 Kit_GraphFree( pGraph );
96 return pRes;
97}
Cube * p
Definition exorList.c:222
struct If_Obj_t_ If_Obj_t
Definition if.h:79
struct Kit_Graph_t_ Kit_Graph_t
Definition kit.h:88
struct Kit_Node_t_ Kit_Node_t
Definition kit.h:69
void Kit_GraphFree(Kit_Graph_t *pGraph)
Definition kitGraph.c:132
#define Kit_GraphForEachLeaf(pGraph, pLeaf, i)
Definition kit.h:505
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition kitGraph.c:356
ABC_NAMESPACE_IMPL_START If_Obj_t * Lpk_MapPrimeInternal(If_Man_t *pIfMan, Kit_Graph_t *pGraph)
DECLARATIONS ///.
Definition lpkMap.c:45
void * pFunc
Definition kit.h:76
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapPrimeInternal()

ABC_NAMESPACE_IMPL_START If_Obj_t * Lpk_MapPrimeInternal ( If_Man_t * pIfMan,
Kit_Graph_t * pGraph )

DECLARATIONS ///.

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

FileName [lpkMap.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
lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Transforms the decomposition graph into the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkMap.c.

46{
47 Kit_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
48 If_Obj_t * pAnd0, * pAnd1;
49 int i;
50 // check for constant function
51 if ( Kit_GraphIsConst(pGraph) )
52 return If_ManConst1(pIfMan);
53 // check for a literal
54 if ( Kit_GraphIsVar(pGraph) )
55 return (If_Obj_t *)Kit_GraphVar(pGraph)->pFunc;
56 // build the AIG nodes corresponding to the AND gates of the graph
57 Kit_GraphForEachNode( pGraph, pNode, i )
58 {
59 pAnd0 = (If_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
60 pAnd1 = (If_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
61 pNode->pFunc = If_ManCreateAnd( pIfMan,
62 If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ),
63 If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
64 }
65 return (If_Obj_t *)pNode->pFunc;
66}
If_Obj_t * If_ManCreateAnd(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1)
Definition ifMan.c:384
#define Kit_GraphForEachNode(pGraph, pAnd, i)
Definition kit.h:507
unsigned fCompl
Definition kit.h:65
unsigned Node
Definition kit.h:66
Kit_Edge_t eEdge0
Definition kit.h:72
Kit_Edge_t eEdge1
Definition kit.h:73
Here is the call graph for this function:
Here is the caller graph for this function:

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

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file lpkMap.c.

111{
112 Kit_DsdObj_t * pObj;
113 If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
114 unsigned i, iLitFanin;
115
116 assert( iLit >= 0 );
117
118 // consider the case of a gate
119 pObj = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iLit) );
120 if ( pObj == NULL )
121 {
122 pObjNew = ppLeaves[Abc_Lit2Var(iLit)];
123 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
124 }
125 if ( pObj->Type == KIT_DSD_CONST1 )
126 {
127 return If_NotCond( If_ManConst1(p->pIfMan), Abc_LitIsCompl(iLit) );
128 }
129 if ( pObj->Type == KIT_DSD_VAR )
130 {
131 pObjNew = ppLeaves[Abc_Lit2Var(pObj->pFans[0])];
132 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(pObj->pFans[0]) );
133 }
134 if ( pObj->Type == KIT_DSD_AND )
135 {
136 assert( pObj->nFans == 2 );
137 pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
138 pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
139 if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
140 return NULL;
141 pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] );
142 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
143 }
144 if ( pObj->Type == KIT_DSD_XOR )
145 {
146 int fCompl = Abc_LitIsCompl(iLit);
147 assert( pObj->nFans == 2 );
148 pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
149 pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
150 if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
151 return NULL;
152 fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
153 pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
154 return If_NotCond( pObjNew, fCompl );
155 }
156 assert( pObj->Type == KIT_DSD_PRIME );
157 p->nBlocks[pObj->nFans]++;
158
159 // solve for the inputs
160 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
161 {
162 if ( i == 0 )
163 pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
164 else
165 pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
166 if ( pFansNew[i] == NULL )
167 return NULL;
168 }
169/*
170 if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
171 {
172 pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
173 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
174 }
175*/
176/*
177 if ( (int)pObj->nFans > p->pPars->nLutSize )
178 {
179 pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
180// if ( pObjNew2 )
181// return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
182 }
183*/
184
185 // find best cofactoring variable
186 if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
187 {
188 pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
189 if ( pObjNew2 )
190 return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
191 }
192
193 pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
194
195 // add choice
196 if ( pObjNew && pObjNew2 )
197 {
198 If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
199 If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
200 }
201 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
202}
void If_ManCreateChoice(If_Man_t *p, If_Obj_t *pRepr)
Definition ifMan.c:460
If_Obj_t * If_ManCreateXor(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1)
Definition ifMan.c:422
@ KIT_DSD_XOR
Definition kit.h:106
@ KIT_DSD_CONST1
Definition kit.h:103
@ KIT_DSD_PRIME
Definition kit.h:107
@ KIT_DSD_AND
Definition kit.h:105
@ KIT_DSD_VAR
Definition kit.h:104
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition kit.h:160
If_Obj_t * Lpk_MapSuppRedDec_rec(Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
Definition lpkMux.c:133
If_Obj_t * Lpk_MapPrime(Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
Definition lpkMap.c:79
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
unsigned Type
Definition kit.h:115
unsigned nFans
Definition kit.h:119
unsigned short pFans[0]
Definition kit.h:120
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function: