From 433fc734607b67d1be7819a0fce8a55bda0cf8c4 Mon Sep 17 00:00:00 2001 From: tangxifan Date: Fri, 27 Sep 2019 23:10:43 -0600 Subject: [PATCH] refactored local encoder support for Verilog MUX generation --- .../libarchfpga/SRC/circuit_library_utils.cpp | 22 +++- .../libarchfpga/SRC/circuit_library_utils.h | 7 +- vpr7_x2p/libarchfpga/SRC/device_port.cpp | 12 +- .../vpr/SRC/device/decoder_library_utils.cpp | 6 +- .../vpr/SRC/device/decoder_library_utils.h | 2 + .../vpr/SRC/fpga_x2p/base/fpga_x2p_naming.cpp | 27 +++++ .../vpr/SRC/fpga_x2p/base/fpga_x2p_naming.h | 6 + .../SRC/fpga_x2p/verilog/verilog_decoders.cpp | 22 +++- .../SRC/fpga_x2p/verilog/verilog_memory.cpp | 2 +- .../vpr/SRC/fpga_x2p/verilog/verilog_mux.cpp | 107 +++++++++++++----- .../fpga_x2p/verilog/verilog_writer_utils.cpp | 6 +- 11 files changed, 173 insertions(+), 46 deletions(-) diff --git a/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.cpp b/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.cpp index d74b2b2d7..63fcb15eb 100644 --- a/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.cpp +++ b/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.cpp @@ -54,8 +54,8 @@ * Get the model id of a SRAM model that is used to configure * a circuit model *******************************************************************/ -std::vector get_circuit_sram_models(const CircuitLibrary& circuit_lib, - const CircuitModelId& circuit_model) { +std::vector find_circuit_sram_models(const CircuitLibrary& circuit_lib, + const CircuitModelId& circuit_model) { /* SRAM model id is stored in the sram ports of a circuit model */ std::vector sram_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_SRAM); std::vector sram_models; @@ -73,3 +73,21 @@ std::vector get_circuit_sram_models(const CircuitLibrary& circui return sram_models; } + +/******************************************************************** + * Find regular (not mode select) sram ports of a circuit model + *******************************************************************/ +std::vector find_circuit_regular_sram_ports(const CircuitLibrary& circuit_lib, + const CircuitModelId& circuit_model) { + std::vector sram_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_SRAM, true); + std::vector regular_sram_ports; + + for (const auto& port : sram_ports) { + if (true == circuit_lib.port_is_mode_select(port)) { + continue; + } + regular_sram_ports.push_back(port); + } + + return regular_sram_ports; +} diff --git a/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.h b/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.h index e80e5c388..f4323f391 100644 --- a/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.h +++ b/vpr7_x2p/libarchfpga/SRC/circuit_library_utils.h @@ -10,7 +10,10 @@ #include #include "circuit_library.h" -std::vector get_circuit_sram_models(const CircuitLibrary& circuit_lib, - const CircuitModelId& circuit_model); +std::vector find_circuit_sram_models(const CircuitLibrary& circuit_lib, + const CircuitModelId& circuit_model); + +std::vector find_circuit_regular_sram_ports(const CircuitLibrary& circuit_lib, + const CircuitModelId& circuit_model); #endif diff --git a/vpr7_x2p/libarchfpga/SRC/device_port.cpp b/vpr7_x2p/libarchfpga/SRC/device_port.cpp index 2de15172d..38241f198 100644 --- a/vpr7_x2p/libarchfpga/SRC/device_port.cpp +++ b/vpr7_x2p/libarchfpga/SRC/device_port.cpp @@ -136,10 +136,14 @@ void BasicPort::revert() { /* rotate: increase both lsb and msb by an offset */ bool BasicPort::rotate(const size_t& offset) { - /* If current port is invalid or offset is 0, - * we do nothing - */ - if ((0 == offset) || (0 == get_width())) { + /* If offset is 0, we do nothing */ + if (0 == offset) { + return true; + } + + /* If current width is 0, we set a width using the offset! */ + if (0 == get_width()) { + set_width(offset); return true; } /* check if leads to overflow: diff --git a/vpr7_x2p/vpr/SRC/device/decoder_library_utils.cpp b/vpr7_x2p/vpr/SRC/device/decoder_library_utils.cpp index ca773819e..47ec9a9a9 100644 --- a/vpr7_x2p/vpr/SRC/device/decoder_library_utils.cpp +++ b/vpr7_x2p/vpr/SRC/device/decoder_library_utils.cpp @@ -27,12 +27,14 @@ * We plus 1, which is all-zero condition for outputs ***************************************************************************************/ size_t find_mux_local_decoder_addr_size(const size_t& data_size) { - /* Make sure we have a encoder which is at least 2 ! */ + /* if data size is 1, it is an corner case for the decoder (addr = 1) */ + if (1 == data_size) { + return 1; + } VTR_ASSERT (2 <= data_size); return ceil(log(data_size) / log(2)); } - /*************************************************************************************** * Try to find if the decoder already exists in the library, * If there is no such decoder, add it to the library diff --git a/vpr7_x2p/vpr/SRC/device/decoder_library_utils.h b/vpr7_x2p/vpr/SRC/device/decoder_library_utils.h index f0719f2e6..100f04da7 100644 --- a/vpr7_x2p/vpr/SRC/device/decoder_library_utils.h +++ b/vpr7_x2p/vpr/SRC/device/decoder_library_utils.h @@ -6,6 +6,8 @@ #include "decoder_library.h" +bool need_mux_local_decoder(const size_t& data_size); + size_t find_mux_local_decoder_addr_size(const size_t& data_size); DecoderId add_mux_local_decoder_to_library(DecoderLibrary& decoder_lib, diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.cpp index 8323acfd4..1ab7a2ebd 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.cpp @@ -332,6 +332,33 @@ std::string generate_configuration_chain_tail_name() { return std::string("ccff_tail"); } +/********************************************************************* + * Generate the addr port (input) for a local decoder of a multiplexer + * TODO: This could be replaced as a constexpr string + *********************************************************************/ +std::string generate_mux_local_decoder_addr_port_name() { + return std::string("addr"); +} + + + +/********************************************************************* + * Generate the data port (output) for a local decoder of a multiplexer + * TODO: This could be replaced as a constexpr string + *********************************************************************/ +std::string generate_mux_local_decoder_data_port_name() { + return std::string("data"); +} + +/********************************************************************* + * Generate the inverted data port (output) for a local decoder of a multiplexer + * TODO: This could be replaced as a constexpr string + *********************************************************************/ +std::string generate_mux_local_decoder_data_inv_port_name() { + return std::string("data_inv"); +} + + /********************************************************************* * Generate the port name for a regular sram port which appears in the * port list of a module diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.h b/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.h index f68fee17d..f3b748a77 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.h +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/base/fpga_x2p_naming.h @@ -76,6 +76,12 @@ std::string generate_configuration_chain_head_name(); std::string generate_configuration_chain_tail_name(); +std::string generate_mux_local_decoder_addr_port_name(); + +std::string generate_mux_local_decoder_data_port_name(); + +std::string generate_mux_local_decoder_data_inv_port_name(); + std::string generate_sram_port_name(const CircuitLibrary& circuit_lib, const CircuitModelId& sram_model, const e_sram_orgz& sram_orgz_type, diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_decoders.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_decoders.cpp index 0de1249cd..4e3a7c422 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_decoders.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_decoders.cpp @@ -59,17 +59,17 @@ void print_verilog_mux_local_decoder_module(std::fstream& fp, VTR_ASSERT(ModuleId::INVALID() != module_id); /* Add module ports */ /* Add each input port */ - BasicPort addr_port("addr", addr_size); + BasicPort addr_port(generate_mux_local_decoder_addr_port_name(), addr_size); module_manager.add_port(module_id, addr_port, ModuleManager::MODULE_INPUT_PORT); /* Add each output port */ - BasicPort data_port("data", data_size); + BasicPort data_port(generate_mux_local_decoder_data_port_name(), data_size); module_manager.add_port(module_id, data_port, ModuleManager::MODULE_OUTPUT_PORT); /* Data port is registered. It should be outputted as * output reg [lsb:msb] data */ module_manager.set_port_is_register(module_id, data_port.get_name(), true); /* Add data_in port */ - BasicPort data_inv_port("data_inv", data_size); + BasicPort data_inv_port(generate_mux_local_decoder_data_inv_port_name(), data_size); VTR_ASSERT(true == decoder_lib.use_data_inv_port(decoder)); module_manager.add_port(module_id, data_inv_port, ModuleManager::MODULE_OUTPUT_PORT); @@ -81,6 +81,20 @@ void print_verilog_mux_local_decoder_module(std::fstream& fp, /* Print the truth table of this decoder */ /* Internal logics */ + /* Early exit: Corner case for data size = 1 the logic is very simple: + * data = addr; + * data_inv = ~data_inv + */ + if (1 == data_size) { + print_verilog_wire_connection(fp, addr_port, data_port, false); + print_verilog_wire_connection(fp, data_inv_port, data_port, true); + print_verilog_comment(fp, std::string("----- END Verilog codes for Decoder convert " + std::to_string(addr_size) + "-bit addr to " + std::to_string(data_size) + "-bit data -----")); + + /* Put an end to the Verilog module */ + print_verilog_module_end(fp, module_name); + return; + } + /* We use a magic number -1 as the addr=1 should be mapped to ...1 * Otherwise addr will map addr=1 to ..10 * Note that there should be a range for the shift operators @@ -194,7 +208,7 @@ void print_verilog_submodule_mux_local_decoders(ModuleManager& module_manager, * Note that only when there are >=2 memories, a decoder is needed */ size_t decoder_data_size = branch_mux_graph.num_memory_bits(); - if (2 > decoder_data_size) { + if (0 == decoder_data_size) { continue; } /* Try to find if the decoder already exists in the library, diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_memory.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_memory.cpp index d260b6ec7..61090aaab 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_memory.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_memory.cpp @@ -442,7 +442,7 @@ void print_verilog_mux_memory_module(ModuleManager& module_manager, std::string(verilog_mem_posfix)); /* Get the sram ports from the mux */ - std::vector sram_models = get_circuit_sram_models(circuit_lib, mux_model); + std::vector sram_models = find_circuit_sram_models(circuit_lib, mux_model); VTR_ASSERT( 1 == sram_models.size() ); /* Find the number of SRAMs in the module, this is also the port width */ diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_mux.cpp b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_mux.cpp index f38cd106a..0f4b10579 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_mux.cpp +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_mux.cpp @@ -17,6 +17,8 @@ #include "physical_types.h" #include "vpr_types.h" #include "mux_utils.h" +#include "circuit_library_utils.h" +#include "decoder_library_utils.h" /* FPGA-X2P context header files */ #include "spice_types.h" @@ -853,6 +855,10 @@ void generate_verilog_cmos_mux_module_mux2_multiplexing_structure(ModuleManager& /* Generate the port info of each mem node */ BasicPort instance_mem_port(circuit_lib.port_lib_name(mux_regular_sram_ports[0]), size_t(mem), size_t(mem)); std::string module_mem_port_name = circuit_lib.port_lib_name(std_cell_input_ports[2]); + /* If use local decoders, we should use another name for the mem port */ + if (true == circuit_lib.mux_use_local_encoder(circuit_model)) { + instance_mem_port.set_name(generate_mux_local_decoder_data_port_name()); + } port2port_name_map[module_mem_port_name] = instance_mem_port; } @@ -910,19 +916,8 @@ void generate_verilog_cmos_mux_module_tgate_multiplexing_structure(ModuleManager /* Find the actual mux size */ size_t mux_size = find_mux_num_datapath_inputs(circuit_lib, circuit_model, mux_graph.num_inputs()); - /* TODO: these are duplicated codes, find a way to simplify it!!! - * Get the regular (non-mode-select) sram ports from the mux - */ - std::vector mux_regular_sram_ports; - for (const auto& port : circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_SRAM, true)) { - /* Multiplexing structure does not mode_sram_ports, they are handled in LUT modules - * Here we just bypass it. - */ - if (true == circuit_lib.port_is_mode_select(port)) { - continue; - } - mux_regular_sram_ports.push_back(port); - } + /* Get the regular (non-mode-select) sram ports from the mux */ + std::vector mux_regular_sram_ports = find_circuit_regular_sram_ports(circuit_lib, circuit_model); VTR_ASSERT(1 == mux_regular_sram_ports.size()); /* Build the location map of intermediate buffers */ @@ -1035,6 +1030,10 @@ void generate_verilog_cmos_mux_module_tgate_multiplexing_structure(ModuleManager for (const auto& mem : mems) { /* Generate the port info of each mem node */ BasicPort branch_node_mem_port(circuit_lib.port_lib_name(mux_regular_sram_ports[0]), size_t(mem), size_t(mem)); + /* If use local decoders, we should use another name for the mem port */ + if (true == circuit_lib.mux_use_local_encoder(circuit_model)) { + branch_node_mem_port.set_name(generate_mux_local_decoder_data_port_name()); + } branch_node_mem_ports.push_back(branch_node_mem_port); } @@ -1065,6 +1064,10 @@ void generate_verilog_cmos_mux_module_tgate_multiplexing_structure(ModuleManager for (const auto& mem : mems) { /* Generate the port info of each mem node */ BasicPort branch_node_mem_inv_port(circuit_lib.port_lib_name(mux_regular_sram_ports[0]) + "_inv", size_t(mem), size_t(mem)); + /* If use local decoders, we should use another name for the mem port */ + if (true == circuit_lib.mux_use_local_encoder(circuit_model)) { + branch_node_mem_inv_port.set_name(generate_mux_local_decoder_data_inv_port_name()); + } branch_node_mem_inv_ports.push_back(branch_node_mem_inv_port); } @@ -1315,8 +1318,11 @@ void generate_verilog_cmos_mux_module(ModuleManager& module_manager, std::vector mux_input_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_INPUT, true); /* Get the output ports from the mux */ std::vector mux_output_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_OUTPUT, true); - /* Get the sram ports from the mux */ - std::vector mux_sram_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_SRAM, true); + /* Get the sram ports from the mux + * Multiplexing structure does not mode_sram_ports, they are handled in LUT modules + * Here we just bypass it. + */ + std::vector mux_sram_ports = find_circuit_regular_sram_ports(circuit_lib, circuit_model); /* Make sure we have a valid file handler*/ check_file_handler(fp); @@ -1329,6 +1335,18 @@ void generate_verilog_cmos_mux_module(ModuleManager& module_manager, /* Find out the number of memory bits */ size_t num_mems = mux_graph.num_memory_bits(); + /* The size of of memory ports depend on + * if a local encoder is used for the mux or not + * Multiplexer local encoders are applied to memory bits at each stage + */ + if (true == circuit_lib.mux_use_local_encoder(circuit_model)) { + num_mems = 0; + for (const auto& lvl : mux_graph.levels()) { + size_t data_size = mux_graph.num_memory_bits_at_level(lvl); + num_mems += find_mux_local_decoder_addr_size(data_size); + } + } + /* Check codes to ensure the port of Verilog netlists will match */ /* MUX graph must have only 1 output */ VTR_ASSERT(1 == mux_input_ports.size()); @@ -1381,18 +1399,8 @@ void generate_verilog_cmos_mux_module(ModuleManager& module_manager, module_manager.add_port(module_id, output_port, ModuleManager::MODULE_OUTPUT_PORT); } - - /* TODO: the size of of memory ports depend on - * if a local encoder is used for the mux or not - */ size_t sram_port_cnt = 0; for (const auto& port : mux_sram_ports) { - /* Multiplexing structure does not mode_sram_ports, they are handled in LUT modules - * Here we just bypass it. - */ - if (true == circuit_lib.port_is_mode_select(port)) { - continue; - } BasicPort mem_port(circuit_lib.port_lib_name(port), num_mems); module_manager.add_port(module_id, mem_port, ModuleManager::MODULE_INPUT_PORT); BasicPort mem_inv_port(std::string(circuit_lib.port_lib_name(port) + "_inv"), num_mems); @@ -1400,11 +1408,56 @@ void generate_verilog_cmos_mux_module(ModuleManager& module_manager, /* Update counter */ sram_port_cnt++; } + VTR_ASSERT(1 == sram_port_cnt); /* dump module definition + ports */ print_verilog_module_declaration(fp, module_manager, module_id); - /* TODO: Print the internal logic in Verilog codes */ + /* Add local decoder instance here */ + if (true == circuit_lib.mux_use_local_encoder(circuit_model)) { + BasicPort decoder_data_port(generate_mux_local_decoder_data_port_name(), mux_graph.num_memory_bits()); + BasicPort decoder_data_inv_port(generate_mux_local_decoder_data_inv_port_name(), mux_graph.num_memory_bits()); + /* Print local wires to bridge the port of module and memory inputs + * of each MUX branch instance + */ + fp << generate_verilog_port(VERILOG_PORT_WIRE, decoder_data_port) << ";" << std::endl; + fp << generate_verilog_port(VERILOG_PORT_WIRE, decoder_data_inv_port) << ";" << std::endl; + + /* Local port to record the LSB and MSB of each level, here, we deposite (0, 0) */ + BasicPort lvl_addr_port(circuit_lib.port_lib_name(mux_sram_ports[0]), 0); + BasicPort lvl_data_port(decoder_data_port.get_name(), 0); + BasicPort lvl_data_inv_port(decoder_data_inv_port.get_name(), 0); + for (const auto& lvl : mux_graph.levels()) { + size_t addr_size = find_mux_local_decoder_addr_size(mux_graph.num_memory_bits_at_level(lvl)); + size_t data_size = mux_graph.num_memory_bits_at_level(lvl); + /* Update the LSB and MSB of addr and data port for the current level */ + lvl_addr_port.rotate(addr_size); + lvl_data_port.rotate(data_size); + lvl_data_inv_port.rotate(data_size); + /* Print the instance of local decoder */ + std::string decoder_module_name = generate_mux_local_decoder_subckt_name(addr_size, data_size); + ModuleId decoder_module = module_manager.find_module(decoder_module_name); + VTR_ASSERT(ModuleId::INVALID() != decoder_module); + + /* Create a port-to-port map */ + std::map decoder_port2port_name_map; + decoder_port2port_name_map[generate_mux_local_decoder_addr_port_name()] = lvl_addr_port; + decoder_port2port_name_map[generate_mux_local_decoder_data_port_name()] = lvl_data_port; + decoder_port2port_name_map[generate_mux_local_decoder_data_inv_port_name()] = lvl_data_inv_port; + + /* Print an instance of the MUX Module */ + print_verilog_comment(fp, std::string("----- BEGIN Instanciation of a local decoder -----")); + print_verilog_module_instance(fp, module_manager, module_id, decoder_module, decoder_port2port_name_map, circuit_lib.dump_explicit_port_map(circuit_model)); + print_verilog_comment(fp, std::string("----- END Instanciation of a local decoder -----")); + fp << std::endl; + /* IMPORTANT: this update MUST be called after the instance outputting!!!! + * update the module manager with the relationship between the parent and child modules + */ + module_manager.add_child_module(module_id, decoder_module); + } + } + + /* Print the internal logic in Verilog codes */ /* Print the Multiplexing structure in Verilog codes * Separated generation strategy on using standard cell MUX2 or TGATE, * 1. MUX2 has a fixed port map: input_port[0] and input_port[1] is the data_path input @@ -1430,8 +1483,6 @@ void generate_verilog_cmos_mux_module(ModuleManager& module_manager, generate_verilog_cmos_mux_module_input_buffers(module_manager, circuit_lib, fp, module_id, circuit_model, mux_graph); generate_verilog_cmos_mux_module_output_buffers(module_manager, circuit_lib, fp, module_id, circuit_model, mux_graph); - /* TODO: add local decoder instance here */ - /* Put an end to the Verilog module */ print_verilog_module_end(fp, module_name); } 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 7e6cdd693..72590fc9e 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 @@ -872,7 +872,7 @@ void print_verilog_cmos_mux_config_bus(std::fstream& fp, fp << generate_verilog_port(VERILOG_PORT_WIRE, inverted_sram_output_bus) << ";" << std::endl; /* Get the SRAM model of the mux_model */ - std::vector sram_models = get_circuit_sram_models(circuit_lib, 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() ); std::vector blb_ports = circuit_lib.model_ports_by_type(sram_models[0], SPICE_MODEL_PORT_BLB); @@ -998,7 +998,7 @@ void print_verilog_rram_mux_config_bus(std::fstream& fp, fp << generate_verilog_port(VERILOG_PORT_WIRE, inverted_sram_output_bus) << ";" << std::endl; /* Get the SRAM model of the mux_model */ - std::vector sram_models = get_circuit_sram_models(circuit_lib, 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() ); @@ -1078,7 +1078,7 @@ void print_verilog_formal_verification_mux_sram_ports_wiring(std::fstream& fp, 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 = get_circuit_sram_models(circuit_lib, 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]),