| 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 |