micro_arch.c

Go to the documentation of this file.

extern "C" {

#include "tarski.h"


array_t *
build_double_instr()
{
  array_t *result_array = array_alloc(Fnode *, 0);
  
  F instr_data_reg1 = sr("double_instr_data_reg1");
  F instr_data_reg2 = sr("double_instr_data_reg2");
  F instr_data1 = si("instr_data1");
  F instr_data2 = si("instr_data2");
  F instr_data = si("instr_data");
  
  F instr_valid = br("double_instr_valid");
  F instr_valid2 = br("double_instr_valid2");

  F LD = sc("LD");

  F regfile = sr("mem@doubleRF");
  F init_regfile = si("initRF");
  F instr_buffer_valid = br("double_instr_buffer_valid");
  F instr_buffer = sr("double_instr_buffer");
  F init_instr_buffer_valid = FALSE();
  
  F init_instr_buffer = si("init_instr_buffer");

  F instr_buffer_load = instr_valid & !instr_buffer_valid;
  F next_instr_buffer = mux(instr_buffer_load,
                            instr_data_reg1,
                            instr_buffer);  
  instr_buffer << (init_instr_buffer % next_instr_buffer);
  
  F first_instr = uif("first_instr",
                      instr_buffer);
  
  F second_instr = uif("second_instr",
                       instr_buffer);
  
  // all the data for first instruction
  F first_address1 = uif("src1",
                         first_instr);  
  F first_address2 = uif("src2",
                         first_instr);  
  F first_arg1 = uif2("mem@read", 
                      regfile,
                      first_address1);
  F first_arg2 = uif2("mem@read",
                      regfile,
                      first_address2);
  F first_op = uif("op",
                   first_instr);  
  F first_alu_result = uif3("alu",
                            first_op,
                            first_arg1,
                            first_arg2);
  F first_dest = uif("dest",
                     first_instr);
  F first_load_value = uif("imm",
                           first_instr);
  F first_select_alu = !(first_instr == LD);
  F first_result = mux(first_select_alu,
                       first_alu_result,
                       first_load_value);
  
  // all the data for second instruction
  F second_address1 = uif("src1",
                          second_instr);
  F second_address2 = uif("src2",
                      second_instr);
  F second_arg1 = uif2("mem@read",
                       regfile,
                       second_address1);
  F second_arg2 = uif2("mem@read",
                       regfile,
                       second_address2);
  F second_op = uif("op",
                    second_instr);
  F second_alu_result = uif3("alu",
                             second_op,
                             second_arg1,
                             second_arg2);
  F second_dest = uif("dest",
                      second_instr);
  F second_load_value = uif("imm",
                            second_instr);
  F second_select_alu = !(second_instr == LD);
  F second_result = mux(second_select_alu,
                        second_alu_result,
                        second_load_value);
  
  F resource_conflict = instr_buffer_valid & ((first_dest == second_dest) | (second_select_alu & ((second_address1 == first_dest) | (second_address2 == first_dest))));

  F first_instr_only_committed_last_cycle = br("first_instr_only_committed");
  
  F second_instruction_not_stalled = first_instr_only_committed_last_cycle | (! resource_conflict);
  
  F first_instr_write = instr_buffer_valid & (!first_instr_only_committed_last_cycle);
  
  F second_instr_write = instr_buffer_valid & second_instruction_not_stalled;
  
  F next_first_instr_only_committed_last_cycle = first_instr_write & (!second_instruction_not_stalled);
  
  first_instr_only_committed_last_cycle << (FALSE() % next_first_instr_only_committed_last_cycle);
  
  F next_regfile1 = mux(first_instr_write,
                        uif3("mem#write",
                             regfile,
                             first_dest,
                             first_result),
                        regfile);
  
  F next_regfile2 = mux(second_instr_write,
                        uif3("mem#write",
                             regfile,
                             second_dest,
                             second_result),
                        next_regfile1);

  regfile << (init_regfile % next_regfile2);
  
  F instr_ready = (!instr_buffer_valid);
  
  F next_instr_valid = (instr_ready & instr_valid2) | ((!instr_ready) & instr_valid);
  F next_instr_valid2 = (instr_ready & FALSE()) | ((!instr_ready) & instr_valid2);  
  instr_valid << (TRUE() % next_instr_valid);
  instr_valid2 << (FALSE() % next_instr_valid2);

  F next_instr_data_reg1 = mux(instr_ready,
                               instr_data_reg2,
                               instr_data_reg1);
  
  F next_instr_data_reg2 = mux(instr_ready,
                               instr_data,
                               instr_data_reg2);
  
  instr_data_reg1 << (instr_data1 % next_instr_data_reg1);
  instr_data_reg2 << (instr_data2 % next_instr_data_reg2);    

  F instr_committed = br("double_instr_committed");
  F next_instr_committed = (second_instr_write | instr_committed); 
  instr_committed << (FALSE() % next_instr_committed);
  
  // next state function of instr_buffer_valid
  F next_instr_buffer_valid = ((instr_ready & instr_valid) | instr_buffer_valid) & (!next_instr_committed);
  instr_buffer_valid << (init_instr_buffer_valid % next_instr_buffer_valid);

  F arbitrary_read_address = si("read_address");
  F regfile_read_data = uif2("mem@read",
                             regfile,
                             arbitrary_read_address);
  array_insert_last(Fnode*, result_array, instr_ready.raw);
  array_insert_last(Fnode*, result_array, instr_committed.raw);
  array_insert_last(Fnode*, result_array, regfile_read_data.raw);
  return result_array;
}


F 
build_microarch_wrapper()
{
  array_t *double_array = build_double_instr();
  Net_t *double_net;
  double_net = Net_CreateFromFormulaArray(double_array);
  
  array_t *single_array = build_single_instr();
  Net_t *single_net;
  single_net = Net_CreateFromFormulaArray(single_array);
  
  F double_instr_ready;
  double_instr_ready.raw = array_fetch(Fnode *, double_array, 0);  
  F double_instr_committed;
  double_instr_committed.raw = array_fetch(Fnode *, double_array, 1);  
  F double_regfile_data;
  double_regfile_data.raw = array_fetch(Fnode *, double_array, 2);

  // print the double micro-arch
  //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
  //Net_PrintFormula(double_net, array_fetch(Fnode *, double_net->formulas,0),  processedTable);
  //Net_PrintFormula(double_net, array_fetch(Fnode *, double_net->formulas,1),  processedTable);
  //Net_PrintFormula(double_net, array_fetch(Fnode *, double_net->formulas,2),  processedTable);
  // print the VHDL
  //Net_PrintVHDL(double_net, stdout, 4);
  //return double_regfile_data;

  F single_instr_ready;
  single_instr_ready.raw = array_fetch(Fnode *, single_array, 0);
  F single_instr_committed;
  single_instr_committed.raw = array_fetch(Fnode *, single_array, 1);
  F single_regfile_data;
  single_regfile_data.raw = array_fetch(Fnode *, single_array, 2);

  // print the single micro-arch
  //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
  //Net_PrintFormula(single_net, array_fetch(Fnode *, single_net->formulas,0),  processedTable);
  //Net_PrintFormula(single_net, array_fetch(Fnode *, single_net->formulas,1),  processedTable);
  //Net_PrintFormula(single_net, array_fetch(Fnode *, single_net->formulas,2),  processedTable);
  //Net_PrintVHDL(single_net, stdout, 4);
  
  F both_instr_committed = double_instr_committed & single_instr_committed;
  F regfile_data_different = !(single_regfile_data == double_regfile_data);
  
  F fail_condition = both_instr_committed & regfile_data_different;
  Net_t  *fail_net = Net_CreateFromFormula(fail_condition.raw);
  //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
  //Net_PrintFormula(fail_net, array_fetch(Fnode *, fail_net->formulas,0),  processedTable);
  Net_PrintVHDL(fail_net, 4, "microarch.vhdl", "microarch");
  return double_regfile_data;
}

array_t *
build_single_instr()
{
  array_t *result_array = array_alloc(Fnode *, 0);

  F instr_data_reg1 = sr("single_instr_data_reg1");
  F instr_data_reg2 = sr("single_instr_data_reg2");
  F instr_data1 = si("instr_data1");
  F instr_data2 = si("instr_data2");
  F instr_data = si("instr_data");
  
  F instr_valid = br("single_instr_valid");
  F instr_valid2 = br("single_instr_valid2");

  F LD = sc("LD");

  F regfile = sr("mem@singleRF");
  F init_regfile = si("initRF");
  F instr_buffer_valid = br("single_instr_buffer_valid");
  F instr_buffer = sr("single_instr_buffer");
  F init_instr_buffer_valid = FALSE();  
  F init_instr_buffer = si("init_instr_buffer");

  F instr_buffer_load = instr_valid & !instr_buffer_valid;
  F next_instr_buffer = mux(instr_buffer_load,
                            instr_data_reg1,
                            instr_buffer);
  
  instr_buffer << (init_instr_buffer % next_instr_buffer);
  F instr_pointer = br("instr_pointer");  
  F first_instr = uif("first_instr",
                      instr_buffer);
  
  F second_instr = uif("second_instr",
                       instr_buffer);
  
  F executable_instr = mux(instr_pointer,
                           second_instr,
                           first_instr);

  // all the data for executable instruction

  F executable_address1 = uif("src1",
                              executable_instr);  
  F executable_address2 = uif("src2",
                              executable_instr);  
  F executable_arg1 = uif2("mem@read", 
                           regfile,
                           executable_address1);
  F executable_arg2 = uif2("mem@read",
                           regfile,
                           executable_address2);
  F executable_op = uif("op",
                        executable_instr);  
  F executable_alu_result = uif3("alu",
                                 executable_op,
                                 executable_arg1,
                                 executable_arg2);
  F executable_dest = uif("dest",
                          executable_instr);
  F executable_load_value = uif("imm",
                                executable_instr);
  F executable_select_alu = !(executable_instr == LD);
  F executable_result = mux(executable_select_alu,
                            executable_alu_result,
                            executable_load_value);
  
  F executable_instr_write = instr_buffer_valid;
  
  F next_regfile = mux(executable_instr_write,
                       uif3("mem#write",
                            regfile,
                            executable_dest,
                            executable_result),
                       regfile);
  regfile << (init_regfile % next_regfile);
  
  F instr_ready = (!instr_buffer_valid);

  F next_instr_valid = (instr_ready & instr_valid2) | ((!instr_ready) & instr_valid);
  F next_instr_valid2 = (instr_ready & FALSE()) | ((!instr_ready) & instr_valid2);  
  instr_valid << (TRUE() % next_instr_valid);
  instr_valid2 << (FALSE() % next_instr_valid2);
  
  F next_instr_data_reg1 = mux(instr_ready,
                               instr_data_reg2,
                               instr_data_reg1);
  
  F next_instr_data_reg2 = mux(instr_ready,
                               instr_data,
                               instr_data_reg2);
  
  instr_data_reg1 << (instr_data1 % next_instr_data_reg1);
  instr_data_reg2 << (instr_data2 % next_instr_data_reg2);
  
  F next_instr_pointer = (executable_instr_write & (!instr_pointer)) | ((!executable_instr_write) & instr_pointer);
  
  instr_pointer << (FALSE() % next_instr_pointer);

  F instr_committed = br("single_instr_committed");
  F next_instr_committed = (instr_pointer & executable_instr_write) | instr_committed;
  instr_committed << (FALSE() % next_instr_committed);
  
  // next state function of instr_buffer_valid
  F next_instr_buffer_valid = ((instr_ready & instr_valid) | instr_buffer_valid) & (!next_instr_committed);
  instr_buffer_valid << (init_instr_buffer_valid % next_instr_buffer_valid);

  F arbitrary_read_address = si("read_address");
  F regfile_read_data = uif2("mem@read",
                             regfile,
                             arbitrary_read_address);

  array_insert_last(Fnode*, result_array, instr_ready.raw);
  array_insert_last(Fnode*, result_array, instr_committed.raw);
  array_insert_last(Fnode*, result_array, regfile_read_data.raw);
  return result_array;
}



} // "C" linkage

---