1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
|
/**CFile****************************************************************
FileName [cutExpand.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Computes the truth table of the cut after expansion.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutExpand.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define CUT_CELL_MVAR 9
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
{
unsigned uPhase = 0;
int i, k;
for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
{
if ( k == (int)pCut1->nLeaves )
break;
if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
continue;
assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
uPhase |= (1 << i);
k++;
}
return uPhase;
}
/**Function*************************************************************
Synopsis [Computes the truth table of the composition of cuts.]
Description [Inputs are:
- a factor cut (truth table is stored inside)
- a node in the factor cut
- a tree cut to be substituted (truth table is stored inside)
- the resulting cut (truth table will be filled in).
Note that all cuts, including the resulting one, should be already
computed and the nodes should be stored in the ascending order.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthCompose( Cut_Cut_t * pCutF, int Node, Cut_Cut_t * pCutT, Cut_Cut_t * pCutRes )
{
static unsigned uCof0[1<<(CUT_CELL_MVAR-5)];
static unsigned uCof1[1<<(CUT_CELL_MVAR-5)];
static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
unsigned * pIn, * pOut, * pTemp;
unsigned uPhase;
int NodeIndex, i, k;
// sanity checks
assert( pCutF->nVarsMax == pCutT->nVarsMax );
assert( pCutF->nVarsMax == pCutRes->nVarsMax );
assert( pCutF->nVarsMax <= CUT_CELL_MVAR );
// the factor cut (pCutF) should have its nodes sorted in the ascending order
assert( pCutF->nLeaves <= pCutF->nVarsMax );
for ( i = 0; i < (int)pCutF->nLeaves - 1; i++ )
assert( pCutF->pLeaves[i] < pCutF->pLeaves[i+1] );
// the tree cut (pCutT) should have its nodes sorted in the ascending order
assert( pCutT->nLeaves <= pCutT->nVarsMax );
for ( i = 0; i < (int)pCutT->nLeaves - 1; i++ )
assert( pCutT->pLeaves[i] < pCutT->pLeaves[i+1] );
// the resulting cut (pCutRes) should have its nodes sorted in the ascending order
assert( pCutRes->nLeaves <= pCutRes->nVarsMax );
for ( i = 0; i < (int)pCutRes->nLeaves - 1; i++ )
assert( pCutRes->pLeaves[i] < pCutRes->pLeaves[i+1] );
// make sure that every node in pCutF (except Node) appears in pCutRes
for ( i = 0; i < (int)pCutF->nLeaves; i++ )
{
if ( pCutF->pLeaves[i] == Node )
continue;
for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
if ( pCutF->pLeaves[i] == pCutRes->pLeaves[k] )
break;
assert( k < (int)pCutRes->nLeaves ); // node i from pCutF is not found in pCutRes!!!
}
// make sure that every node in pCutT appears in pCutRes
for ( i = 0; i < (int)pCutT->nLeaves; i++ )
{
for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
if ( pCutT->pLeaves[i] == pCutRes->pLeaves[k] )
break;
assert( k < (int)pCutRes->nLeaves ); // node i from pCutT is not found in pCutRes!!!
}
// find the index of the given node in the factor cut
NodeIndex = -1;
for ( NodeIndex = 0; NodeIndex < (int)pCutF->nLeaves; NodeIndex++ )
if ( pCutF->pLeaves[NodeIndex] == Node )
break;
assert( NodeIndex >= 0 ); // Node should be in pCutF
// copy the truth table
Extra_TruthCopy( uTemp, Cut_CutReadTruth(pCutF), pCutF->nLeaves );
// bubble-move the NodeIndex variable to be the last one (the most significant one)
pIn = uTemp; pOut = uCof0; // uCof0 is used for temporary storage here
for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
{
Extra_TruthSwapAdjacentVars( pOut, pIn, pCutF->nLeaves, i );
pTemp = pIn; pIn = pOut; pOut = pTemp;
}
if ( (pCutF->nLeaves - 1 - NodeIndex) & 1 )
Extra_TruthCopy( pOut, pIn, pCutF->nLeaves );
// the result of stretching is in uTemp
// cofactor the factor cut with respect to the node
Extra_TruthCopy( uCof0, uTemp, pCutF->nLeaves );
Extra_TruthCofactor0( uCof0, pCutF->nLeaves, pCutF->nLeaves-1 );
Extra_TruthCopy( uCof1, uTemp, pCutF->nLeaves );
Extra_TruthCofactor1( uCof1, pCutF->nLeaves, pCutF->nLeaves-1 );
// temporarily shrink the factor cut's variables by removing Node
for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
pCutF->pLeaves[i] = pCutF->pLeaves[i+1];
pCutF->nLeaves--;
// spread out the cofactors' truth tables to the same var order as the resulting cut
uPhase = Cut_TruthPhase(pCutRes, pCutF);
assert( Extra_WordCountOnes(uPhase) == (int)pCutF->nLeaves );
Extra_TruthStretch( uTemp, uCof0, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
Extra_TruthCopy( uCof0, uTemp, pCutF->nVarsMax );
Extra_TruthStretch( uTemp, uCof1, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
Extra_TruthCopy( uCof1, uTemp, pCutF->nVarsMax );
// spread out the tree cut's truth table to the same var order as the resulting cut
uPhase = Cut_TruthPhase(pCutRes, pCutT);
assert( Extra_WordCountOnes(uPhase) == (int)pCutT->nLeaves );
Extra_TruthStretch( uTemp, Cut_CutReadTruth(pCutT), pCutT->nLeaves, pCutT->nVarsMax, uPhase );
// create the resulting truth table
pTemp = Cut_CutReadTruth(pCutRes);
for ( i = Extra_TruthWordNum(pCutRes->nLeaves)-1; i >= 0; i-- )
pTemp[i] = (uCof0[i] & ~uTemp[i]) | (uCof1[i] & uTemp[i]);
// undo the removal of the node from the cut
for ( i = (int)pCutF->nLeaves - 1; i >= NodeIndex; --i )
pCutF->pLeaves[i+1] = pCutF->pLeaves[i];
pCutF->pLeaves[NodeIndex] = Node;
pCutF->nLeaves++;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
