1 | #include "debugInt.h" |
---|
2 | /**Function******************************************************************** |
---|
3 | |
---|
4 | Synopsis [create New node] |
---|
5 | |
---|
6 | Description [Create new primary input in the current network at a given |
---|
7 | output node. Return the variable created] |
---|
8 | |
---|
9 | SideEffects [Modify the network] |
---|
10 | |
---|
11 | SeeAlso [] |
---|
12 | |
---|
13 | ******************************************************************************/ |
---|
14 | Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t* |
---|
15 | node, char * varName ) |
---|
16 | { |
---|
17 | array_t * fanin = array_dup(Ntk_NodeReadFanins(node)); |
---|
18 | array_t * fanout = array_alloc(Ntk_Node_t*,0); |
---|
19 | char * nodeName = util_strsav(Ntk_NodeReadName(node)); |
---|
20 | //Create var Name |
---|
21 | char * newVarName = (char *) malloc(strlen(nodeName) + strlen(varName) +1); |
---|
22 | sprintf(newVarName,"%s_%s",nodeName,varName); |
---|
23 | Var_Variable_t * var = Var_VariableAlloc(NIL(Hrc_Node_t),newVarName); |
---|
24 | //Create new Node |
---|
25 | Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, newVarName,var); |
---|
26 | Ntk_NodeDeclareAsPrimaryInput(newNode); |
---|
27 | //Add in the fanin of the node |
---|
28 | array_insert_last(Ntk_Node_t*,fanin,newNode); |
---|
29 | Ntk_NodeSetFanins(node,fanin); |
---|
30 | //Add Fanout to the newNode |
---|
31 | array_insert_last(Ntk_Node_t*,fanout,node); |
---|
32 | Ntk_NodeSetFanouts(newNode,fanout); |
---|
33 | free(newVarName); |
---|
34 | |
---|
35 | return newNode; |
---|
36 | |
---|
37 | } |
---|
38 | /**Function******************************************************************** |
---|
39 | |
---|
40 | Synopsis [Add abnormal predicates to the network] |
---|
41 | |
---|
42 | Description [Given a network after flatten the hierarchy, |
---|
43 | change the table of each combinatorial node |
---|
44 | with a new table including the abnormal predicate. |
---|
45 | For a combinatorial node n is tranformed into (abn_n)?i_n:n |
---|
46 | If the abnormal predicate is activ then n is replaced by a free input] |
---|
47 | |
---|
48 | SideEffects [fill the abnormal structure] |
---|
49 | |
---|
50 | SeeAlso [] |
---|
51 | |
---|
52 | ******************************************************************************/ |
---|
53 | |
---|
54 | void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/ |
---|
55 | { |
---|
56 | |
---|
57 | Ntk_Network_t * ntk = abnormal->network; |
---|
58 | lsGen gen; |
---|
59 | Ntk_Node_t* node; |
---|
60 | Ntk_NetworkForEachNode(ntk,gen,node){ |
---|
61 | //For each combinatorial node |
---|
62 | if(Ntk_NodeTestIsCombinational(node)){ |
---|
63 | if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0) |
---|
64 | { |
---|
65 | char * nodeName = util_strsav(Ntk_NodeReadName(node)); |
---|
66 | printf("%s \n", nodeName); |
---|
67 | |
---|
68 | Tbl_Table_t *table = Ntk_NodeReadTable(node); |
---|
69 | (void) fprintf(vis_stdout, "** old table\n"); |
---|
70 | Tbl_TableWriteBlifMvToFile(table,2,vis_stdout); |
---|
71 | // Build new variables abnormal and input |
---|
72 | Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn"); |
---|
73 | Ntk_Node_t * iNode = Dbg_CreateNewNode(ntk,node,"i"); |
---|
74 | Dbg_AddFreeInput(abnormal,iNode); |
---|
75 | Dbg_AddAbnormalPredicate(abnormal,abnNode); |
---|
76 | Var_Variable_t * abn = Ntk_NodeReadVariable(abnNode); |
---|
77 | Var_Variable_t * i = Ntk_NodeReadVariable(iNode); |
---|
78 | //Add in the table |
---|
79 | Tbl_TableAddColumn(table,abn,0); |
---|
80 | int abnIndex = Tbl_TableReadVarIndex(table, abn, 0); |
---|
81 | Tbl_TableAddColumn(table,i,0); |
---|
82 | int iIndex = Tbl_TableReadVarIndex(table, i, 0); |
---|
83 | |
---|
84 | //For each row already there in the table |
---|
85 | int rowNum; |
---|
86 | for(rowNum = 0; rowNum < Tbl_TableReadNumRows(table);rowNum++){ |
---|
87 | Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
88 | Tbl_EntrySetValue(abnEntry,0,0); |
---|
89 | Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0); |
---|
90 | Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
91 | Tbl_EntrySetValue(iEntry,0,1); |
---|
92 | Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0); |
---|
93 | } |
---|
94 | //the new row |
---|
95 | int r = Tbl_TableAddRow(table); |
---|
96 | |
---|
97 | int colNum; |
---|
98 | for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) { |
---|
99 | Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
100 | if(colNum == abnIndex || colNum == iIndex) |
---|
101 | Tbl_EntrySetValue(entry,1,1); |
---|
102 | else |
---|
103 | Tbl_EntrySetValue(entry,0,1); |
---|
104 | Tbl_TableSetEntry(table, entry, r, colNum, 0); |
---|
105 | } |
---|
106 | for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){ |
---|
107 | Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
108 | Tbl_EntrySetValue(entry,1,1); |
---|
109 | Tbl_TableSetEntry(table, entry, r, colNum, 1); |
---|
110 | } |
---|
111 | printf("---------------\n"); |
---|
112 | Tbl_TableWriteBlifMvToFile(table,0,vis_stdout); |
---|
113 | } |
---|
114 | } |
---|
115 | } |
---|
116 | Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY, |
---|
117 | (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback, |
---|
118 | (void *) abnormal); |
---|
119 | } |
---|
120 | /**Function******************************************************************** |
---|
121 | |
---|
122 | Synopsis [Allocate a new abnormal structure] |
---|
123 | |
---|
124 | Description [The structure contains the network with abnormal predicate, |
---|
125 | and two sets of Ntk_Node_t for the abnormal and the free inputs] |
---|
126 | |
---|
127 | SideEffects [Allocate the abnormal structure] |
---|
128 | |
---|
129 | SeeAlso [] |
---|
130 | |
---|
131 | ******************************************************************************/ |
---|
132 | |
---|
133 | Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network) |
---|
134 | { |
---|
135 | Dbg_Abnormal_t * abn = ALLOC(Dbg_Abnormal_t, 1); |
---|
136 | |
---|
137 | abn->network = network; |
---|
138 | abn->abnormal = array_alloc(Ntk_Node_t*,0); |
---|
139 | abn->freeInputs = array_alloc(Ntk_Node_t*,0); |
---|
140 | abn->abnAigArray = NIL(array_t); |
---|
141 | abn->abnCnfIndexArray = NIL(array_t); |
---|
142 | abn->verbose = 0; |
---|
143 | return abn; |
---|
144 | } |
---|
145 | |
---|
146 | /**Function******************************************************************** |
---|
147 | |
---|
148 | Synopsis [Deallocate a new abnormal structure] |
---|
149 | |
---|
150 | Description [Free the arrays not the network] |
---|
151 | |
---|
152 | SideEffects [free the abnormal structure] |
---|
153 | |
---|
154 | SeeAlso [] |
---|
155 | |
---|
156 | ******************************************************************************/ |
---|
157 | |
---|
158 | void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn) |
---|
159 | { |
---|
160 | array_free(abn->abnormal); |
---|
161 | array_free(abn->freeInputs); |
---|
162 | array_free(abn->abnCnfIndexArray); |
---|
163 | array_free(abn->abnAigArray); |
---|
164 | FREE(abn); |
---|
165 | } |
---|
166 | /**Function******************************************************************** |
---|
167 | |
---|
168 | Synopsis [Call-back function to free an abnormal structure.] |
---|
169 | |
---|
170 | Description [This function will be stored in the network together with the |
---|
171 | pointer to the structure. Whenever the network deletes the partitioning |
---|
172 | information, this function is called and it will deallocate the abnormal and |
---|
173 | the information attached to it.] |
---|
174 | |
---|
175 | SideEffects [] |
---|
176 | |
---|
177 | SeeAlso [Ntk_NetworkAddApplInfo] |
---|
178 | |
---|
179 | ******************************************************************************/ |
---|
180 | void |
---|
181 | Dbg_AbnormalFreeCallback( |
---|
182 | void *data) |
---|
183 | { |
---|
184 | Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data); |
---|
185 | } /* End of Part_PartitionFreeCallback */ |
---|
186 | |
---|
187 | |
---|
188 | /**Function******************************************************************** |
---|
189 | |
---|
190 | Synopsis [Add abnormal predicate] |
---|
191 | |
---|
192 | Description [add a node to the predicates array, it should not be already |
---|
193 | present by construction of abnormal predicate] |
---|
194 | |
---|
195 | SideEffects [] |
---|
196 | |
---|
197 | SeeAlso [] |
---|
198 | |
---|
199 | ******************************************************************************/ |
---|
200 | |
---|
201 | void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode) |
---|
202 | { |
---|
203 | assert(abnNode != NIL(Ntk_Node_t*)); |
---|
204 | array_insert_last(Ntk_Node_t*,abn->abnormal, abnNode); |
---|
205 | } |
---|
206 | /**Function******************************************************************** |
---|
207 | |
---|
208 | Synopsis [Add free inputs] |
---|
209 | |
---|
210 | Description [add a node to the free inputs, it should not be already |
---|
211 | present by construction of abnormal predicate] |
---|
212 | |
---|
213 | SideEffects [] |
---|
214 | |
---|
215 | SeeAlso [] |
---|
216 | |
---|
217 | ******************************************************************************/ |
---|
218 | void Dbg_AddFreeInput(Dbg_Abnormal_t * abn, Ntk_Node_t* fNode) |
---|
219 | { |
---|
220 | assert(fNode != NIL(Ntk_Node_t*)); |
---|
221 | array_insert_last(Ntk_Node_t*,abn->freeInputs, fNode); |
---|
222 | } |
---|
223 | |
---|
224 | /**Function******************************************************************** |
---|
225 | |
---|
226 | Synopsis [returns a free inputs] |
---|
227 | |
---|
228 | Description [returns the array of freeinputs] |
---|
229 | |
---|
230 | SideEffects [] |
---|
231 | |
---|
232 | SeeAlso [Dbg_ReadAbn] |
---|
233 | |
---|
234 | ******************************************************************************/ |
---|
235 | array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal) |
---|
236 | { |
---|
237 | assert(abnormal != NIL(Dbg_Abnormal_t)); |
---|
238 | return abnormal->freeInputs; |
---|
239 | } |
---|
240 | /**Function******************************************************************** |
---|
241 | |
---|
242 | Synopsis [returns a abnormal predicates] |
---|
243 | |
---|
244 | Description [returns the array of abnormal predicates] |
---|
245 | |
---|
246 | SideEffects [] |
---|
247 | |
---|
248 | SeeAlso [Dbg_ReadFreeInputs] |
---|
249 | |
---|
250 | ******************************************************************************/ |
---|
251 | array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal) |
---|
252 | { |
---|
253 | assert(abnormal != NIL(Dbg_Abnormal_t)); |
---|
254 | return abnormal->abnormal; |
---|
255 | } |
---|
256 | /**Function******************************************************************** |
---|
257 | |
---|
258 | Synopsis [returns the abnormal structure] |
---|
259 | |
---|
260 | Description [returns the abnormal structure associated to the network] |
---|
261 | |
---|
262 | SideEffects [] |
---|
263 | |
---|
264 | SeeAlso [] |
---|
265 | |
---|
266 | ******************************************************************************/ |
---|
267 | Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network) |
---|
268 | { |
---|
269 | Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY); |
---|
270 | |
---|
271 | return abn; |
---|
272 | } |
---|
273 | /**Function******************************************************************** |
---|
274 | |
---|
275 | Synopsis [Initialize the abnormal predicate in the clauses array abni =0] |
---|
276 | |
---|
277 | Description [Fill the Dbg data structure, abnAigArray conains the set of Aig |
---|
278 | for the set of abnormal perdicate. Each abnormal are set to zero in the clause |
---|
279 | array.predicabnCnfIndexArray is the cnf index. The correspondance is made by |
---|
280 | the index in the table, the index of a node in abnArray is the same in |
---|
281 | abnAigArray and in abnIndexArray. If this array were alredy computed nothing |
---|
282 | is done, if the aig or index information either.] |
---|
283 | |
---|
284 | SideEffects [Fill abnAigArray and abnCnfIndexArray] |
---|
285 | |
---|
286 | SeeAlso [] |
---|
287 | |
---|
288 | ******************************************************************************/ |
---|
289 | void Dbg_InitAbn(Dbg_Abnormal_t * abn, |
---|
290 | bAig_Manager_t * manager, |
---|
291 | st_table * nodeToMvfAigTable, |
---|
292 | BmcCnfClauses_t *cnfClauses) |
---|
293 | { |
---|
294 | if(abn->abnAigArray != NIL(array_t)) |
---|
295 | (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n"); |
---|
296 | if(abn->abnCnfIndexArray != NIL(array_t)){ |
---|
297 | (void) fprintf(vis_stdout, "Abnormal index alredy filled\n"); |
---|
298 | return; |
---|
299 | } |
---|
300 | //Fill |
---|
301 | int size = array_n(abn->abnormal); |
---|
302 | array_t * abnAigArray = array_alloc(bAigEdge_t *,size); |
---|
303 | array_t * abnIndexArray = array_alloc(int,size); |
---|
304 | int aIndex; |
---|
305 | Ntk_Node_t * abnNode; |
---|
306 | Dbg_ForEachAbnormal(abn, aIndex,abnNode){ |
---|
307 | MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable); |
---|
308 | if (abnMvfAig == NIL(MvfAig_Function_t)){ |
---|
309 | (void) fprintf(vis_stdout, "No multi-valued function for this node %s \ |
---|
310 | create abnormal predicate firs \n", Ntk_NodeReadName(abnNode)); |
---|
311 | return ; |
---|
312 | } |
---|
313 | int mvfSize = array_n(abnMvfAig); |
---|
314 | int i; |
---|
315 | bAigEdge_t * abnBAig = ALLOC(bAigEdge_t, mvfSize); |
---|
316 | |
---|
317 | for(i=0; i< mvfSize; i++) |
---|
318 | { |
---|
319 | abnBAig[i] = bAig_GetCanonical(manager, |
---|
320 | MvfAig_FunctionReadComponent(abnMvfAig, i)); |
---|
321 | } |
---|
322 | array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig); |
---|
323 | int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses); |
---|
324 | array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex); |
---|
325 | // Create clause |
---|
326 | array_t *abnClause = NIL(array_t); |
---|
327 | abnClause = array_alloc(int, 0); |
---|
328 | array_insert_last(int, abnClause, abnIndex); |
---|
329 | BmcCnfInsertClause(cnfClauses, abnClause); |
---|
330 | array_free(abnClause); |
---|
331 | } |
---|
332 | abn->abnAigArray = abnAigArray; |
---|
333 | abn->abnCnfIndexArray = abnIndexArray; |
---|
334 | } |
---|