read_verilog splice.v hierarchy -check; opt copy test gold cd test splice # show cd .. rename test gate miter -equiv -make_assert -make_outputs gold gate miter flatten miter sat -verify -prove-asserts -show-inputs -show-outputs miter