Blackbox

[AdamKeith1]

I am testing to see if I can blackbox modules and just test the wiring connections between them. So there are a few issues. The source code has import statements like USE work.axi_pkg.ALL; and I haven't found a way to specify a 'work' library in sby and importing the modules in my SV test bench is a paid feature. I tested the blckboxing by adding a constant that is completely internal and doesn't affect ports to one of the modules.

-- CONSTANT DUMMY_CONST : integer := 
signal blackbox : std_logic_vector(DUMMY_CONST-1 downto 0);

I commented it out and got a compiler error (which shouldn't happen if it's blackboxed correct?) The reason I'm doing this is because the actual design I want to connect check is very large with lots of constants and types imported from a lot of different packages. My idea was to just declare the constants that affected ports and via blackbox ignore the completely internal constants but now that im understanding more about how sby provides stimulus I'm not sure this approach is valid. Any clues on how to import these packages or how to truly blackbox these modules?

Here's my code.

a.vhd - test module 1

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 - test module b

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
            );

end top_arch;

tb.sv - system verilog testbench

`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 - sby config file

[tasks]
bmc
cover

[options]
bmc:
mode bmc
depth 50
--
cover:
mode cover
depth 50
--

[engines]
smtbmc boolector -- --keep-going

[script]
read -formal tb.sv
ghdl --std=08 --ieee=synopsys a.vhd -e mod_a
ghdl --std=08 --ieee=synopsys b.vhd -e mod_b
ghdl --std=08 --ieee=synopsys top.vhd -e top
blackbox mod_b
blackbox mod_a
prep -top test -flatten
show

[files]
tb.sv
b.vhd
a.vhd
top.vhd