source: vis_dev/vis-2.3/src/debug/debugAbnormal.c @ 42

Last change on this file since 42 was 42, checked in by cecile, 12 years ago

Fault candidates OK
File size: 11.3 KB
Line 
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******************************************************************************/
14Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t*
15node, 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 active then n is replaced by a free input.
47  We assume that the combinatorial gate at on one bit only.]
48
49  SideEffects [fill the abnormal structure]
50
51  SeeAlso     []
52
53******************************************************************************/
54
55void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/
56{
57
58  Ntk_Network_t * ntk = abnormal->network;
59  lsGen gen;
60  Ntk_Node_t* node;
61  Ntk_NetworkForEachNode(ntk,gen,node){
62  //For each combinatorial node
63  if(Ntk_NodeTestIsCombinational(node)){
64        if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
65        {
66                char * nodeName = util_strsav(Ntk_NodeReadName(node));
67        printf("%s \n",  nodeName); 
68
69                Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
70        if(abnormal->verbose){
71                  (void) fprintf(vis_stdout, "** old table\n");
72                  Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
73        }
74                // Build new variables abnormal  and  input
75                Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn");
76                Ntk_Node_t * iNode   = Dbg_CreateNewNode(ntk,node,"i");
77                Dbg_AddFreeInput(abnormal,iNode);
78                Dbg_AddAbnormalPredicate(abnormal,abnNode);
79                Var_Variable_t * abn = Ntk_NodeReadVariable(abnNode);
80                Var_Variable_t * i   = Ntk_NodeReadVariable(iNode);
81                //Add in the table
82                Tbl_TableAddColumn(table,abn,0);
83                int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
84                Tbl_TableAddColumn(table,i,0);
85                int iIndex = Tbl_TableReadVarIndex(table, i, 0);
86       
87                int rowNum;
88                for(rowNum = 0; rowNum <  Tbl_TableReadNumRows(table);rowNum++){
89                        Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
90                        Tbl_EntrySetValue(abnEntry,0,0);
91                        Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
92                        Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
93                        Tbl_EntrySetValue(iEntry,0,1);
94                        Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
95                }
96                //the new row
97                int r = Tbl_TableAddRow(table);
98       
99                int colNum;
100            for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
101                        Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
102                        if(colNum == abnIndex || colNum == iIndex)
103                                Tbl_EntrySetValue(entry,1,1);
104                        else
105                                Tbl_EntrySetValue(entry,0,1);
106                    Tbl_TableSetEntry(table, entry, r, colNum, 0);
107                }
108        int defaultVal = Dbg_GetDefaultValue(table);
109        if(defaultVal == -1)
110        {
111                (void) fprintf(vis_stdout, "Error default value of the table \
112            of node %s\n", nodeName);
113            return;
114        }
115        int outVal = (defaultVal +1 )% 2;
116        if(abnormal->verbose)
117                (void) fprintf(vis_stdout, "Default value : %d\n",defaultVal);
118                for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
119                        Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
120                        Tbl_EntrySetValue(entry,outVal,outVal);
121                    Tbl_TableSetEntry(table, entry, r, colNum, 1);
122                }
123        if(abnormal->verbose){
124                 printf("---------------\n");
125                 Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
126        }
127          }
128        }
129}
130 Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
131 (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
132 (void *) abnormal);
133}
134/**Function********************************************************************
135 
136  Synopsis    [Allocate a new abnormal structure]
137
138  Description [The structure contains the network with abnormal predicate,
139  and two sets of Ntk_Node_t for the abnormal and the free inputs]
140
141  SideEffects [Allocate the abnormal structure]
142
143  SeeAlso     []
144
145******************************************************************************/
146
147Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network)
148{
149         Dbg_Abnormal_t * abn = ALLOC(Dbg_Abnormal_t, 1);
150
151         abn->network = network;
152         abn->abnormal = array_alloc(Ntk_Node_t*,0);
153         abn->freeInputs = array_alloc(Ntk_Node_t*,0);
154     abn->abnAigArray = NIL(array_t);
155     abn->abnCnfIndexArray = NIL(array_t);
156         abn->verbose = 0;
157         return abn;
158}       
159
160/**Function********************************************************************
161 
162  Synopsis    [Deallocate a new abnormal structure]
163
164  Description [Free the arrays not the network]
165
166  SideEffects [free the abnormal structure]
167
168  SeeAlso     []
169
170******************************************************************************/
171
172void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn)
173{
174         array_free(abn->abnormal);
175         array_free(abn->freeInputs);
176     array_free(abn->abnCnfIndexArray);
177     array_free(abn->abnAigArray);
178         FREE(abn);
179}       
180/**Function********************************************************************
181
182  Synopsis    [Call-back function to free an abnormal structure.]
183
184  Description [This function will be stored in the network together with the
185  pointer to the structure. Whenever the network deletes the partitioning
186  information, this function is called and it will deallocate the abnormal and
187  the information attached to it.]
188
189  SideEffects []
190
191  SeeAlso     [Ntk_NetworkAddApplInfo]
192
193******************************************************************************/
194void
195Dbg_AbnormalFreeCallback(
196   void *data)
197{
198  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
199} /* End of Part_PartitionFreeCallback */
200
201
202/**Function********************************************************************
203 
204  Synopsis    [Add abnormal predicate]
205
206  Description [add a node to the predicates array, it should not be already
207  present by construction of abnormal predicate]
208
209  SideEffects []
210
211  SeeAlso     []
212
213******************************************************************************/
214
215void  Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode)
216{
217        assert(abnNode != NIL(Ntk_Node_t*));
218        array_insert_last(Ntk_Node_t*,abn->abnormal, abnNode);
219}
220/**Function********************************************************************
221 
222  Synopsis    [Add free inputs]
223
224  Description [add a node to the free inputs, it should not be already
225  present by construction of abnormal predicate]
226
227  SideEffects []
228
229  SeeAlso     []
230
231******************************************************************************/
232void  Dbg_AddFreeInput(Dbg_Abnormal_t * abn, Ntk_Node_t* fNode)
233{
234        assert(fNode != NIL(Ntk_Node_t*));
235        array_insert_last(Ntk_Node_t*,abn->freeInputs, fNode);
236}
237
238/**Function********************************************************************
239 
240  Synopsis    [returns a free inputs]
241
242  Description [returns the array of freeinputs]
243
244  SideEffects []
245
246  SeeAlso     [Dbg_ReadAbn]
247
248******************************************************************************/
249array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal)
250{
251        assert(abnormal != NIL(Dbg_Abnormal_t));
252        return abnormal->freeInputs;
253}
254/**Function********************************************************************
255 
256  Synopsis    [returns a abnormal predicates]
257
258  Description [returns the array of abnormal predicates]
259
260  SideEffects []
261
262  SeeAlso     [Dbg_ReadFreeInputs]
263
264******************************************************************************/
265array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal)
266{
267        assert(abnormal != NIL(Dbg_Abnormal_t));
268        return abnormal->abnormal;
269}
270/**Function********************************************************************
271 
272  Synopsis    [returns the abnormal structure]
273
274  Description [returns the abnormal structure associated to the network]
275
276  SideEffects []
277
278  SeeAlso     []
279
280******************************************************************************/
281Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
282{
283        Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);
284
285        return abn;
286}
287/**Function********************************************************************
288 
289  Synopsis    [Initialize the abnormal predicate in the clauses array abni =0]
290
291  Description [Fill the Dbg data structure, abnAigArray conains the set of Aig
292  for the set of abnormal perdicate. Each abnormal are set to zero in the clause
293  array.predicabnCnfIndexArray is the cnf index. The   correspondance is made by
294  the index in the table, the index of a node in   abnArray is the same in
295  abnAigArray and in abnIndexArray. If this array were  alredy computed nothing
296  is done, if the aig or index information either.]
297
298  SideEffects [Fill abnAigArray and abnCnfIndexArray]
299
300  SeeAlso     []
301
302******************************************************************************/
303void Dbg_InitAbn(Dbg_Abnormal_t * abn,
304bAig_Manager_t   * manager,
305st_table * nodeToMvfAigTable,
306BmcCnfClauses_t *cnfClauses)
307{
308  if(abn->abnAigArray != NIL(array_t))
309    (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
310  if(abn->abnCnfIndexArray != NIL(array_t)){
311    (void) fprintf(vis_stdout, "Abnormal index alredy filled\n"); 
312     return;
313  }
314  //Fill
315   int size = array_n(abn->abnormal);
316   array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
317   array_t * abnIndexArray = array_alloc(int,size);
318   int aIndex;
319   Ntk_Node_t * abnNode;
320   Dbg_ForEachAbnormal(abn, aIndex,abnNode){
321   MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
322    if (abnMvfAig ==  NIL(MvfAig_Function_t)){
323     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
324     create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
325     return ;
326    }
327    int mvfSize   = array_n(abnMvfAig);
328    int i;
329    bAigEdge_t         * abnBAig  = ALLOC(bAigEdge_t, mvfSize);
330
331    for(i=0; i< mvfSize; i++)
332    {
333      abnBAig[i] = bAig_GetCanonical(manager,
334      MvfAig_FunctionReadComponent(abnMvfAig,  i));
335    }
336    array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
337    int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
338    array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
339    // Create clause
340     array_t           *abnClause = NIL(array_t);
341         abnClause = array_alloc(int, 0);   
342         array_insert_last(int, abnClause, abnIndex);
343         BmcCnfInsertClause(cnfClauses, abnClause);
344     array_free(abnClause);
345   }
346   abn->abnAigArray = abnAigArray;
347   abn->abnCnfIndexArray = abnIndexArray;
348}
Note: See TracBrowser for help on using the repository browser.