SymbiYosys Hierarchical Reference

[AdamKeith1]

I am trying to verify connectivity between two modules. It seems that when I make the assertion, it created an identical net to the signal I want to reference and thinks it's poorly written identifier. I'll post my code and some other snippets below. The modules are simple just to use as a proof of concept for checking connection between two modules using sby. It seems to just think I didn't declare the wire and then makes a new instance even though the name in the hierarchy is the same as the signal I want to reference.

connect.sby...

[tasks]
bmc

[options]
bmc:
mode bmc
depth 50
--

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

[script]
read -formal tb.sv
read -formal a.sv
read -formal b.sv
prep -top top

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

a.sv...

module mod_a (
    input  logic clk,
    input  logic n_rst,
    input  logic a,
    input  logic b,
    output logic and_o,
    output logic xor_o,
    output logic or_o,
);
    logic nxt_and, nxt_or, nxt_xor;
    logic and_reg, or_reg, xor_reg;

    always_ff @(posedge clk, negedge n_rst) begin : FF
        if (!n_rst) begin
            and_reg <= '0;
            xor_reg <= '0;
            or_reg  <= '0;
        end else begin
            and_reg <= nxt_and;
            xor_reg <= nxt_xor;
            or_reg  <= nxt_or;
        end
    end

    always_comb begin : COMB
        nxt_and = a & b;
        nxt_or  = a | b;
        nxt_xor = a ^ b;
    end

    assign and_o = and_reg;
    assign or_o = or_reg;
    assign xor_o = xor_reg;

endmodule

b.sv...

module mod_b (
    input  logic clk,
    input  logic n_rst,
    input  logic and_i,
    input  logic xor_i,
    input  logic or_i,
    output logic [2:0] dummy_o
);

    assign dummy_o = {and_i, xor_i, or_i};

endmodule

tb.sv

`default_nettype none

module top (
    input  logic clk,
    input  logic n_rst,
    input  logic a_t, b_t,
    output logic [2:0] dummy_t
);
    // --- Wires --- //
    logic and_s, or_s, xor_s;

    // --- Instances --- //
    mod_a MODA (
        .clk(clk),
        .n_rst(n_rst),
        .a(a_t),
        .b(b_t),
        .and_o(and_s),
        .xor_o(xor_s),
        .or_o(or_s)
    );

    mod_b MODB (
        .clk(clk),
        .n_rst(n_rst),
        .and_i(and_s),
        .xor_i(xor_s),
        .or_i(or_s),
        .dummy_o(dummy_t)
    );

    `ifdef FORMAL
        logic [15:0] counter;
        initial counter <= '0;

        // Prevent checking on first step
        always @(posedge clk) begin
            counter += 1;
        end

        always @(posedge clk) begin
            if (n_rst && (counter > 0)) assert(MODB.and_i === MODA.and_o);
        end

    `endif

endmodule

`default_nettype wire

console output...

root@fpga-symbiyosys--0_43_0:~/demos/connect_check# sby -f connect.sby
SBY 15:13:38 [connect_bmc] Removing directory '/root/demos/connect_check/connect_bmc'.
SBY 15:13:38 [connect_bmc] Copy '/root/demos/connect_check/b.sv' to '/root/demos/connect_check/connect_bmc/src/b.sv'.
SBY 15:13:38 [connect_bmc] Copy '/root/demos/connect_check/a.sv' to '/root/demos/connect_check/connect_bmc/src/a.sv'.
SBY 15:13:38 [connect_bmc] Copy '/root/demos/connect_check/tb.sv' to '/root/demos/connect_check/connect_bmc/src/tb.sv'.
SBY 15:13:38 [connect_bmc] engine_0: smtbmc boolector -- --keep-going
SBY 15:13:38 [connect_bmc] base: starting process "cd connect_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:13:38 [connect_bmc] base: tb.sv:41: Warning: Identifier `\$root.top.MODA.and_o' is implicitly declared.
SBY 15:13:38 [connect_bmc] base: Warning: Wire top.\$root.top.MODA.and_o is used but has no driver.
SBY 15:13:38 [connect_bmc] base: finished (returncode=0)
SBY 15:13:38 [connect_bmc] prep: starting process "cd connect_bmc/model; yosys -ql design_prep.log design_prep.ys"
SBY 15:13:38 [connect_bmc] prep: Warning: Wire top.\$root.top.MODA.and_o is used but has no driver.
SBY 15:13:38 [connect_bmc] prep: finished (returncode=0)
SBY 15:13:38 [connect_bmc] smt2: starting process "cd connect_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:13:38 [connect_bmc] smt2: finished (returncode=0)
SBY 15:13:38 [connect_bmc] engine_0: starting process "cd connect_bmc; yosys-smtbmc -s boolector --keep-going --presat --unroll --noprogress -t 50  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Solver: boolector
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assertions in step 1..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assumptions in step 2..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Checking assertions in step 2..
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Assert failed in top: tb.sv:41.41-41.75 (_witness_.check_assert_tb_sv_41_6)
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 15:13:38 [connect_bmc] engine_0: ##   0:00:00  Status: failed
SBY 15:13:38 [connect_bmc] engine_0: finished (returncode=1)
SBY 15:13:38 [connect_bmc] engine_0: Status returned by engine: FAIL
SBY 15:13:38 [connect_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:13:38 [connect_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:13:38 [connect_bmc] summary: engine_0 (smtbmc boolector -- --keep-going) returned FAIL
SBY 15:13:38 [connect_bmc] summary: counterexample trace: connect_bmc/engine_0/trace.vcd
SBY 15:13:38 [connect_bmc] summary:   failed assertion top._witness_.check_assert_tb_sv_41_6 at tb.sv:41.41-41.75 in step 2
SBY 15:13:38 [connect_bmc] DONE (FAIL, rc=2)
SBY 15:13:38 The following tasks failed: ['bmc']
root@fpga-symbiyosys--0_43_0:~/demos/connect_check# 

trace.vcd...

$version Generated by Yosys-SMTBMC $end
$timescale 1ns $end
$var integer 32 t smt_step $end
$var event 1 ! smt_clock $end
$scope module top $end
$scope module MODA $end
$scope module _witness_ $end
$var wire 1 n0 anyinit_procdff_17 $end
$var wire 1 n1 anyinit_procdff_18 $end
$var wire 1 n2 anyinit_procdff_19 $end
$upscope $end
$var wire 1 n3 a $end
$var wire 1 n4 and_o $end
$var wire 1 n5 and_reg $end
$var wire 1 n6 b $end
$var wire 1 n7 clk $end
$var wire 1 n8 n_rst $end
$var wire 1 n9 nxt_and $end
$var wire 1 n10 nxt_or $end
$var wire 1 n11 nxt_xor $end
$var wire 1 n12 or_o $end
$var wire 1 n13 or_reg $end
$var wire 1 n14 xor_o $end
$var wire 1 n15 xor_reg $end
$var wire 1 n16 and_o $end
$upscope $end
$scope module MODB $end
$var wire 1 n17 and_i $end
$var wire 1 n18 clk $end
$var wire 3 n19 dummy_o $end
$var wire 1 n20 n_rst $end
$var wire 1 n21 or_i $end
$var wire 1 n22 xor_i $end
$upscope $end
$var wire 1 n23 a_t $end
$var wire 1 n24 and_s $end
$var wire 1 n25 b_t $end
$var wire 1 n26 clk $end
$var wire 16 n27 counter $end
$var wire 3 n28 dummy_t $end
$var wire 1 n29 n_rst $end
$var wire 1 n30 or_s $end
$var wire 1 n31 xor_s $end
$upscope $end
$enddefinitions $end
#0
1!
b00000000000000000000000000000000 t
b1 n7
b1 n26
b0 n0
b0 n1
b0 n2
b0 n3
b0 n4
b0 n5
b0 n6
b0 n8
b0 n9
b0 n10
b0 n11
b0 n12
b0 n13
b0 n14
b0 n15
b1 n16
b0 n17
b0 n18
b000 n19
b0 n20
b0 n21
b0 n22
b0 n23
b0 n24
b0 n25
b0000000000000000 n27
b000 n28
b0 n29
b0 n30
b0 n31
#5
b0 n7
b0 n26
#10
1!
b00000000000000000000000000000001 t
b1 n7
b1 n26
b0 n0
b0 n1
b0 n2
b0 n3
b0 n4
b0 n5
b0 n6
b1 n8
b0 n9
b0 n10
b0 n11
b0 n12
b0 n13
b0 n14
b0 n15
b1 n16
b0 n17
b0 n18
b000 n19
b1 n20
b0 n21
b0 n22
b0 n23
b0 n24
b0 n25
b0000000000000001 n27
b000 n28
b1 n29
b0 n30
b0 n31
#15
b0 n7
b0 n26
#20
1!
b00000000000000000000000000000010 t
b1 n7
b1 n26
b0 n0
b0 n1
b0 n2
b0 n3
b0 n4
b0 n5
b0 n6
b0 n8
b0 n9
b0 n10
b0 n11
b0 n12
b0 n13
b0 n14
b0 n15
b0 n16
b0 n17
b0 n18
b000 n19
b0 n20
b0 n21
b0 n22
b0 n23
b0 n24
b0 n25
b0000000000000010 n27
b000 n28
b0 n29
b0 n30
b0 n31
#25
b0 n7
b0 n26
#30
1!
b00000000000000000000000000000011 t
b1 n7
b1 n26

[whitequark]

Try creating a new wire as e.g. (* hierconn *) wire \MODB.and_i ; and make sure you run flatten on your design. Then use this wire in your assertion.

Also, `default_nettype none instructs Verilog frontends to not automatically create wires for unknown identifiers.

[AdamKeith1]

Ok a few questions.

1. what is (* hierconn *)? I've never seen this before. (found it on Yosys repo)
2. how to incorporate flatten, is it a command line option or something that needs configured in .sby file
3. I have default nettype set to none and then set back to wire should it just be none?
4. I'm looking to make sure that the actual values in the ports for mod_a and mod_b are equal for the whole 'sim', so I'm nopt necessarily looking to make a new wire unless necessary.

Sorry if this is a lot.

[whitequark]

• what is (* hierconn *)? I've never seen this before.

A Yosys-specific extension which allows you to address a wire from an inner module. It is recognized by the flatten pass and otherwise the wire is inert.

• how to incorporate flatten, is it a command line option or something that needs configured in .sby file

Use prep -top top -flatten instead of prep -top top.

• I have default nettype set to none and then set back to wire should it just be none?

If you set it to wire you request any unknown identifier to be created as a new wire. This is a bad idea generally.

4. I'm looking to make sure that the actual values in the ports for mod_a and mod_b are equal for the whole 'sim', so I'm nopt necessarily looking to make a new wire unless necessary.

No new wire is created, the wire declaration is just a phantom construct Yosys uses internally to fill in standard SystemVerilog functionality that it is missing.

[AdamKeith1]

Thank you so much for the quick response. This is a super small design to use as a proof of concept before I test a large design. Is there a way to include an entire folder of a lot of design files in the [files] section or do I have to reference the path for them all individually, there's also pycode plots and I was wondering if there's a way to like use an external yaml file with pycode in the sby file to add all my design files.

[whitequark]

You could use pycode blocks, yes. I don't think there's any functionality that traverses a directory out of the box.

[AdamKeith1]

So I have vhdl designs that references packages, say for example USE work.axi_pkg.ALL. So I include that package in my [files] section but because it's referenced in the work library it doesn't get recognized by the actual design (not my duts are vhd and my tb is sv). How can I get those files into a place my dut will recognize them without modifying the source code?

[whitequark]

I honestly have no idea, I don't use GHDL (or SystemVerilog for that reason).