What a failure contains

A failure names one key point, one input vector, and the two values. That triple reproduces the divergence in simulation without further search.

Everything else is context. The vector is the fact; the cone explains it.

A mutated netlist

The script below places the RTL and the mutated block side by side with full input ports. On the vector a=0, b=0, c=1 the RTL gives 1 and the mutated block gives 0, since the mutated term drops the inverter on a.

The miter exposes the shared inputs as in_a, in_b and in_c. The solver call pins those to that vector and asks for the trigger output at 1, so it exits cleanly only when a counterexample exists there.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

read_verilog <<EOV
module gold(input wire a, b, c, output wire y);
assign y = (a & b) | (~a & c);
endmodule
module gate(input wire a, b, c, output wire y);
assign y = (a & b) | (a & c);
endmodule
EOV
proc
opt
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
sat -set in_a 0 -set in_b 0 -set in_c 1 -set trigger 1 -verify m
log PASS: vector a0 b0 c1 separates RTL 1 from mutated netlist 0

Hand evaluation agrees: RTL gives (0 AND 0) OR (1 AND 1), which is 1. The mutated block gives (0 AND 0) OR (0 AND 1), which is 0.

Localising the cone

From the failing key point, walk backwards through its fan-in on both sides. The first gate whose inputs agree but whose outputs differ is the divergence origin.

Here the origin is the inverter on a in the second product term. The full table splits eight vectors into five agreements and three differences.

8 vectors total: 5 agree, 3 differ
agree share = 5 / 8 = 62.5%
differ share = 3 / 8 = 37.5%
62.5 + 37.5 = 100

Common mistakes

Related topics

• Combinational equivalence

• Constants and brute force