[14] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [ntmaigCmd.c] |
---|
| 4 | |
---|
| 5 | PackageName [ntmaig] |
---|
| 6 | |
---|
| 7 | Synopsis [Command interface for the Aig partition package] |
---|
| 8 | |
---|
| 9 | Author [Mohammad Awedh] |
---|
| 10 | |
---|
| 11 | Copyright [This file was created at the University of Colorado at |
---|
| 12 | Boulder. The University of Colorado at Boulder makes no warranty |
---|
| 13 | about the suitability of this software for any purpose. It is |
---|
| 14 | presented on an AS IS basis.] |
---|
| 15 | ******************************************************************************/ |
---|
| 16 | |
---|
| 17 | #include "ntmaigInt.h" |
---|
| 18 | |
---|
| 19 | static char rcsid[] UNUSED = "$Id: ntmaigCmd.c,v 1.26 2009/01/18 01:54:51 fabio Exp $"; |
---|
| 20 | |
---|
| 21 | /**AutomaticStart*************************************************************/ |
---|
| 22 | |
---|
| 23 | /*---------------------------------------------------------------------------*/ |
---|
| 24 | /* Static function prototypes */ |
---|
| 25 | /*---------------------------------------------------------------------------*/ |
---|
| 26 | |
---|
| 27 | static int CommandBuildPartitionMAigs(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
| 28 | static int nodenameCompare(const void * node1, const void * node2); |
---|
| 29 | |
---|
| 30 | /**AutomaticEnd***************************************************************/ |
---|
| 31 | |
---|
| 32 | |
---|
| 33 | /*---------------------------------------------------------------------------*/ |
---|
| 34 | /* Definition of exported functions */ |
---|
| 35 | /*---------------------------------------------------------------------------*/ |
---|
| 36 | extern void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep); |
---|
| 37 | extern void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray); |
---|
| 38 | |
---|
| 39 | /**Function******************************************************************** |
---|
| 40 | |
---|
| 41 | Synopsis [Initializes the network to MAIG package.] |
---|
| 42 | |
---|
| 43 | SideEffects [] |
---|
| 44 | |
---|
| 45 | SeeAlso [ntmaig_End] |
---|
| 46 | |
---|
| 47 | ******************************************************************************/ |
---|
| 48 | void |
---|
| 49 | ntmaig_Init(void) |
---|
| 50 | { |
---|
| 51 | Cmd_CommandAdd("build_partition_maigs", CommandBuildPartitionMAigs, /* doesn't changes_network */ 0); |
---|
| 52 | } |
---|
| 53 | |
---|
| 54 | /**Function******************************************************************** |
---|
| 55 | |
---|
| 56 | Synopsis [Ends the network to MAIG package.] |
---|
| 57 | |
---|
| 58 | SideEffects [] |
---|
| 59 | |
---|
| 60 | SeeAlso [ntmaig_Init] |
---|
| 61 | |
---|
| 62 | ******************************************************************************/ |
---|
| 63 | void |
---|
| 64 | ntmaig_End(void) |
---|
| 65 | { |
---|
| 66 | } |
---|
| 67 | |
---|
| 68 | /*---------------------------------------------------------------------------*/ |
---|
| 69 | /* Definition of internal functions */ |
---|
| 70 | /*---------------------------------------------------------------------------*/ |
---|
| 71 | |
---|
| 72 | |
---|
| 73 | /*---------------------------------------------------------------------------*/ |
---|
| 74 | /* Definition of static functions */ |
---|
| 75 | /*---------------------------------------------------------------------------*/ |
---|
| 76 | |
---|
| 77 | |
---|
| 78 | /**Function******************************************************************** |
---|
| 79 | |
---|
| 80 | Synopsis [] |
---|
| 81 | |
---|
| 82 | Description [] |
---|
| 83 | |
---|
| 84 | SideEffects [] |
---|
| 85 | |
---|
| 86 | SeeAlso [] |
---|
| 87 | |
---|
| 88 | ******************************************************************************/ |
---|
| 89 | static int |
---|
| 90 | nodenameCompare( |
---|
| 91 | const void * node1, |
---|
| 92 | const void * node2) |
---|
| 93 | { |
---|
| 94 | Ntk_Node_t *v1, *v2; |
---|
| 95 | char *name1, *name2; |
---|
| 96 | |
---|
| 97 | v1 = *(Ntk_Node_t **)(node1); |
---|
| 98 | v2 = *(Ntk_Node_t **)(node2); |
---|
| 99 | name1 = Ntk_NodeReadName(v1); |
---|
| 100 | name2 = Ntk_NodeReadName(v2); |
---|
| 101 | |
---|
| 102 | return (strcmp(name1, name2)); |
---|
| 103 | } |
---|
| 104 | |
---|
| 105 | /**Function******************************************************************** |
---|
| 106 | |
---|
| 107 | Synopsis [Implements the build_partition_maigs command.] |
---|
| 108 | |
---|
| 109 | Description [] |
---|
| 110 | |
---|
| 111 | CommandName [build_partition_maigs] |
---|
| 112 | |
---|
| 113 | CommandSynopsis [build a partition of MAIGs for the flattened network] |
---|
| 114 | |
---|
| 115 | CommandArguments [\[-h\] \[-d\] \[-n\] ] |
---|
| 116 | |
---|
| 117 | CommandDescription [ |
---|
| 118 | Build the multi-valued AND/INVERTER graph (MAIG) of a flattened network. |
---|
| 119 | It builds the MAIG for the combinational outputs (COs) in terms of the |
---|
| 120 | combinational inputs (CIs). The pointer to this graph is stored in the |
---|
| 121 | network to be used by other commands, such as bounded_model_check. |
---|
| 122 | |
---|
| 123 | This command must be preceded by the commands flatten_hierarchy. This |
---|
| 124 | command will remove any previous build to this graph. |
---|
| 125 | |
---|
| 126 | <p> |
---|
| 127 | |
---|
| 128 | Command options: |
---|
| 129 | <p> |
---|
| 130 | |
---|
| 131 | <dl> |
---|
| 132 | |
---|
| 133 | <dt> -n |
---|
| 134 | <dd> Disable BDD sweeping. |
---|
| 135 | |
---|
| 136 | <p> |
---|
| 137 | <dt> -d |
---|
| 138 | <dd> Build aig structure in depth first manner. |
---|
| 139 | <p> |
---|
| 140 | ] |
---|
| 141 | |
---|
| 142 | SideEffects [] |
---|
| 143 | |
---|
| 144 | SeeAlso [] |
---|
| 145 | |
---|
| 146 | ******************************************************************************/ |
---|
| 147 | static int |
---|
| 148 | CommandBuildPartitionMAigs( |
---|
| 149 | Hrc_Manager_t ** hmgr, |
---|
| 150 | int argc, |
---|
| 151 | char ** argv) |
---|
| 152 | { |
---|
| 153 | Ntk_Node_t *node, *latch; |
---|
| 154 | lsGen gen; |
---|
| 155 | array_t *result; /* array of MvfAig_Function_t* */ |
---|
| 156 | array_t *roots; |
---|
| 157 | st_table *leaves; |
---|
| 158 | array_t *inputs; |
---|
| 159 | Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 160 | mAig_Manager_t *manager; |
---|
| 161 | MvfAig_Function_t *mvfAig; |
---|
| 162 | st_table *nodeToMvfAigTable; /* mapes each node with its mvfAig */ |
---|
| 163 | int c, sweepFlag, DFSFlag; |
---|
| 164 | int i; |
---|
| 165 | |
---|
| 166 | sweepFlag = 1; |
---|
| 167 | DFSFlag = 0; |
---|
| 168 | util_getopt_reset(); |
---|
| 169 | while ((c = util_getopt(argc,argv,"sdnh")) != EOF){ |
---|
| 170 | switch(c){ |
---|
| 171 | case 's': |
---|
| 172 | sweepFlag = 1; |
---|
| 173 | break; |
---|
| 174 | case 'd': |
---|
| 175 | DFSFlag = 1; |
---|
| 176 | break; |
---|
| 177 | case 'n': |
---|
| 178 | sweepFlag = 0; |
---|
| 179 | break; |
---|
| 180 | case 'h': |
---|
| 181 | goto usage; |
---|
| 182 | default: |
---|
| 183 | goto usage; |
---|
| 184 | } |
---|
| 185 | } |
---|
| 186 | if (network == NIL(Ntk_Network_t)) { |
---|
| 187 | return 1; |
---|
| 188 | } |
---|
| 189 | |
---|
| 190 | manager = Ntk_NetworkReadMAigManager(network); |
---|
| 191 | |
---|
| 192 | if (manager == NIL(mAig_Manager_t)) { |
---|
| 193 | manager = mAig_initAig(); |
---|
| 194 | Ntk_NetworkSetMAigManager(network, manager); |
---|
| 195 | /* |
---|
| 196 | mAig_mAigSetNetwork(manager, network); |
---|
| 197 | */ |
---|
| 198 | } |
---|
| 199 | |
---|
| 200 | /* Check if there is already a MvfAigs Table attached to the network */ |
---|
| 201 | nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, |
---|
| 202 | MVFAIG_NETWORK_APPL_KEY); |
---|
| 203 | |
---|
| 204 | if (nodeToMvfAigTable != NIL(st_table)){ |
---|
| 205 | /* |
---|
| 206 | st_foreach_item(nodeToMvfAigTable, stGen, (char **) &node, (char **) &MvfAig) { |
---|
| 207 | printf("\nNode name = %s :",Ntk_NodeReadName(node)); |
---|
| 208 | for (j=0; j< array_n(MvfAig); j++){ |
---|
| 209 | printf(" %d ",array_fetch(bAigEdge_t, (array_t *) MvfAig, j)); |
---|
| 210 | } |
---|
| 211 | } |
---|
| 212 | */ |
---|
| 213 | (void) fprintf(vis_stderr, "maig partition already built; reinvoke\n"); |
---|
| 214 | (void) fprintf(vis_stderr, "flatten_hierarchy to remove the current maig partition\n"); |
---|
| 215 | return 1; |
---|
| 216 | } |
---|
| 217 | |
---|
| 218 | roots = array_alloc(Ntk_Node_t *, 0); |
---|
| 219 | Ntk_NetworkForEachCombOutput(network, gen, node) { |
---|
| 220 | array_insert_last(Ntk_Node_t *, roots, node); |
---|
| 221 | } |
---|
| 222 | Ntk_NetworkForEachNode(network, gen, node) { |
---|
| 223 | if(Ntk_NodeTestIsShadow(node)) continue; |
---|
| 224 | if(Ntk_NodeTestIsCombInput(node)) continue; |
---|
| 225 | if(Ntk_NodeTestIsCombOutput(node))continue; |
---|
| 226 | |
---|
| 227 | if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) { |
---|
| 228 | /** |
---|
| 229 | fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node)); |
---|
| 230 | **/ |
---|
| 231 | array_insert_last(Ntk_Node_t *, roots, node); |
---|
| 232 | } |
---|
| 233 | } |
---|
| 234 | |
---|
| 235 | leaves = st_init_table(st_ptrcmp, st_ptrhash); |
---|
| 236 | |
---|
| 237 | inputs = array_alloc(Ntk_Node_t *, 16); |
---|
| 238 | Ntk_NetworkForEachCombInput(network, gen, node) { |
---|
| 239 | array_insert_last(Ntk_Node_t *, inputs, node); |
---|
| 240 | } |
---|
| 241 | array_sort(inputs, nodenameCompare); |
---|
| 242 | for(i=0; i<array_n(inputs); i++) { |
---|
| 243 | node = array_fetch(Ntk_Node_t *, inputs, i); |
---|
| 244 | st_insert(leaves, node, (char *) ntmaig_UNUSED); |
---|
| 245 | Ntk_NodeSetMAigId(node, |
---|
| 246 | mAig_CreateVar(manager, |
---|
| 247 | Ntk_NodeReadName(node), |
---|
| 248 | Var_VariableReadNumValues(Ntk_NodeReadVariable(node)))); |
---|
| 249 | } |
---|
| 250 | |
---|
| 251 | if(DFSFlag == 0) |
---|
| 252 | bAig_BuildAigBFSManner(network, manager, leaves, sweepFlag); |
---|
| 253 | |
---|
| 254 | result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves); |
---|
| 255 | |
---|
| 256 | nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, |
---|
| 257 | MVFAIG_NETWORK_APPL_KEY); |
---|
| 258 | Ntk_NetworkForEachLatch(network, gen, latch) { |
---|
| 259 | node = Ntk_LatchReadDataInput(latch); |
---|
| 260 | st_lookup(nodeToMvfAigTable, node, &mvfAig); |
---|
| 261 | Ntk_NodeSetMAigId(node, |
---|
| 262 | mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig)); |
---|
| 263 | node = Ntk_LatchReadInitialInput(latch); |
---|
| 264 | st_lookup(nodeToMvfAigTable, node, &mvfAig); |
---|
| 265 | Ntk_NodeSetMAigId(node, |
---|
| 266 | mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig)); |
---|
| 267 | } |
---|
| 268 | |
---|
| 269 | roots->num = 0; |
---|
| 270 | Ntk_NetworkForEachLatch(network, gen, latch) { |
---|
| 271 | if(!st_lookup(nodeToMvfAigTable, latch, &mvfAig)) |
---|
| 272 | array_insert_last(Ntk_Node_t *, roots, latch); |
---|
| 273 | } |
---|
| 274 | result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves); |
---|
| 275 | |
---|
| 276 | array_free(roots); |
---|
| 277 | array_free(inputs); |
---|
| 278 | st_free_table(leaves); |
---|
| 279 | |
---|
| 280 | /* |
---|
| 281 | * Free the array of MvfAigs. |
---|
| 282 | */ |
---|
| 283 | MvfAig_FunctionArrayFree(result); |
---|
| 284 | |
---|
| 285 | if(sweepFlag) |
---|
| 286 | bAig_BddSweepMain(network, 0); |
---|
| 287 | |
---|
| 288 | return 0; |
---|
| 289 | |
---|
| 290 | usage: |
---|
| 291 | (void) fprintf(vis_stderr, "usage: build_partition_maig [-h]\n"); |
---|
| 292 | (void) fprintf(vis_stderr, " -h print the command usage\n"); |
---|
| 293 | (void) fprintf(vis_stderr, " -n disable bdd sweeping\n"); |
---|
| 294 | (void) fprintf(vis_stderr, " -d build AIG DFS manner\n"); |
---|
| 295 | return 1; /* error exit */ |
---|
| 296 | } |
---|