yosys/tests/various/submod.ys

read_verilog <<EOT
module top(input a, output [1:0] b);
wire c;
(* submod="bar" *) sub s1(a, c);
assign b[0] = c;
endmodule

module sub(input a, output c);
assign c = a;
endmodule
EOT

hierarchy -top top
proc
design -save gold

submod
design -stash gate

design -import gold -as gold
design -import gate -as gate

miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter


design -reset
read_verilog <<EOT
module top(input a, output [1:0] b);
(* submod="bar" *) sub s1(a, b[1]);
assign b[0] = 1'b0;
endmodule

module sub(input a, output c);
assign c = a;
endmodule
EOT

hierarchy -top top
proc
design -save gold

submod
design -stash gate

design -import gold -as gold
design -import gate -as gate

miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter