I am trying to verify that modules are connected correctly. I have a system verilog testbench that instantiates a vhdl top module which has instances of module_a and module_b in it. So when the modules actually are built and have insides then the engine can drive the necessary stimulus in tb.sv (which is prepped as the top module) to find fault connections. The issue arises when I want to black box them, using blackbox command didn't work (I added an undefined internal const to a module and it threw an error), so instead I just emptied the modules but the issue now is that from the tb.sv file there's no way to stimulate those internal wires, If i could have the engine provide stimulus to module b to disprove an assertion in tb.sv that should work but I'm not sure how to do that/if it's possible.
Here's the code...
a.vhd
library IEEE;
use IEEE.NUMERIC_STD.ALL;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.STD_LOGIC_ARITH.all;
use IEEE.STD_LOGIC_UNSIGNED.all;
entity mod_a is
generic (
CONSTANT NUM_BITS : integer := 4
);
port(
-- In --
clk : in std_logic;
n_rst : in std_logic;
a : in std_logic;
b : in std_logic;
-- Out --
bus_a : out std_logic_vector(NUM_BITS-1 downto 0);
bus_b : out std_logic_vector(NUM_BITS-1 downto 0)
);
end mod_a;
architecture mod_a_arch of mod_a is
-- CONSTANT DUMMY_CONST : integer := 6;
-- signal blackbox : std_logic_vector(DUMMY_CONST-1 downto 0);
begin
-- bus_a <= (a and b) & (a xor b) & (a or b) & '0';
-- bus_b <= (a or b) & (a and b) & (a xor b) & '1';
end mod_a_arch;
b.vhd
library IEEE;
use IEEE.NUMERIC_STD.ALL;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.STD_LOGIC_ARITH.all;
use IEEE.STD_LOGIC_UNSIGNED.all;
entity mod_b is
generic (
CONSTANT NUM_BITS: integer := 4;
CONSTANT OUT_BITS: integer := 8
);
port(
-- In --
clk : in std_logic;
n_rst : in std_logic;
a_in : in std_logic_vector(NUM_BITS-1 downto 0);
b_in : in std_logic_vector(NUM_BITS-1 downto 0);
-- Out --
dummy : out std_logic_vector(OUT_BITS-1 downto 0)
);
end entity mod_b;
architecture mod_b_arch of mod_b is
begin
end mod_b_arch;
top.vhd
----------------------------------------------------------------------
library IEEE;
use IEEE.NUMERIC_STD.ALL;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.STD_LOGIC_ARITH.all;
use IEEE.STD_LOGIC_UNSIGNED.all;
entity top is
generic (
CONSTANT NUM_BITS: integer := 4;
CONSTANT OUT_BITS: integer := 8
);
port(
clk : in std_logic;
n_rst : in std_logic;
a_t : in std_logic;
b_t : in std_logic;
dummy_t : out std_logic_vector(OUT_BITS-1 downto 0)
);
end entity top;
architecture top_arch of top is
signal bus_a_s : std_logic_vector(NUM_BITS-1 downto 0);
signal bus_b_s : std_logic_vector(NUM_BITS-1 downto 0);
component mod_a is
generic (
CONSTANT NUM_BITS: integer := 4
);
port(
-- In --
clk : in std_logic;
n_rst : in std_logic;
a : in std_logic;
b : in std_logic;
-- Out --
bus_a : out std_logic_vector(NUM_BITS-1 downto 0);
bus_b : out std_logic_vector(NUM_BITS-1 downto 0)
);
end component mod_a;
component mod_b is
generic (
CONSTANT NUM_BITS: integer := 4;
CONSTANT OUT_BITS: integer := 8
);
port(
-- In --
clk : in std_logic;
n_rst : in std_logic;
a_in : in std_logic_vector(NUM_BITS-1 downto 0);
b_in : in std_logic_vector(NUM_BITS-1 downto 0);
-- Out --
dummy : out std_logic_vector(OUT_BITS-1 downto 0)
);
end component mod_b;
begin
module_b : mod_b
generic map (
NUM_BITS => NUM_BITS,
OUT_BITS => OUT_BITS
)
port map (
clk => clk,
n_rst => n_rst,
a_in => bus_a_s,
b_in => bus_b_s,
dummy => dummy_t
);
module_a : mod_a
generic map (NUM_BITS => NUM_BITS)
port map (
clk => clk,
n_rst => n_rst,
a => a_t,
b => b_t,
bus_a => bus_a_s,
bus_b => bus_b_s
);
-- Formal Block --
-- formal: block
-- -- Past Value Registers --
-- -- alias bus_a_c is << signal module_a.bus_a : std_logic_vector(NUM_BITS-1 downto 0) >>;
-- -- alias a_in_c is << signal module_b.a_in : std_logic_vector(NUM_BITS-1 downto 0) >>;
-- signal count : std_logic_vector(NUM_BITS-1 downto 0);
-- -- signal tmp_a_in : std_logic_vector(NUM_BITS-1 downto 0);
-- begin
-- -- Past Value Assignment --
-- process(clk)
-- begin
-- if rising_edge(clk) then
-- count <= count + 1;
-- end if;
-- end process;
-- -- Assertions --
-- default clock is rising_edge(clk);
-- -- assert (bus_a_c = a_in_c) report "FAIL" severity error;
-- if (count > "0011") then
-- assert (bus_a_s = bus_b_s);
-- end if;
-- -- assert (tmp_bus_a = tmp_a_in) report "FAIL" severity error;
-- end block;
end top_arch;
tb.sv
`timescale 1ns/1ns
`default_nettype none
module test (
input logic tb_clk,
input logic tb_n_rst,
input logic tb_a_t,
input logic tb_b_t,
output logic [7:0] tb_dummy_t
);
(* hierconn *) wire \TOP1.module_a.bus_a ;
(* hierconn *) wire \TOP1.module_a.bus_b ;
(* hierconn *) wire \TOP1.module_b.a_in ;
(* hierconn *) wire \TOP1.module_a.clk ;
(* hierconn *) wire \TOP1.module_a.n_rst ;
top TOP1(tb_clk, tb_n_rst, tb_a_t, tb_b_t, tb_dummy_t);
// --- Formal Block --- //
`ifdef FORMAL
always @(posedge TOP1.module_a.clk) begin
// Good
if (TOP1.module_a.n_rst) GOOD_CLK: assert(TOP1.module_b.a_in === TOP1.module_a.bus_a);
// Bad
if (TOP1.module_a.n_rst) BAD_CLK: assert(TOP1.module_b.a_in === TOP1.module_a.bus_b);
end
// always @(posedge tb_clk) begin
// // Good
// if (tb_n_rst) GOOD: assert(TOP1.module_b.a_in === TOP1.module_a.bus_a);
// // Bad
// if (tb_n_rst) BAD: assert(TOP1.module_b.a_in === TOP1.module_a.bus_b);
// end
`endif
endmodule
test.sby (I assume the changes would need to go in here)
AdamKeith1
commented
3 months ago
I am trying to verify that modules are connected correctly. I have a system verilog testbench that instantiates a vhdl top module which has instances of module_a and module_b in it. So when the modules actually are built and have insides then the engine can drive the necessary stimulus in tb.sv (which is prepped as the top module) to find fault connections. The issue arises when I want to black box them, using blackbox command didn't work (I added an undefined internal const to a module and it threw an error), so instead I just emptied the modules but the issue now is that from the tb.sv file there's no way to stimulate those internal wires, If i could have the engine provide stimulus to module b to disprove an assertion in tb.sv that should work but I'm not sure how to do that/if it's possible.
Here's the code...
a.vhd
b.vhd
top.vhd
tb.sv
test.sby (I assume the changes would need to go in here)