Equiv_opt on hierarchical designs

Users
1

One of the tests I’m debugging currently runs a pass on a design that happens to have a submodule:

read_verilog <<EOF
module sub (
  input wire in,
  output wire out1,
  output wire out2,
  output wire out3,
  output wire out4,
  output wire out5
);
  assign out1 = in;
  assign out2 = in;
  assign out3 = in;
  assign out4 = in;
  assign out5 = in;
endmodule

module top (
  input wire a,
  output wire w1,
  output wire w2,
  output wire w3,
  output wire w4,
  output wire w5
);
  sub u1 (.in(a), .out1(w1), .out2(w2), .out3(w3), .out4(w4), .out5(w5));
endmodule
EOF

equiv_opt log "hi"

Before, this worked, automatically black-boxing the submodules:

1.9. Executing EQUIV_INDUCT pass.
Found 5 unproven $equiv cells in module equiv:
Warning: No SAT model available for cell u1_gate (sub).
Warning: No SAT model available for cell u1_gold (sub).
  Proving existence of base case for step 1. (38 clauses over 17 variables)
  Proving induction step 1. (73 clauses over 32 variables)
  Proof for induction step holds. Entire workset of 5 cells proven!
Proved 5 previously unproven $equiv cells.

Since equiv_simple, equiv_induct: error by default on missing model, add -i… · YosysHQ/yosys@8d1c1fa · GitHub however, this fails:

2.5. Executing EQUIV_INDUCT pass.
Found 5 unproven $equiv cells in module equiv:
ERROR: No SAT model available for cell u1_gate (sub)

I agree with this change, but what I cannot tell is what is the “intended” path here, do I flatten the design first or is there a way I’m missing to equiv_opt recursively?