Refactored Verilog wiring for formal verification ports in Switch Blocks

This commit is contained in:
tangxifan 2019-09-27 13:51:22 -06:00
parent ead014e7d8
commit dbe1625267
5 changed files with 153 additions and 34 deletions

View File

@ -0,0 +1,75 @@
/**********************************************************
* MIT License
*
* Copyright (c) 2018 LNIS - The University of Utah
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
***********************************************************************/
/************************************************************************
* Filename: circuit_library_utils.cpp
* Created by: Xifan Tang
* Change history:
* +-------------------------------------+
* | Date | Author | Notes
* +-------------------------------------+
* | 2019/09/27 | Xifan Tang | Created
* +-------------------------------------+
***********************************************************************/
/************************************************************************
* Function to perform fundamental operation for the circuit library
* These functions are not universal methods for the CircuitLibrary class
* They are made to ease the development in some specific purposes
* Please classify such functions in this file
***********************************************************************/
/* Header files should be included in a sequence */
/* Standard header files required go first */
#include <algorithm>
#include "vtr_assert.h"
#include "util.h"
#include "circuit_library_utils.h"
/********************************************************************
* Get the model id of a SRAM model that is used to configure
* a circuit model
*******************************************************************/
std::vector<CircuitModelId> get_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<CircuitPortId> sram_ports = circuit_lib.model_ports_by_type(circuit_model, SPICE_MODEL_PORT_SRAM);
std::vector<CircuitModelId> sram_models;
/* Create a list of sram models, but avoid duplicated model ids */
for (const auto& sram_port : sram_ports) {
CircuitModelId sram_model = circuit_lib.port_tri_state_model(sram_port);
VTR_ASSERT( true == circuit_lib.valid_model_id(sram_model) );
if (sram_models.end() != std::find(sram_models.begin(), sram_models.end(), sram_model)) {
continue; /* Already in the list, skip the addition */
}
/* Not in the list, add it */
sram_models.push_back(sram_model);
}
return sram_models;
}

View File

@ -0,0 +1,16 @@
/********************************************************************
* Header file for circuit_library_utils.cpp
*******************************************************************/
#ifndef CIRCUIT_LIBRARY_UTILS_H
#define CIRCUIT_LIBRARY_UTILS_H
/* Header files should be included in a sequence */
/* Standard header files required go first */
#include <vector>
#include "circuit_library.h"
std::vector<CircuitModelId> get_circuit_sram_models(const CircuitLibrary& circuit_lib,
const CircuitModelId& circuit_model);
#endif

View File

@ -2376,7 +2376,9 @@ void print_verilog_unique_switch_box_mux(ModuleManager& module_manager,
/* Generate input ports that are wired to the input bus of the routing multiplexer */
std::vector<BasicPort> mux_input_ports = generate_switch_block_input_ports(rr_sb, drive_rr_nodes);
/* Connect input ports to bus */
print_verilog_comment(fp, std::string("----- A local bus wire for multiplexer inputs -----"));
fp << generate_verilog_local_wire(inbus_port, mux_input_ports) << std::endl;
fp << std::endl;
/* Find the number of reserved configuration bits for the routing multiplexer */
size_t mux_num_reserved_config_bits = find_mux_num_reserved_config_bits(circuit_lib, mux_model, mux_graph);
@ -2385,31 +2387,32 @@ void print_verilog_unique_switch_box_mux(ModuleManager& module_manager,
size_t mux_num_config_bits = find_mux_num_config_bits(circuit_lib, mux_model, mux_graph, cur_sram_orgz_info->type);
/* Print the configuration bus for the routing multiplexers */
print_verilog_comment(fp, std::string("----- Local wires to group configuration ports -----"));
print_verilog_mux_config_bus(fp, circuit_lib, mux_model, cur_sram_orgz_info->type,
datapath_mux_size, mux_instance_id,
mux_num_reserved_config_bits, mux_num_config_bits);
fp << std::endl;
/* Dump ports visible only during formal verification */
fp << std::endl;
print_verilog_comment(fp, std::string("----- Local wires used in only formal verification purpose -----"));
print_verilog_preprocessing_flag(fp, std::string(verilog_formal_verification_preproc_flag));
/* TODO: Print the SRAM configuration ports for formal verification
dump_verilog_formal_verification_mux_sram_ports_wiring(fp, cur_sram_orgz_info,
verilog_model, mux_size,
cur_num_sram,
cur_num_sram + num_mux_conf_bits - 1);
*/
/* Print the SRAM configuration ports for formal verification */
print_verilog_formal_verification_mux_sram_ports_wiring(fp, circuit_lib, mux_model,
datapath_mux_size, mux_instance_id, mux_num_config_bits);
print_verilog_endif(fp);
fp << std::endl;
/* TODO: Instanciate the Mux Module */
/* TODO: add global ports */
/* TODO: add input bus port */
/* TODO: add output port */
/* TODO: Add different configuraton port for the routing multiplexer
/* TODO: Instanciate the MUX Module */
/* TODO: create port-to-port map */
/* Link input bus port to Switch Block inputs */
/* Link output port to Switch Block outputs */
/* Link SRAM port to different configuraton port for the routing multiplexer
* Different design technology requires different configuration bus!
dump_verilog_mux_config_bus_ports(fp, verilog_model, cur_sram_orgz_info,
mux_size, cur_num_sram, num_mux_reserved_conf_bits,
num_mux_conf_bits, is_explicit_mapping);
*/
/* TODO: Print an instance of the MUX Module */
/* TODO: Instanciate memory modules */
switch (circuit_lib.design_tech_type(mux_model)) {

View File

@ -9,6 +9,7 @@
#include "vtr_assert.h"
/* Device-level header files */
#include "circuit_library_utils.h"
/* FPGA-X2P context header files */
#include "spice_types.h"
@ -870,21 +871,18 @@ void print_verilog_cmos_mux_config_bus(std::fstream& fp,
num_conf_bits);
fp << generate_verilog_port(VERILOG_PORT_WIRE, inverted_sram_output_bus) << ";" << std::endl;
/* TODO: This should be handled as a function */
/* Get the SRAM model of the mux_model */
std::vector<CircuitPortId> sram_ports = circuit_lib.model_ports_by_type(mux_model, SPICE_MODEL_PORT_SRAM);
/* This may be too strict for a multiplexer, what if a routing multiplexer has a mode select port? */
VTR_ASSERT( 1 == sram_ports.size() );
CircuitModelId sram_model = circuit_lib.port_tri_state_model(sram_ports[0]);
VTR_ASSERT( true == circuit_lib.valid_model_id(sram_model) );
std::vector<CircuitPortId> blb_ports = circuit_lib.model_ports_by_type(sram_model, SPICE_MODEL_PORT_BLB);
std::vector<CircuitPortId> wlb_ports = circuit_lib.model_ports_by_type(sram_model, SPICE_MODEL_PORT_WLB);
std::vector<CircuitModelId> sram_models = get_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<CircuitPortId> blb_ports = circuit_lib.model_ports_by_type(sram_models[0], SPICE_MODEL_PORT_BLB);
std::vector<CircuitPortId> wlb_ports = circuit_lib.model_ports_by_type(sram_models[0], SPICE_MODEL_PORT_WLB);
/* Connect SRAM BL/WLs to bus */
BasicPort mux_bl_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_BL),
BasicPort mux_bl_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_BL),
num_conf_bits);
print_verilog_wire_connection(fp, bl_bus, mux_bl_wire, false);
BasicPort mux_wl_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_WL),
BasicPort mux_wl_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_WL),
num_conf_bits);
print_verilog_wire_connection(fp, wl_bus, mux_wl_wire, false);
@ -894,7 +892,7 @@ void print_verilog_cmos_mux_config_bus(std::fstream& fp,
num_conf_bits);
fp << generate_verilog_port(VERILOG_PORT_WIRE, blb_bus) << ";" << std::endl;
/* Connect SRAM BLBs to bus */
BasicPort mux_blb_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_BLB),
BasicPort mux_blb_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_BLB),
num_conf_bits);
print_verilog_wire_connection(fp, blb_bus, mux_blb_wire, false);
}
@ -905,7 +903,7 @@ void print_verilog_cmos_mux_config_bus(std::fstream& fp,
num_conf_bits);
fp << generate_verilog_port(VERILOG_PORT_WIRE, wlb_bus) << ";" << std::endl;
/* Connect SRAM WLBs to bus */
BasicPort mux_wlb_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_WLB),
BasicPort mux_wlb_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_WLB),
num_conf_bits);
print_verilog_wire_connection(fp, wlb_bus, mux_wlb_wire, false);
}
@ -913,7 +911,8 @@ void print_verilog_cmos_mux_config_bus(std::fstream& fp,
break;
}
default:
vpr_printf(TIO_MESSAGE_ERROR,"(File:%s,[LINE%d])Invalid SRAM organization!\n",
vpr_printf(TIO_MESSAGE_ERROR,
"(File:%s,[LINE%d])Invalid SRAM organization!\n",
__FILE__, __LINE__);
exit(1);
}
@ -998,13 +997,10 @@ void print_verilog_rram_mux_config_bus(std::fstream& fp,
num_conf_bits);
fp << generate_verilog_port(VERILOG_PORT_WIRE, inverted_sram_output_bus) << ";" << std::endl;
/* TODO: This should be handled as a function */
/* Get the SRAM model of the mux_model */
std::vector<CircuitPortId> sram_ports = circuit_lib.model_ports_by_type(mux_model, SPICE_MODEL_PORT_SRAM);
/* This may be too strict for a multiplexer, what if a routing multiplexer has a mode select port? */
VTR_ASSERT( 1 == sram_ports.size() );
CircuitModelId sram_model = circuit_lib.port_tri_state_model(sram_ports[0]);
VTR_ASSERT( true == circuit_lib.valid_model_id(sram_model) );
std::vector<CircuitModelId> sram_models = get_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() );
/* Wire the reserved configuration bits to part of bl/wl buses */
BasicPort bl_bus_reserved_bits(bl_bus.get_name(), num_reserved_conf_bits);
@ -1013,11 +1009,11 @@ void print_verilog_rram_mux_config_bus(std::fstream& fp,
print_verilog_wire_connection(fp, wl_bus_reserved_bits, reserved_wl_bus, false);
/* Connect SRAM BL/WLs to bus */
BasicPort mux_bl_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_BL),
BasicPort mux_bl_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_BL),
num_conf_bits);
BasicPort bl_bus_regular_bits(bl_bus.get_name(), num_reserved_conf_bits, num_reserved_conf_bits + num_conf_bits - 1);
print_verilog_wire_connection(fp, bl_bus_regular_bits, mux_bl_wire, false);
BasicPort mux_wl_wire(generate_sram_port_name(circuit_lib, sram_model, sram_orgz_type, SPICE_MODEL_PORT_WL),
BasicPort mux_wl_wire(generate_sram_port_name(circuit_lib, sram_models[0], sram_orgz_type, SPICE_MODEL_PORT_WL),
num_conf_bits);
BasicPort wl_bus_regular_bits(wl_bus.get_name(), num_reserved_conf_bits, num_reserved_conf_bits + num_conf_bits - 1);
print_verilog_wire_connection(fp, wl_bus_regular_bits, mux_wl_wire, false);
@ -1025,7 +1021,8 @@ void print_verilog_rram_mux_config_bus(std::fstream& fp,
break;
}
default:
vpr_printf(TIO_MESSAGE_ERROR,"(File:%s,[LINE%d])Invalid SRAM organization!\n",
vpr_printf(TIO_MESSAGE_ERROR,
"(File:%s,[LINE%d])Invalid SRAM organization!\n",
__FILE__, __LINE__);
exit(1);
}
@ -1067,3 +1064,25 @@ 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
*********************************************************************/
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) {
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<CircuitModelId> sram_models = get_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);
print_verilog_wire_connection(fp, mux_sram_output, formal_verification_port, false);
}

View File

@ -99,5 +99,11 @@ void print_verilog_mux_config_bus(std::fstream& fp,
const size_t& num_reserved_conf_bits,
const size_t& num_conf_bits);
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);
#endif