1 | /**CFile*********************************************************************** |
---|
2 | |
---|
3 | FileName [ tblAigUtil.c ] |
---|
4 | |
---|
5 | PackageName [ tbl ] |
---|
6 | |
---|
7 | Synopsis [] |
---|
8 | |
---|
9 | Description [] |
---|
10 | |
---|
11 | SeeAlso [ tbl.h, tblEntryUtil.c, tblAigEntryUtil, tblUtil.c ] |
---|
12 | |
---|
13 | Author [Mohammad Awedh ] |
---|
14 | |
---|
15 | Copyright [] |
---|
16 | |
---|
17 | ******************************************************************************/ |
---|
18 | #include "tblInt.h" |
---|
19 | #include "baig.h" |
---|
20 | |
---|
21 | static char rcsid[] UNUSED = "$Id: tblAigUtil.c,v 1.3 2005/04/17 14:37:23 awedh Exp $"; |
---|
22 | |
---|
23 | /**AutomaticStart*************************************************************/ |
---|
24 | |
---|
25 | /*---------------------------------------------------------------------------*/ |
---|
26 | /* Static function prototypes */ |
---|
27 | /*---------------------------------------------------------------------------*/ |
---|
28 | |
---|
29 | |
---|
30 | /**AutomaticEnd***************************************************************/ |
---|
31 | |
---|
32 | |
---|
33 | /*---------------------------------------------------------------------------*/ |
---|
34 | /* Definition of exported functions */ |
---|
35 | /*---------------------------------------------------------------------------*/ |
---|
36 | |
---|
37 | /**Function******************************************************************** |
---|
38 | |
---|
39 | Synopsis [Compute the Mvf_Function_t for a non-deterministic constant.] |
---|
40 | |
---|
41 | Description [Given a Tbl_Table_t, an integer for the table output value |
---|
42 | index, an integer MAigId, and an mAig Manager, this function builds the |
---|
43 | MvfAig_Function_t associated with the output. The table cannot have |
---|
44 | any inputs; the function fails if it does. The output cannot be equal to |
---|
45 | another output, because this would make the table a relation, and that is |
---|
46 | not permissible. If this occurs, the function will fail on an assert |
---|
47 | statement.] |
---|
48 | |
---|
49 | SideEffects [ Table must have no inputs.] |
---|
50 | |
---|
51 | SeeAlso [] |
---|
52 | [Done] |
---|
53 | ******************************************************************************/ |
---|
54 | MvfAig_Function_t * |
---|
55 | Tbl_TableBuildNonDetConstantMvfAig( |
---|
56 | Tbl_Table_t *table, |
---|
57 | int outIndex, |
---|
58 | int mAigId, |
---|
59 | mAig_Manager_t *manager) |
---|
60 | { |
---|
61 | |
---|
62 | lsGen gen; |
---|
63 | Tbl_Entry_t *entry; |
---|
64 | Tbl_Range_t *range; |
---|
65 | int value, rowNum, colNum; |
---|
66 | mAigEdge_t x; |
---|
67 | MvfAig_Function_t *function; |
---|
68 | |
---|
69 | assert(Tbl_TableReadNumInputs(table) ==0); |
---|
70 | |
---|
71 | value = Var_VariableReadNumValues(Tbl_TableReadIndexVar(table, outIndex, 1)); |
---|
72 | function = MvfAig_FunctionAlloc(value); |
---|
73 | Tbl_TableForEachOutputEntry(table,rowNum,colNum,entry) { |
---|
74 | if (colNum == outIndex) { |
---|
75 | assert(entry->type == Tbl_EntryNormal_c); |
---|
76 | Tbl_EntryForEachValue(entry,value,gen,range) { |
---|
77 | x = mAig_EquC(manager, mAigId, value); |
---|
78 | MvfAig_FunctionAddMintermsToComponent(manager, function, value, x); |
---|
79 | } |
---|
80 | } |
---|
81 | } |
---|
82 | return function; |
---|
83 | } |
---|
84 | |
---|
85 | |
---|
86 | /**Function******************************************************************** |
---|
87 | |
---|
88 | Synopsis [Compute the Mvf_Function_t for a table output in terms of fanins] |
---|
89 | |
---|
90 | Description [Given a Tbl_Table_t, an integer for the table output value |
---|
91 | index, an array of fanin mAigEdge_t* , and an mAigManager, this function builds the |
---|
92 | MvfAig_Function_t associated with the output. The output cannot be equal to |
---|
93 | another output, because this would make the table a relation, and that is |
---|
94 | not permissible. For each row, the function will build the mAigEdge_t for the inputs |
---|
95 | using their MvfAig_Function_t's and AND them together. If the input is of the |
---|
96 | type equal, it will build the equivalent set mAig (see See Also) and AND it in. |
---|
97 | If the input of the type Tbl_EntryUniverse_c, this input will be set tomAig_One.] |
---|
98 | |
---|
99 | SideEffects [ ] |
---|
100 | |
---|
101 | SeeAlso [ MvfAig_FunctionComputeEquivalentSet, TblEntryNormalConstructAig] |
---|
102 | [Done] |
---|
103 | ******************************************************************************/ |
---|
104 | MvfAig_Function_t * |
---|
105 | Tbl_TableBuildMvfAigFromFanins( |
---|
106 | Tbl_Table_t * table, |
---|
107 | int outIndex, |
---|
108 | array_t * faninArray, |
---|
109 | mAig_Manager_t *manager) |
---|
110 | { |
---|
111 | |
---|
112 | lsGen gen; |
---|
113 | Tbl_Entry_t *entry, *equalEntry, *inputEntry; |
---|
114 | Tbl_Range_t *range; |
---|
115 | int value, rowNum, colNum, rowColNum, i; |
---|
116 | mAigEdge_t x, result, temp; |
---|
117 | MvfAig_Function_t *function, *mvf1, *mvf2; |
---|
118 | |
---|
119 | |
---|
120 | x = mAig_NULL; |
---|
121 | value = Var_VariableReadNumValues(Tbl_TableReadIndexVar(table,outIndex,1)); |
---|
122 | function = MvfAig_FunctionAlloc(value); |
---|
123 | |
---|
124 | Tbl_TableForEachOutputEntry(table,rowNum,colNum,entry) { |
---|
125 | if (colNum == outIndex) { |
---|
126 | if (entry->type == Tbl_EntryNormal_c) { |
---|
127 | result = mAig_One; |
---|
128 | Tbl_RowForEachInputEntry(table,rowNum,inputEntry,rowColNum) { |
---|
129 | if (inputEntry->type == Tbl_EntryNormal_c) { |
---|
130 | mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum); |
---|
131 | x = TblEntryNormalConstructAig(manager, inputEntry, mvf1); |
---|
132 | } |
---|
133 | else if (inputEntry->type == Tbl_EntryUniverse_c) { |
---|
134 | x = mAig_One; |
---|
135 | } |
---|
136 | else if (inputEntry->type == Tbl_EntryEqual_c) { |
---|
137 | value =Tbl_EntryReadVarIndex(inputEntry); |
---|
138 | mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum); |
---|
139 | mvf2 = array_fetch(MvfAig_Function_t*,faninArray,value); |
---|
140 | x = MvfAig_FunctionsComputeEquivalentSet(manager, mvf1,mvf2); |
---|
141 | } |
---|
142 | temp = result; |
---|
143 | result = mAig_And(manager, x,temp); |
---|
144 | } |
---|
145 | /* add the result to each value of the output */ |
---|
146 | Tbl_EntryForEachValue(entry,value,gen,range) { |
---|
147 | MvfAig_FunctionAddMintermsToComponent(manager, function, value,result); |
---|
148 | } |
---|
149 | |
---|
150 | } /* output is not Normal */ |
---|
151 | else if (entry->type == Tbl_EntryEqual_c) { |
---|
152 | value = Tbl_EntryReadVarIndex(entry); |
---|
153 | if (value == -1) { |
---|
154 | fail("Failure: Not equal to any input var in this table\n"); |
---|
155 | } |
---|
156 | |
---|
157 | /* must be equal to an input */ |
---|
158 | |
---|
159 | equalEntry = Tbl_TableReadEntry(table,rowNum,value,0); |
---|
160 | result = mAig_One; |
---|
161 | Tbl_RowForEachInputEntry(table,rowNum,inputEntry,rowColNum) { |
---|
162 | if (inputEntry->type == Tbl_EntryNormal_c) { |
---|
163 | /* Don't include this input if the output is set be equal to it |
---|
164 | */ |
---|
165 | if ( inputEntry == equalEntry){ |
---|
166 | continue; |
---|
167 | } |
---|
168 | mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum); |
---|
169 | x = TblEntryNormalConstructAig(manager, inputEntry, mvf1); |
---|
170 | } |
---|
171 | else if (inputEntry->type == Tbl_EntryUniverse_c) { |
---|
172 | x = mAig_One; |
---|
173 | } |
---|
174 | else if (inputEntry->type == Tbl_EntryEqual_c) { |
---|
175 | value =Tbl_EntryReadVarIndex(inputEntry); |
---|
176 | mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum); |
---|
177 | mvf2 = array_fetch(MvfAig_Function_t*,faninArray,value); |
---|
178 | x = MvfAig_FunctionsComputeEquivalentSet(manager, mvf1,mvf2); |
---|
179 | } |
---|
180 | temp = result; |
---|
181 | result = mAig_And(manager, x, temp); |
---|
182 | } |
---|
183 | |
---|
184 | temp = result; |
---|
185 | rowColNum = Tbl_EntryReadVarIndex(entry); |
---|
186 | mvf1 = array_fetch(MvfAig_Function_t*, faninArray, rowColNum); |
---|
187 | |
---|
188 | if (equalEntry->type == Tbl_EntryNormal_c) { |
---|
189 | /* add the result to each value of the equal input */ |
---|
190 | Tbl_EntryForEachValue(equalEntry, value, gen, range) { |
---|
191 | x = MvfAig_FunctionReadComponent(mvf1, value); |
---|
192 | result = mAig_And(manager, temp, x); |
---|
193 | MvfAig_FunctionAddMintermsToComponent(manager, function, value, result); |
---|
194 | } |
---|
195 | }else { /* Add Minterms for all vlaues */ |
---|
196 | value = Var_VariableReadNumValues(Tbl_EntryReadActualVar(table, equalEntry)); |
---|
197 | for(i=0; i< value; i++) { |
---|
198 | x = MvfAig_FunctionReadComponent(mvf1,i); |
---|
199 | result = mAig_And(manager, temp, x); |
---|
200 | MvfAig_FunctionAddMintermsToComponent(manager, function, i,result); |
---|
201 | } |
---|
202 | } |
---|
203 | } |
---|
204 | } |
---|
205 | } |
---|
206 | |
---|
207 | /* accounting for the defaults */ |
---|
208 | entry = Tbl_TableDefaultReadEntry(table,outIndex); |
---|
209 | if (entry != NIL(Tbl_Entry_t)) { |
---|
210 | temp = MvfAig_FunctionComputeDomain(manager, function); |
---|
211 | result = mAig_Not(temp); |
---|
212 | |
---|
213 | if (entry->type == Tbl_EntryNormal_c) { |
---|
214 | Tbl_EntryForEachValue(entry,value,gen,range) { |
---|
215 | MvfAig_FunctionAddMintermsToComponent(manager, function, value, result); |
---|
216 | } |
---|
217 | } |
---|
218 | else { |
---|
219 | value = Tbl_EntryReadVarIndex(entry); |
---|
220 | if (value == -1) { |
---|
221 | fail("Failure: Not equal to any input var in this table\n"); |
---|
222 | } |
---|
223 | mvf1 = array_fetch(MvfAig_Function_t*, faninArray, value); |
---|
224 | |
---|
225 | MvfAig_FunctionForEachComponent(mvf1, i, x) { |
---|
226 | temp = mAig_And(manager, x, result); |
---|
227 | MvfAig_FunctionAddMintermsToComponent(manager, function, i ,temp); |
---|
228 | } |
---|
229 | } |
---|
230 | |
---|
231 | } |
---|
232 | |
---|
233 | return function; |
---|
234 | } |
---|
235 | |
---|
236 | |
---|
237 | |
---|
238 | |
---|
239 | |
---|
240 | |
---|
241 | |
---|
242 | |
---|
243 | |
---|
244 | |
---|
245 | |
---|