diff --git a/include/ilang/util/str_util.h b/include/ilang/util/str_util.h index 68e18320f..7ab37acfd 100644 --- a/include/ilang/util/str_util.h +++ b/include/ilang/util/str_util.h @@ -24,6 +24,9 @@ bool StrToBool(const std::string& str); /// Return the value represented in the string, e.g. "10". int StrToInt(const std::string& str, int base = 10); +/// Return the value represented in the string in long type, e.g. "10". +long long StrToLong(const std::string& str, int base); + /// Python-style split , return a vector of splitted strings std::vector Split(const std::string& str, const std::string& delim); diff --git a/src/util/str_util.cc b/src/util/str_util.cc index 3c34b1d95..aad524ca8 100644 --- a/src/util/str_util.cc +++ b/src/util/str_util.cc @@ -39,6 +39,15 @@ int StrToInt(const std::string& str, int base) { } +long long StrToLong(const std::string& str, int base) { + try { + return std::stoll(str, NULL, base); + } catch (const std::exception& e) { + ILA_ERROR << "Converting non-numeric value " << str << " to long int.\n"; + return 0; + } +} + std::vector Split(const std::string& str, const std::string& delim) { std::vector tokens; diff --git a/src/verilog-in/verilog_analysis.cc b/src/verilog-in/verilog_analysis.cc index 6c5e6df3b..5578ab7f1 100644 --- a/src/verilog-in/verilog_analysis.cc +++ b/src/verilog-in/verilog_analysis.cc @@ -692,8 +692,8 @@ VerilogAnalyzer::module_io_vec_t VerilogAnalyzer::get_top_module_io() const { void* ptr_from_list_ = ast_list_get_not_null(port_ptr->port_names, name_idx); ast_identifier port_id_ptr; - if (port_ptr - ->is_reg) { // in this case, it is not a list of ast_identifier + if (! port_ptr + ->is_list_id) { // in this case, it is not a list of ast_identifier // but a list of ast_single_assignment(ast_new_lvalue_id) ast_single_assignment* asm_ptr = (ast_single_assignment*)ptr_from_list_; ILA_ASSERT(asm_ptr->lval->type == ast_lvalue_type_e::NET_IDENTIFIER || diff --git a/src/verilog-in/verilog_const_parser.cc b/src/verilog-in/verilog_const_parser.cc index 4b53df9f0..eda472a95 100644 --- a/src/verilog-in/verilog_const_parser.cc +++ b/src/verilog-in/verilog_const_parser.cc @@ -14,6 +14,12 @@ VerilogConstantExprEval::VerilogConstantExprEval() : eval_error(false) { // do nothing } +static void* ast_list_get_not_null(ast_list* list, unsigned int item) { + void* ret = ast_list_get(list, item); + ILA_NOT_NULL(ret); + return ret; +} + double VerilogConstantExprEval::_eval(ast_expression* e, const named_parameter_dict_t& param_defs) { @@ -51,7 +57,7 @@ VerilogConstantExprEval::_eval(ast_expression* e, ast_number_base_e::BASE_HEX ? 16 : 10; - ret = StrToInt(resp, base); + ret = StrToLong(resp, base); } else { // float try { ret = std::stod(resp); @@ -72,6 +78,30 @@ VerilogConstantExprEval::_eval(ast_expression* e, return 0; } return _eval(e->primary->value.minmax->aux, param_defs); + } else if (e->primary->value_type == ast_primary_value_type::PRIMARY_CONCATENATION) { + ast_concatenation * cc = e->primary->value.concatenation; + unsigned repeat = cc->repeat? _eval(cc->repeat, param_defs ) : 1; + unsigned total_width = 0; + long long ret = 0; + for (size_t idx = 0; idx < cc->items->items; ++idx) { + ast_expression * it = (ast_expression *)ast_list_get_not_null(cc->items, idx); + unsigned v = _eval(it, param_defs); + unsigned width = it->primary->value.number->width; + if (width == 0) { + error_str = ast_expression_tostring(e); + eval_error = true; + return 0; + } + ret = ret << width; + ret = ret | v; + total_width += width; + } + unsigned origin = ret; + for (unsigned idx = 1; idx < repeat; ++ idx) { + ret = ret << total_width; + ret = ret | origin; + } + return ret; } else { // parser error: unable to handle error_str = ast_expression_tostring(e); @@ -95,10 +125,23 @@ VerilogConstantExprEval::_eval(ast_expression* e, return left / right; if (e->operation == ast_operator::OPERATOR_MOD) return left % right; + if (e->operation == ast_operator::OPERATOR_L_OR) + return left || right; + if (e->operation == ast_operator::OPERATOR_L_AND) + return left && right; + if (e->operation == ast_operator::OPERATOR_B_OR) + return left | right; + if (e->operation == ast_operator::OPERATOR_B_AND) + return left & right; eval_error = true; error_str = ast_expression_tostring(e); return 0; + } else if (e->type == ast_expression_type::CONDITIONAL_EXPRESSION) { + double left = _eval(e->left, param_defs); + double right = _eval(e->right, param_defs); + double cond = _eval(e->aux, param_defs); + return cond?left:right; } eval_error = true; @@ -121,11 +164,6 @@ double VerilogConstantExprEval::Eval(ast_expression* _s) { return val; } -static void* ast_list_get_not_null(ast_list* list, unsigned int item) { - void* ret = ast_list_get(list, item); - ILA_NOT_NULL(ret); - return ret; -} /// parse only the current module's parameter definitions, will update /// param_defs diff --git a/src/vtarget-out/CMakeLists.txt b/src/vtarget-out/CMakeLists.txt index a0cf505a3..9687b0fd5 100644 --- a/src/vtarget-out/CMakeLists.txt +++ b/src/vtarget-out/CMakeLists.txt @@ -7,6 +7,10 @@ target_sources(${ILANG_LIB_NAME} PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/var_extract.cc ${CMAKE_CURRENT_SOURCE_DIR}/vtarget_gen_impl.cc ${CMAKE_CURRENT_SOURCE_DIR}/single_target.cc + ${CMAKE_CURRENT_SOURCE_DIR}/single_target_connect.cc + ${CMAKE_CURRENT_SOURCE_DIR}/single_target_misc.cc + ${CMAKE_CURRENT_SOURCE_DIR}/single_target_cond.cc + ${CMAKE_CURRENT_SOURCE_DIR}/single_target_inv_syn_support.cc ${CMAKE_CURRENT_SOURCE_DIR}/vtarget_gen_cosa.cc ${CMAKE_CURRENT_SOURCE_DIR}/vtarget_gen_jasper.cc ${CMAKE_CURRENT_SOURCE_DIR}/vtarget_gen.cc diff --git a/src/vtarget-out/single_target.cc b/src/vtarget-out/single_target.cc index 0d5c78994..16c967051 100644 --- a/src/vtarget-out/single_target.cc +++ b/src/vtarget-out/single_target.cc @@ -171,314 +171,8 @@ VlgSglTgtGen::VlgSglTgtGen( } // END of constructor -void VlgSglTgtGen::ConstructWrapper_add_ila_input() { - // add ila input - size_t ila_input_num = _host->input_num(); - for (size_t input_idx = 0; input_idx < ila_input_num; input_idx++) { - const auto& input_ = _host->input(input_idx); - const auto& name_ = input_->name().str(); - auto width_ = get_width(input_); - - vlg_wrapper.add_wire("__ILA_I_" + name_, width_, true); - vlg_wrapper.add_input("__ILA_I_" + name_, width_); - } - // remember to add ila_outputs (reg) - size_t ila_state_num = _host->state_num(); - for (size_t state_idx = 0; state_idx < ila_state_num; ++state_idx) { - const auto& state_ = _host->state(state_idx); - const auto& name_ = state_->name().str(); - if (state_->sort()->is_mem()) - continue; // please ignore memory, they should not be connected this way - auto width_ = get_width(state_); - - vlg_wrapper.add_wire("__ILA_SO_" + name_, width_, true); - vlg_wrapper.add_output("__ILA_SO_" + name_, width_); - // remember to connect in the instantiation step - } -} // ConstructWrapper_add_ila_input - -std::string VlgSglTgtGen::ConstructWrapper_get_ila_module_inst() { - if (target_type == target_type_t::INVARIANTS) - return ""; - - ILA_ASSERT(vlg_ila.decodeNames.size() == 1) - << "Implementation bug: decode condition."; - vlg_wrapper.add_wire(vlg_ila.validName, 1, true); - vlg_wrapper.add_wire(vlg_ila.decodeNames[0], 1, true); - - // TODO: check whether all ports have been dealt with - // TODO: check whether there are any extra ports we create - std::set port_connected; // store the name of ila port - std::set port_of_ila; // store the name of ila port also - - // .. record function - - // this is the string to construct - auto retStr = vlg_ila.moduleName + " " + _ila_mod_inst_name + " (\n"; - - std::set func_port_skip_set; - for (auto&& func_app : vlg_ila.ila_func_app) { - func_port_skip_set.insert(func_app.result.first); - port_connected.insert(func_app.result.first); - /// new reg : put in when __START__ - if (not IN(func_app.func_name, func_cnt)) - func_cnt.insert({func_app.func_name, 0}); - unsigned func_no = func_cnt[func_app.func_name]++; - - std::string func_reg_w = - func_app.func_name + "_" + IntToStr(func_no) + "_result_wire"; - std::string func_reg = - func_app.func_name + "_" + IntToStr(func_no) + "_result_reg"; - vlg_wrapper.add_reg(func_reg, func_app.result.second); - vlg_wrapper.add_wire(func_reg_w, func_app.result.second, true); - // add as a module input, also - vlg_wrapper.add_input(func_reg_w, func_app.result.second); - - add_reg_cassign_assumption(func_reg, func_reg_w, "__START__", - "func_result"); - // vlg_wrapper.add_always_stmt( "if( __START__ ) " + func_reg + " <= " + - // func_reg_w + ";" ); - - retStr += " ." + func_app.result.first + "(" + func_reg_w + "),\n"; - - unsigned argNo = 0; - for (auto&& arg : func_app.args) { - func_port_skip_set.insert(arg.first); - port_connected.insert(arg.first); - - std::string func_arg_w = func_app.func_name + "_" + IntToStr(func_no) + - "_arg" + IntToStr(argNo) + "_wire"; - std::string func_arg = func_app.func_name + "_" + IntToStr(func_no) + - "_arg" + IntToStr(argNo) + "_reg"; - vlg_wrapper.add_reg(func_arg, arg.second); - vlg_wrapper.add_wire(func_arg_w, arg.second, true); - add_reg_cassign_assumption(func_arg, func_arg_w, "__START__", "func_arg"); - // vlg_wrapper.add_always_stmt( "if( __START__ ) " + func_arg + " <= " + - // func_arg_w + ";" ); - - retStr += " ." + arg.first + "(" + func_arg_w + "),\n"; - argNo++; - } - } // end of functions - // handle input - for (auto&& w : vlg_ila.inputs) { - if (IN(w.first, func_port_skip_set)) - continue; - // w.first will be connected - port_connected.insert(w.first); - // deal w. clock and reset and start - if (w.first == vlg_ila.clkName) // .clk(clk) - retStr += " ." + vlg_ila.clkName + "(" + vlg_wrapper.clkName + "),\n"; - else if (w.first == - vlg_ila.rstName) // .rst(rst) -- this does not need to be changed - retStr += " ." + vlg_ila.rstName + "(" + vlg_wrapper.rstName + - "),\n"; // no init anyway! - else if (w.first == vlg_ila.startName) { // .__START__(__START__) - retStr += " ." + vlg_ila.startName + "(" + "__START__" + "),\n"; - } else { - ILA_ERROR_IF(not IN("__ILA_I_" + w.first, vlg_wrapper.wires)) - << "__ILA_I_" + w.first << " has not been defined yet"; - retStr += " ." + w.first + "(__ILA_I_" + w.first + "),\n"; - } - } // end of inputs - // TODO:: FUnction here ! - // handle output - for (auto&& w : vlg_ila.outputs) { - if (IN(w.first, func_port_skip_set)) - continue; - // w.first will be connected - port_connected.insert(w.first); - // deal w. valid and decode - if (w.first == vlg_ila.decodeNames[0]) - retStr += " ." + vlg_ila.decodeNames[0] + "(" + vlg_ila.decodeNames[0] + - "),\n"; - else if (w.first == vlg_ila.validName) - retStr += " ." + vlg_ila.validName + "(" + vlg_ila.validName + "),\n"; - else { - // ILA_ERROR_IF( not IN ("__ILA_I_" + w.first , vlg_wrapper.wires) ) << - // "__ILA_I_" + w.first << " has not been defined yet"; - ILA_ERROR << "Does not know how to connect:" << w.first << ", ignored."; - // std::cout<< w.first< 0 && dw > 0) - << "Implementation bug: unable to find mem:" << ila_name; - - for (auto&& rport : rports) { - auto no = rport.first; // is the num - auto port = rport.second; // is the port - auto rdw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_rdata"; - auto raw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_raddr"; - // auto rew = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_ren"; no need, - // r_en is the start signal - - vlg_wrapper.add_wire(rdw, dw, true); - vlg_wrapper.add_wire(raw, aw, true); - - retStr += " ." + port.rdata + "(" + rdw + "),\n"; - retStr += " ." + port.raddr + "(" + raw + "),\n"; - - // port.rdata/raddr will be connected - port_connected.insert(port.rdata); - port_connected.insert(port.raddr); - - } // for rport - } // for ila_rports - - for (auto&& ila_name_wport_pair : vlg_ila.ila_wports) { - - const auto& ila_name = ila_name_wport_pair.first; - const auto& wports = ila_name_wport_pair.second; - const auto adw = GetMemInfo(ila_name); - auto aw = adw.first; - auto dw = adw.second; // address/data width - ILA_ASSERT(aw > 0 && dw > 0) - << "Implementation bug: unable to find mem:" << ila_name; - - for (auto&& wport : wports) { - auto no = wport.first; // is the num - auto port = wport.second; // is the port - auto wdw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_wdata"; - auto waw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_waddr"; - auto wew = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_wen"; - - vlg_wrapper.add_wire(wdw, dw, true); - vlg_wrapper.add_wire(waw, aw, true); - vlg_wrapper.add_wire(wew, 1, true); - - retStr += " ." + port.wdata + "(" + wdw + "),\n"; - retStr += " ." + port.waddr + "(" + waw + "),\n"; - retStr += " ." + port.wen + "(" + wew + "),\n"; - - // port.rdata/raddr will be connected - port_connected.insert(port.wdata); - port_connected.insert(port.waddr); - port_connected.insert(port.wen); - - } // for wport - } // for ila_wports - - // handle state-output - std::string sep; - for (auto&& r : vlg_ila.regs) { - if (not IN("__ILA_SO_" + r.first, vlg_wrapper.wires)) { - ILA_WARN << "__ILA_SO_" + r.first << " will be ignored"; - - retStr += sep + " ." + r.first + "()"; // __ILA_SO_" + r.first + " - port_connected.insert(r.first); - sep = ",\n"; - continue; - } // else - retStr += sep + " ." + r.first + "(__ILA_SO_" + r.first + ")"; - sep = ",\n"; - // reg out will be connected - port_connected.insert(r.first); - } - retStr += "\n);"; - // TODO: check port_conencted and port_ila - // currently not - return retStr; -} // ConstructWrapper_get_ila_module_inst() - -void VlgSglTgtGen::ConstructWrapper_add_vlg_input_output() { - - auto vlg_inputs = vlg_info_ptr->get_top_module_io(); - auto& io_map = rf_vmap["interface mapping"]; - for (auto&& name_siginfo_pair : vlg_inputs) { - std::string refstr = - IN(name_siginfo_pair.first, io_map) - ? io_map[name_siginfo_pair.first].get() - : ""; - _idr.RegisterInterface( - name_siginfo_pair.second, refstr, - // Verifier_compatible_w_ila_input - [this](const std::string& ila_name, - const SignalInfoBase& vlg_sig_info) -> bool { - return TypeMatched(IlaGetInput(ila_name), vlg_sig_info) != 0; - }, - // no need to worry about the nullptr in IlaGetInput, TypeMatched will - // be able to handle. - // Verifier_get_ila_mem_info - [this]( - const std::string& ila_mem_name) -> std::pair { - return GetMemInfo(ila_mem_name); - }); // end of function call: RegisterInterface - } -} // ConstructWrapper_add_vlg_input_output - -void VlgSglTgtGen::ConstructWrapper_add_cycle_count_moniter() { - // find in rf_cond, how many cycles will be needed - max_bound = 0; - - auto& instr = get_current_instruction_rf(); - - if (!instr.is_null() && IN("ready bound", instr) && - instr["ready bound"].is_number_integer()) - max_bound = instr["ready bound"].get(); - else - max_bound = _vtg_config.MaxBound; - - cnt_width = (int)std::ceil(std::log2(max_bound + 10)); - vlg_wrapper.add_reg("__CYCLE_CNT__", - cnt_width); // by default it will be an output reg - vlg_wrapper.add_stmt("always @(posedge clk) begin"); - vlg_wrapper.add_stmt("if (rst) __CYCLE_CNT__ <= 0;"); - vlg_wrapper.add_stmt( - "else if ( ( __START__ || __STARTED__ ) && __CYCLE_CNT__ < " + - IntToStr(max_bound + 5) + ") __CYCLE_CNT__ <= __CYCLE_CNT__ + 1;"); - vlg_wrapper.add_stmt("end"); - - vlg_wrapper.add_reg("__START__", 1); - vlg_wrapper.add_stmt("always @(posedge clk) begin"); - vlg_wrapper.add_stmt("if (rst) __START__ <= 0;"); - vlg_wrapper.add_stmt("else if (__START__ || __STARTED__) __START__ <= 0;"); - vlg_wrapper.add_stmt("else if (__ISSUE__) __START__ <= 1;"); - vlg_wrapper.add_stmt("end"); - - vlg_wrapper.add_reg("__STARTED__", 1); - vlg_wrapper.add_stmt("always @(posedge clk) begin"); - vlg_wrapper.add_stmt("if (rst) __STARTED__ <= 0;"); - vlg_wrapper.add_stmt( - "else if (__START__) __STARTED__ <= 1;"); // will never return to zero - vlg_wrapper.add_stmt("end"); - - vlg_wrapper.add_reg("__ENDED__", 1); - vlg_wrapper.add_stmt("always @(posedge clk) begin"); - vlg_wrapper.add_stmt("if (rst) __ENDED__ <= 0;"); - vlg_wrapper.add_stmt( - "else if (__IEND__) __ENDED__ <= 1;"); // will never return to zero - vlg_wrapper.add_stmt("end"); - - vlg_wrapper.add_reg("__RESETED__", 1); - vlg_wrapper.add_stmt("always @(posedge clk) begin"); - vlg_wrapper.add_stmt("if (rst) __RESETED__ <= 1;"); - vlg_wrapper.add_stmt("end"); - - // remember to generate - // __RESETED__ - // __ISSUE__ == start condition (if no flush, issue == true?) - // __IEND__ == ( end condition ) && STARTED - // __ENDFLUSH__ == (end flush condition ) && ENDED - // flush : !( __ISSUE__ ? || __START__ || __STARTED__ ) |-> flush -} // ConstructWrapper_add_cycle_count_moniter void VlgSglTgtGen::ConstructWrapper_generate_header() { vlg_wrapper.add_preheader("\n`define true 1'b1\n"); @@ -643,355 +337,7 @@ void VlgSglTgtGen::ConstructWrapper_add_inv_assertions() { } } -void VlgSglTgtGen::ConstructWrapper_add_additional_mapping_control() { - if (IN("mapping control", rf_vmap)) { - if (not rf_vmap["mapping control"].is_array()) - ILA_ERROR << "mapping control field must be an array of string"; - for (auto&& c : rf_vmap["mapping control"]) { - if (not c.is_string()) { - ILA_ERROR << "mapping control field must be an array of string"; - continue; - } - add_an_assumption(ReplExpr(c.get()), - "additional_mapping_control_assume"); - } - } -} // ConstructWrapper_add_additional_mapping_control - -// NON-FLUSH case -// 1 RESET -// 2 ISSUE = true RESETED (forever) -// 3 START ---> assume varmap ---> assume inv -// 4 STARTED -// 5 STARTED -// ... ... -// 6 IEND ---> check varmap -// 7 ENDED - -// FLUSH case -// 1 RESET -// 2 RESETED ---> assume flush & preflush cond -// ... ---> assume flush & preflush cond -// n ISSUE = pre-flush end ---> assume flush & preflush cond -// n+1 START ---> assume varmap ---> assume inv -// (maybe globally?) n+2 STARTED n+3 STARTED -// ... ... (forever) -// m IEND -// m+1 ENDED ---> assume flush & postflush cond -// ... ENDED (forever) ---> assume flush & postflush cond -// l ENDFLUSH = post-flush end ---> assume flush & postflush cond -// ---> assert varmap l+1 FLUSHENDED ---> assume flush -// & postflush cond -// - -void VlgSglTgtGen::ConstructWrapper_add_condition_signals() { - // TODO - // remember to generate - // __ISSUE__ == start condition (if no flush, issue == true?) - // __IEND__ == ( end condition ) && STARTED - // __ENDFLUSH__ == (end flush condition ) && ENDED - // flush : !( __ISSUE__ ? || __START__ || __STARTED__ ) |-> flush - - if (target_type == target_type_t::INVARIANTS) - return; - // we don't need additional signals, just make reset drives the design - - // find the instruction - auto& instr = get_current_instruction_rf(); - ILA_ASSERT(!instr.is_null()); - - // __IEND__ - std::string iend_cond = VLG_FALSE; - // bool no_started_signal = false; - if (ready_type & ready_type_t::READY_SIGNAL) { - if (instr["ready signal"].is_string()) { - iend_cond += "|| (" + - ReplExpr(instr["ready signal"].get(), true) + - ")"; // force vlg - } else if (instr["ready signal"].is_array()) { - for (auto&& cond : instr["ready signal"]) - if (cond.is_string()) - iend_cond += " || (" + ReplExpr(cond.get()) + ")"; - else - ILA_ERROR << "ready signal field of instruction: " - << _instr_ptr->name().str() - << " has to be string or array or string"; - } else - ILA_ERROR << "ready signal field of instruction: " - << _instr_ptr->name().str() - << " has to be string or array or string"; - } - if (ready_type & ready_type_t::READY_BOUND) { // can be both applied - if (instr["ready bound"].is_number_integer()) { - int bound = instr["ready bound"].get(); - if (bound > 0) { - // okay now we enforce the bound - iend_cond += "|| ( __CYCLE_CNT__ == " + - ReplExpr(IntToStr(cnt_width) + "'d" + IntToStr(bound)) + - ")"; - } else if (bound == 0) { - // iend_cond += "|| (__START__)"; - // no_started_signal = true; // please don't use && STARTED - ILA_ERROR << "Does not support bound : 0, please use a buffer to hold " - "the signal."; - } else - ILA_ERROR << "ready bound field of instruction: " - << _instr_ptr->name().str() - << " has to a non negative integer"; - } else - ILA_ERROR << "ready bound field of instruction: " - << _instr_ptr->name().str() << " has to a non negative integer"; - } // end of ready bound/condition - - // max bound for max checking range - std::string max_bound_constr; - if (IN("max bound", instr)) { - if (instr["max bound"].is_number_integer()) { - max_bound_constr = - "&& ( __CYCLE_CNT__ <= " + IntToStr(instr["max bound"].get()) + - ")"; - } - } - - vlg_wrapper.add_wire("__IEND__", 1, true); - // if(no_started_signal) - // add_wire_assign_assumption("__IEND__", "(" + iend_cond + ")", - // "IEND"); - // else - auto end_no_recur = has_flush ? "(~ __FLUSHENDED__ )" : "(~ __ENDED__)"; - - add_wire_assign_assumption("__IEND__", - "(" + iend_cond + ") && __STARTED__ && " + - end_no_recur + max_bound_constr, - "IEND"); - // handle start decode - ILA_ERROR_IF(IN("start decode", instr)) - << "'start decode' is replaced by start condition!"; - if (IN("start condition", instr)) { - handle_start_condition(instr["start condition"]); - } else { - add_an_assumption("(~ __START__) || (" + vlg_ila.decodeNames[0] + ")", - "issue_decode"); // __ISSUE__ |=> decode - add_an_assumption("(~ __START__) || (" + vlg_ila.validName + ")", - "issue_valid"); // __ISSUE__ |=> decode - } - - if (has_flush) { - ILA_ASSERT(IN("pre-flush end", instr) && - IN("post-flush end", instr)); // there has to be something - - std::string issue_cond; - if (instr["pre-flush end"].is_string()) - issue_cond = "(" + ReplExpr(instr["pre-flush end"].get()) + - ") && __RESETED__"; - else { - issue_cond = "1"; - ILA_ERROR << "pre-flush end field should be a string!"; - } - vlg_wrapper.add_wire("__ISSUE__", 1, true); - add_wire_assign_assumption("__ISSUE__", issue_cond, "ISSUE"); - - std::string finish_cond; - if (instr["post-flush end"].is_string()) - finish_cond = "(" + ReplExpr(instr["post-flush end"].get()) + - ") && __ENDED__"; - else { - finish_cond = "1"; - ILA_ERROR << "post-flush end field should be a string!"; - } - vlg_wrapper.add_wire("__ENDFLUSH__", 1, true); - add_wire_assign_assumption("__ENDFLUSH__", finish_cond, "ENDFLUSH"); - - vlg_wrapper.add_reg("__FLUSHENDED__", 1); - vlg_wrapper.add_stmt( - "always @(posedge clk) begin\n" - "if(rst) __FLUSHENDED__ <= 0;\n" - "else if( __ENDFLUSH__ && __ENDED__ ) __FLUSHENDED__ <= 1;\n end"); - - // enforcing flush constraints - std::string flush_enforcement = VLG_TRUE; - if (instr["flush constraints"].is_null()) { - } // do nothing. we are good - else if (instr["flush constraints"].is_string()) { - flush_enforcement += - "&& (" + ReplExpr(instr["flush constraints"].get()) + - ")"; - } else if (instr["flush constraints"].is_array()) { - for (auto&& c : instr["flush constraints"]) - if (c.is_string()) - flush_enforcement += "&& (" + ReplExpr(c.get()) + ")"; - else - ILA_ERROR << "flush constraint field of instruction:" - << _instr_ptr->name().str() - << " must be a string or an array of string."; - } else - ILA_ERROR << "flush constraint field of instruction:" - << _instr_ptr->name().str() - << " must be string or array of string."; - - // TODO: preflush and postflush - - add_an_assumption( - "(~ ( __RESETED__ && ~ ( __START__ || __STARTED__ ) ) ) || (" + - flush_enforcement + ")", - "flush_enforce_pre"); - add_an_assumption("(~ ( __ENDED__ )) || (" + flush_enforcement + ")", - "flush_enforce_post"); - - } else { - vlg_wrapper.add_wire("__ISSUE__", 1, true); - if (_vtg_config.ForceInstCheckReset) { - vlg_wrapper.add_input("__ISSUE__", 1); - } else - add_wire_assign_assumption("__ISSUE__", "1", "ISSUE"); // issue ASAP - // start decode -- issue enforce (e.g. valid, input) - } // end of no flush -} - -void VlgSglTgtGen::ConstructWrapper_register_extra_io_wire() { - for (auto&& refered_vlg_item : _all_referred_vlg_names) { - - auto idx = refered_vlg_item.first.find("["); - auto removed_range_name = refered_vlg_item.first.substr(0, idx); - auto vlg_sig_info = vlg_info_ptr->get_signal(removed_range_name); - - auto vname = ReplaceAll( - ReplaceAll(ReplaceAll(refered_vlg_item.first, ".", "__DOT__"), "[", - "_"), - "]", "_"); - // + ReplaceAll(ReplaceAll(refered_vlg_item.second.range, "[","_"),"]","_"); - // // name for verilog - auto width = vlg_sig_info.get_width(); - - vlg_wrapper.add_wire(vname, width, 1); // keep - vlg_wrapper.add_output(vname, width); // add as output of the wrapper - _idr.RegisterExtraWire(vname, vname); - // these will be connected to the verilog module, so register as extra wires - // so, later they will be connected - } -} - -void VlgSglTgtGen::ConstructWrapper_add_module_instantiation() { - // instantiate ila module - if (target_type == target_type_t::INSTRUCTIONS) { - auto ila_mod_inst = ConstructWrapper_get_ila_module_inst(); - vlg_wrapper.add_stmt(ila_mod_inst); - } - - // instantiate verilog module - std::string verilog_inst_str = - vlg_info_ptr->get_top_module_name() + " " + _vlg_mod_inst_name + "(\n"; - _idr.VlgAddTopInteface( - vlg_wrapper); // put the extra wire there, and it should add wire also - verilog_inst_str += _idr.GetVlgModInstString(vlg_wrapper); - verilog_inst_str += ");"; - - vlg_wrapper.add_stmt(verilog_inst_str); -} - -void VlgSglTgtGen::ConstructWrapper_add_helper_memory() { - auto endCond = - has_flush ? "__ENDFLUSH__ || __FLUSHENDED__" : "__IEND__ || __ENDED__"; - - auto stmt = _idr.GetAbsMemInstString(vlg_wrapper, endCond); - vlg_wrapper.add_stmt(stmt); - - // check if we need to insert any assumptions - auto inserter = [this](const std::string& p) -> void { - add_an_assumption(p, "absmem"); - }; - _idr.InsertAbsMemAssmpt(inserter); -} - -void VlgSglTgtGen::ConstructWrapper_add_uf_constraints() { - if (not IN("functions", rf_vmap)) - return; // do nothing - auto& fm = rf_vmap["functions"]; - if (not fm.is_object()) { - ILA_ERROR << "expect functions field to be funcName -> list of list of " - "pair of (cond,val)."; - return; - } - - // convert vlg_ila.ila_func_app to name->list of func_app - std::map - name_to_fnapp_vec; - for (auto&& func_app : vlg_ila.ila_func_app) - name_to_fnapp_vec[func_app.func_name].push_back(func_app); - - for (auto&& it : fm.items()) { - const auto& funcName = it.key(); - const auto& list_of_time_of_apply = it.value(); - if (not list_of_time_of_apply.is_array()) { - ILA_ERROR << funcName - << ": expect functions field to be funcName -> list of list of " - "pair of (cond,val)."; - continue; - } - if (not IN(funcName, name_to_fnapp_vec)) { - // ILA_WARN << "uninterpreted function mapping:" << funcName - // << " does not exist. Skipped."; - continue; - } - if (list_of_time_of_apply.size() != name_to_fnapp_vec[funcName].size()) { - ILA_ERROR << "uninterpreted function mapping:" << funcName << " map:#" - << list_of_time_of_apply.size() << " use in ila:#" - << name_to_fnapp_vec[funcName].size() - << " not matched. Skipped."; - continue; - } - - auto& ila_app_list = name_to_fnapp_vec[funcName]; - - size_t idx = 0; - for (auto&& each_apply : list_of_time_of_apply.items()) { - if (not each_apply.value().is_array()) { - ILA_ERROR << funcName - << ": expecting mapping to be list of pair of (cond,val)."; - idx++; - continue; - } - auto& ila_app_item = ila_app_list[idx]; - idx++; - if (each_apply.value().size() != (ila_app_item.args.size() + 1) * 2) { - ILA_ERROR << "ila func app expect: (1(retval) + " - << ila_app_item.args.size() << "(args) )*2" - << " items. Given:" << each_apply.value().size() - << " items, for func: " << funcName; - continue; - } - auto val_arg_map_str_vec = - each_apply.value().get>(); - - std::string func_reg = funcName + "_" + IntToStr(idx - 1) + "_result_reg"; - // okay now get the chance - auto val_cond = ReplExpr(val_arg_map_str_vec[0]); - auto val_map = ReplExpr(val_arg_map_str_vec[1], - true); // force vlg name on the mapping - auto res_map = "~(" + val_cond + ")||(" + func_reg + "==" + val_map + ")"; - - std::string prep = VLG_TRUE; - for (size_t arg_idx = 2; arg_idx < val_arg_map_str_vec.size(); - arg_idx += 2) { - const auto& cond = ReplExpr(val_arg_map_str_vec[arg_idx]); - const auto& map = ReplExpr(val_arg_map_str_vec[arg_idx + 1], true); - - std::string func_arg = funcName + "_" + IntToStr(idx - 1) + "_arg" + - IntToStr(arg_idx / 2 - 1) + "_reg"; - - prep += "&&(~(" + cond + ")||((" + func_arg + ") == (" + map + ")))"; - } - - add_an_assumption("~(" + prep + ") || (" + res_map + ")", "funcmap"); - } // for each apply in the list of apply - - name_to_fnapp_vec.erase(funcName); // remove from it - } - // check for unmapped func - for (auto&& nf : name_to_fnapp_vec) - ILA_ERROR << "lacking function map for func:" << nf.first; -} // ConstructWrapper_add_uf_constraints // for invariants or for instruction void VlgSglTgtGen::ConstructWrapper() { @@ -1064,10 +410,6 @@ void VlgSglTgtGen::ConstructWrapper() { ConstructWrapper_add_module_instantiation(); } -bool VlgSglTgtGen::bad_state_return(void) { - ILA_ERROR_IF(_bad_state) << "VlgSglTgtGen is in a bad state, cannot proceed."; - return _bad_state; -} // bad_state_return /// create the wrapper file void VlgSglTgtGen::Export_wrapper(const std::string& wrapper_name) { diff --git a/src/vtarget-out/single_target_cond.cc b/src/vtarget-out/single_target_cond.cc new file mode 100644 index 000000000..10b3a0339 --- /dev/null +++ b/src/vtarget-out/single_target_cond.cc @@ -0,0 +1,278 @@ +/// \file Source for Verilog Verification Targets Generation (single target) +/// the conditions +// --- Hongce Zhang + + +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +namespace ilang { + +// ------------- CONFIGURATIONS -------------------- // + +#define VLG_TRUE "`true" +#define VLG_FALSE "`false" + +#define IntToStr(x) (std::to_string(x)) + +// ------------- END of CONFIGURAIONS -------------------- // + +void VlgSglTgtGen::ConstructWrapper_add_cycle_count_moniter() { + // find in rf_cond, how many cycles will be needed + max_bound = 0; + + auto& instr = get_current_instruction_rf(); + + if (!instr.is_null() && IN("ready bound", instr) && + instr["ready bound"].is_number_integer()) + max_bound = instr["ready bound"].get(); + else + max_bound = _vtg_config.MaxBound; + + cnt_width = (int)std::ceil(std::log2(max_bound + 10)); + vlg_wrapper.add_reg("__CYCLE_CNT__", + cnt_width); // by default it will be an output reg + vlg_wrapper.add_stmt("always @(posedge clk) begin"); + vlg_wrapper.add_stmt("if (rst) __CYCLE_CNT__ <= 0;"); + vlg_wrapper.add_stmt( + "else if ( ( __START__ || __STARTED__ ) && __CYCLE_CNT__ < " + + IntToStr(max_bound + 5) + ") __CYCLE_CNT__ <= __CYCLE_CNT__ + 1;"); + vlg_wrapper.add_stmt("end"); + + vlg_wrapper.add_reg("__START__", 1); + vlg_wrapper.add_stmt("always @(posedge clk) begin"); + vlg_wrapper.add_stmt("if (rst) __START__ <= 0;"); + vlg_wrapper.add_stmt("else if (__START__ || __STARTED__) __START__ <= 0;"); + vlg_wrapper.add_stmt("else if (__ISSUE__) __START__ <= 1;"); + vlg_wrapper.add_stmt("end"); + + vlg_wrapper.add_reg("__STARTED__", 1); + vlg_wrapper.add_stmt("always @(posedge clk) begin"); + vlg_wrapper.add_stmt("if (rst) __STARTED__ <= 0;"); + vlg_wrapper.add_stmt( + "else if (__START__) __STARTED__ <= 1;"); // will never return to zero + vlg_wrapper.add_stmt("end"); + + vlg_wrapper.add_reg("__ENDED__", 1); + vlg_wrapper.add_stmt("always @(posedge clk) begin"); + vlg_wrapper.add_stmt("if (rst) __ENDED__ <= 0;"); + vlg_wrapper.add_stmt( + "else if (__IEND__) __ENDED__ <= 1;"); // will never return to zero + vlg_wrapper.add_stmt("end"); + + vlg_wrapper.add_reg("__RESETED__", 1); + vlg_wrapper.add_stmt("always @(posedge clk) begin"); + vlg_wrapper.add_stmt("if (rst) __RESETED__ <= 1;"); + vlg_wrapper.add_stmt("end"); + + // remember to generate + // __RESETED__ + // __ISSUE__ == start condition (if no flush, issue == true?) + // __IEND__ == ( end condition ) && STARTED + // __ENDFLUSH__ == (end flush condition ) && ENDED + // flush : !( __ISSUE__ ? || __START__ || __STARTED__ ) |-> flush +} // ConstructWrapper_add_cycle_count_moniter + + + +// NON-FLUSH case +// 1 RESET +// 2 ISSUE = true RESETED (forever) +// 3 START ---> assume varmap ---> assume inv +// 4 STARTED +// 5 STARTED +// ... ... +// 6 IEND ---> check varmap +// 7 ENDED + +// FLUSH case +// 1 RESET +// 2 RESETED ---> assume flush & preflush cond +// ... ---> assume flush & preflush cond +// n ISSUE = pre-flush end ---> assume flush & preflush cond +// n+1 START ---> assume varmap ---> assume inv +// (maybe globally?) n+2 STARTED n+3 STARTED +// ... ... (forever) +// m IEND +// m+1 ENDED ---> assume flush & postflush cond +// ... ENDED (forever) ---> assume flush & postflush cond +// l ENDFLUSH = post-flush end ---> assume flush & postflush cond +// ---> assert varmap l+1 FLUSHENDED ---> assume flush +// & postflush cond +// + +void VlgSglTgtGen::ConstructWrapper_add_condition_signals() { + // TODO + // remember to generate + // __ISSUE__ == start condition (if no flush, issue == true?) + // __IEND__ == ( end condition ) && STARTED + // __ENDFLUSH__ == (end flush condition ) && ENDED + // flush : !( __ISSUE__ ? || __START__ || __STARTED__ ) |-> flush + + if (target_type == target_type_t::INVARIANTS) + return; + // we don't need additional signals, just make reset drives the design + + // find the instruction + auto& instr = get_current_instruction_rf(); + ILA_ASSERT(!instr.is_null()); + + // __IEND__ + std::string iend_cond = VLG_FALSE; + // bool no_started_signal = false; + if (ready_type & ready_type_t::READY_SIGNAL) { + if (instr["ready signal"].is_string()) { + iend_cond += "|| (" + + ReplExpr(instr["ready signal"].get(), true) + + ")"; // force vlg + } else if (instr["ready signal"].is_array()) { + for (auto&& cond : instr["ready signal"]) + if (cond.is_string()) + iend_cond += " || (" + ReplExpr(cond.get()) + ")"; + else + ILA_ERROR << "ready signal field of instruction: " + << _instr_ptr->name().str() + << " has to be string or array or string"; + } else + ILA_ERROR << "ready signal field of instruction: " + << _instr_ptr->name().str() + << " has to be string or array or string"; + } + if (ready_type & ready_type_t::READY_BOUND) { // can be both applied + if (instr["ready bound"].is_number_integer()) { + int bound = instr["ready bound"].get(); + if (bound > 0) { + // okay now we enforce the bound + iend_cond += "|| ( __CYCLE_CNT__ == " + + ReplExpr(IntToStr(cnt_width) + "'d" + IntToStr(bound)) + + ")"; + } else if (bound == 0) { + // iend_cond += "|| (__START__)"; + // no_started_signal = true; // please don't use && STARTED + ILA_ERROR << "Does not support bound : 0, please use a buffer to hold " + "the signal."; + } else + ILA_ERROR << "ready bound field of instruction: " + << _instr_ptr->name().str() + << " has to a non negative integer"; + } else + ILA_ERROR << "ready bound field of instruction: " + << _instr_ptr->name().str() << " has to a non negative integer"; + } // end of ready bound/condition + + // max bound for max checking range + std::string max_bound_constr; + if (IN("max bound", instr)) { + if (instr["max bound"].is_number_integer()) { + max_bound_constr = + "&& ( __CYCLE_CNT__ <= " + IntToStr(instr["max bound"].get()) + + ")"; + } + } + + vlg_wrapper.add_wire("__IEND__", 1, true); + // if(no_started_signal) + // add_wire_assign_assumption("__IEND__", "(" + iend_cond + ")", + // "IEND"); + // else + auto end_no_recur = has_flush ? "(~ __FLUSHENDED__ )" : "(~ __ENDED__)"; + + add_wire_assign_assumption("__IEND__", + "(" + iend_cond + ") && __STARTED__ && " + + end_no_recur + max_bound_constr, + "IEND"); + // handle start decode + ILA_ERROR_IF(IN("start decode", instr)) + << "'start decode' is replaced by start condition!"; + if (IN("start condition", instr)) { + handle_start_condition(instr["start condition"]); + } else { + add_an_assumption("(~ __START__) || (" + vlg_ila.decodeNames[0] + ")", + "issue_decode"); // __ISSUE__ |=> decode + add_an_assumption("(~ __START__) || (" + vlg_ila.validName + ")", + "issue_valid"); // __ISSUE__ |=> decode + } + + if (has_flush) { + ILA_ASSERT(IN("pre-flush end", instr) && + IN("post-flush end", instr)); // there has to be something + + std::string issue_cond; + if (instr["pre-flush end"].is_string()) + issue_cond = "(" + ReplExpr(instr["pre-flush end"].get()) + + ") && __RESETED__"; + else { + issue_cond = "1"; + ILA_ERROR << "pre-flush end field should be a string!"; + } + vlg_wrapper.add_wire("__ISSUE__", 1, true); + add_wire_assign_assumption("__ISSUE__", issue_cond, "ISSUE"); + + std::string finish_cond; + if (instr["post-flush end"].is_string()) + finish_cond = "(" + ReplExpr(instr["post-flush end"].get()) + + ") && __ENDED__"; + else { + finish_cond = "1"; + ILA_ERROR << "post-flush end field should be a string!"; + } + vlg_wrapper.add_wire("__ENDFLUSH__", 1, true); + add_wire_assign_assumption("__ENDFLUSH__", finish_cond, "ENDFLUSH"); + + vlg_wrapper.add_reg("__FLUSHENDED__", 1); + vlg_wrapper.add_stmt( + "always @(posedge clk) begin\n" + "if(rst) __FLUSHENDED__ <= 0;\n" + "else if( __ENDFLUSH__ && __ENDED__ ) __FLUSHENDED__ <= 1;\n end"); + + // enforcing flush constraints + std::string flush_enforcement = VLG_TRUE; + if (instr["flush constraints"].is_null()) { + } // do nothing. we are good + else if (instr["flush constraints"].is_string()) { + flush_enforcement += + "&& (" + ReplExpr(instr["flush constraints"].get()) + + ")"; + } else if (instr["flush constraints"].is_array()) { + for (auto&& c : instr["flush constraints"]) + if (c.is_string()) + flush_enforcement += "&& (" + ReplExpr(c.get()) + ")"; + else + ILA_ERROR << "flush constraint field of instruction:" + << _instr_ptr->name().str() + << " must be a string or an array of string."; + } else + ILA_ERROR << "flush constraint field of instruction:" + << _instr_ptr->name().str() + << " must be string or array of string."; + + // TODO: preflush and postflush + + add_an_assumption( + "(~ ( __RESETED__ && ~ ( __START__ || __STARTED__ ) ) ) || (" + + flush_enforcement + ")", + "flush_enforce_pre"); + add_an_assumption("(~ ( __ENDED__ )) || (" + flush_enforcement + ")", + "flush_enforce_post"); + + } else { + vlg_wrapper.add_wire("__ISSUE__", 1, true); + if (_vtg_config.ForceInstCheckReset) { + vlg_wrapper.add_input("__ISSUE__", 1); + } else + add_wire_assign_assumption("__ISSUE__", "1", "ISSUE"); // issue ASAP + // start decode -- issue enforce (e.g. valid, input) + } // end of no flush +} // ConstructWrapper_add_condition_signals + + +} // namespace ilang + diff --git a/src/vtarget-out/single_target_connect.cc b/src/vtarget-out/single_target_connect.cc new file mode 100644 index 000000000..ecba3f65d --- /dev/null +++ b/src/vtarget-out/single_target_connect.cc @@ -0,0 +1,333 @@ +/// \file Source for Verilog Verification Targets Generation (single target) +/// the connection wires / instantiation and etc. +// --- Hongce Zhang + + +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +namespace ilang { + +// ------------- CONFIGURATIONS -------------------- // + +#define VLG_TRUE "`true" +#define VLG_FALSE "`false" + +#define IntToStr(x) (std::to_string(x)) + +// ------------- END of CONFIGURAIONS -------------------- // + +// ------------------------ ILA ----------------------------- // + +void VlgSglTgtGen::ConstructWrapper_add_ila_input() { + // add ila input + size_t ila_input_num = _host->input_num(); + for (size_t input_idx = 0; input_idx < ila_input_num; input_idx++) { + const auto& input_ = _host->input(input_idx); + const auto& name_ = input_->name().str(); + auto width_ = get_width(input_); + + vlg_wrapper.add_wire("__ILA_I_" + name_, width_, true); + vlg_wrapper.add_input("__ILA_I_" + name_, width_); + } + // remember to add ila_outputs (reg) + size_t ila_state_num = _host->state_num(); + for (size_t state_idx = 0; state_idx < ila_state_num; ++state_idx) { + const auto& state_ = _host->state(state_idx); + const auto& name_ = state_->name().str(); + if (state_->sort()->is_mem()) + continue; // please ignore memory, they should not be connected this way + auto width_ = get_width(state_); + + vlg_wrapper.add_wire("__ILA_SO_" + name_, width_, true); + vlg_wrapper.add_output("__ILA_SO_" + name_, width_); + // remember to connect in the instantiation step + } +} // ConstructWrapper_add_ila_input + + +std::string VlgSglTgtGen::ConstructWrapper_get_ila_module_inst() { + if (target_type == target_type_t::INVARIANTS) + return ""; + + ILA_ASSERT(vlg_ila.decodeNames.size() == 1) + << "Implementation bug: decode condition."; + vlg_wrapper.add_wire(vlg_ila.validName, 1, true); + vlg_wrapper.add_wire(vlg_ila.decodeNames[0], 1, true); + + // TODO: check whether all ports have been dealt with + // TODO: check whether there are any extra ports we create + std::set port_connected; // store the name of ila port + std::set port_of_ila; // store the name of ila port also + + // .. record function + + // this is the string to construct + auto retStr = vlg_ila.moduleName + " " + _ila_mod_inst_name + " (\n"; + + std::set func_port_skip_set; + for (auto&& func_app : vlg_ila.ila_func_app) { + func_port_skip_set.insert(func_app.result.first); + port_connected.insert(func_app.result.first); + /// new reg : put in when __START__ + if (not IN(func_app.func_name, func_cnt)) + func_cnt.insert({func_app.func_name, 0}); + unsigned func_no = func_cnt[func_app.func_name]++; + + std::string func_reg_w = + func_app.func_name + "_" + IntToStr(func_no) + "_result_wire"; + std::string func_reg = + func_app.func_name + "_" + IntToStr(func_no) + "_result_reg"; + vlg_wrapper.add_reg(func_reg, func_app.result.second); + vlg_wrapper.add_wire(func_reg_w, func_app.result.second, true); + // add as a module input, also + vlg_wrapper.add_input(func_reg_w, func_app.result.second); + + add_reg_cassign_assumption(func_reg, func_reg_w, "__START__", + "func_result"); + // vlg_wrapper.add_always_stmt( "if( __START__ ) " + func_reg + " <= " + + // func_reg_w + ";" ); + + retStr += " ." + func_app.result.first + "(" + func_reg_w + "),\n"; + + unsigned argNo = 0; + for (auto&& arg : func_app.args) { + func_port_skip_set.insert(arg.first); + port_connected.insert(arg.first); + + std::string func_arg_w = func_app.func_name + "_" + IntToStr(func_no) + + "_arg" + IntToStr(argNo) + "_wire"; + std::string func_arg = func_app.func_name + "_" + IntToStr(func_no) + + "_arg" + IntToStr(argNo) + "_reg"; + vlg_wrapper.add_reg(func_arg, arg.second); + vlg_wrapper.add_wire(func_arg_w, arg.second, true); + add_reg_cassign_assumption(func_arg, func_arg_w, "__START__", "func_arg"); + // vlg_wrapper.add_always_stmt( "if( __START__ ) " + func_arg + " <= " + + // func_arg_w + ";" ); + + retStr += " ." + arg.first + "(" + func_arg_w + "),\n"; + argNo++; + } + } // end of functions + + // handle input + for (auto&& w : vlg_ila.inputs) { + if (IN(w.first, func_port_skip_set)) + continue; + // w.first will be connected + port_connected.insert(w.first); + // deal w. clock and reset and start + if (w.first == vlg_ila.clkName) // .clk(clk) + retStr += " ." + vlg_ila.clkName + "(" + vlg_wrapper.clkName + "),\n"; + else if (w.first == + vlg_ila.rstName) // .rst(rst) -- this does not need to be changed + retStr += " ." + vlg_ila.rstName + "(" + vlg_wrapper.rstName + + "),\n"; // no init anyway! + else if (w.first == vlg_ila.startName) { // .__START__(__START__) + retStr += " ." + vlg_ila.startName + "(" + "__START__" + "),\n"; + } else { + ILA_ERROR_IF(not IN("__ILA_I_" + w.first, vlg_wrapper.wires)) + << "__ILA_I_" + w.first << " has not been defined yet"; + retStr += " ." + w.first + "(__ILA_I_" + w.first + "),\n"; + } + } // end of inputs + + // TODO:: FUnction here ! + // handle output + for (auto&& w : vlg_ila.outputs) { + if (IN(w.first, func_port_skip_set)) + continue; + // w.first will be connected + port_connected.insert(w.first); + // deal w. valid and decode + if (w.first == vlg_ila.decodeNames[0]) + retStr += " ." + vlg_ila.decodeNames[0] + "(" + vlg_ila.decodeNames[0] + + "),\n"; + else if (w.first == vlg_ila.validName) + retStr += " ." + vlg_ila.validName + "(" + vlg_ila.validName + "),\n"; + else { + // ILA_ERROR_IF( not IN ("__ILA_I_" + w.first , vlg_wrapper.wires) ) << + // "__ILA_I_" + w.first << " has not been defined yet"; + ILA_ERROR << "Does not know how to connect:" << w.first << ", ignored."; + // std::cout<< w.first< 0 && dw > 0) + << "Implementation bug: unable to find mem:" << ila_name; + + for (auto&& rport : rports) { + auto no = rport.first; // is the num + auto port = rport.second; // is the port + auto rdw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_rdata"; + auto raw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_raddr"; + // auto rew = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_ren"; no need, + // r_en is the start signal + + vlg_wrapper.add_wire(rdw, dw, true); + vlg_wrapper.add_wire(raw, aw, true); + + retStr += " ." + port.rdata + "(" + rdw + "),\n"; + retStr += " ." + port.raddr + "(" + raw + "),\n"; + + // port.rdata/raddr will be connected + port_connected.insert(port.rdata); + port_connected.insert(port.raddr); + + } // for rport + } // for ila_rports + + for (auto&& ila_name_wport_pair : vlg_ila.ila_wports) { + + const auto& ila_name = ila_name_wport_pair.first; + const auto& wports = ila_name_wport_pair.second; + const auto adw = GetMemInfo(ila_name); + auto aw = adw.first; + auto dw = adw.second; // address/data width + ILA_ASSERT(aw > 0 && dw > 0) + << "Implementation bug: unable to find mem:" << ila_name; + + for (auto&& wport : wports) { + auto no = wport.first; // is the num + auto port = wport.second; // is the port + auto wdw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_wdata"; + auto waw = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_waddr"; + auto wew = "__IMEM_" + ila_name + "_" + IntToStr(no) + "_wen"; + + vlg_wrapper.add_wire(wdw, dw, true); + vlg_wrapper.add_wire(waw, aw, true); + vlg_wrapper.add_wire(wew, 1, true); + + retStr += " ." + port.wdata + "(" + wdw + "),\n"; + retStr += " ." + port.waddr + "(" + waw + "),\n"; + retStr += " ." + port.wen + "(" + wew + "),\n"; + + // port.rdata/raddr will be connected + port_connected.insert(port.wdata); + port_connected.insert(port.waddr); + port_connected.insert(port.wen); + + } // for wport + } // for ila_wports + + // handle state-output + std::string sep; + for (auto&& r : vlg_ila.regs) { + if (not IN("__ILA_SO_" + r.first, vlg_wrapper.wires)) { + ILA_WARN << "__ILA_SO_" + r.first << " will be ignored"; + + retStr += sep + " ." + r.first + "()"; // __ILA_SO_" + r.first + " + port_connected.insert(r.first); + sep = ",\n"; + continue; + } // else + retStr += sep + " ." + r.first + "(__ILA_SO_" + r.first + ")"; + sep = ",\n"; + // reg out will be connected + port_connected.insert(r.first); + } + retStr += "\n);"; + // TODO: check port_conencted and port_ila + // currently not + return retStr; +} // ConstructWrapper_get_ila_module_inst() + + +// ------------------------ VERILOG ----------------------------- // + +void VlgSglTgtGen::ConstructWrapper_add_vlg_input_output() { + + auto vlg_inputs = vlg_info_ptr->get_top_module_io(); + auto& io_map = rf_vmap["interface mapping"]; + for (auto&& name_siginfo_pair : vlg_inputs) { + std::string refstr = + IN(name_siginfo_pair.first, io_map) + ? io_map[name_siginfo_pair.first].get() + : ""; + _idr.RegisterInterface( + name_siginfo_pair.second, refstr, + // Verifier_compatible_w_ila_input + [this](const std::string& ila_name, + const SignalInfoBase& vlg_sig_info) -> bool { + return TypeMatched(IlaGetInput(ila_name), vlg_sig_info) != 0; + }, + // no need to worry about the nullptr in IlaGetInput, TypeMatched will + // be able to handle. + // Verifier_get_ila_mem_info + [this]( + const std::string& ila_mem_name) -> std::pair { + return GetMemInfo(ila_mem_name); + }); // end of function call: RegisterInterface + } +} // ConstructWrapper_add_vlg_input_output + + +// ------------------------ ALL instantiation ----------------------------- // +void VlgSglTgtGen::ConstructWrapper_add_module_instantiation() { + // instantiate ila module + if (target_type == target_type_t::INSTRUCTIONS) { + auto ila_mod_inst = ConstructWrapper_get_ila_module_inst(); + vlg_wrapper.add_stmt(ila_mod_inst); + } + + // instantiate verilog module + std::string verilog_inst_str = + vlg_info_ptr->get_top_module_name() + " " + _vlg_mod_inst_name + "(\n"; + + _idr.VlgAddTopInteface( + vlg_wrapper); // put the extra wire there, and it should add wire also + verilog_inst_str += _idr.GetVlgModInstString(vlg_wrapper); + verilog_inst_str += ");"; + + vlg_wrapper.add_stmt(verilog_inst_str); +} // ConstructWrapper_add_module_instantiation + +// ------------------------ OTERHS (refs) ----------------------------- // +void VlgSglTgtGen::ConstructWrapper_register_extra_io_wire() { + for (auto&& refered_vlg_item : _all_referred_vlg_names) { + + auto idx = refered_vlg_item.first.find("["); + auto removed_range_name = refered_vlg_item.first.substr(0, idx); + auto vlg_sig_info = vlg_info_ptr->get_signal(removed_range_name); + + auto vname = ReplaceAll( + ReplaceAll(ReplaceAll(refered_vlg_item.first, ".", "__DOT__"), "[", + "_"), + "]", "_"); + // + ReplaceAll(ReplaceAll(refered_vlg_item.second.range, "[","_"),"]","_"); + // // name for verilog + auto width = vlg_sig_info.get_width(); + + vlg_wrapper.add_wire(vname, width, 1); // keep + vlg_wrapper.add_output(vname, width); // add as output of the wrapper + _idr.RegisterExtraWire(vname, vname); + // these will be connected to the verilog module, so register as extra wires + // so, later they will be connected + } +} // ConstructWrapper_register_extra_io_wire + +} // namespace ilang + diff --git a/src/vtarget-out/single_target_inv_syn_support.cc b/src/vtarget-out/single_target_inv_syn_support.cc new file mode 100644 index 000000000..21e37f94d --- /dev/null +++ b/src/vtarget-out/single_target_inv_syn_support.cc @@ -0,0 +1,30 @@ +/// \file Source for Verilog Verification Targets Generation (single target) +/// the invariants (how they assume and assert) +/// the support for inv-syn (monolithic/cegar) +// --- Hongce Zhang + + +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +namespace ilang { + +// ------------- CONFIGURATIONS -------------------- // + +#define VLG_TRUE "`true" +#define VLG_FALSE "`false" + +#define IntToStr(x) (std::to_string(x)) + + + +} // namespace ilang + diff --git a/src/vtarget-out/single_target_misc.cc b/src/vtarget-out/single_target_misc.cc new file mode 100644 index 000000000..1db2d0a0e --- /dev/null +++ b/src/vtarget-out/single_target_misc.cc @@ -0,0 +1,154 @@ +/// \file Source for Verilog Verification Targets Generation (single target) +/// the miscs : UF/MEM/AMC/Post-value-holder/cycle-count +// --- Hongce Zhang + + +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +namespace ilang { + +// ------------- CONFIGURATIONS -------------------- // + +#define VLG_TRUE "`true" +#define VLG_FALSE "`false" + +#define IntToStr(x) (std::to_string(x)) + +// ------------- END of CONFIGURAIONS -------------------- // + +bool VlgSglTgtGen::bad_state_return(void) { + ILA_ERROR_IF(_bad_state) << "VlgSglTgtGen is in a bad state, cannot proceed."; + return _bad_state; +} // bad_state_return + +void VlgSglTgtGen::ConstructWrapper_add_additional_mapping_control() { + if (IN("mapping control", rf_vmap)) { + if (not rf_vmap["mapping control"].is_array()) + ILA_ERROR << "mapping control field must be an array of string"; + for (auto&& c : rf_vmap["mapping control"]) { + if (not c.is_string()) { + ILA_ERROR << "mapping control field must be an array of string"; + continue; + } + add_an_assumption(ReplExpr(c.get()), + "additional_mapping_control_assume"); + } + } +} // ConstructWrapper_add_additional_mapping_control + +void VlgSglTgtGen::ConstructWrapper_add_helper_memory() { + auto endCond = + has_flush ? "__ENDFLUSH__ || __FLUSHENDED__" : "__IEND__ || __ENDED__"; + + auto stmt = _idr.GetAbsMemInstString(vlg_wrapper, endCond); + vlg_wrapper.add_stmt(stmt); + + // check if we need to insert any assumptions + auto inserter = [this](const std::string& p) -> void { + add_an_assumption(p, "absmem"); + }; + _idr.InsertAbsMemAssmpt(inserter); +} // ConstructWrapper_add_helper_memory + + +void VlgSglTgtGen::ConstructWrapper_add_uf_constraints() { + if (not IN("functions", rf_vmap)) + return; // do nothing + auto& fm = rf_vmap["functions"]; + if (not fm.is_object()) { + ILA_ERROR << "expect functions field to be funcName -> list of list of " + "pair of (cond,val)."; + return; + } + + // convert vlg_ila.ila_func_app to name->list of func_app + std::map + name_to_fnapp_vec; + for (auto&& func_app : vlg_ila.ila_func_app) + name_to_fnapp_vec[func_app.func_name].push_back(func_app); + + for (auto&& it : fm.items()) { + const auto& funcName = it.key(); + const auto& list_of_time_of_apply = it.value(); + if (not list_of_time_of_apply.is_array()) { + ILA_ERROR << funcName + << ": expect functions field to be funcName -> list of list of " + "pair of (cond,val)."; + continue; + } + if (not IN(funcName, name_to_fnapp_vec)) { + // ILA_WARN << "uninterpreted function mapping:" << funcName + // << " does not exist. Skipped."; + continue; + } + if (list_of_time_of_apply.size() != name_to_fnapp_vec[funcName].size()) { + ILA_ERROR << "uninterpreted function mapping:" << funcName << " map:#" + << list_of_time_of_apply.size() << " use in ila:#" + << name_to_fnapp_vec[funcName].size() + << " not matched. Skipped."; + continue; + } + + auto& ila_app_list = name_to_fnapp_vec[funcName]; + + size_t idx = 0; + for (auto&& each_apply : list_of_time_of_apply.items()) { + if (not each_apply.value().is_array()) { + ILA_ERROR << funcName + << ": expecting mapping to be list of pair of (cond,val)."; + idx++; + continue; + } + auto& ila_app_item = ila_app_list[idx]; + idx++; + if (each_apply.value().size() != (ila_app_item.args.size() + 1) * 2) { + ILA_ERROR << "ila func app expect: (1(retval) + " + << ila_app_item.args.size() << "(args) )*2" + << " items. Given:" << each_apply.value().size() + << " items, for func: " << funcName; + continue; + } + auto val_arg_map_str_vec = + each_apply.value().get>(); + + std::string func_reg = funcName + "_" + IntToStr(idx - 1) + "_result_reg"; + // okay now get the chance + auto val_cond = ReplExpr(val_arg_map_str_vec[0]); + auto val_map = ReplExpr(val_arg_map_str_vec[1], + true); // force vlg name on the mapping + auto res_map = "~(" + val_cond + ")||(" + func_reg + "==" + val_map + ")"; + + std::string prep = VLG_TRUE; + for (size_t arg_idx = 2; arg_idx < val_arg_map_str_vec.size(); + arg_idx += 2) { + const auto& cond = ReplExpr(val_arg_map_str_vec[arg_idx]); + const auto& map = ReplExpr(val_arg_map_str_vec[arg_idx + 1], true); + + std::string func_arg = funcName + "_" + IntToStr(idx - 1) + "_arg" + + IntToStr(arg_idx / 2 - 1) + "_reg"; + + prep += "&&(~(" + cond + ")||((" + func_arg + ") == (" + map + ")))"; + } + + add_an_assumption("~(" + prep + ") || (" + res_map + ")", "funcmap"); + } // for each apply in the list of apply + + name_to_fnapp_vec.erase(funcName); // remove from it + } + // check for unmapped func + for (auto&& nf : name_to_fnapp_vec) + ILA_ERROR << "lacking function map for func:" << nf.first; +} // ConstructWrapper_add_uf_constraints + + + +} // namespace ilang diff --git a/test/t_verilog_analysis.cc b/test/t_verilog_analysis.cc index 99d5698c8..106053517 100644 --- a/test/t_verilog_analysis.cc +++ b/test/t_verilog_analysis.cc @@ -107,7 +107,7 @@ TEST(TestVerilogAnalysis, RangeAnalysis) { IS_WIDTH("rm", 2); IS_WIDTH("a", 1); // F IS_WIDTH("b", 1); // F - IS_WIDTH("c", 1); // F + IS_WIDTH("c", 2); // F IS_WIDTH("d", 1); // F } // end of test1 { // test 2