34 lines
666 B
Plaintext
34 lines
666 B
Plaintext
|
|
||
|
|
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
|