[14] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [synthSynth.c] |
---|
| 4 | |
---|
| 5 | PackageName [synth] |
---|
| 6 | |
---|
| 7 | Synopsis [Synthesis Algorithms] |
---|
| 8 | |
---|
| 9 | Description [This file contains main routines that implement symbolic |
---|
| 10 | factorization algorithms.] |
---|
| 11 | |
---|
| 12 | SeeAlso [synthDiv.c synthFactor.c synthGen.c synthOpt.c synthSimple.c] |
---|
| 13 | |
---|
| 14 | Author [Balakrishna Kumthekar, In-Ho Moon] |
---|
| 15 | |
---|
| 16 | Copyright [This file was created at the University of Colorado at |
---|
| 17 | Boulder. The University of Colorado at Boulder makes no warranty |
---|
| 18 | about the suitability of this software for any purpose. It is |
---|
| 19 | presented on an AS IS basis.] |
---|
| 20 | |
---|
| 21 | ******************************************************************************/ |
---|
| 22 | |
---|
| 23 | #include "synthInt.h" |
---|
| 24 | |
---|
| 25 | static char rcsid[] UNUSED = "$Id: synthSynth.c,v 1.47 2005/04/23 14:37:51 jinh Exp $"; |
---|
| 26 | |
---|
| 27 | |
---|
| 28 | /*---------------------------------------------------------------------------*/ |
---|
| 29 | /* Constant declarations */ |
---|
| 30 | /*---------------------------------------------------------------------------*/ |
---|
| 31 | |
---|
| 32 | |
---|
| 33 | /*---------------------------------------------------------------------------*/ |
---|
| 34 | /* Type declarations */ |
---|
| 35 | /*---------------------------------------------------------------------------*/ |
---|
| 36 | |
---|
| 37 | |
---|
| 38 | /*---------------------------------------------------------------------------*/ |
---|
| 39 | /* Structure declarations */ |
---|
| 40 | /*---------------------------------------------------------------------------*/ |
---|
| 41 | |
---|
| 42 | |
---|
| 43 | /*---------------------------------------------------------------------------*/ |
---|
| 44 | /* Variable declarations */ |
---|
| 45 | /*---------------------------------------------------------------------------*/ |
---|
| 46 | |
---|
| 47 | |
---|
| 48 | /*---------------------------------------------------------------------------*/ |
---|
| 49 | /* Macro declarations */ |
---|
| 50 | /*---------------------------------------------------------------------------*/ |
---|
| 51 | |
---|
| 52 | |
---|
| 53 | /**AutomaticStart*************************************************************/ |
---|
| 54 | |
---|
| 55 | /*---------------------------------------------------------------------------*/ |
---|
| 56 | /* Static function prototypes */ |
---|
| 57 | /*---------------------------------------------------------------------------*/ |
---|
| 58 | |
---|
| 59 | static int synthesizeNetwork(Ntk_Network_t *network, graph_t *partition, Fsm_Fsm_t *fsm, st_table *careBddTable, Synth_InfoData_t *synthInfo, int verbosity); |
---|
| 60 | static int IsPartitionValid(Ntk_Network_t *network, graph_t *partition); |
---|
| 61 | static array_t * GetCombOutputNameArray(Ntk_Network_t *network); |
---|
| 62 | static array_t * GetCombInputIdArray(Ntk_Network_t *network); |
---|
| 63 | static bdd_node ** GetBddArray(Mvf_Function_t *combMvfs); |
---|
| 64 | |
---|
| 65 | /**AutomaticEnd***************************************************************/ |
---|
| 66 | |
---|
| 67 | |
---|
| 68 | /*---------------------------------------------------------------------------*/ |
---|
| 69 | /* Definition of exported functions */ |
---|
| 70 | /*---------------------------------------------------------------------------*/ |
---|
| 71 | |
---|
| 72 | /**Function******************************************************************** |
---|
| 73 | |
---|
| 74 | Synopsis [Initialize the info data structure.] |
---|
| 75 | |
---|
| 76 | Description [Initialize the info data structure. See the documentation for |
---|
| 77 | CommandSynthesizeNetwork for the meaning of the various fields.] |
---|
| 78 | |
---|
| 79 | SideEffects [None] |
---|
| 80 | |
---|
| 81 | SeeAlso [Synth_FreeInfo] |
---|
| 82 | |
---|
| 83 | ******************************************************************************/ |
---|
| 84 | Synth_InfoData_t * |
---|
| 85 | Synth_InitializeInfo(int factoring, |
---|
| 86 | int divisor, |
---|
| 87 | int unreachDC, |
---|
| 88 | int reordering, |
---|
| 89 | int trySharing, |
---|
| 90 | int realign, |
---|
| 91 | char *filehead, |
---|
| 92 | char *prefix, |
---|
| 93 | boolean eqn) |
---|
| 94 | { |
---|
| 95 | |
---|
| 96 | Synth_InfoData_t *synthInfo; |
---|
| 97 | |
---|
| 98 | synthInfo = ALLOC(Synth_InfoData_t, 1); |
---|
| 99 | if (!synthInfo) { |
---|
| 100 | (void) fprintf(vis_stderr, |
---|
| 101 | "** synth error: Could not initialize info structure.\n"); |
---|
| 102 | return NIL(Synth_InfoData_t); |
---|
| 103 | } |
---|
| 104 | synthInfo->factoring = factoring; |
---|
| 105 | synthInfo->divisor = divisor; |
---|
| 106 | synthInfo->unreachDC = unreachDC; |
---|
| 107 | synthInfo->reordering = reordering; |
---|
| 108 | synthInfo->trySharing = trySharing; |
---|
| 109 | synthInfo->realign = realign; |
---|
| 110 | synthInfo->filehead = filehead; |
---|
| 111 | synthInfo->prefix = prefix; |
---|
| 112 | synthInfo->eqn = eqn; |
---|
| 113 | return synthInfo; |
---|
| 114 | } |
---|
| 115 | |
---|
| 116 | /**Function******************************************************************** |
---|
| 117 | |
---|
| 118 | Synopsis [Free info data.] |
---|
| 119 | |
---|
| 120 | Description [Free Info data.] |
---|
| 121 | |
---|
| 122 | SideEffects [None] |
---|
| 123 | |
---|
| 124 | SeeAlso [Synth_InitializeInfo] |
---|
| 125 | |
---|
| 126 | ******************************************************************************/ |
---|
| 127 | void |
---|
| 128 | Synth_FreeInfo(Synth_InfoData_t *synthInfo) |
---|
| 129 | { |
---|
| 130 | FREE(synthInfo); |
---|
| 131 | } |
---|
| 132 | |
---|
| 133 | /**Function******************************************************************** |
---|
| 134 | |
---|
| 135 | Synopsis [Synthesize a network.] |
---|
| 136 | |
---|
| 137 | Description [Synthesize a network. Here a major assumption is that, if the |
---|
| 138 | network is sequential, and an FSM is already hooked to the network, then the |
---|
| 139 | partition field of the FSM and that of the network are isomorphic.] |
---|
| 140 | |
---|
| 141 | SideEffects [If an FSM (in case of a sequential design) or the circuit |
---|
| 142 | partition does not already exist in the network, they are created and hooked |
---|
| 143 | to the network. However, they are freed at the end of this procedure. ] |
---|
| 144 | |
---|
| 145 | SeeAlso [Synth_SynthesizeFsm] |
---|
| 146 | |
---|
| 147 | ******************************************************************************/ |
---|
| 148 | int |
---|
| 149 | Synth_SynthesizeNetwork(Ntk_Network_t *network, |
---|
| 150 | graph_t *partition, |
---|
| 151 | st_table *careTable, |
---|
| 152 | Synth_InfoData_t *synthInfo, |
---|
| 153 | int verbosity) |
---|
| 154 | { |
---|
| 155 | graph_t *newPartition = NIL(graph_t); |
---|
| 156 | Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); |
---|
| 157 | st_table *careBddTable; |
---|
| 158 | int status; |
---|
| 159 | int createdPart = 0; |
---|
| 160 | int createdFsm = 0; |
---|
| 161 | int ntkIsSeq = 1; |
---|
| 162 | |
---|
| 163 | if (bdd_get_package_name() != CUDD) { |
---|
| 164 | (void) fprintf(vis_stderr, |
---|
| 165 | "** synth error: The synthesis package can be used only with CUDD package\n"); |
---|
| 166 | (void) fprintf(vis_stderr, |
---|
| 167 | "** synth error: Please link with the CUDD package\n"); |
---|
| 168 | return 0; |
---|
| 169 | } |
---|
| 170 | if (partition == NIL(graph_t)) { |
---|
| 171 | newPartition = (graph_t *) Ntk_NetworkReadApplInfo(network, |
---|
| 172 | PART_NETWORK_APPL_KEY); |
---|
| 173 | createdPart = 0; /* Using partition of the network. */ |
---|
| 174 | if (newPartition == NIL(graph_t) || |
---|
| 175 | (!IsPartitionValid(network,newPartition))) { |
---|
| 176 | newPartition = Part_NetworkCreatePartition(network, |
---|
| 177 | NIL(Hrc_Node_t), |
---|
| 178 | "dummy", (lsList) 0, |
---|
| 179 | (lsList) 0, NIL(mdd_t), |
---|
| 180 | Part_InOut_c, |
---|
| 181 | (lsList) 0, |
---|
| 182 | FALSE, FALSE, TRUE); |
---|
| 183 | if (newPartition == NIL(graph_t)) { |
---|
| 184 | (void) fprintf(vis_stderr,"** synth error: Could not create an InOut"); |
---|
| 185 | (void) fprintf(vis_stderr,"partition.\n"); |
---|
| 186 | return 0; |
---|
| 187 | } |
---|
| 188 | createdPart = 1; /* Using new partition */ |
---|
| 189 | } |
---|
| 190 | } else { |
---|
| 191 | if (IsPartitionValid(network,partition)) { |
---|
| 192 | newPartition = partition; |
---|
| 193 | createdPart = 2; /* Using the partition provided. */ |
---|
| 194 | } else { |
---|
| 195 | newPartition = Part_NetworkCreatePartition(network, |
---|
| 196 | NIL(Hrc_Node_t), |
---|
| 197 | "dummy", (lsList) 0, |
---|
| 198 | (lsList) 0, NIL(mdd_t), |
---|
| 199 | Part_InOut_c, |
---|
| 200 | (lsList) 0, |
---|
| 201 | FALSE, FALSE, TRUE); |
---|
| 202 | if (newPartition == NIL(graph_t)) { |
---|
| 203 | (void) fprintf(vis_stderr,"** synth error: Could not create an InOut"); |
---|
| 204 | (void) fprintf(vis_stderr,"partition.\n"); |
---|
| 205 | return 0; |
---|
| 206 | } |
---|
| 207 | createdPart = 1; |
---|
| 208 | } |
---|
| 209 | } |
---|
| 210 | |
---|
| 211 | |
---|
| 212 | if(!Ntk_NetworkReadNumLatches(network)) { |
---|
| 213 | (void) fprintf(vis_stdout, "** synth info: No latches present in the "); |
---|
| 214 | (void) fprintf(vis_stdout, "current network.\n"); |
---|
| 215 | (void) fprintf(vis_stdout, |
---|
| 216 | "** synth info: Proceeding with combinational synthesis.\n"); |
---|
| 217 | ntkIsSeq = 0; |
---|
| 218 | } |
---|
| 219 | |
---|
| 220 | if (ntkIsSeq) { |
---|
| 221 | switch (createdPart) { |
---|
| 222 | case 0: |
---|
| 223 | /* Check if there is already an Fsm attached to |
---|
| 224 | * the network. |
---|
| 225 | */ |
---|
| 226 | fsm = (Fsm_Fsm_t *) Ntk_NetworkReadApplInfo(network, |
---|
| 227 | FSM_NETWORK_APPL_KEY); |
---|
| 228 | if (fsm == NIL(Fsm_Fsm_t)) { |
---|
| 229 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, |
---|
| 230 | NIL(graph_t)); |
---|
| 231 | if (fsm == NIL(Fsm_Fsm_t)) { |
---|
| 232 | (void) fprintf(vis_stderr,"** synth error: Could not create "); |
---|
| 233 | (void) fprintf(vis_stderr,"an Fsm\n"); |
---|
| 234 | goto endgame; |
---|
| 235 | } |
---|
| 236 | createdFsm = 1; |
---|
| 237 | } else { |
---|
| 238 | createdFsm = 0; |
---|
| 239 | } |
---|
| 240 | break; |
---|
| 241 | case 1: |
---|
| 242 | case 2: |
---|
| 243 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, |
---|
| 244 | Part_PartitionDuplicate(newPartition)); |
---|
| 245 | |
---|
| 246 | if (fsm == NIL(Fsm_Fsm_t)) { |
---|
| 247 | (void) fprintf(vis_stderr,"** synth error: Could not create "); |
---|
| 248 | (void) fprintf(vis_stderr,"an Fsm\n"); |
---|
| 249 | goto endgame; |
---|
| 250 | } |
---|
| 251 | createdFsm = 1; |
---|
| 252 | break; |
---|
| 253 | } |
---|
| 254 | } |
---|
| 255 | |
---|
| 256 | careBddTable = NIL(st_table); |
---|
| 257 | if (careTable != NIL(st_table)) { |
---|
| 258 | mdd_t *mddTemp; |
---|
| 259 | bdd_node *ddNode; |
---|
| 260 | char *name; |
---|
| 261 | st_generator *stGen; |
---|
| 262 | |
---|
| 263 | careBddTable = st_init_table(strcmp, st_strhash); |
---|
| 264 | st_foreach_item(careTable,stGen,&name,&mddTemp) { |
---|
| 265 | ddNode = bdd_extract_node_as_is(mddTemp); |
---|
| 266 | st_insert(careBddTable,name,(char *)ddNode); |
---|
| 267 | } |
---|
| 268 | } |
---|
| 269 | if (fsm) |
---|
| 270 | status = synthesizeNetwork(network, newPartition, |
---|
| 271 | fsm, careBddTable, synthInfo, |
---|
| 272 | verbosity); |
---|
| 273 | else |
---|
| 274 | status = synthesizeNetwork(network,newPartition, |
---|
| 275 | NIL(Fsm_Fsm_t), careBddTable, |
---|
| 276 | synthInfo, verbosity); |
---|
| 277 | |
---|
| 278 | if (careBddTable) |
---|
| 279 | st_free_table(careBddTable); |
---|
| 280 | if (createdPart == 1) |
---|
| 281 | Part_PartitionFree(newPartition); |
---|
| 282 | if (createdFsm == 1) |
---|
| 283 | Fsm_FsmFree(fsm); |
---|
| 284 | |
---|
| 285 | return status; |
---|
| 286 | |
---|
| 287 | endgame: |
---|
| 288 | if (createdPart == 1) |
---|
| 289 | Part_PartitionFree(newPartition); |
---|
| 290 | if (createdFsm == 1) |
---|
| 291 | Fsm_FsmFree(fsm); |
---|
| 292 | |
---|
| 293 | return 0; |
---|
| 294 | |
---|
| 295 | } |
---|
| 296 | |
---|
| 297 | /**Function******************************************************************** |
---|
| 298 | |
---|
| 299 | Synopsis [Synthesize an FSM.] |
---|
| 300 | |
---|
| 301 | Description [Synthesize an FSM. This procedure can be used if the default FSM |
---|
| 302 | attached to the network is different from the one that needs to be |
---|
| 303 | synthesized.] |
---|
| 304 | |
---|
| 305 | SideEffects [None] |
---|
| 306 | |
---|
| 307 | SeeAlso [Synth_SynthesizeNetwork] |
---|
| 308 | |
---|
| 309 | ******************************************************************************/ |
---|
| 310 | int |
---|
| 311 | Synth_SynthesizeFsm(Fsm_Fsm_t *fsm, |
---|
| 312 | st_table *careTable, |
---|
| 313 | Synth_InfoData_t *synthInfo, |
---|
| 314 | int verbosity) |
---|
| 315 | { |
---|
| 316 | Ntk_Network_t *network; |
---|
| 317 | graph_t *partition; |
---|
| 318 | st_table *careBddTable; |
---|
| 319 | int status; |
---|
| 320 | |
---|
| 321 | network = Fsm_FsmReadNetwork(fsm); |
---|
| 322 | partition = Fsm_FsmReadPartition(fsm); |
---|
| 323 | |
---|
| 324 | careBddTable = NIL(st_table); |
---|
| 325 | if (careTable != NIL(st_table)) { |
---|
| 326 | mdd_t *mddTemp; |
---|
| 327 | bdd_node *ddNode; |
---|
| 328 | char *name; |
---|
| 329 | st_generator *stGen; |
---|
| 330 | |
---|
| 331 | careBddTable = st_init_table(strcmp, st_strhash); |
---|
| 332 | st_foreach_item(careTable,stGen,&name,&mddTemp) { |
---|
| 333 | ddNode = bdd_extract_node_as_is(mddTemp); |
---|
| 334 | st_insert(careBddTable,name,(char *)ddNode); |
---|
| 335 | } |
---|
| 336 | } |
---|
| 337 | |
---|
| 338 | status = synthesizeNetwork(network,partition,fsm,careBddTable,synthInfo, |
---|
| 339 | verbosity); |
---|
| 340 | if (careBddTable) |
---|
| 341 | st_free_table(careBddTable); |
---|
| 342 | |
---|
| 343 | return status; |
---|
| 344 | } |
---|
| 345 | |
---|
| 346 | /*---------------------------------------------------------------------------*/ |
---|
| 347 | /* Definition of internal functions */ |
---|
| 348 | /*---------------------------------------------------------------------------*/ |
---|
| 349 | |
---|
| 350 | |
---|
| 351 | /*---------------------------------------------------------------------------*/ |
---|
| 352 | /* Definition of static functions */ |
---|
| 353 | /*---------------------------------------------------------------------------*/ |
---|
| 354 | |
---|
| 355 | /**Function******************************************************************** |
---|
| 356 | |
---|
| 357 | Synopsis [Core function of Synth_SynthesizeNetwork.] |
---|
| 358 | |
---|
| 359 | Description [Core function of Synth_SynthesizeNetwork and |
---|
| 360 | Synth_SynthesizeFsm.] |
---|
| 361 | |
---|
| 362 | SideEffects [None] |
---|
| 363 | |
---|
| 364 | SeeAlso [] |
---|
| 365 | |
---|
| 366 | ******************************************************************************/ |
---|
| 367 | static int |
---|
| 368 | synthesizeNetwork(Ntk_Network_t *network, |
---|
| 369 | graph_t *partition, |
---|
| 370 | Fsm_Fsm_t *fsm, |
---|
| 371 | st_table *careBddTable, |
---|
| 372 | Synth_InfoData_t *synthInfo, |
---|
| 373 | int verbosity) |
---|
| 374 | { |
---|
| 375 | bdd_manager *ddManager = (bdd_manager *) Ntk_NetworkReadMddManager(network); |
---|
| 376 | int i, numOut; |
---|
| 377 | int *initStates = NIL(int); |
---|
| 378 | Mvf_Function_t *combMvfs; |
---|
| 379 | array_t *inputIds, *combOutNamesArray; |
---|
| 380 | bdd_node **combOutBdds, *ddTemp; |
---|
| 381 | bdd_node *unReachable = NIL(bdd_node), *reachable = NIL(bdd_node); |
---|
| 382 | bdd_node **combUpperBdds; |
---|
| 383 | bdd_node *initBdd = NIL(bdd_node), *temp; |
---|
| 384 | char **combOutNames; |
---|
| 385 | char *str; |
---|
| 386 | int realign_bdd, realign_zdd; |
---|
| 387 | Fsm_RchType_t reachMethod; |
---|
| 388 | |
---|
| 389 | /* Save current values of realignment flags. */ |
---|
| 390 | realign_zdd = bdd_zdd_realignment_enabled(ddManager); |
---|
| 391 | realign_bdd = bdd_realignment_enabled(ddManager); |
---|
| 392 | |
---|
| 393 | if (synthInfo->reordering == 1) { |
---|
| 394 | if (synthInfo->realign) |
---|
| 395 | bdd_zdd_realign_enable(ddManager); |
---|
| 396 | else |
---|
| 397 | bdd_zdd_realign_disable(ddManager); |
---|
| 398 | bdd_realign_disable(ddManager); |
---|
| 399 | } else if (synthInfo->reordering == 2) { |
---|
| 400 | bdd_zdd_realign_disable(ddManager); |
---|
| 401 | if (synthInfo->realign) |
---|
| 402 | bdd_realign_enable(ddManager); |
---|
| 403 | else |
---|
| 404 | bdd_realign_disable(ddManager); |
---|
| 405 | } else { |
---|
| 406 | bdd_zdd_realign_disable(ddManager); |
---|
| 407 | bdd_realign_disable(ddManager); |
---|
| 408 | } |
---|
| 409 | |
---|
| 410 | /* Get the names of the combinational outputs, i.e, next state functions |
---|
| 411 | * as well as primary outputs. In VIS even latch initial inputs are |
---|
| 412 | * considered combinational outputs. Since, we support only blif files, |
---|
| 413 | * latch initial inputs are not present in combOutNamesArray. |
---|
| 414 | */ |
---|
| 415 | combOutNamesArray = GetCombOutputNameArray(network); |
---|
| 416 | if (combOutNamesArray == NIL(array_t)) { |
---|
| 417 | if (realign_zdd == 1) |
---|
| 418 | bdd_zdd_realign_enable(ddManager); |
---|
| 419 | else |
---|
| 420 | bdd_zdd_realign_disable(ddManager); |
---|
| 421 | if (realign_bdd == 1) |
---|
| 422 | bdd_realign_enable(ddManager); |
---|
| 423 | else |
---|
| 424 | bdd_realign_disable(ddManager); |
---|
| 425 | return 0; |
---|
| 426 | } |
---|
| 427 | /* Get the array of combinational inputs, i.e., primary inputs, |
---|
| 428 | * present state variables. |
---|
| 429 | */ |
---|
| 430 | inputIds = GetCombInputIdArray(network); |
---|
| 431 | if (inputIds == NIL(array_t)) { |
---|
| 432 | array_free(combOutNamesArray); |
---|
| 433 | /* Restore values of realignment flags. */ |
---|
| 434 | if (realign_zdd == 1) |
---|
| 435 | bdd_zdd_realign_enable(ddManager); |
---|
| 436 | else |
---|
| 437 | bdd_zdd_realign_disable(ddManager); |
---|
| 438 | if (realign_bdd == 1) |
---|
| 439 | bdd_realign_enable(ddManager); |
---|
| 440 | else |
---|
| 441 | bdd_realign_disable(ddManager); |
---|
| 442 | return 0; |
---|
| 443 | } |
---|
| 444 | /* Compute the Bdds */ |
---|
| 445 | combMvfs = Part_PartitionBuildFunctions(partition,combOutNamesArray, |
---|
| 446 | inputIds,NIL(mdd_t)); |
---|
| 447 | combOutBdds = (bdd_node **) GetBddArray(combMvfs); |
---|
| 448 | if (combOutBdds == NIL(bdd_node *)) { |
---|
| 449 | array_free(combOutNamesArray); |
---|
| 450 | array_free(inputIds); |
---|
| 451 | Mvf_FunctionArrayFree(combMvfs); |
---|
| 452 | if (realign_zdd == 1) |
---|
| 453 | bdd_zdd_realign_enable(ddManager); |
---|
| 454 | else |
---|
| 455 | bdd_zdd_realign_disable(ddManager); |
---|
| 456 | if (realign_bdd == 1) |
---|
| 457 | bdd_realign_enable(ddManager); |
---|
| 458 | else |
---|
| 459 | bdd_realign_disable(ddManager); |
---|
| 460 | return 0; |
---|
| 461 | } |
---|
| 462 | Mvf_FunctionArrayFree(combMvfs); |
---|
| 463 | |
---|
| 464 | numOut = array_n(combOutNamesArray); |
---|
| 465 | combOutNames = ALLOC(char *, numOut); |
---|
| 466 | if (combOutNames == NIL(char *)) { |
---|
| 467 | (void) fprintf(vis_stderr,"** synth error: Could not allocate memory\n"); |
---|
| 468 | array_free(combOutNamesArray); |
---|
| 469 | array_free(inputIds); |
---|
| 470 | |
---|
| 471 | for (i = 0; i < numOut; i++) { |
---|
| 472 | bdd_recursive_deref(ddManager,combOutBdds[i]); |
---|
| 473 | } |
---|
| 474 | FREE(combOutBdds); |
---|
| 475 | if (realign_zdd == 1) |
---|
| 476 | bdd_zdd_realign_enable(ddManager); |
---|
| 477 | else |
---|
| 478 | bdd_zdd_realign_disable(ddManager); |
---|
| 479 | if (realign_bdd == 1) |
---|
| 480 | bdd_realign_enable(ddManager); |
---|
| 481 | else |
---|
| 482 | bdd_realign_disable(ddManager); |
---|
| 483 | return 0; |
---|
| 484 | } |
---|
| 485 | arrayForEachItem(char *, combOutNamesArray, i, str) { |
---|
| 486 | combOutNames[i] = str; |
---|
| 487 | } |
---|
| 488 | array_free(combOutNamesArray); |
---|
| 489 | |
---|
| 490 | |
---|
| 491 | combUpperBdds = ALLOC(bdd_node *,numOut); |
---|
| 492 | /* Initialize the upper bound to be the lower bound */ |
---|
| 493 | for (i = 0; i < numOut; i++) { |
---|
| 494 | bdd_ref(combUpperBdds[i] = combOutBdds[i]); |
---|
| 495 | } |
---|
| 496 | |
---|
| 497 | if (fsm) { |
---|
| 498 | mdd_t *initMdd; |
---|
| 499 | /* Duplicate copy of initial States is returned */ |
---|
| 500 | initMdd = Fsm_FsmComputeInitialStates(fsm); |
---|
| 501 | initBdd = (bdd_node *)bdd_extract_node_as_is(initMdd); |
---|
| 502 | bdd_ref(initBdd); |
---|
| 503 | mdd_free(initMdd); |
---|
| 504 | |
---|
| 505 | if (synthInfo->unreachDC) { |
---|
| 506 | mdd_t *reachStates; |
---|
| 507 | |
---|
| 508 | (void) fprintf(vis_stdout, |
---|
| 509 | "** synth info: Using unreachable states as dont cares\n"); |
---|
| 510 | if (synthInfo->unreachDC == 1) { |
---|
| 511 | reachMethod = Fsm_Rch_Bfs_c; |
---|
| 512 | } else if (synthInfo->unreachDC == 2) { |
---|
| 513 | reachMethod = Fsm_Rch_Hd_c; |
---|
| 514 | } else if (synthInfo->unreachDC == 3) { |
---|
| 515 | reachMethod = Fsm_Rch_Oa_c; |
---|
| 516 | } else { |
---|
| 517 | reachMethod = Fsm_Rch_Default_c; |
---|
| 518 | } |
---|
| 519 | reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0, |
---|
| 520 | 0,0,1000,reachMethod, |
---|
| 521 | 0,0,NIL(array_t), FALSE, |
---|
| 522 | NIL(array_t)); |
---|
| 523 | reachable = (bdd_node *)bdd_extract_node_as_is(reachStates); |
---|
| 524 | bdd_ref(reachable); |
---|
| 525 | unReachable = bdd_not_bdd_node(reachable); |
---|
| 526 | bdd_ref(unReachable); |
---|
| 527 | mdd_free(reachStates); |
---|
| 528 | } |
---|
| 529 | } |
---|
| 530 | |
---|
| 531 | if (careBddTable == NIL(st_table)) { |
---|
| 532 | if (fsm && synthInfo->unreachDC) { |
---|
| 533 | /* Upper bound = LowerBould + DC */ |
---|
| 534 | for (i = 0; i < numOut; i++) { |
---|
| 535 | bdd_recursive_deref(ddManager,combUpperBdds[i]); |
---|
| 536 | combUpperBdds[i] = bdd_bdd_or(ddManager,combOutBdds[i], |
---|
| 537 | unReachable); |
---|
| 538 | bdd_ref(combUpperBdds[i]); |
---|
| 539 | } |
---|
| 540 | |
---|
| 541 | /* LowerBound = OutputFuns . Care */ |
---|
| 542 | bdd_recursive_deref(ddManager,unReachable); |
---|
| 543 | for (i = 0; i < numOut; i++) { |
---|
| 544 | bdd_node *temp; |
---|
| 545 | temp = bdd_bdd_and(ddManager,combOutBdds[i],reachable); |
---|
| 546 | bdd_ref(temp); |
---|
| 547 | bdd_recursive_deref(ddManager,combOutBdds[i]); |
---|
| 548 | combOutBdds[i] = temp; |
---|
| 549 | } |
---|
| 550 | bdd_recursive_deref(ddManager,reachable); |
---|
| 551 | } |
---|
| 552 | } else { /* Use the cares supplied. */ |
---|
| 553 | if (fsm && synthInfo->unreachDC) { |
---|
| 554 | bdd_recursive_deref(ddManager,unReachable); |
---|
| 555 | } |
---|
| 556 | for (i = 0; i < numOut; i++) { |
---|
| 557 | bdd_node *dontCare,*care; |
---|
| 558 | |
---|
| 559 | if (st_lookup(careBddTable,combOutNames[i],&ddTemp) == 1) { |
---|
| 560 | if (fsm && synthInfo->unreachDC) { |
---|
| 561 | bdd_ref(care = bdd_bdd_or(ddManager,ddTemp,reachable)); |
---|
| 562 | } else { |
---|
| 563 | bdd_ref(care = ddTemp); |
---|
| 564 | } |
---|
| 565 | bdd_ref(dontCare = bdd_not_bdd_node(care)); |
---|
| 566 | |
---|
| 567 | /* Update the upper bound for each combinational output */ |
---|
| 568 | bdd_recursive_deref(ddManager,combUpperBdds[i]); |
---|
| 569 | combUpperBdds[i] = bdd_bdd_or(ddManager,combOutBdds[i],dontCare); |
---|
| 570 | bdd_ref(combUpperBdds[i]); |
---|
| 571 | bdd_recursive_deref(ddManager,dontCare); |
---|
| 572 | |
---|
| 573 | /* Update the lower bound */ |
---|
| 574 | bdd_ref(temp = bdd_bdd_and(ddManager,combOutBdds[i],care)); |
---|
| 575 | bdd_recursive_deref(ddManager,combOutBdds[i]); |
---|
| 576 | bdd_recursive_deref(ddManager,care); |
---|
| 577 | combOutBdds[i]=temp; |
---|
| 578 | } |
---|
| 579 | } |
---|
| 580 | } |
---|
| 581 | |
---|
| 582 | if (fsm) { |
---|
| 583 | bdd_t *bddVar, *bddTInit, *bddTtemp; |
---|
| 584 | int id, i = 0; |
---|
| 585 | lsGen gen; |
---|
| 586 | Ntk_Node_t *node; |
---|
| 587 | bdd_node *logicZero = bdd_read_logic_zero(ddManager); |
---|
| 588 | |
---|
| 589 | bddTInit = bdd_construct_bdd_t(ddManager,initBdd); |
---|
| 590 | initStates = ALLOC(int, Ntk_NetworkReadNumLatches(network)); |
---|
| 591 | Ntk_NetworkForEachLatch(network,gen,node) { |
---|
| 592 | id = Ntk_NodeReadMddId(node); |
---|
| 593 | bddVar = bdd_get_variable(ddManager,id); |
---|
| 594 | bddTtemp = bdd_cofactor(bddTInit, bddVar); |
---|
| 595 | if (bdd_extract_node_as_is(bddTtemp) == logicZero) |
---|
| 596 | initStates[i] = 0; |
---|
| 597 | else |
---|
| 598 | initStates[i] = 1; |
---|
| 599 | i++; |
---|
| 600 | bdd_free(bddVar); |
---|
| 601 | bdd_free(bddTtemp); |
---|
| 602 | } |
---|
| 603 | /* This will free initBdd too. So, no need to deref it again. */ |
---|
| 604 | bdd_free(bddTInit); |
---|
| 605 | } |
---|
| 606 | |
---|
| 607 | SynthMultiLevelOptimize(network,combOutBdds,combUpperBdds, |
---|
| 608 | combOutNames, initStates,synthInfo, |
---|
| 609 | verbosity); |
---|
| 610 | |
---|
| 611 | /* Clean up. */ |
---|
| 612 | if (fsm) { |
---|
| 613 | FREE(initStates); |
---|
| 614 | } |
---|
| 615 | for (i = 0; i < numOut; i++) { |
---|
| 616 | bdd_recursive_deref(ddManager,combUpperBdds[i]); |
---|
| 617 | bdd_recursive_deref(ddManager,combOutBdds[i]); |
---|
| 618 | } |
---|
| 619 | FREE(combOutNames); |
---|
| 620 | FREE(combOutBdds); |
---|
| 621 | FREE(combUpperBdds); |
---|
| 622 | array_free(inputIds); |
---|
| 623 | if (realign_zdd == 1) |
---|
| 624 | bdd_zdd_realign_enable(ddManager); |
---|
| 625 | else |
---|
| 626 | bdd_zdd_realign_disable(ddManager); |
---|
| 627 | if (realign_bdd == 1) |
---|
| 628 | bdd_realign_enable(ddManager); |
---|
| 629 | else |
---|
| 630 | bdd_realign_disable(ddManager); |
---|
| 631 | return(1); |
---|
| 632 | } |
---|
| 633 | |
---|
| 634 | /**Function******************************************************************** |
---|
| 635 | |
---|
| 636 | Synopsis [Checks whether partition is valid.] |
---|
| 637 | |
---|
| 638 | Description [Checks whether partition is valid. The condition is that the |
---|
| 639 | given partition should have a vertex for each combinational output (PO and |
---|
| 640 | NS) and combinational input (PI and PS) of the network. This is necessary to |
---|
| 641 | completely synthesize the network.] |
---|
| 642 | |
---|
| 643 | SideEffects [None] |
---|
| 644 | |
---|
| 645 | SeeAlso [] |
---|
| 646 | |
---|
| 647 | ******************************************************************************/ |
---|
| 648 | static int |
---|
| 649 | IsPartitionValid(Ntk_Network_t *network, |
---|
| 650 | graph_t *partition) |
---|
| 651 | { |
---|
| 652 | Ntk_Node_t *node; |
---|
| 653 | lsGen gen; |
---|
| 654 | char *name; |
---|
| 655 | |
---|
| 656 | Ntk_NetworkForEachCombOutput(network, gen, node) { |
---|
| 657 | name = Ntk_NodeReadName(node); |
---|
| 658 | if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) { |
---|
| 659 | return(0); |
---|
| 660 | } |
---|
| 661 | } |
---|
| 662 | Ntk_NetworkForEachCombInput(network, gen, node) { |
---|
| 663 | name = Ntk_NodeReadName(node); |
---|
| 664 | if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) { |
---|
| 665 | return(0); |
---|
| 666 | } |
---|
| 667 | } |
---|
| 668 | |
---|
| 669 | return 1; |
---|
| 670 | } |
---|
| 671 | |
---|
| 672 | |
---|
| 673 | /**Function******************************************************************** |
---|
| 674 | |
---|
| 675 | Synopsis [Returns an array containing all combinational output names.] |
---|
| 676 | |
---|
| 677 | Description [Returns an array containing all combinational output names.] |
---|
| 678 | |
---|
| 679 | SideEffects [None] |
---|
| 680 | |
---|
| 681 | SeeAlso [] |
---|
| 682 | |
---|
| 683 | ******************************************************************************/ |
---|
| 684 | static array_t * |
---|
| 685 | GetCombOutputNameArray(Ntk_Network_t *network) |
---|
| 686 | { |
---|
| 687 | array_t *outputFunNames; |
---|
| 688 | lsGen gen; |
---|
| 689 | Ntk_Node_t *node; |
---|
| 690 | |
---|
| 691 | outputFunNames = array_alloc(char *, 0); |
---|
| 692 | if (outputFunNames == NIL(array_t)) { |
---|
| 693 | (void) fprintf(vis_stderr,"** synth error: Could not allocate space "); |
---|
| 694 | (void) fprintf(vis_stderr,"for the names of combinational outputs\n"); |
---|
| 695 | return NIL(array_t); |
---|
| 696 | } |
---|
| 697 | Ntk_NetworkForEachCombOutput(network, gen, node){ |
---|
| 698 | if (Ntk_NodeTestIsLatchInitialInput(node)) |
---|
| 699 | continue; |
---|
| 700 | array_insert_last(char *, outputFunNames, |
---|
| 701 | Ntk_NodeReadName(node)); |
---|
| 702 | } |
---|
| 703 | return outputFunNames; |
---|
| 704 | } |
---|
| 705 | |
---|
| 706 | /**Function******************************************************************** |
---|
| 707 | |
---|
| 708 | Synopsis [Returns an array containing mdd-ids of all combinational inputs.] |
---|
| 709 | |
---|
| 710 | Description [Returns an array containing mdd-ids of all combinational inputs.] |
---|
| 711 | |
---|
| 712 | SideEffects [] |
---|
| 713 | |
---|
| 714 | SeeAlso [] |
---|
| 715 | |
---|
| 716 | ******************************************************************************/ |
---|
| 717 | static array_t * |
---|
| 718 | GetCombInputIdArray(Ntk_Network_t *network) |
---|
| 719 | { |
---|
| 720 | array_t *inputIds; |
---|
| 721 | lsGen gen; |
---|
| 722 | Ntk_Node_t *node; |
---|
| 723 | |
---|
| 724 | inputIds = array_alloc(int, 0); |
---|
| 725 | if (inputIds == NIL(array_t)) { |
---|
| 726 | (void) fprintf(vis_stderr,"** synth error: Could not allocate space "); |
---|
| 727 | (void) fprintf(vis_stderr,"for an array of ids of comb. inputs\n"); |
---|
| 728 | return NIL(array_t); |
---|
| 729 | } |
---|
| 730 | Ntk_NetworkForEachCombInput(network, gen, node){ |
---|
| 731 | array_insert_last(int, inputIds, Ntk_NodeReadMddId(node)); |
---|
| 732 | } |
---|
| 733 | return inputIds; |
---|
| 734 | } |
---|
| 735 | |
---|
| 736 | |
---|
| 737 | /**Function******************************************************************** |
---|
| 738 | |
---|
| 739 | Synopsis [Returns array of bdds of combinational outputs.] |
---|
| 740 | |
---|
| 741 | Description [Returns array of bdds of combinational outputs.] |
---|
| 742 | |
---|
| 743 | SideEffects [None] |
---|
| 744 | |
---|
| 745 | SeeAlso [] |
---|
| 746 | |
---|
| 747 | ******************************************************************************/ |
---|
| 748 | static bdd_node ** |
---|
| 749 | GetBddArray(Mvf_Function_t *combMvfs) |
---|
| 750 | { |
---|
| 751 | bdd_node **bddArray; |
---|
| 752 | Mvf_Function_t *mvf; |
---|
| 753 | int i; |
---|
| 754 | |
---|
| 755 | bddArray = ALLOC(bdd_node *,array_n(combMvfs)); |
---|
| 756 | if (bddArray == NIL(bdd_node *)) { |
---|
| 757 | (void) fprintf(vis_stderr,"** synth error: Could not allocate space "); |
---|
| 758 | (void) fprintf(vis_stderr,"for an array of Bdd nodes.\n"); |
---|
| 759 | return NIL(bdd_node *); |
---|
| 760 | } |
---|
| 761 | arrayForEachItem(Mvf_Function_t *, combMvfs, i, mvf) { |
---|
| 762 | mdd_t *mddTemp; |
---|
| 763 | |
---|
| 764 | mddTemp = array_fetch(mdd_t *, mvf, 1); |
---|
| 765 | bddArray[i] = (bdd_node *) bdd_extract_node_as_is(mddTemp); |
---|
| 766 | bdd_ref(bddArray[i]); |
---|
| 767 | } |
---|
| 768 | return bddArray; |
---|
| 769 | } |
---|
| 770 | |
---|