Undriven "C-like Top-level Signals" in SystemVerilog model

[NicolasVanPhan]

Issue

I encountered failures in formal verification testbenches on the Sail-generated SystemVerilog (SV) model caused by "C-like top-level signals."

These signals are declared at the top level, outside any module, and are referenced within modules without being explicitly passed as inputs or declared internally. Consequently, they are treated as undriven signals, which leads to garbage values and failures during simulation.

Example: zero_reg Signal

Below is a snippet illustrating the issue with the zero_reg signal:

logic [31:0] zero_reg;

module sail_setup_let_18(
    output logic [31:0] zero_reg_1
);
    always_comb begin
        zero_reg_1 = 32'h0;
    end;
endmodule

module rX(
  /* inputs don't mention `zero_reg` */
);
 /* internal signals declaration doesn't mention `zero_reg` */
...
    regval_from_reg inst_0_regval_from_reg(((r_0 == 64'h0) ? zero_reg : ... /* zero_reg not driven anywhere */
...
endmodule

Problem Summary

The zero_reg signal is declared at the top level but is neither passed as an input nor declared as an internal signal in modules such as rX.
SystemVerilog does not support C-like global variables, so such signals are treated as undriven, leading to incorrect behavior.

Request for Suggestions

Has anyone encountered a similar issue? If so, do you have ideas for fixes or workarounds?

Possible directions might include:

• Explicitly passing these signals as module inputs.
• Creating a dedicated driver module to encapsulate such signals.

Any feedback or suggestions would be greatly appreciated!

Many thanks,
Nicolas

[Alasdair]

The idea is the sail_setup_let_18 is instantiated to drive the toplevel signal. Currently I generate toplevel signals for any let-bound constant in Sail, which means they only have to be assigned once. In theory there is no reason why I couldn't have them as input ports for every module that needs them, it just seemed a bit nicer to have them at the toplevel to avoid adding even more ports to the modules.

Previously we have used genuinely very C-like SystemVerilog where we both read and wrote to toplevel signals, and that didn't cause us any issues other than some debugging features in Jasper not liking it very much, so I guess it depends on the tool?

[NicolasVanPhan]

I agree that passing all those signals through the module’s I/Os can be quite cumbersome.

From my experience, this approach works well when the generated model is used as the top-level module. However, when it is instantiated inside another module, EDA tools require the full hierarchical path to the signal; otherwise, they won’t be able to locate it.

In the example above, I modified the references to zero_reg by prefixing them with my_wrapper_module.zero_reg, and instantiated the sail_toplevel() module. This approach worked as expected.

That said, the change was done manually on the generated model, which is neither efficient nor sustainable in the long term. I was wondering if this adjustment could be automated via the compiler or if there’s a more elegant workaround available?