Blackbox modules, Dynamic Port widths and write_smt2

[jakobwenzel]

Steps to reproduce the issue

This Verilog code contains a Blackbox module with a parameterized port width:

module top();
    parameter W = 10;
    wire [W-1:0] x;
    empty #(.W(W)) empty_inst(.x(x));
endmodule

module empty#(parameter W = 0)(output wire [W-1:0] x);
endmodule

Running Yosys with this Script on the File:

read_verilog xyz.v
hierarchy -top top
write_smt2

Expected behavior

Yosys does not crash.

Actual behavior

Yosys crashes with this error message:

ERROR: Assert `sig.size() == 1 && sig.chunks().size() == 1' failed in ./kernel/rtlil.h:1443.

The Blackbox module does not seem to get derived for the parameter values. Therefore, port widths between the toplevel module and the black box module do not match.

[arcturusannamalai]

Not crashing today on Jun 29th, SHAID: b5b0b7e83 ,

vim xyz.v
muthu@rtlworks-16gb-8cpu-sfo3:~/devel/yosys$ vim issue.ys
muthu@rtlworks-16gb-8cpu-sfo3:~/devel/yosys$ ./yosys issue.ys 
 Yosys 0.30+48 (git sha1 b5b0b7e83, clang 15.0.7 -fPIC -Os)

-- Executing script file `issue.ys' --

1. Executing Verilog-2005 frontend: xyz.v
Parsing Verilog input from `xyz.v' to AST representation.
Generating RTLIL representation for module `\top'.
Generating RTLIL representation for module `\empty'.
Successfully finished Verilog frontend.

2. Executing HIERARCHY pass (managing design hierarchy).

2.1. Analyzing design hierarchy..
Top module:  \top

2.2. Analyzing design hierarchy..
Top module:  \top
Removed 0 unused modules.

3. Executing SMT2 backend.

3.1. Executing BMUXMAP pass.

3.2. Executing DEMUXMAP pass.
; SMT-LIBv2 description generated by Yosys 0.30+48 (git sha1 b5b0b7e83, clang 15.0.7 -fPIC -Os)
Creating SMT-LIBv2 representation of module top.
; yosys-smt2-module top
(declare-sort |top_s| 0)
(declare-fun |top_is| (|top_s|) Bool)
; yosys-smt2-cell empty empty_inst
; yosys-smt2-witness {"path": ["\\empty_inst"], "smtname": "empty_inst", "type": "cell"}
(declare-fun |top#0| (|top_s|) (_ BitVec 2)) ; \x
(declare-fun |top_h empty_inst| (|top_s|) |empty_s|)
(define-fun |top_a| ((state |top_s|)) Bool 
  (|empty_a| (|top_h empty_inst| state))
)
(define-fun |top_u| ((state |top_s|)) Bool 
  (|empty_u| (|top_h empty_inst| state))
)
(define-fun |top_i| ((state |top_s|)) Bool 
  (|empty_i| (|top_h empty_inst| state))
)
(define-fun |top_h| ((state |top_s|)) Bool (and
  (= (|top_is| state) (|empty_is| (|top_h empty_inst| state)))
  (= (|top#0| state) (|empty_n x| (|top_h empty_inst| state))) ; empty.x
  (|empty_h| (|top_h empty_inst| state))
))
(define-fun |top_t| ((state |top_s|) (next_state |top_s|)) Bool 
  (|empty_t| (|top_h empty_inst| state) (|top_h empty_inst| next_state))
) ; end of module top
; yosys-smt2-topmod top
; end of yosys output

End of script. Logfile hash: cf560bcb53, CPU: user 0.00s system 0.00s, MEM: 8.11 MB peak
Yosys 0.30+48 (git sha1 b5b0b7e83, clang 15.0.7 -fPIC -Os)
Time spent: 55% 2x write_smt2 (0 sec), 30% 2x read_verilog (0 sec), ...