[36] | 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 |
---|
[42] | 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.] |
---|
[36] | 48 | |
---|
| 49 | SideEffects [fill the abnormal structure] |
---|
| 50 | |
---|
| 51 | SeeAlso [] |
---|
| 52 | |
---|
| 53 | ******************************************************************************/ |
---|
| 54 | |
---|
| 55 | void 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); |
---|
[42] | 70 | if(abnormal->verbose){ |
---|
| 71 | (void) fprintf(vis_stdout, "** old table\n"); |
---|
| 72 | Tbl_TableWriteBlifMvToFile(table,2,vis_stdout); |
---|
| 73 | } |
---|
[36] | 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); |
---|
[42] | 86 | |
---|
[36] | 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); |
---|
[42] | 98 | |
---|
[36] | 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 | } |
---|
[42] | 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); |
---|
[36] | 118 | for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){ |
---|
| 119 | Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c); |
---|
[42] | 120 | Tbl_EntrySetValue(entry,outVal,outVal); |
---|
[36] | 121 | Tbl_TableSetEntry(table, entry, r, colNum, 1); |
---|
| 122 | } |
---|
[42] | 123 | if(abnormal->verbose){ |
---|
[36] | 124 | printf("---------------\n"); |
---|
| 125 | Tbl_TableWriteBlifMvToFile(table,0,vis_stdout); |
---|
[42] | 126 | } |
---|
[36] | 127 | } |
---|
| 128 | } |
---|
| 129 | } |
---|
[40] | 130 | Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY, |
---|
| 131 | (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback, |
---|
| 132 | (void *) abnormal); |
---|
[36] | 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 | |
---|
| 147 | Dbg_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); |
---|
[41] | 154 | abn->abnAigArray = NIL(array_t); |
---|
| 155 | abn->abnCnfIndexArray = NIL(array_t); |
---|
[36] | 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 | |
---|
| 172 | void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn) |
---|
| 173 | { |
---|
| 174 | array_free(abn->abnormal); |
---|
| 175 | array_free(abn->freeInputs); |
---|
[41] | 176 | array_free(abn->abnCnfIndexArray); |
---|
| 177 | array_free(abn->abnAigArray); |
---|
[36] | 178 | FREE(abn); |
---|
| 179 | } |
---|
[40] | 180 | /**Function******************************************************************** |
---|
[36] | 181 | |
---|
[40] | 182 | Synopsis [Call-back function to free an abnormal structure.] |
---|
[36] | 183 | |
---|
[40] | 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 | ******************************************************************************/ |
---|
| 194 | void |
---|
| 195 | Dbg_AbnormalFreeCallback( |
---|
| 196 | void *data) |
---|
| 197 | { |
---|
| 198 | Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data); |
---|
| 199 | } /* End of Part_PartitionFreeCallback */ |
---|
| 200 | |
---|
| 201 | |
---|
[36] | 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 | |
---|
| 215 | void 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 | ******************************************************************************/ |
---|
| 232 | void 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 | ******************************************************************************/ |
---|
| 249 | array_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 | ******************************************************************************/ |
---|
| 265 | array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal) |
---|
| 266 | { |
---|
| 267 | assert(abnormal != NIL(Dbg_Abnormal_t)); |
---|
| 268 | return abnormal->abnormal; |
---|
| 269 | } |
---|
[40] | 270 | /**Function******************************************************************** |
---|
| 271 | |
---|
| 272 | Synopsis [returns the abnormal structure] |
---|
[36] | 273 | |
---|
[40] | 274 | Description [returns the abnormal structure associated to the network] |
---|
| 275 | |
---|
| 276 | SideEffects [] |
---|
| 277 | |
---|
| 278 | SeeAlso [] |
---|
| 279 | |
---|
| 280 | ******************************************************************************/ |
---|
| 281 | Dbg_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 | } |
---|
[41] | 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 | ******************************************************************************/ |
---|
| 303 | void Dbg_InitAbn(Dbg_Abnormal_t * abn, |
---|
| 304 | bAig_Manager_t * manager, |
---|
| 305 | st_table * nodeToMvfAigTable, |
---|
| 306 | BmcCnfClauses_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 | } |
---|