2 read_verilog -formal <<EOT
3 module gate(input clk, output [32:0] o, p, q, r, s, t, u);
16 ## Equivalence checking
18 read_verilog -formal <<EOT
19 module gold(input clk, output [32:0] o, p, q, r, s, t, u);
20 assign o = {33{1'bx}};
21 assign p = {{32{1'b0}}, 1'bx};
22 assign q = {33{1'bz}};
23 assign r = {{32{1'b0}}, 1'bz};
24 assign s = {33{1'b0}};
25 assign t = {{32{1'b0}}, 1'b1};
26 assign u = {33{1'b1}};
32 miter -equiv -flatten -make_assert -make_outputs gold gate miter
33 sat -verify -prove-asserts -show-ports -enable_undef miter