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