read_verilog -formal <<EOT module gate(input clk, output [32:0] o, p, q, r, s, t, u); assign o = 'bx; assign p = 1'bx; assign q = 'bz; assign r = 1'bz; assign s = 1'b0; assign t = 'b1; assign u = -'sb1; endmodule EOT proc ## Equivalence checking read_verilog -formal <<EOT module gold(input clk, output [32:0] o, p, q, r, s, t, u); assign o = {33{1'bx}}; assign p = {{32{1'b0}}, 1'bx}; assign q = {33{1'bz}}; assign r = {{32{1'b0}}, 1'bz}; assign s = {33{1'b0}}; assign t = {{32{1'b0}}, 1'b1}; assign u = {33{1'b1}}; endmodule EOT proc miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports -enable_undef miter