From 393f0b0ac3899646ceb6a644e91d98023c2fbe33 Mon Sep 17 00:00:00 2001 From: tangxifan Date: Sat, 5 Oct 2019 21:16:48 -0600 Subject: [PATCH] align formal verification port inside refactored routing blocks --- .../vpr/SRC/fpga_x2p/base/rr_blocks_utils.cpp | 80 +++++++++++++++++ .../vpr/SRC/fpga_x2p/base/rr_blocks_utils.h | 14 +++ .../SRC/fpga_x2p/verilog/verilog_routing.c | 87 ++++++++++++++++--- .../fpga_x2p/verilog/verilog_writer_utils.cpp | 13 ++- .../fpga_x2p/verilog/verilog_writer_utils.h | 3 +- 5 files changed, 182 insertions(+), 15 deletions(-) diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.cpp index 9184e29d6..96dff6375 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.cpp @@ -6,6 +6,7 @@ #include "vtr_assert.h" #include "vpr_types.h" +#include "mux_utils.h" #include "fpga_x2p_types.h" #include "rr_blocks_utils.h" @@ -176,3 +177,82 @@ size_t find_switch_block_number_of_muxes(const RRGSB& rr_gsb) { return num_muxes; } +/********************************************************************* + * Find the number of configuration bits of a Connection Block + ********************************************************************/ +size_t find_connection_block_num_conf_bits(t_sram_orgz_info* cur_sram_orgz_info, + const CircuitLibrary& circuit_lib, + const MuxLibrary& mux_lib, + const std::vector& rr_switches, + const RRGSB& rr_gsb, + const t_rr_type& cb_type) { + size_t num_conf_bits = 0; + + std::vector cb_ipin_sides = rr_gsb.get_cb_ipin_sides(cb_type); + for (size_t iside = 0; iside < cb_ipin_sides.size(); ++iside) { + enum e_side cb_ipin_side = cb_ipin_sides[iside]; + for (size_t inode = 0; inode < rr_gsb.get_num_ipin_nodes(cb_ipin_side); ++inode) { + /* Find the size of routing multiplexers driving this IPIN node */ + int mux_size = rr_gsb.get_ipin_node(cb_ipin_side, inode)->fan_in; + /* Bypass fan_in == 1 or 0, they are not considered as routing multiplexers */ + if (2 > mux_size) { + continue; + } + + /* Get the circuit model id of the routing multiplexer */ + size_t switch_index = rr_gsb.get_ipin_node(cb_ipin_side, inode)->drive_switches[DEFAULT_SWITCH_ID]; + CircuitModelId mux_model = rr_switches[switch_index].circuit_model; + + /* Find the input size of the implementation of a routing multiplexer */ + size_t datapath_mux_size = rr_gsb.get_ipin_node(cb_ipin_side, inode)->fan_in; + /* Get the multiplexing graph from the Mux Library */ + MuxId mux_id = mux_lib.mux_graph(mux_model, datapath_mux_size); + const MuxGraph& mux_graph = mux_lib.mux_graph(mux_id); + num_conf_bits += find_mux_num_config_bits(circuit_lib, mux_model, mux_graph, cur_sram_orgz_info->type); + } + } + + return num_conf_bits; +} + + +/********************************************************************* + * Find the number of configuration bits of a Switch Block + ********************************************************************/ +size_t find_switch_block_num_conf_bits(t_sram_orgz_info* cur_sram_orgz_info, + const CircuitLibrary& circuit_lib, + const MuxLibrary& mux_lib, + const std::vector& rr_switches, + const RRGSB& rr_gsb) { + size_t num_conf_bits = 0; + + for (size_t side = 0; side < rr_gsb.get_num_sides(); ++side) { + Side side_manager(side); + for (size_t itrack = 0; itrack < rr_gsb.get_chan_width(side_manager.get_side()); ++itrack) { + if (OUT_PORT != rr_gsb.get_chan_node_direction(side_manager.get_side(), itrack)) { + continue; + } + /* Check if this node is just a passing wire */ + if (true == rr_gsb.is_sb_node_passing_wire(side_manager.get_side(), itrack)) { + continue; + } + /* Check if this node has more than 2 drivers */ + if (2 > rr_gsb.get_chan_node(side_manager.get_side(), itrack)->num_drive_rr_nodes) { + continue; + } + /* Get the circuit model id of the routing multiplexer */ + size_t switch_index = rr_gsb.get_chan_node(side_manager.get_side(), itrack)->drive_switches[DEFAULT_SWITCH_ID]; + CircuitModelId mux_model = rr_switches[switch_index].circuit_model; + + /* Find the input size of the implementation of a routing multiplexer */ + size_t datapath_mux_size = rr_gsb.get_chan_node(side_manager.get_side(), itrack)->num_drive_rr_nodes; + /* Get the multiplexing graph from the Mux Library */ + MuxId mux_id = mux_lib.mux_graph(mux_model, datapath_mux_size); + const MuxGraph& mux_graph = mux_lib.mux_graph(mux_id); + num_conf_bits += find_mux_num_config_bits(circuit_lib, mux_model, mux_graph, cur_sram_orgz_info->type); + } + } + + return num_conf_bits; +} + diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.h b/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.h index 0ad9113fb..78bb981d5 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.h +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/base/rr_blocks_utils.h @@ -9,6 +9,7 @@ #include "physical_types.h" #include "circuit_library.h" #include "rr_blocks.h" +#include "mux_library.h" std::vector find_connection_block_global_ports(const RRGSB& rr_gsb, const t_rr_type& cb_type, @@ -24,4 +25,17 @@ size_t find_connection_block_number_of_muxes(const RRGSB& rr_gsb, size_t find_switch_block_number_of_muxes(const RRGSB& rr_gsb); +size_t find_connection_block_num_conf_bits(t_sram_orgz_info* cur_sram_orgz_info, + const CircuitLibrary& circuit_lib, + const MuxLibrary& mux_lib, + const std::vector& rr_switches, + const RRGSB& rr_gsb, + const t_rr_type& cb_type); + +size_t find_switch_block_num_conf_bits(t_sram_orgz_info* cur_sram_orgz_info, + const CircuitLibrary& circuit_lib, + const MuxLibrary& mux_lib, + const std::vector& rr_switches, + const RRGSB& rr_gsb); + #endif diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_routing.c b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_routing.c index 4ba51216f..57eb32e21 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_routing.c +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_routing.c @@ -97,6 +97,30 @@ void print_verilog_switch_block_local_sram_wires(std::fstream& fp, print_verilog_local_sram_wires(fp, circuit_lib, sram_model, sram_orgz_type, local_port_size); } +/******************************************************************** + * Check if the MSB of a configuration bus of a connection block + * matches the expected value + * Exception: + * 1. Configuration bus for configuration chain will follow + * the number of multiplexers in the connection block + ********************************************************************/ +static +bool check_connection_block_mem_config_bus(const e_sram_orgz& sram_orgz_type, + const RRGSB& rr_gsb, + const t_rr_type& cb_type, + const BasicPort& config_bus, + const size_t& expected_msb) { + size_t local_expected_msb = expected_msb; + if (SPICE_SRAM_SCAN_CHAIN == sram_orgz_type) { + /* Note the size of local wires is number of routing multiplexers + 1 + * Wire MSB is the number of routing multiplexers in the configuration chain + */ + local_expected_msb = find_connection_block_number_of_muxes(rr_gsb, cb_type); + } + return check_mem_config_bus(sram_orgz_type, config_bus, local_expected_msb); +} + + /******************************************************************** * Check if the MSB of a configuration bus of a switch block * matches the expected value @@ -2452,6 +2476,7 @@ void print_verilog_unique_switch_box_mux(ModuleManager& module_manager, std::fstream& fp, t_sram_orgz_info* cur_sram_orgz_info, BasicPort& config_bus, + BasicPort& fm_config_bus, const ModuleId& sb_module, const RRGSB& rr_sb, const CircuitLibrary& circuit_lib, @@ -2522,9 +2547,15 @@ void print_verilog_unique_switch_box_mux(ModuleManager& module_manager, print_verilog_comment(fp, std::string("----- BEGIN Local wires used in only formal verification purpose -----")); print_verilog_preprocessing_flag(fp, std::string(verilog_formal_verification_preproc_flag)); /* Print the SRAM configuration ports for formal verification */ - /* TODO: align with the port width of formal verification port of SB module */ + /* Update config bus for formal verification, + * shift with number of configuration bit of the MUX + */ + fm_config_bus.set_width(fm_config_bus.get_msb() + 1, fm_config_bus.get_msb() + mux_num_config_bits); + + /* Align with the port width of formal verification port of SB module */ print_verilog_formal_verification_mux_sram_ports_wiring(fp, circuit_lib, mux_model, - datapath_mux_size, mux_instance_id, mux_num_config_bits); + datapath_mux_size, mux_instance_id, + mux_num_config_bits, fm_config_bus); print_verilog_endif(fp); print_verilog_comment(fp, std::string("----- END Local wires used in only formal verification purpose -----")); fp << std::endl; @@ -2627,6 +2658,7 @@ void print_verilog_unique_switch_box_interc(ModuleManager& module_manager, std::fstream& fp, t_sram_orgz_info* cur_sram_orgz_info, BasicPort& config_bus, + BasicPort& fm_config_bus, const ModuleId& sb_module, const RRGSB& rr_sb, const CircuitLibrary& circuit_lib, @@ -2661,7 +2693,8 @@ void print_verilog_unique_switch_box_interc(ModuleManager& module_manager, drive_rr_nodes[DEFAULT_SWITCH_ID]); } else if (1 < drive_rr_nodes.size()) { /* Print the multiplexer, fan_in >= 2 */ - print_verilog_unique_switch_box_mux(module_manager, fp, cur_sram_orgz_info, config_bus, + print_verilog_unique_switch_box_mux(module_manager, fp, cur_sram_orgz_info, + config_bus, fm_config_bus, sb_module, rr_sb, circuit_lib, mux_lib, rr_switches, chan_side, cur_rr_node, drive_rr_nodes, @@ -2745,7 +2778,7 @@ void print_verilog_routing_switch_box_unique_module(ModuleManager& module_manage const bool& is_explicit_mapping) { /* TODO: move this part to another function where we count the conf bits for all the switch blocks !!!*/ /* Count the number of configuration bits to be consumed by this Switch block */ - int num_conf_bits = count_verilog_switch_box_conf_bits(cur_sram_orgz_info, rr_sb); + int num_conf_bits = find_switch_block_num_conf_bits(cur_sram_orgz_info, circuit_lib, mux_lib, rr_switches, rr_sb); /* Count the number of reserved configuration bits to be consumed by this Switch block */ int num_reserved_conf_bits = count_verilog_switch_box_reserved_conf_bits(cur_sram_orgz_info, rr_sb); /* Estimate the sram_verilog_model->cnt */ @@ -2866,6 +2899,11 @@ void print_verilog_routing_switch_box_unique_module(ModuleManager& module_manage /* Counter start from 0 */ config_bus.set_width(0, 0); + /* Create a counter for the configuration bus used for formal verification */ + BasicPort fm_config_bus; + /* fm_config_bus has an invalid width here. It is designed to be easy to rotate */ + fm_config_bus.set_width(0, -1); + /* TODO: Print routing multiplexers */ for (size_t side = 0; side < rr_gsb.get_num_sides(); ++side) { Side side_manager(side); @@ -2873,7 +2911,8 @@ void print_verilog_routing_switch_box_unique_module(ModuleManager& module_manage for (size_t itrack = 0; itrack < rr_gsb.get_chan_width(side_manager.get_side()); ++itrack) { /* We care INC_DIRECTION tracks at this side*/ if (OUT_PORT == rr_gsb.get_chan_node_direction(side_manager.get_side(), itrack)) { - print_verilog_unique_switch_box_interc(module_manager, fp, cur_sram_orgz_info, config_bus, + print_verilog_unique_switch_box_interc(module_manager, fp, cur_sram_orgz_info, + config_bus, fm_config_bus, module_id, rr_sb, circuit_lib, mux_lib, rr_switches, side_manager.get_side(), @@ -2882,10 +2921,13 @@ void print_verilog_routing_switch_box_unique_module(ModuleManager& module_manage } } - /* TODO: Add check code for config_bus. The MSB should match the number of configuration bits!!! */ + /* Add check code for config_bus. + * The MSB should match the number of configuration bits!!! + */ VTR_ASSERT(true == check_switch_block_mem_config_bus(cur_sram_orgz_info->type, rr_gsb, config_bus, rr_gsb.get_sb_num_conf_bits())); + VTR_ASSERT(fm_config_bus.get_msb() == rr_gsb.get_sb_num_conf_bits() - 1); /* Put an end to the Verilog module */ print_verilog_module_end(fp, module_manager.module_name(module_id)); @@ -3598,6 +3640,7 @@ void print_verilog_connection_box_mux(ModuleManager& module_manager, std::fstream& fp, t_sram_orgz_info* cur_sram_orgz_info, BasicPort& config_bus, + BasicPort& fm_config_bus, const ModuleId& cb_module, const RRGSB& rr_gsb, const t_rr_type& cb_type, @@ -3674,9 +3717,14 @@ void print_verilog_connection_box_mux(ModuleManager& module_manager, print_verilog_comment(fp, std::string("----- BEGIN Local wires used in only formal verification purpose -----")); print_verilog_preprocessing_flag(fp, std::string(verilog_formal_verification_preproc_flag)); /* Print the SRAM configuration ports for formal verification */ - /* TODO: align with the port width of formal verification port of SB module */ + /* Update config bus for formal verification, + * shift with number of configuration bit of the MUX + */ + fm_config_bus.set_width(fm_config_bus.get_msb() + 1, fm_config_bus.get_msb() + mux_num_config_bits); + /* Align with the port width of formal verification port of SB module */ print_verilog_formal_verification_mux_sram_ports_wiring(fp, circuit_lib, mux_model, - datapath_mux_size, mux_instance_id, mux_num_config_bits); + datapath_mux_size, mux_instance_id, + mux_num_config_bits, fm_config_bus); print_verilog_endif(fp); print_verilog_comment(fp, std::string("----- END Local wires used in only formal verification purpose -----")); fp << std::endl; @@ -4273,6 +4321,7 @@ void print_verilog_connection_box_interc(ModuleManager& module_manager, std::fstream& fp, t_sram_orgz_info* cur_sram_orgz_info, BasicPort& config_bus, + BasicPort& fm_config_bus, const ModuleId& cb_module, const RRGSB& rr_gsb, const t_rr_type& cb_type, @@ -4289,7 +4338,8 @@ void print_verilog_connection_box_interc(ModuleManager& module_manager, } else if (1 < src_rr_node->fan_in) { /* Print the multiplexer, fan_in >= 2 */ - print_verilog_connection_box_mux(module_manager, fp, cur_sram_orgz_info, config_bus, + print_verilog_connection_box_mux(module_manager, fp, cur_sram_orgz_info, + config_bus, fm_config_bus, cb_module, rr_gsb, cb_type, circuit_lib, mux_lib, rr_switches, src_rr_node, use_explicit_mapping); @@ -4514,7 +4564,7 @@ void print_verilog_routing_connection_box_unique_module(ModuleManager& module_ma /* TODO: These should be done when initializing the tool */ /* Count the number of configuration bits to be consumed by this Switch block */ - int num_conf_bits = count_verilog_connection_box_conf_bits(cur_sram_orgz_info, rr_gsb, cb_type); + int num_conf_bits = (int)find_connection_block_num_conf_bits(cur_sram_orgz_info, circuit_lib, mux_lib, rr_switches, rr_gsb, cb_type); /* Count the number of reserved configuration bits to be consumed by this Switch block */ int num_reserved_conf_bits = count_verilog_connection_box_reserved_conf_bits(cur_sram_orgz_info, rr_gsb, cb_type); /* Estimate the sram_verilog_model->cnt */ @@ -4689,18 +4739,33 @@ void print_verilog_routing_connection_box_unique_module(ModuleManager& module_ma /* Counter start from 0 */ config_bus.set_width(0, 0); + /* Create a counter for the configuration bus used for formal verification */ + BasicPort fm_config_bus; + /* fm_config_bus has an invalid width here. It is designed to be easy to rotate */ + fm_config_bus.set_width(0, -1); + /* TODO: Print routing multiplexers or direct interconnect*/ for (size_t iside = 0; iside < cb_ipin_sides.size(); ++iside) { enum e_side cb_ipin_side = cb_ipin_sides[iside]; for (size_t inode = 0; inode < rr_gsb.get_num_ipin_nodes(cb_ipin_side); ++inode) { print_verilog_connection_box_interc(module_manager, fp, cur_sram_orgz_info, - config_bus, module_id, rr_gsb, cb_type, + config_bus, fm_config_bus, + module_id, rr_gsb, cb_type, circuit_lib, mux_lib, rr_switches, rr_gsb.get_ipin_node(cb_ipin_side, inode), use_explicit_mapping); } } + /* Add check code for config_bus. + * The MSB should match the number of configuration bits!!! + */ + VTR_ASSERT(true == check_connection_block_mem_config_bus(cur_sram_orgz_info->type, + rr_gsb, cb_type, config_bus, + rr_gsb.get_cb_num_conf_bits(cb_type))); + VTR_ASSERT(fm_config_bus.get_msb() == rr_gsb.get_cb_num_conf_bits(cb_type) - 1); + + /* Put an end to the Verilog module */ print_verilog_module_end(fp, module_manager.module_name(module_id)); diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.cpp index 4b93c2cd2..2a4025cf3 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.cpp @@ -1027,21 +1027,28 @@ void print_verilog_mux_config_bus(std::fstream& fp, * Print a wire to connect MUX configuration ports * This function connects the sram ports to the ports of a Verilog module * used for formal verification + * + * Note: MSB and LSB of formal verification configuration bus MUST be updated + * before running this function !!!! *********************************************************************/ void print_verilog_formal_verification_mux_sram_ports_wiring(std::fstream& fp, const CircuitLibrary& circuit_lib, const CircuitModelId& mux_model, const size_t& mux_size, const size_t& mux_instance_id, - const size_t& num_conf_bits) { + const size_t& num_conf_bits, + const BasicPort& fm_config_bus) { BasicPort mux_sram_output(generate_mux_sram_port_name(circuit_lib, mux_model, mux_size, mux_instance_id, SPICE_MODEL_PORT_INPUT), num_conf_bits); /* Get the SRAM model of the mux_model */ std::vector sram_models = find_circuit_sram_models(circuit_lib, mux_model); /* TODO: maybe later multiplexers may have mode select ports... This should be relaxed */ VTR_ASSERT( 1 == sram_models.size() ); - BasicPort formal_verification_port(generate_formal_verification_sram_port_name(circuit_lib, sram_models[0]), - num_conf_bits); + BasicPort formal_verification_port; + formal_verification_port.set_name(generate_formal_verification_sram_port_name(circuit_lib, sram_models[0])); + VTR_ASSERT(num_conf_bits == fm_config_bus.get_width()); + formal_verification_port.set_lsb(fm_config_bus.get_lsb()); + formal_verification_port.set_msb(fm_config_bus.get_msb()); print_verilog_wire_connection(fp, mux_sram_output, formal_verification_port, false); } diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.h b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.h index c95bfbb18..e53ac0a40 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.h +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.h @@ -104,6 +104,7 @@ void print_verilog_formal_verification_mux_sram_ports_wiring(std::fstream& fp, const CircuitModelId& mux_model, const size_t& mux_size, const size_t& mux_instance_id, - const size_t& num_conf_bits); + const size_t& num_conf_bits, + const BasicPort& fm_config_bus); #endif