ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cutExpand.c
Go to the documentation of this file.
1
20
21#include "cutInt.h"
22
24
25
29
30#define CUT_CELL_MVAR 9
31
35
47static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
48{
49 unsigned uPhase = 0;
50 int i, k;
51 for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
52 {
53 if ( k == (int)pCut1->nLeaves )
54 break;
55 if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
56 continue;
57 assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
58 uPhase |= (1 << i);
59 k++;
60 }
61 return uPhase;
62}
63
81void Cut_TruthCompose( Cut_Cut_t * pCutF, int Node, Cut_Cut_t * pCutT, Cut_Cut_t * pCutRes )
82{
83 static unsigned uCof0[1<<(CUT_CELL_MVAR-5)];
84 static unsigned uCof1[1<<(CUT_CELL_MVAR-5)];
85 static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
86 unsigned * pIn, * pOut, * pTemp;
87 unsigned uPhase;
88 int NodeIndex, i, k;
89
90 // sanity checks
91 assert( pCutF->nVarsMax == pCutT->nVarsMax );
92 assert( pCutF->nVarsMax == pCutRes->nVarsMax );
93 assert( pCutF->nVarsMax <= CUT_CELL_MVAR );
94 // the factor cut (pCutF) should have its nodes sorted in the ascending order
95 assert( pCutF->nLeaves <= pCutF->nVarsMax );
96 for ( i = 0; i < (int)pCutF->nLeaves - 1; i++ )
97 assert( pCutF->pLeaves[i] < pCutF->pLeaves[i+1] );
98 // the tree cut (pCutT) should have its nodes sorted in the ascending order
99 assert( pCutT->nLeaves <= pCutT->nVarsMax );
100 for ( i = 0; i < (int)pCutT->nLeaves - 1; i++ )
101 assert( pCutT->pLeaves[i] < pCutT->pLeaves[i+1] );
102 // the resulting cut (pCutRes) should have its nodes sorted in the ascending order
103 assert( pCutRes->nLeaves <= pCutRes->nVarsMax );
104 for ( i = 0; i < (int)pCutRes->nLeaves - 1; i++ )
105 assert( pCutRes->pLeaves[i] < pCutRes->pLeaves[i+1] );
106 // make sure that every node in pCutF (except Node) appears in pCutRes
107 for ( i = 0; i < (int)pCutF->nLeaves; i++ )
108 {
109 if ( pCutF->pLeaves[i] == Node )
110 continue;
111 for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
112 if ( pCutF->pLeaves[i] == pCutRes->pLeaves[k] )
113 break;
114 assert( k < (int)pCutRes->nLeaves ); // node i from pCutF is not found in pCutRes!!!
115 }
116 // make sure that every node in pCutT appears in pCutRes
117 for ( i = 0; i < (int)pCutT->nLeaves; i++ )
118 {
119 for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
120 if ( pCutT->pLeaves[i] == pCutRes->pLeaves[k] )
121 break;
122 assert( k < (int)pCutRes->nLeaves ); // node i from pCutT is not found in pCutRes!!!
123 }
124
125
126 // find the index of the given node in the factor cut
127 NodeIndex = -1;
128 for ( NodeIndex = 0; NodeIndex < (int)pCutF->nLeaves; NodeIndex++ )
129 if ( pCutF->pLeaves[NodeIndex] == Node )
130 break;
131 assert( NodeIndex >= 0 ); // Node should be in pCutF
132
133 // copy the truth table
134 Extra_TruthCopy( uTemp, Cut_CutReadTruth(pCutF), pCutF->nLeaves );
135
136 // bubble-move the NodeIndex variable to be the last one (the most significant one)
137 pIn = uTemp; pOut = uCof0; // uCof0 is used for temporary storage here
138 for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
139 {
140 Extra_TruthSwapAdjacentVars( pOut, pIn, pCutF->nLeaves, i );
141 pTemp = pIn; pIn = pOut; pOut = pTemp;
142 }
143 if ( (pCutF->nLeaves - 1 - NodeIndex) & 1 )
144 Extra_TruthCopy( pOut, pIn, pCutF->nLeaves );
145 // the result of stretching is in uTemp
146
147 // cofactor the factor cut with respect to the node
148 Extra_TruthCopy( uCof0, uTemp, pCutF->nLeaves );
149 Extra_TruthCofactor0( uCof0, pCutF->nLeaves, pCutF->nLeaves-1 );
150 Extra_TruthCopy( uCof1, uTemp, pCutF->nLeaves );
151 Extra_TruthCofactor1( uCof1, pCutF->nLeaves, pCutF->nLeaves-1 );
152
153 // temporarily shrink the factor cut's variables by removing Node
154 for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
155 pCutF->pLeaves[i] = pCutF->pLeaves[i+1];
156 pCutF->nLeaves--;
157
158 // spread out the cofactors' truth tables to the same var order as the resulting cut
159 uPhase = Cut_TruthPhase(pCutRes, pCutF);
160 assert( Extra_WordCountOnes(uPhase) == (int)pCutF->nLeaves );
161 Extra_TruthStretch( uTemp, uCof0, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
162 Extra_TruthCopy( uCof0, uTemp, pCutF->nVarsMax );
163 Extra_TruthStretch( uTemp, uCof1, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
164 Extra_TruthCopy( uCof1, uTemp, pCutF->nVarsMax );
165
166 // spread out the tree cut's truth table to the same var order as the resulting cut
167 uPhase = Cut_TruthPhase(pCutRes, pCutT);
168 assert( Extra_WordCountOnes(uPhase) == (int)pCutT->nLeaves );
169 Extra_TruthStretch( uTemp, Cut_CutReadTruth(pCutT), pCutT->nLeaves, pCutT->nVarsMax, uPhase );
170
171 // create the resulting truth table
172 pTemp = Cut_CutReadTruth(pCutRes);
173 for ( i = Extra_TruthWordNum(pCutRes->nLeaves)-1; i >= 0; i-- )
174 pTemp[i] = (uCof0[i] & ~uTemp[i]) | (uCof1[i] & uTemp[i]);
175
176 // undo the removal of the node from the cut
177 for ( i = (int)pCutF->nLeaves - 1; i >= NodeIndex; --i )
178 pCutF->pLeaves[i+1] = pCutF->pLeaves[i];
179 pCutF->pLeaves[NodeIndex] = Node;
180 pCutF->nLeaves++;
181}
182
186
187
189
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void Cut_TruthCompose(Cut_Cut_t *pCutF, int Node, Cut_Cut_t *pCutT, Cut_Cut_t *pCutRes)
Definition cutExpand.c:81
#define CUT_CELL_MVAR
DECLARATIONS ///.
Definition cutExpand.c:30
struct Cut_CutStruct_t_ Cut_Cut_t
Definition cut.h:50
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int Start)
void Extra_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
unsigned nVarsMax
Definition cut.h:83
int pLeaves[0]
Definition cut.h:89
unsigned nLeaves
Definition cut.h:84
#define assert(ex)
Definition util_old.h:213