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