read_verilog << EOT
  module test(input [7:0] a, b, c, d, output [7:0] x, y, z);
    assign x = a + b, y = b + c, z = c + d;
  endmodule
EOT

copy test gold
rename test gate

submod -name mycell gate/x %ci*
design -copy-to mymap mycell
extract -map %mymap gate

select -assert-count 3 gold/t:*
select -assert-count 3 gold/t:$add

select -assert-count 3 gate/t:*
select -assert-count 3 gate/t:mycell

miter -equiv -flatten gold gate miter
sat -verify -prove trigger 0 miter