Hierarchical Signal Access

[Seek64]

Hello everyone,

I was playing around with the unbounded prover example:

module testbench (
  input clk,
  input reset,
  input [7:0] din,
  output reg [7:0] dout
);
  demo uut (
    .clk  (clk  ),
    .reset(reset),
    .din  (din  ),
    .dout (dout )
  );

  reg init = 1;
  always @(posedge clk) begin
    if (init) assume (reset);
    if (!reset) assert (!dout[1:0]);
    init <= 0;
  end
endmodule

module demo (
  input clk,
  input reset,
  input [7:0] din,
  output reg [7:0] dout
);
  reg [7:0] buffer;
  reg [1:0] state;

  always @(posedge clk) begin
    if (reset) begin
      dout <= 0;
      state <= 0;
    end else
    case (state)
      0: begin
        buffer <= din;
    state <= 1;
      end
      1: begin
        if (buffer[1:0])
      buffer <= buffer + 1;
    else
      state <= 2;
      end
      2: begin
        dout <= dout + buffer;
    state <= 0;
      end
    endcase
  end
endmodule

My question is if there is a way to access the submodule signals from the testbench itself? Essentially, what I would like to do is something like:

if (!reset) assert (uut.state!=3);

If I try it like this, what I get is the following warning

Warning: Identifier `\uut.state' is implicitly declared.

and the assertion is ignored during the proof.

The two workarounds I tried were

• Putting the assertion directly into the demo module
• Creating a separate output for the state signal

Both of them worked. For my use case, however, I would like to compare the signals of the different submodules. Therefore, only the second option would be viable. However, creating a separate output for each signal I want to compare seems very cumbersome, so I would like to know if hierarchical access is also possible somehow?

[nakengelhardt]

No, unfortunately hierarchical access is only possible using the verific frontend (available in the commercial Tabby CAD Suite only). There is an effort to implement it for read_verilog by an external contributor but it seems currently stalled: https://github.com/YosysHQ/yosys/pull/2752

[Seek64]

Thank you for the response. I will then resort to the workaround for the time being and also have a look at the PR.