Main Page | Class List | File List | Class Members | File Members

dlx_deep_pipeline_uclid.c

Go to the documentation of this file.
00001 extern "C" {
00002 #include "tarski.h"
00003 
00004 
00005 F
00006 build_dlx_uclid_compare()
00007 {
00008   int depth;
00009 
00010   // first build the spec and the implementation
00011   array_t *spec_array = build_dlx_uclid_spec();
00012   array_t *impl_array = build_dlx_uclid_impl();
00013 
00014   F spec_rf;
00015   spec_rf.raw = array_fetch(Fnode *, spec_array, 0);
00016   F spec_mem;
00017   spec_mem.raw = array_fetch(Fnode *, spec_array, 1);
00018   F spec_pc;
00019   spec_pc.raw = array_fetch(Fnode *, spec_array, 2);
00020   F impl_rf;
00021   impl_rf.raw = array_fetch(Fnode *, impl_array, 0);
00022   F impl_mem;
00023   impl_mem.raw = array_fetch(Fnode *, impl_array, 1);
00024   F impl_pc;
00025   impl_pc.raw = array_fetch(Fnode *, impl_array, 2);
00026 
00027   Net_t *spec_net, *impl_net;
00028   spec_net = Net_CreateFromFormulaArray(spec_array);
00029   impl_net = Net_CreateFromFormulaArray(impl_array);
00030 
00031   // print spec
00032   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00033   //Net_PrintFormula(spec_net, array_fetch(Fnode *, spec_net->formulas,0),  processedTable);
00034   //Net_PrintFormula(spec_net, array_fetch(Fnode *, spec_net->formulas,1),  processedTable);
00035   //return spec_rf;
00036 
00037   // print impl
00038   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00039   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,0),  processedTable);
00040   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,1),  processedTable);
00041   //return spec_rf;
00042   
00043   // hash tables needed for constant propagation
00044   st_table *processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00045   st_table *sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00046   st_table *equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00047 
00048   // project implementation onto specification
00049   F init_flush_dr = br("init_flush_dr");  
00050   init_flush_dr << (TRUE() % TRUE());
00051   F project_dr = br("project_dr");
00052   project_dr << (TRUE() % TRUE());
00053   F no_project_dr = br("no_project_dr");
00054   no_project_dr << (FALSE() % FALSE());
00055   
00056   // constrain the init and next flush inputs
00057   Net_ConstrainInput(impl_net, "init_flush", init_flush_dr.raw);
00058   Net_ConstrainInput(impl_net, "project", project_dr.raw);
00059   array_t *new_impl_array;
00060   
00061   //new_impl_array = array_alloc(Fnode *, 0);
00062   //array_insert_last(Fnode *, new_impl_array, array_fetch(Fnode *, impl_net->formulas, 0));
00063   //array_insert_last(Fnode *, new_impl_array, array_fetch(Fnode *, impl_net->formulas, 1));
00064   //impl_net = Net_CreateFromFormulaArray(impl_array);
00065 
00066   // print impl
00067   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00068   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,0),  processedTable);
00069   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,1),  processedTable);
00070   //return spec_rf;
00071 
00072   F new_impl_rf, new_impl_mem, new_impl_pc;
00073   new_impl_rf.raw = array_fetch(Fnode *, impl_net->formulas, 0);
00074   new_impl_mem.raw = array_fetch(Fnode *, impl_net->formulas, 1);
00075   new_impl_pc.raw = array_fetch(Fnode *, impl_net->formulas, 2);
00076   
00077   // unfold the implementation rf by 6 steps
00078   Fnode *new_impl_rf_unfolded = node_tfe(array_fetch(Fnode *, impl_net->formulas, 0), 6);
00079   // unfold the implementation mem by 5 steps
00080   Fnode *new_impl_mem_unfolded = node_tfe(array_fetch(Fnode *, impl_net->formulas, 1), 5);
00081   // unfold the implementation pc by 5 steps
00082   Fnode *new_impl_pc_unfolded = node_tfe(array_fetch(Fnode *, impl_net->formulas, 2), 5);
00083   
00084   //Net_t *impl_rf_unfolded_net = Net_CreateFromFormula(new_impl_rf_unfolded);
00085   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00086   //Net_PrintFormula(impl_rf_unfolded_net, array_fetch(Fnode *, impl_rf_unfolded_net->formulas,0),  processedTable);
00087   //return new_impl_rf;  
00088 
00089   // now do constant propagation to simplify the rf unfolded 
00090   depth = Net_TopologicalSort(new_impl_rf_unfolded, sortedTable, processedNodes);
00091   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00092   Fnode *simplified_impl_rf_unfolded;
00093   st_lookup(equivalentNodeHash, (char *) new_impl_rf_unfolded, (char **) &simplified_impl_rf_unfolded);
00094 
00095   st_free_table(sortedTable);
00096   st_free_table(equivalentNodeHash);
00097   st_free_table(processedNodes);
00098   
00099   // print the unfolded rf netlist 
00100   //Net_t *impl_rf_unfolded_net = Net_CreateFromFormula(simplified_impl_rf_unfolded);
00101   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00102   //Net_PrintFormula(impl_rf_unfolded_net, array_fetch(Fnode *, impl_rf_unfolded_net->formulas,0),  processedTable);
00103   //return new_impl_rf;
00104 
00105   // constant propagation to simplify mem
00106   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00107   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00108   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00109   
00110   depth = Net_TopologicalSort(new_impl_mem_unfolded, sortedTable, processedNodes);
00111   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00112   Fnode *simplified_impl_mem_unfolded;
00113   st_lookup(equivalentNodeHash, (char *) new_impl_mem_unfolded, (char **) &simplified_impl_mem_unfolded);
00114 
00115   st_free_table(processedNodes);
00116   st_free_table(sortedTable);
00117   st_free_table(equivalentNodeHash);
00118   
00119   // print the unfolded mem netlist 
00120   //Net_t *impl_mem_unfolded_net = Net_CreateFromFormula(simplified_impl_mem_unfolded);
00121   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00122   //Net_PrintFormula(impl_mem_unfolded_net, array_fetch(Fnode *, impl_mem_unfolded_net->formulas,0),  processedTable);
00123   //return new_impl_rf;
00124 
00125 
00126   // constant propagation to simplify pc
00127   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00128   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00129   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00130   
00131   depth = Net_TopologicalSort(new_impl_pc_unfolded, sortedTable, processedNodes);
00132   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00133   Fnode *simplified_impl_pc_unfolded;
00134   st_lookup(equivalentNodeHash, (char *) new_impl_pc_unfolded, (char **) &simplified_impl_pc_unfolded);
00135 
00136   st_free_table(processedNodes);
00137   st_free_table(sortedTable);
00138   st_free_table(equivalentNodeHash);
00139 
00140   // print the unfolded pc netlist 
00141   //Net_t *impl_pc_unfolded_net = Net_CreateFromFormula(simplified_impl_pc_unfolded);
00142   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00143   //Net_PrintFormula(impl_pc_unfolded_net, array_fetch(Fnode *, impl_pc_unfolded_net->formulas,0),  processedTable);
00144   //return new_impl_rf;
00145 
00146   
00147   // Now unconstraint the flush input
00148   Net_UnConstrainInput(impl_net, "init_flush", init_flush_dr.raw);
00149   Net_UnConstrainInput(impl_net, "project", project_dr.raw);
00150   F no_flush = br("no_flush");
00151 
00152   // print impl
00153   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00154   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,0),  processedTable);
00155   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,1),  processedTable);
00156   //return spec_rf;
00157 
00158   
00159   no_flush << (FALSE() % TRUE());
00160   Net_ConstrainInput(impl_net, "init_flush", no_flush.raw);
00161   Net_ConstrainInput(impl_net, "project", no_project_dr.raw);
00162   
00163   new_impl_array = array_alloc(Fnode *, 0);
00164   array_insert_last(Fnode *, new_impl_array, array_fetch(Fnode *, impl_net->formulas, 0));
00165   array_insert_last(Fnode *, new_impl_array, array_fetch(Fnode *, impl_net->formulas, 1));
00166   array_insert_last(Fnode *, new_impl_array, array_fetch(Fnode *, impl_net->formulas, 2));
00167   impl_net = Net_CreateFromFormulaArray(impl_array);
00168   
00169   new_impl_rf.raw = array_fetch(Fnode *, impl_net->formulas, 0);
00170   new_impl_mem.raw = array_fetch(Fnode *, impl_net->formulas, 1);
00171   new_impl_pc.raw = array_fetch(Fnode*, impl_net->formulas, 2);
00172   
00173   // print impl
00174   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00175   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,0),  processedTable);
00176   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,1),  processedTable);
00177   //Net_PrintFormula(impl_net, array_fetch(Fnode *, impl_net->formulas,2),  processedTable);
00178   //return spec_rf;
00179 
00180 
00181   array_t *unfolded_neq_array = array_alloc(Fnode *, 0);
00182   
00183   // IS SPEC RF != NEW_IMPL?
00184   F neq = !(spec_rf == new_impl_rf);
00185   Fnode *neq_tfe = node_tfe(neq.raw, 10);
00186   
00187   F neq_mem = !(spec_mem == new_impl_mem);
00188   Fnode *neq_mem_tfe = node_tfe(neq_mem.raw, 9);
00189   
00190   F neq_pc = !(spec_pc == new_impl_pc);
00191   Fnode *neq_pc_tfe = node_tfe(neq_pc.raw, 9);
00192   
00193   array_insert_last(Fnode *, unfolded_neq_array, neq_tfe);
00194   array_insert_last(Fnode *, unfolded_neq_array, neq_mem_tfe);
00195   array_insert_last(Fnode *, unfolded_neq_array, neq_pc_tfe);
00196   
00197   //Net_t *neq_mem_net = Net_CreateFromFormula(neq_mem.raw);    
00198   // print the neq for mem
00199   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00200   //Net_PrintFormula(neq_mem_net, array_fetch(Fnode *, neq_mem_net->formulas,0),  processedTable);
00201   //return new_impl_rf;  
00202 
00203   Net_t *new_neq_net = Net_CreateFromFormulaArray(unfolded_neq_array);
00204   
00205   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00206   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00207   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00208   //return new_impl_rf;
00209 
00210   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00211   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00212   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00213   
00214   Fnode *neq_rf_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 0);
00215   Fnode *neq_mem_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 1);
00216   Fnode *neq_pc_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 2);
00217     
00218   // first simplify the rf_unfoled
00219   depth = Net_TopologicalSort(neq_rf_unfolded, sortedTable, processedNodes);
00220   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00221   Fnode *new_neq_rf_unfolded;
00222   st_lookup(equivalentNodeHash, (char *) neq_rf_unfolded, (char **) &new_neq_rf_unfolded);
00223   
00224   st_free_table(sortedTable);
00225   st_free_table(equivalentNodeHash);
00226   st_free_table(processedNodes);
00227   
00228 
00229   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00230   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00231   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00232   
00233   // first simplify the mem_unfoled
00234   depth = Net_TopologicalSort(neq_mem_unfolded, sortedTable, processedNodes);
00235   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00236   Fnode *new_neq_mem_unfolded;
00237   st_lookup(equivalentNodeHash, (char *) neq_mem_unfolded, (char **) &new_neq_mem_unfolded);
00238 
00239   st_free_table(sortedTable);
00240   st_free_table(equivalentNodeHash);
00241   st_free_table(processedNodes);
00242 
00243   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00244   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00245   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00246   
00247   // simplify the pc_unfoled
00248   depth = Net_TopologicalSort(neq_pc_unfolded, sortedTable, processedNodes);
00249   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00250   Fnode *new_neq_pc_unfolded;
00251   st_lookup(equivalentNodeHash, (char *) neq_pc_unfolded, (char **) &new_neq_pc_unfolded);
00252 
00253   st_free_table(sortedTable);
00254   st_free_table(equivalentNodeHash);
00255   st_free_table(processedNodes);
00256 
00257 
00258   array_t *new_unfolded_neq_array = array_alloc(Fnode *, 0);
00259   array_insert_last(Fnode *, new_unfolded_neq_array, new_neq_rf_unfolded);
00260   array_insert_last(Fnode *, new_unfolded_neq_array, new_neq_mem_unfolded);
00261   array_insert_last(Fnode *, new_unfolded_neq_array, new_neq_pc_unfolded);
00262   
00263   new_neq_net = Net_CreateFromFormulaArray(new_unfolded_neq_array);
00264   
00265   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00266   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00267   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00268   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00269   //return new_impl_rf;
00270 
00271   // Add a read at the end to enable replacing write with reads
00272   F readAddress = si("rf_read_address");
00273   AddReadatEnd(new_neq_net, readAddress.raw, "read", 0);
00274   F memreadAddress = si("mem_read_address");
00275   AddReadatEnd(new_neq_net, memreadAddress.raw, "read_mem", 1);
00276   
00277   array_t *new_neq_array = array_alloc(Fnode *, 0);
00278   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 0));
00279   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 1));
00280   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 2));
00281   
00282   Net_t *newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00283   Net_FreeNet(new_neq_net);
00284   new_neq_net = newer_neq_net;
00285 
00286   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00287   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00288   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00289   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00290   //return new_impl_rf;
00291   
00292 
00293   Net_ConstrainInput(new_neq_net, "spec_rf0_0", simplified_impl_rf_unfolded);
00294   Net_ConstrainInput(new_neq_net, "spec_pc0_0", simplified_impl_pc_unfolded);
00295   Net_ConstrainInput(new_neq_net, "spec_mem0_0", simplified_impl_mem_unfolded);
00296   
00297   array_free(new_neq_array);
00298   new_neq_array = array_alloc(Fnode *, 0);
00299   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 0));
00300   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 1));
00301   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 2));
00302   
00303   newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00304   Net_FreeNet(new_neq_net);
00305   new_neq_net = newer_neq_net;
00306 
00307   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00308   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00309   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00310   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00311   //return new_impl_rf;
00312 
00313   // do some simplification
00314   
00315   //simplify rf
00316   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00317   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00318   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00319 
00320   neq_rf_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 0);
00321   neq_mem_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 1);
00322   neq_pc_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 2);
00323 
00324   depth = Net_TopologicalSort(neq_rf_unfolded, sortedTable, processedNodes);
00325   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00326   st_lookup(equivalentNodeHash, (char *) neq_rf_unfolded, (char **) &new_neq_rf_unfolded);
00327 
00328   st_free_table(processedNodes);
00329   st_free_table(sortedTable);
00330   st_free_table(equivalentNodeHash);
00331 
00332   //simplify mem
00333   
00334   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00335   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00336   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00337 
00338   depth = Net_TopologicalSort(neq_mem_unfolded, sortedTable, processedNodes);
00339   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00340   st_lookup(equivalentNodeHash, (char *) neq_mem_unfolded, (char **) &new_neq_mem_unfolded);
00341   
00342   st_free_table(processedNodes);
00343   st_free_table(sortedTable);
00344   st_free_table(equivalentNodeHash);
00345 
00346   //simplify pc
00347   
00348   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00349   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00350   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00351 
00352   depth = Net_TopologicalSort(neq_pc_unfolded, sortedTable, processedNodes);
00353   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00354   st_lookup(equivalentNodeHash, (char *) neq_pc_unfolded, (char **) &new_neq_pc_unfolded);
00355   
00356   st_free_table(processedNodes);
00357   st_free_table(sortedTable);
00358   st_free_table(equivalentNodeHash);
00359 
00360 
00361   array_free(new_neq_array);
00362   new_neq_array = array_alloc(Fnode *, 0);
00363   array_insert_last(Fnode *, new_neq_array, new_neq_rf_unfolded);
00364   array_insert_last(Fnode *, new_neq_array, new_neq_mem_unfolded);
00365   array_insert_last(Fnode *, new_neq_array, new_neq_pc_unfolded);
00366   
00367   newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00368   Net_FreeNet(new_neq_net);
00369   new_neq_net = newer_neq_net;
00370 
00371   // print after simplification
00372   Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  NULL);
00373   Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  NULL);
00374   Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  NULL);
00375   return new_impl_rf;
00376   
00377   // we will now call the replace write with read
00378   while(st_lookup(new_neq_net->UIFs, "write", (char **) 0)) {
00379     ReplaceWritewithRead(new_neq_net, "write", "read");
00380     array_free(new_neq_array);
00381     new_neq_array = array_alloc(Fnode *, 0);
00382     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 0));
00383     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 1));
00384     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 2));    
00385     newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00386     Net_FreeNet(new_neq_net);
00387     new_neq_net = newer_neq_net;
00388   }
00389 
00390   //simplify rf
00391   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00392   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00393   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00394   
00395   neq_rf_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 0);
00396   neq_mem_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 1);
00397   neq_pc_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 2);
00398 
00399   depth = Net_TopologicalSort(neq_rf_unfolded, sortedTable, processedNodes);
00400   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00401   st_lookup(equivalentNodeHash, (char *) neq_rf_unfolded, (char **) &new_neq_rf_unfolded);
00402 
00403   st_free_table(processedNodes);
00404   st_free_table(sortedTable);
00405   st_free_table(equivalentNodeHash);
00406 
00407   //simplify mem
00408   
00409   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00410   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00411   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00412 
00413   depth = Net_TopologicalSort(neq_mem_unfolded, sortedTable, processedNodes);
00414   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00415   st_lookup(equivalentNodeHash, (char *) neq_mem_unfolded, (char **) &new_neq_mem_unfolded);
00416 
00417   st_free_table(processedNodes);
00418   st_free_table(sortedTable);
00419   st_free_table(equivalentNodeHash);
00420 
00421   //simplify pc
00422   
00423   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00424   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00425   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00426 
00427   depth = Net_TopologicalSort(neq_pc_unfolded, sortedTable, processedNodes);
00428   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00429   st_lookup(equivalentNodeHash, (char *) neq_pc_unfolded, (char **) &new_neq_pc_unfolded);
00430 
00431   st_free_table(processedNodes);
00432   st_free_table(sortedTable);
00433   st_free_table(equivalentNodeHash);
00434 
00435   array_free(new_neq_array);
00436   new_neq_array = array_alloc(Fnode *, 0);
00437   array_insert_last(Fnode *, new_neq_array, new_neq_rf_unfolded);
00438   array_insert_last(Fnode *, new_neq_array, new_neq_mem_unfolded);
00439   array_insert_last(Fnode *, new_neq_array, new_neq_pc_unfolded);
00440   
00441   newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00442   Net_FreeNet(new_neq_net);
00443   new_neq_net = newer_neq_net;
00444 
00445   // print after replacing write with read
00446   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00447   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00448   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00449   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00450   //return new_impl_rf;
00451 
00452   // we will now call the replace write_mem with read_mem
00453   while(st_lookup(new_neq_net->UIFs, "write_mem", (char **) 0)) {
00454     ReplaceWritewithRead(new_neq_net, "write_mem", "read_mem");
00455     array_free(new_neq_array);
00456     new_neq_array = array_alloc(Fnode *, 0);
00457     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 0));
00458     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 1));
00459     array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 2));
00460     newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00461     Net_FreeNet(new_neq_net);
00462     new_neq_net = newer_neq_net;
00463   }
00464 
00465   // print after replacing write with read
00466   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00467   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00468   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00469   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00470   //return new_impl_rf;
00471 
00472   //simplify rf
00473   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00474   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00475   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00476   
00477   neq_rf_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 0);
00478   neq_mem_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 1);
00479   neq_pc_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 2);
00480 
00481   depth = Net_TopologicalSort(neq_rf_unfolded, sortedTable, processedNodes);
00482   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00483   st_lookup(equivalentNodeHash, (char *) neq_rf_unfolded, (char **) &new_neq_rf_unfolded);
00484 
00485   st_free_table(processedNodes);
00486   st_free_table(sortedTable);
00487   st_free_table(equivalentNodeHash);
00488 
00489   //simplify mem
00490   
00491   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00492   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00493   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00494 
00495   depth = Net_TopologicalSort(neq_mem_unfolded, sortedTable, processedNodes);
00496   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00497   st_lookup(equivalentNodeHash, (char *) neq_mem_unfolded, (char **) &new_neq_mem_unfolded);
00498 
00499   st_free_table(processedNodes);
00500   st_free_table(sortedTable);
00501   st_free_table(equivalentNodeHash);
00502 
00503 
00504   //simplify pc
00505   
00506   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00507   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00508   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00509 
00510   depth = Net_TopologicalSort(neq_pc_unfolded, sortedTable, processedNodes);
00511   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00512   st_lookup(equivalentNodeHash, (char *) neq_pc_unfolded, (char **) &new_neq_pc_unfolded);
00513 
00514   st_free_table(processedNodes);
00515   st_free_table(sortedTable);
00516   st_free_table(equivalentNodeHash);
00517 
00518   array_free(new_neq_array);
00519   new_neq_array = array_alloc(Fnode *, 0);
00520   array_insert_last(Fnode *, new_neq_array, new_neq_rf_unfolded);
00521   array_insert_last(Fnode *, new_neq_array, new_neq_mem_unfolded);
00522   array_insert_last(Fnode *, new_neq_array, new_neq_pc_unfolded);
00523   
00524   newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00525   Net_FreeNet(new_neq_net);
00526   new_neq_net = newer_neq_net;
00527 
00528   // print after replacing write_mem with read_mem
00529   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00530   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00531   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00532   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00533   //return new_impl_rf;
00534 
00535   // Do the bryant reduction to remove UIFs
00536   Net_DoBryantReduction(new_neq_net);
00537   //array_free(new_neq_array);
00538   new_neq_array = array_alloc(Fnode *, 0);
00539   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 0));
00540   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 1));
00541   array_insert_last(Fnode *, new_neq_array, array_fetch(Fnode *, new_neq_net->formulas, 2));
00542 
00543   Net_t *neq_latest_net = Net_CreateFromFormulaArray(new_neq_array);
00544   Net_FreeNet(new_neq_net);
00545   new_neq_net = neq_latest_net;
00546   // do some simplification
00547   
00548   //simplify rf
00549   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00550   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00551   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00552   
00553   neq_rf_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 0);
00554   depth = Net_TopologicalSort(neq_rf_unfolded, sortedTable, processedNodes);
00555   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00556   st_lookup(equivalentNodeHash, (char *) neq_rf_unfolded, (char **) &new_neq_rf_unfolded);
00557   
00558   st_free_table(processedNodes);
00559   st_free_table(sortedTable);
00560   st_free_table(equivalentNodeHash);
00561 
00562   //simplify mem
00563   
00564   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00565   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00566   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00567   
00568   neq_mem_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 1);
00569   depth = Net_TopologicalSort(neq_mem_unfolded, sortedTable, processedNodes);
00570   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00571   st_lookup(equivalentNodeHash, (char *) neq_mem_unfolded, (char **) &new_neq_mem_unfolded);
00572 
00573   st_free_table(processedNodes);
00574   st_free_table(sortedTable);
00575   st_free_table(equivalentNodeHash);
00576 
00577 
00578   //simplify pc
00579   
00580   processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00581   sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
00582   equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00583   
00584   neq_pc_unfolded = array_fetch(Fnode *, new_neq_net->formulas, 2);
00585   depth = Net_TopologicalSort(neq_pc_unfolded, sortedTable, processedNodes);
00586   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
00587   st_lookup(equivalentNodeHash, (char *) neq_pc_unfolded, (char **) &new_neq_pc_unfolded);
00588 
00589   st_free_table(processedNodes);
00590   st_free_table(sortedTable);
00591   st_free_table(equivalentNodeHash);
00592 
00593   array_free(new_neq_array);
00594   new_neq_array = array_alloc(Fnode *, 0);
00595   array_insert_last(Fnode *, new_neq_array, new_neq_rf_unfolded);
00596   array_insert_last(Fnode *, new_neq_array, new_neq_mem_unfolded);
00597   array_insert_last(Fnode *, new_neq_array, new_neq_pc_unfolded);
00598   
00599   newer_neq_net = Net_CreateFromFormulaArray(new_neq_array);
00600   Net_FreeNet(new_neq_net);
00601   new_neq_net = newer_neq_net;
00602   
00603   // print the unfolded netlist after bryantization
00604   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
00605   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,0),  processedTable);
00606   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,1),  processedTable);
00607   //Net_PrintFormula(new_neq_net, array_fetch(Fnode *, new_neq_net->formulas,2),  processedTable);
00608   //return new_impl_rf;
00609   
00610   //Net_PrintVHDL(new_neq_net, stdout, 8);
00611   return impl_rf;
00612 }
00613 
00614 
00615 array_t *
00616 build_dlx_uclid_impl()
00617 {
00618   array_t *result_array = array_alloc(Fnode *, 0);
00619   
00620   F RR = sc("RR");
00621   F RI = sc("RI");
00622   F LD = sc("LD");
00623   F ST = sc("ST");
00624   F BR = sc("BR");
00625 
00626   F pc0 = si("pc0");
00627   F rf0 = si("rf0");
00628   F mem0 = si("mem0");
00629 
00630   F init_flush = bi("init_flush");
00631   F next_flush = TRUE();
00632   F flush      = br("flush");
00633 
00634   F project = bi("project");
00635 
00636   F pPC         = sr("pPC");
00637 
00638   F fdInstr     = sr("fdInstr");
00639   F fdType      = sr("fdType"); // will be from iclass, i.e., RR, RI, LD, ST, BR
00640   F fdPC        = sr("fdPC");
00641   F fdValid     = br("fdValid");
00642 
00643   F pRF         = sr("pRF");
00644 
00645   F deInstr     = sr("deInstr");
00646   F deType      = sr("deType");
00647   F deArg1      = sr("deArg1");
00648   F deArg2      = sr("deArg2");
00649   F dePC        = sr("dePC");
00650   F deValid     = br("deValid");
00651 
00652   F emInstr     = sr("emInstr");
00653   F emType      = sr("emType");
00654   F emValue     = sr("emValue");
00655   F emArg2      = sr("emArg2");
00656   F emBranch    = br("emBranch");
00657   F emTarget    = sr("emTarget");
00658   F emValid     = br("emValid");
00659 
00660   F dMem        = sr("dMem");
00661   F mwData      = sr("mwData");
00662   F mwDest      = sr("mwDest");
00663   F mwValid     = br("mwValid");
00664 
00665   F squash;
00666   F opcodes = list(LD, BR, ST, RR, RI, nil);
00667 
00668   F fdpc0       = si("fdpc0");
00669   F fdi0        = ri("fdi0", opcodes );
00670   F fdvd0       = bi("fdvd0"); 
00671 
00672   F dei0        = ri("dei0", opcodes );
00673   F dea10       = si("dea10");
00674   F dea20       = si("dea20");
00675   F depc0       = si("depc0");
00676   //F devd0     = bi("devd0");
00677   F devd0       = FALSE();
00678 
00679   F emi0        = ri("emi0", opcodes );
00680   F emv0        = si("emv0");
00681   F ema20       = si("ema20");
00682   F embr0       = bi("embr0"); // boolean
00683   F emtgt0      = si("emtgt0");
00684   F emvd0       = bi("emvd0"); 
00685 
00686 
00687   F mwda0       = si("mwda0");
00688   F mwde0       = si("mwde0");
00689   F mwvd0       = bi("mwvd0");
00690 
00691   // stall logic
00692   F stall_0 =   ( uif( "dest", deInstr ) == uif( "src1", fdInstr ) ) 
00693                 |
00694                  (  ( uif( "dest", deInstr ) == uif( "src2", fdInstr ) ) &
00695                        (  (fdType == RR) | ( (fdType == ST) | (fdType == BR ) ) ) );
00696   F stall =  (deType == LD) & 
00697     (  (deValid & fdValid ) &  stall_0 );
00698   
00699   F instr_fd_valid = br("instr_fd_valid");
00700   instr_fd_valid << (TRUE() % (instr_fd_valid & stall));
00701 
00702   F instr_de_valid = br("instr_de_valid");
00703   instr_de_valid << (FALSE() % (instr_fd_valid & !stall));
00704   
00705   F instr_em_valid = br("instr_em_valid");
00706   instr_em_valid << (FALSE() % (instr_de_valid));
00707 
00708   F instr_mw_valid = br("instr_mw_valid");
00709   instr_mw_valid << (FALSE() % (instr_mw_valid | instr_em_valid));
00710 
00711 
00712   // squash when branch taken
00713   squash = emBranch; 
00714 
00715   F squash_flag = br("squash_flag");
00716   squash_flag << (FALSE() % (squash_flag | squash));
00717   
00718   // flush also needs to be stalled  
00719   F new_next_flush = ((FALSE()) | squash_flag) | ((!squash | project | instr_mw_valid) & next_flush);
00720   F flush_ns = ((stall & !squash) & flush) | ((!stall | squash) & new_next_flush); 
00721   flush << (init_flush % flush_ns);
00722 
00723   // fwd1 logic
00724   F fwd1_0 = emValid & 
00725              ( ( emType == RR ) | ( emType == RI ) ) & 
00726              ( uif( "dest", emInstr ) == uif( "src1", deInstr ) );
00727 
00728   F fwd1_1 = mwValid &  ( mwDest == uif( "src1", deInstr ) );
00729   F fwd1_tmp = mux( fwd1_1, mwData, deArg1 );
00730   F fwd1 = mux( fwd1_0, emValue, fwd1_tmp );
00731 
00732   // fwd2 logic
00733   F fwd2_0 = emValid & 
00734              ( ( emType == RR ) | ( emType == RI ) ) & 
00735              ( uif( "dest", emInstr ) == uif( "src2", deInstr ) );
00736 
00737   F fwd2_1 = mwValid &  ( mwDest == uif( "src2", deInstr ) );
00738   F fwd2_tmp = mux( fwd2_1, mwData, deArg2 );
00739   F fwd2 = mux( fwd2_0, emValue, fwd2_tmp );
00740 
00741   // aluarg2 logic
00742   F aluarg2_0 = ( deType == RI ) | ( deType == ST ) | ( deType == LD );
00743 
00744   F aluarg2 = mux( aluarg2_0, uif("imm", deInstr), fwd2 );
00745 
00746   // given an instruction i, determine its type
00747   // logic defined in the function itype
00748 
00749   F init_pPC = pc0;
00750   F next_pPC = mux( emBranch, emTarget, mux( stall | flush, pPC, uif("succ", pPC ) ) );
00751 
00752   pPC << ( init_pPC % next_pPC );
00753 
00754   F init_fdInstr = fdi0;
00755   F next_fdInstr = mux( (stall | flush), fdInstr, uif("imem", pPC ) );
00756 
00757   fdInstr << ( init_fdInstr % next_fdInstr );
00758 
00759   fdType << ( restrict(fdi0, opcodes) % restrict( next_fdInstr, opcodes ) );
00760 
00761   fdPC << ( fdpc0 % mux( stall, fdPC, pPC ) );
00762 
00763   fdValid << ( fdvd0 % ( ( stall | !flush ) & !squash ) );
00764 
00765   F next_pRF = mux( mwValid, uif3( "write", pRF, mwDest, mwData ), pRF );
00766   pRF << ( rf0 % next_pRF );
00767 
00768   deInstr << ( dei0 % fdInstr );
00769   deType << (dei0 % fdType);
00770 
00771   deArg1 << ( dea10 % uif2( "read", next_pRF, uif("src1", fdInstr ) ) ); 
00772   deArg2 << ( dea20 % uif2( "read", next_pRF, uif("src2", fdInstr ) ) ); 
00773 
00774   dePC << ( depc0 % fdPC );
00775 
00776   deValid << ( devd0 % (  (!squash) & (!stall) & fdValid ) ); 
00777 
00778   emInstr << ( emi0 % deInstr );
00779   emType << ( emi0 % deType );
00780 
00781   F next_emValue = uif3("alu", uif("op", deInstr), fwd1, aluarg2 );
00782   emValue << ( emv0 % next_emValue );
00783 
00784   emArg2 << ( ema20 % fwd2 );
00785 
00786   F init_emBranch = emvd0 & ( ( emi0 == BR) & embr0 );
00787   F next_emBranch = uir3("take", uif("op", deInstr ), fwd1, fwd2 ) & 
00788                         ( (!squash) & ( deValid & ( deType == BR ) ) );
00789 
00790   emBranch << ( init_emBranch % next_emBranch );
00791 
00792   emTarget << ( emtgt0 % uif2( "targ", dePC, uif("imm", deInstr ) ) );
00793 
00794   emValid << ( emvd0 % ( !squash & deValid ) );
00795 
00796   F next_dMem = mux( (emType == ST ) & emValid, 
00797                                 uif3("write_mem", dMem, emValue, emArg2 ), 
00798                                 dMem );
00799 
00800   dMem << ( mem0 % next_dMem );
00801 
00802   mwData << ( mwda0 % mux( (emType == LD), uif2("read_mem", dMem, emValue ), emValue ) ); 
00803 
00804   mwDest << ( mwde0 % uif("dest", emInstr ) );
00805 
00806   mwValid << ( mwvd0 % ( emValid & 
00807                        ( ( emType == RI ) | 
00808                          ( emType == RR ) | 
00809                          ( emType == LD ) ) ) );
00810   
00811   array_insert_last(Fnode *, result_array, pRF.raw);
00812   array_insert_last(Fnode *, result_array, dMem.raw);
00813   array_insert_last(Fnode *, result_array, pPC.raw);
00814   return result_array;
00815 }
00816 
00817 array_t * 
00818 build_dlx_uclid_spec() 
00819 {
00820   array_t *result_array = array_alloc(Fnode *, 0);
00821 
00822   // constants corresponding to opcodes
00823   F RR = sc("RR"); 
00824   F RI = sc("RI");
00825   F LD = sc("LD");
00826   F ST = sc("ST");
00827   F BR = sc("BR");
00828 
00829   F stall = TRUE ();
00830   F stall0 = br("stall0");
00831   F stall0_init = FALSE();
00832   F stall0_ns = stall;
00833 
00834   stall0 << (stall0_init % stall0_ns);
00835   
00836   F sPC = sr("sPC"); // program counter (PC)
00837   F pc0 = si("spec_pc0"); // initial value of PC
00838 
00839   F sRF = sr("sRF"); // Register File (RF)
00840   F rf0 = si("spec_rf0"); // initial value of RF
00841 
00842   F sMem = sr("sMem"); // Data Memory (Mem)
00843   F mem0 = si("spec_mem0"); // initial value of mem
00844   
00845   F instr = uif("imem", sPC); // instruction is a UIF, arg PC
00846   F opcodes = list(LD, BR, ST, RR, RI, nil); // opcodes can only be among this list
00847   
00848   F sType = restrict(instr, opcodes);
00849   F arg1 = uif2("read", 
00850                 sRF,
00851                 uif("src1",
00852                     instr));
00853   F select_imm = ( (sType == RI) | (sType == ST) | (sType == LD)); 
00854   F arg2 = mux(select_imm,
00855                uif("imm",
00856                    instr),
00857                uif2("read",
00858                     sRF,
00859                     uif("src2",
00860                         instr)));
00861   F aluval = uif3("alu",
00862                   uif("op",
00863                       instr),
00864                   arg1,
00865                   arg2);
00866 
00867   F select_ld = (sType == LD);
00868   F writeval = mux(select_ld,
00869                    uif2("read_mem",
00870                         sMem,
00871                         aluval),
00872                    aluval);
00873   F takeBranch = (sType == BR) & uir3("take", 
00874                                       uif("op",
00875                                           instr),
00876                                       arg1,
00877                                       arg2);
00878   F target = uif2("targ",
00879                   sPC,
00880                   uif("imm",
00881                       instr));
00882 
00883   
00884   F sPC_changes = (!stall0);
00885   F sPC_change_value = mux(takeBranch,
00886                            target,
00887                            uif("succ",
00888                                sPC));
00889   
00890   F next_sPC = mux(sPC_changes,
00891                    sPC_change_value,
00892                    sPC);
00893   sPC << (pc0 % next_sPC);
00894 
00895   F sRF_changes = ((sType == RI) | (sType == RR) | (sType == LD)) & (!stall0);
00896 
00897   F next_sRF = mux(sRF_changes,
00898                    uif3("write",
00899                         sRF,
00900                         uif("dest",
00901                             instr),
00902                         writeval),
00903                    sRF);
00904   
00905   sRF << (rf0 % next_sRF);
00906   
00907   F mem_changes = (sType == ST) & (!stall0);
00908   
00909   F next_mem = mux(mem_changes,
00910                    uif3("write_mem",
00911                         sMem,
00912                         aluval,
00913                         uif2("read",
00914                              sRF,
00915                              uif("src2", 
00916                                  instr))),
00917                    sMem);
00918   sMem << (mem0 % next_mem);               
00919   array_insert_last(Fnode *, result_array, sRF.raw);
00920   array_insert_last(Fnode *, result_array, sMem.raw);
00921   array_insert_last(Fnode *, result_array, sPC.raw);
00922   return result_array;
00923  }
00924 
00925 
00926 F
00927 build_dlx_uclid_superscalar()
00928 {
00929   
00930   F RR = sc("RR");
00931   F RI = sc("RI");
00932   F LD = sc("LD");
00933   F ST = sc("ST");
00934   F BR = sc("BR");
00935 
00936   F pc0 = si("pc0");
00937   F rf0 = si("rf0");
00938   F mem0 = si("mem0");
00939 
00940   F flush   = br("flush");  
00941   F flush1  = br("flush1");
00942   F flush2  = br("flush2");
00943   F flush3  = br("flush3");
00944   F flush4  = br("flush4");
00945 
00946   F pPC         = sr("pPC");
00947   
00948   F fdInstr     = sr("fdInstr");
00949   F fdType      = sr("fdType"); // will be from iclass, i.e., RR, RI, LD, ST, BR
00950   F fdPC        = sr("fdPC");
00951   F fdValid     = br("fdValid");
00952 
00953   // pipeline registers for the second instruction
00954   F fd2Instr    = sr("fd2Instr");
00955   F fd2Type     = sr("fd2Type");
00956   F fd2PC       = sr("fd2PC");
00957   F fd2Valid    = br("fd2Valid");
00958 
00959   F pRF         = sr("mem@pRF");
00960 
00961   F deInstr     = sr("deInstr");
00962   F deType      = sr("deType");
00963   F deArg1      = sr("deArg1");
00964   F deArg2      = sr("deArg2");
00965   F dePC        = sr("dePC");
00966   F deValid     = br("deValid");
00967 
00968   F de2Instr     = sr("de2Instr");
00969   F de2Type      = sr("de2Type");
00970   F de2Arg1      = sr("de2Arg1");
00971   F de2Arg2      = sr("de2Arg2");
00972   F de2PC        = sr("de2PC");
00973   F de2Valid     = br("de2Valid");
00974 
00975   F emInstr     = sr("emInstr");
00976   F emType      = sr("emType");
00977   F emValue     = sr("emValue");
00978   F emArg2      = sr("emArg2");
00979   F emBranch    = br("emBranch");
00980   F emTarget    = sr("emTarget");
00981   F emValid     = br("emValid");
00982 
00983   F em2Instr     = sr("em2Instr");
00984   F em2Type      = sr("em2Type");
00985   F em2Value     = sr("em2Value");
00986   F em2Arg2      = sr("em2Arg2");
00987   F em2Branch    = br("em2Branch");
00988   F em2Target    = sr("em2Target");
00989   F em2Valid     = br("em2Valid");
00990 
00991   F dMem        = sr("mem@dMem");
00992   F mwData      = sr("mwData");
00993   F mwDest      = sr("mwDest");
00994   F mwValid     = br("mwValid");
00995   F mwInstr     = sr("mwInstr");
00996 
00997   F mw2Data      = sr("mw2Data");
00998   F mw2Dest      = sr("mw2Dest");
00999   F mw2Valid     = br("mw2Valid");
01000   F mw2Instr     = sr("mw2Instr");
01001 
01002   F squash;
01003   //F opcodes = list(LD, BR, ST, RR, RI, nil);
01004   F opcodes = list(LD, RR, RI, nil);
01005 
01006   F fdpc0       = si("fdpc0");
01007   F fdi0        = ri("fdi0", opcodes );
01008   F fdvd0       = FALSE();
01009 
01010   F fd2pc0      = si("fd2pc0");
01011   F fd2i0       = ri("fd2i0", opcodes );
01012   F fd2vd0      = FALSE();
01013   
01014   F dei0        = ri("dei0", opcodes );
01015   F dea10       = si("dea10");
01016   F dea20       = si("dea20");
01017   F depc0       = si("depc0");
01018   F devd0       = FALSE();
01019   
01020   F de2i0       = ri("de2i0", opcodes );
01021   F de2a10      = si("de2a10");
01022   F de2a20      = si("de2a20");
01023   F de2pc0      = si("de2pc0");
01024   F de2vd0      = FALSE();
01025 
01026   F emi0        = ri("emi0", opcodes );
01027   F emv0        = si("emv0");
01028   F ema20       = si("ema20");
01029   F embr0       = bi("embr0"); // boolean
01030   F emtgt0      = si("emtgt0");
01031   F emvd0       = FALSE();
01032 
01033   F em2i0       = ri("em2i0", opcodes );
01034   F em2v0       = si("em2v0");
01035   F em2a20      = si("em2a20");
01036   F em2br0      = bi("em2br0"); // boolean
01037   F em2tgt0     = si("em2tgt0");
01038   F em2vd0      = FALSE();
01039 
01040   F mwi0        = ri("mwi0", opcodes);
01041   F mwda0       = si("mwda0");
01042   F mwde0       = si("mwde0");
01043   F mwvd0       = FALSE();
01044 
01045   F mw2i0        = ri("mw2i0", opcodes);
01046   F mw2da0       = si("mw2da0");
01047   F mw2de0       = si("mw2de0");
01048   F mw2vd0       = FALSE();
01049 
01050   // stall logic for first instruction
01051   F stall_first_instr_0 =   ( uif( "dest", deInstr ) == uif( "src1", fdInstr ) ) 
01052                              |
01053                              (  ( uif( "dest", deInstr ) == uif( "src2", fdInstr ) ) &
01054                                 (  (fdType == RR) | ( (fdType == ST) | (fdType == BR ) ) ) );
01055   F stall_first_instr_1 =  (deType == LD) & 
01056                            ((deValid & fdValid) &  stall_first_instr_0);
01057 
01058   F stall_first_instr_2 = (uif("dest", de2Instr) == uif("src1", fdInstr)) | 
01059     ((uif("dest", de2Instr) == uif("src2", fdInstr)) &
01060      ((fdType == RR) | ((fdType == ST) | (fdType == BR))));
01061 
01062   F stall_first_instr_3 = (de2Type == LD) & ((de2Valid & fdValid) & stall_first_instr_2);
01063 
01064   F stall_first_instr = (stall_first_instr_1 | stall_first_instr_3);
01065 
01066   // stall logic for second instruction
01067   F stall_second_instr_basic = (fdValid & fd2Valid) & (((uif("dest", fdInstr) == uif("src1", fd2Instr)) | ((uif("dest", fdInstr) == uif("src2", fd2Instr)) &
01068                                                                                                             ((fd2Type == RR) | ((fd2Type == ST) | (fd2Type == BR))))) |
01069                                                        (uif("dest", fdInstr) == uif("dest", fd2Instr)));
01070   
01071 
01072   F stall_second_instr_0 =   ( uif( "dest", deInstr ) == uif( "src1", fd2Instr ) ) 
01073                              |
01074                              (  ( uif( "dest", deInstr ) == uif( "src2", fd2Instr ) ) &
01075                                 (  (fd2Type == RR) | ( (fd2Type == ST) | (fd2Type == BR ) ) ) );
01076 
01077   F stall_second_instr_1 =  (deType == LD) & 
01078                             ((deValid & fd2Valid) &  stall_second_instr_0);
01079 
01080   F stall_second_instr_2 = (uif("dest", de2Instr) == uif("src1", fd2Instr)) | 
01081     ((uif("dest", de2Instr) == uif("src2", fd2Instr)) &
01082      ((fd2Type == RR) | ((fd2Type == ST) | (fd2Type == BR))));
01083 
01084   F stall_second_instr_3 = (de2Type == LD) & ((de2Valid & fd2Valid) & stall_second_instr_2);
01085 
01086   F stall_second_instr = (stall_second_instr_1 | stall_second_instr_3) | stall_second_instr_basic;
01087   
01088   F branch_stall = (fdValid & fd2Valid) & (fdType == BR) & (fd2Type == BR);
01089 
01090   F stall = ((stall_first_instr | stall_second_instr) | branch_stall);
01091 
01092   // squash logic
01093   squash = (emBranch | em2Branch); 
01094 
01095   // the flush logic (for now let us only include stalls in the equation )
01096   F next_flush4 = ((stall & flush4) | (!stall & TRUE()));
01097   F next_flush3 = ((stall & flush3) | (!stall & flush4));
01098   F next_flush2 = ((stall & flush2) | (!stall & flush3));
01099   F next_flush1 = ((stall & flush1) | (!stall & flush2));
01100   F next_flush = ((stall & flush) | (!stall & flush1));
01101 
01102   flush4 << (FALSE() % next_flush4);
01103   flush3 <<(FALSE() % next_flush3);
01104   flush2 << (FALSE() % next_flush2);
01105   flush1 << (FALSE() % next_flush1);
01106   flush << (FALSE() % next_flush);
01107 
01108   // fwd1 logic
01109   F fwd1_0 = emValid & 
01110              ( ( emType == RR ) | ( emType == RI ) ) & 
01111              ( uif( "dest", emInstr ) == uif( "src1", deInstr ) );
01112 
01113   F fwd1_1 = mwValid &  ( mwDest == uif( "src1", deInstr ) );
01114   F fwd1_tmp = mux( fwd1_1, mwData, deArg1 );
01115   F fwd1_first = mux( fwd1_0, emValue, fwd1_tmp );
01116 
01117   // logic to determine forwarding from the second instruction
01118   F fwd1_2 = em2Valid &
01119     (( em2Type == RR) | (em2Type == RI)) & 
01120     (uif("dest", em2Instr) == uif("src1", deInstr));
01121 
01122   F fwd1_3 = mw2Valid & (mw2Dest == uif("src1", deInstr));
01123   F fwd1_tmp2 = mux (fwd1_3, mw2Data, fwd1_first);
01124 
01125   F fwd1 = mux(fwd1_2, em2Value, fwd1_tmp2);
01126 
01127   // fwd2 logic
01128   F fwd2_0 = emValid & 
01129              ( ( emType == RR ) | ( emType == RI ) ) & 
01130              ( uif( "dest", emInstr ) == uif( "src2", deInstr ) );
01131 
01132   F fwd2_1 = mwValid &  ( mwDest == uif( "src2", deInstr ) );
01133   F fwd2_tmp = mux( fwd2_1, mwData, deArg2 );
01134   F fwd2_first = mux( fwd2_0, emValue, fwd2_tmp );
01135   
01136   // logic to determine forwarding from the second instruction
01137   F fwd2_2 = em2Valid &
01138     ((em2Type == RR) | (em2Type == RI)) &
01139     ( uif("dest", em2Instr) == uif("src2", deInstr));
01140   
01141   F fwd2_3 = mw2Valid & (mw2Dest == uif("src2", deInstr));
01142   F fwd2_tmp2 = mux(fwd2_3, mw2Data, fwd2_first);
01143   F fwd2 = mux(fwd2_2, em2Value, fwd2_tmp2);
01144 
01145   // aluarg2 logic
01146   F aluarg2_0 = ( deType == RI ) | ( deType == ST ) | ( deType == LD );
01147   F aluarg2 = mux( aluarg2_0, uif("imm", deInstr), fwd2 );
01148 
01149 
01150   // Forward logic for second instruction
01151 
01152   // fwd1 logic for 2nd instr
01153   F second_fwd1_0 = emValid & 
01154     ( ( emType == RR ) | ( emType == RI ) ) & 
01155     ( uif( "dest", emInstr ) == uif( "src1", de2Instr ) );
01156 
01157   F second_fwd1_1 = mwValid &  ( mwDest == uif( "src1", de2Instr ) );
01158   F second_fwd1_tmp = mux( second_fwd1_1, mwData, de2Arg1 );
01159   F second_fwd1_first = mux( second_fwd1_0, emValue, second_fwd1_tmp );
01160 
01161   // logic to determine forwarding from the second instruction
01162   F second_fwd1_2 = em2Valid &
01163     (( em2Type == RR) | (em2Type == RI)) & 
01164     (uif("dest", em2Instr) == uif("src1", de2Instr));
01165 
01166   F second_fwd1_3 = mw2Valid & (mw2Dest == uif("src1", de2Instr));
01167   F second_fwd1_tmp2 = mux (second_fwd1_3, mw2Data, second_fwd1_first);
01168 
01169   F second_fwd1 = mux(second_fwd1_2, em2Value, second_fwd1_tmp2);
01170 
01171   // fwd2 logic for 2nd_instr
01172   F second_fwd2_0 = emValid & 
01173              ( ( emType == RR ) | ( emType == RI ) ) & 
01174              ( uif( "dest", emInstr ) == uif( "src2", de2Instr ) );
01175 
01176   F second_fwd2_1 = mwValid &  ( mwDest == uif( "src2", de2Instr ) );
01177   F second_fwd2_tmp = mux( second_fwd2_1, mwData, de2Arg2 );
01178   F second_fwd2_first = mux( second_fwd2_0, emValue, second_fwd2_tmp );
01179   
01180   // logic to determine forwarding from the second instruction
01181   F second_fwd2_2 = em2Valid &
01182     ((em2Type == RR) | (em2Type == RI)) &
01183     ( uif("dest", em2Instr) == uif("src2", de2Instr));
01184   
01185   F second_fwd2_3 = mw2Valid & (mw2Dest == uif("src2", de2Instr));
01186   F second_fwd2_tmp2 = mux(second_fwd2_3, mw2Data, second_fwd2_first);
01187   F second_fwd2 = mux(second_fwd2_2, em2Value, second_fwd2_tmp2);
01188 
01189   // aluarg2 logic
01190   F second_aluarg2_0 = ( de2Type == RI ) | ( de2Type == ST ) | ( de2Type == LD );
01191   F second_aluarg2 = mux( second_aluarg2_0, uif("imm", de2Instr), second_fwd2 );  
01192 
01193 
01194   // given an instruction i, determine its type
01195   // logic defined in the function itype
01196 
01197   F init_pPC = pc0;
01198   F next_pPC = mux( emBranch, emTarget, mux( stall | flush, pPC, uif("succ", pPC ) ) );
01199 
01200   pPC << ( init_pPC % next_pPC );
01201 
01202   // first instruction
01203   F init_fdInstr = fdi0;
01204   F next_fdInstr = mux( (stall | flush), fdInstr, uif("first_instr", pPC ) );
01205   fdInstr << ( init_fdInstr % next_fdInstr );
01206   fdType << ( restrict(fdi0, opcodes) % restrict( next_fdInstr, opcodes ) );
01207   fdPC << ( fdpc0 % mux( stall, fdPC, pPC ) );
01208   fdValid << ( fdvd0 % ( ( stall | !flush ) & !squash ) );
01209 
01210   // second instruction
01211   F init_fd2Instr = fd2i0;
01212   F next_fd2Instr = mux( (stall | flush), fd2Instr, uif("second_instr", pPC ) );
01213   fd2Instr << ( init_fd2Instr % next_fd2Instr );
01214   fd2Type << ( restrict(fd2i0, opcodes) % restrict( next_fd2Instr, opcodes ) );
01215   fd2PC << ( fd2pc0 % mux( stall, fd2PC, pPC ) );
01216   fd2Valid << ( fd2vd0 % ( ( stall | !flush ) & !squash ) );
01217 
01218 
01219   // register file
01220   F next_pRF = mux( mwValid, uif3("mem#write", pRF, mwDest, mwData ), pRF );
01221   F next_pRF2 = mux( mw2Valid, uif3("mem#write", pRF, mw2Dest, mw2Data ), next_pRF );
01222 
01223   pRF << ( rf0 % next_pRF2 );
01224 
01225 
01226   // decode stage for first instruction
01227   deInstr << ( dei0 % fdInstr );
01228   deType << (dei0 % fdType);
01229 
01230   // we need to change the assignment to deArg1 and deArg2, they cannot access next_pRF, only pRF is possible
01231   F mwDest_eq_fdSrc1 = (mwDest == uif("src1", fdInstr));
01232   F next_deArg1 = mux (mwValid, mux(mwDest_eq_fdSrc1, mwData, uif2("mem@read", pRF, uif("src1", fdInstr))), uif2("mem@read", pRF, uif("src1", fdInstr)));
01233   
01234   // look for second instruction also
01235   F mw2Dest_eq_fdSrc1 = (mw2Dest == uif("src1", fdInstr));
01236   F second_next_deArg1 = mux(mw2Valid , mux(mw2Dest_eq_fdSrc1, mw2Data, next_deArg1), next_deArg1);
01237   
01238   deArg1 << ( dea10 % second_next_deArg1 ); 
01239 
01240   F mwDest_eq_fdSrc2 = (mwDest == uif("src2", fdInstr));
01241   F next_deArg2 = mux (mwValid, mux(mwDest_eq_fdSrc2, mwData, uif2("mem@read", pRF, uif("src2", fdInstr))), uif2("mem@read", pRF, uif("src2", fdInstr)));
01242   
01243   // look for second instruction for Arg2
01244   F mw2Dest_eq_fdSrc2 = (mw2Dest == uif("src2", fdInstr));
01245   F second_next_deArg2 = mux (mw2Valid, mux(mw2Dest_eq_fdSrc2, mw2Data, next_deArg2), next_deArg2);
01246   deArg2 << ( dea20 % second_next_deArg2 );
01247 
01248   dePC << ( depc0 % fdPC );
01249   deValid << ( devd0 % (  (!squash) & (!stall) & fdValid ) ); 
01250 
01251   // decode stage for second instruction
01252 
01253   de2Instr << (de2i0 % fd2Instr );
01254   de2Type << (de2i0 % fd2Type);
01255 
01256   // we need to change the assignment to de2Arg1 and de2Arg2, they cannot access next_pRF, only pRF is possible
01257   F mwDest_eq_fd2Src1 = (mwDest == uif("src1", fd2Instr));
01258   F next_de2Arg1 = mux (mwValid, mux(mwDest_eq_fd2Src1, mwData, uif2("mem@read", pRF, uif("src1", fd2Instr))), uif2("mem@read", pRF, uif("src1", fd2Instr)));
01259   
01260   // look for second instruction also
01261   F mw2Dest_eq_fd2Src1 = (mw2Dest == uif("src1", fd2Instr));
01262   F second_next_de2Arg1 = mux(mw2Valid , mux(mw2Dest_eq_fd2Src1, mw2Data, next_de2Arg1), next_de2Arg1);
01263   
01264   de2Arg1 << ( de2a10 % second_next_de2Arg1 ); 
01265 
01266   F mwDest_eq_fd2Src2 = (mwDest == uif("src2", fd2Instr));
01267   F next_de2Arg2 = mux (mwValid, mux(mwDest_eq_fd2Src2, mwData, uif2("mem@read", pRF, uif("src2", fd2Instr))), uif2("mem@read", pRF, uif("src2", fd2Instr)));
01268   
01269   // look for second instruction for Arg2
01270   F mw2Dest_eq_fd2Src2 = (mw2Dest == uif("src2", fd2Instr));
01271   F second_next_de2Arg2 = mux (mw2Valid, mux(mw2Dest_eq_fd2Src2, mw2Data, next_de2Arg2), next_de2Arg2);
01272   de2Arg2 << ( de2a20 % second_next_de2Arg2 );
01273 
01274   de2PC << ( depc0 % fd2PC );
01275   de2Valid << ( de2vd0 % (  (!squash) & (!stall) & fd2Valid ) ); 
01276   
01277 
01278   // execute stage for first instruction
01279   emInstr << ( emi0 % deInstr );
01280   emType << ( emi0 % deType );
01281   F next_emValue = uif3("alu", uif("op", deInstr), fwd1, aluarg2 );
01282   emValue << ( emv0 % next_emValue );
01283   emArg2 << ( ema20 % fwd2 );
01284 
01285   F init_emBranch = emvd0 & ( ( emi0 == BR) & embr0 );
01286   F next_emBranch = uir3("take", uif("op", deInstr ), fwd1, fwd2 ) & 
01287                         ( (!squash) & ( deValid & ( deType == BR ) ) );
01288 
01289   emBranch << ( init_emBranch % next_emBranch );
01290   emTarget << ( emtgt0 % uif2( "targ", dePC, uif("imm", deInstr ) ) );
01291   emValid << ( emvd0 % ( !squash & deValid ) );
01292 
01293   // execute stage for second instruction
01294   em2Instr << ( em2i0 % de2Instr );
01295   em2Type << ( em2i0 % de2Type );
01296   F next_em2Value = uif3("alu", uif("op", de2Instr), second_fwd1, second_aluarg2 );
01297   em2Value << ( em2v0 % next_em2Value );
01298   em2Arg2 << ( em2a20 % second_fwd2 );
01299 
01300   F init_em2Branch = em2vd0 & ( ( em2i0 == BR) & em2br0 );
01301   F next_em2Branch = uir3("take", uif("op", de2Instr ), second_fwd1, second_fwd2 ) & 
01302                         ( (!squash) & ( de2Valid & ( de2Type == BR ) ) );
01303 
01304   em2Branch << ( init_em2Branch % next_em2Branch );
01305   em2Target << ( em2tgt0 % uif2( "targ", de2PC, uif("imm", de2Instr ) ) );
01306   em2Valid << ( em2vd0 % ( !squash & de2Valid ) );
01307 
01308 
01309   F next_dMem = mux( (emType == ST ) & emValid, 
01310                                 uif3("mem#write_mem", dMem, emValue, emArg2 ), 
01311                                 dMem );
01312 
01313   dMem << ( mem0 % next_dMem );
01314 
01315   
01316   // writeback stage for first instruction
01317   mwInstr << (mwi0 % emInstr);
01318   mwData << ( mwda0 % mux( (emType == LD), uif2("mem@read_mem", dMem, emValue ), emValue ) ); 
01319   mwDest << ( mwde0 % uif("dest", emInstr ) );
01320   mwValid << ( mwvd0 % ( emValid & 
01321                        ( ( emType == RI ) | 
01322                          ( emType == RR ) | 
01323                          ( emType == LD ) ) ) );
01324 
01325   // writeback stage for second instruction
01326   mw2Instr << (mw2i0 % em2Instr);
01327   mw2Data << ( mw2da0 % mux( (em2Type == LD), uif2("mem@read_mem", dMem, em2Value ), em2Value ) ); 
01328   mw2Dest << ( mw2de0 % uif("dest", em2Instr ) );
01329   mw2Valid << (mw2vd0 % ( em2Valid & 
01330                         ( ( em2Type == RI ) | 
01331                           ( em2Type == RR ) | 
01332                           ( em2Type == LD ) ) ) );
01333 
01334 
01335   // impl data and address for first instruction
01336   F default_rf_data = si("default_rf_data");
01337   F impl_rf_data = mux( mwValid, mwData, default_rf_data);
01338   
01339   F default_rf_address = si("default_rf_address");
01340   F impl_rf_address = mux(mwValid, mwDest, default_rf_address);
01341 
01342   //  impl data and address for second instruction
01343   F default_rf2_data = si("default_rf2_data");
01344   F impl_rf2_data = mux(mw2Valid, mw2Data, default_rf2_data);
01345   
01346   F default_rf2_address = si("default_rf2_address");
01347   F impl_rf2_address = mux(mw2Valid, mw2Dest, default_rf2_address);
01348 
01349   // Now let us define the spec
01350   
01351   // spec for first address
01352 
01353   F sType = restrict(mwInstr, opcodes);
01354   F arg1 = uif2("mem@read", 
01355                 pRF,
01356                 uif("src1",
01357                     mwInstr));
01358 
01359   F select_imm = ( (sType == RI) | (sType == ST) | (sType == LD));
01360   F arg2 = mux(select_imm,
01361                uif("imm",
01362                    mwInstr),
01363                uif2("mem@read",
01364                     pRF,
01365                     uif("src2",
01366                         mwInstr)));
01367   F aluval = uif3("alu",
01368                   uif("op",
01369                       mwInstr),
01370                   arg1,
01371                   arg2);
01372 
01373   F select_ld = (sType == LD); // NEED changes
01374   F writeval = mux(select_ld,
01375                    uif2("mem@read_mem",
01376                         dMem,
01377                         aluval),
01378                    aluval);
01379 
01380   F spec_dest = uif("dest",
01381                     mwInstr);
01382 
01383   F spec_rf_data = mux( mwValid, writeval, default_rf_data);
01384   
01385   F spec_rf_address = mux(mwValid, spec_dest, default_rf_address);
01386 
01387   // spec for second address
01388   F second_sType = restrict(mw2Instr, opcodes);
01389   F second_arg1 = uif2("mem@read", 
01390                        pRF,
01391                        uif("src1",
01392                            mw2Instr));
01393 
01394   F second_select_imm = ( (second_sType == RI) | (second_sType == ST) | (second_sType == LD));
01395 
01396   F second_arg2 = mux(second_select_imm,
01397                       uif("imm",
01398                           mw2Instr),
01399                       uif2("mem@read",
01400                            pRF,
01401                            uif("src2",
01402                                mw2Instr)));
01403   F second_aluval = uif3("alu",
01404                          uif("op",
01405                              mw2Instr),
01406                          second_arg1,
01407                          second_arg2);
01408 
01409   F second_select_ld = (second_sType == LD); // NEED changes
01410   F second_writeval = mux(second_select_ld,
01411                           uif2("mem@read_mem",
01412                                dMem,
01413                                second_aluval),
01414                           second_aluval);
01415   
01416   F second_spec_dest = uif("dest",
01417                            mw2Instr);
01418 
01419   F spec_rf2_data = mux( mw2Valid, second_writeval, default_rf2_data);
01420   
01421   F spec_rf2_address = mux(mw2Valid, second_spec_dest, default_rf2_address);
01422   
01423   F first_spec_neq_impl = !(spec_rf_data == impl_rf_data);
01424   F second_spec_neq_impl = !(spec_rf2_data == impl_rf2_data);
01425   
01426   F spec_neq_impl = (first_spec_neq_impl | second_spec_neq_impl);
01427 
01428   return spec_neq_impl;
01429 }
01430 
01431 F
01432 build_dlx_uclid_superscalar_seq()
01433 {
01434   int depth = 0;
01435   F spec_neq_impl = build_dlx_uclid_superscalar();
01436   
01437   // hash tables needed for constant propagation
01438   st_table *processedNodes = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
01439   st_table *sortedTable = st_init_table( (int (*)() ) st_numcmp, (int (*)() ) st_numhash );
01440   st_table *equivalentNodeHash = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
01441 
01442   // now do constant propagation to simplify the rf unfolded 
01443   depth = Net_TopologicalSort(spec_neq_impl.raw, sortedTable, processedNodes);
01444   Net_ConstantPropagation(sortedTable, equivalentNodeHash, depth);
01445   Fnode *simplified_spec_neq_impl;
01446   st_lookup(equivalentNodeHash, (char *) spec_neq_impl.raw, (char **) &simplified_spec_neq_impl);
01447 
01448   st_free_table(sortedTable);
01449   st_free_table(equivalentNodeHash);
01450   st_free_table(processedNodes);
01451 
01452   Net_t *neq_net;
01453   neq_net = Net_CreateFromFormula(simplified_spec_neq_impl);
01454   
01455   //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
01456   //Net_PrintFormula(neq_net, array_fetch(Fnode *, neq_net->formulas,0),  processedTable);
01457   Net_PrintVHDL(neq_net, 4, "dlxuclid.vhdl", "dlxuclid");
01458   return spec_neq_impl;
01459 }
01460 
01461 } // "C" linkage
01462
Generated on Thu Oct 11 11:47:27 2007 for Tarski by  doxygen 1.3.9.1