LEC: Combinational Equivalence

Turn "is the netlist the RTL?" into a safety property, split it at matched flops, and read an equivalence report, including the failures that are not real.

Lesson: F6.1
Time: 20 min
Runs on: SymbiYosys
Check: 5 questions

A new synthesis option restructured a FIFO's write-accept logic, and the gate-level regression passed. The netlist now let a write through when the FIFO was full and a read arrived in the same cycle, a corner the slow gate-level run never reached. An equivalence check finds it in under a second.

Run	Strategy	Partitions	Result	Wall time
RTL as A8.1 writes it, against its netlist	`sat`	19	18 proved, `aw` not proven	0.7 s
The same, `sby` (word level, depth 1)	`sby`	19	`aw` not proven	3.5 s
The same, with `merge aw full`	`sat`	18	all proved	0.7 s
Write accept written `!full`	`sat`	19	all proved	0.7 s
Edited netlist, with `merge aw full`	`sat`	18	`aw` fails	0.7 s

EQY from the pinned suite, run directly so the partition commands and the sat strategy are available. The lab below uses the runner's fixed script.

The Miter

The Miter: Two Designs, One Set of InputsGold is the RTL, gate is its netlist. Every input drives both copies; every output pair meets at an XOR.

Read the diagram as text

Shared inputs: write_en, read_en, write_data, reset, initialize
Gold: hardware_fifo RTL: the design you verified
Gate: Yosys netlist: 570 lines, 47 single-bit flops
XOR on every output pair: full, empty, read_valid, read_data
Property: the XOR is never 1: a safety property on the combined design

Shared inputs → Gold: hardware_fifo RTL
Shared inputs → Gate: Yosys netlist
Gold: hardware_fifo RTL → XOR on every output pair
Gate: Yosys netlist → XOR on every output pair
XOR on every output pair → Property: the XOR is never 1

Inputs that make an XOR 1 are a counterexample. Everything from F1 to F4 applies to this bench.

Put the RTL and the netlist side by side and drive both from the same inputs. XOR each pair of outputs. If any XOR can be 1, the designs differ, and the values that make it 1 are the counterexample.

"The XOR is never 1" is a safety property on the combined design. Equivalence is model checking with a second design as the specification. Here the gold is the A8.1 FIFO and the gate is what synthesis (R1.1) made of it.

Key Points: One Cone per Matched Flop

Matched State Turns One Question into Many Small OnesFlops with the same name in both designs are paired. Each pair, and each output, gets its own cone of logic to compare.

call: who calls whom

Read the diagram as text

Key points in: inputs, plus every matched flop output
One cone per key point: gold logic and gate logic, side by side
Key points out: each flop input and each output
Flops paired by name: wp, used, rp, response_valid, response, memory

Key points in → One cone per key point
One cone per key point → Key points out
Flops paired by name → One cone per key point

EQY made 19 partitions for this FIFO: the flops above, eight read_data bits, and the named wires aw, ar, full, empty, read_valid.

Combinational equivalence, the LEC that signs off synthesis, adds one assumption: both designs have the same flops, paired by name. Each pair is cut. Its output becomes a free input on both sides, and its input becomes a point to compare.

Every check is now a cone of logic between key points. Nothing is unrolled and no state is explored, which is why LEC runs on whole chips while property checking struggles with a single block.

A False Failure

The suite run: sat is a bit-level SAT check per partition.

[gold]
read_verilog -sv fifo.sv
prep -top hardware_fifo

[gate]
read_verilog fifo_net.v
prep -top hardware_fifo

[strategy sat]
use sat

Signal at the cut	Value
`full`	0
`used`	3
`write_en`	1
`aw (gate)`	1
`aw (gold)`	0

The counterexample for partition aw. The netlist computes aw from full; the RTL computes it from used. Both are cut points, so the solver may set them apart.

full = 0 with used = 3 is impossible: full is defined as used == 3. The cut threw away the logic that ties the two together. This is a false negative, and EQY prints it in the same words as a real failure.

Merging the two partitions ([partition *] then merge aw full) puts that logic back, and all 18 partitions prove. Writing the RTL's accept as !full does the same from the other side. The function is unchanged; only the key points line up.

A Failure That Is Real

The one-line edit to the netlist.

- assign aw = write_en & ~(full);
+ assign aw = write_en & ~(full & ~read_en);

Signal at the cut	Value
`read_en`	1
`used`	3
`write_en`	1
`aw (gate)`	1
`aw (gold)`	0
`full (gate)`	1
`full (gold)`	1

The merged partition's counterexample. Every value is consistent: three entries, a write and a read offered together.

With used = 3 the FIFO is full, so the RTL refuses the write and the edited netlist takes it. The inputs are legal and the state is reachable: a real bug.

What LEC cannot check: any change to the flops themselves, such as retiming, re-encoding or an added pipeline stage. That needs sequential equivalence (F6.2). Compare it with simulation (F1.1): a gate-level regression samples the space the RTL regression sampled, slower. LEC decides every cone for every value.

Asked in Interviews

Question	Answer
LEC versus SEC?	LEC pairs the same flops in both designs and compares the logic cones between them. SEC lets the flops differ and must reason over sequences of states.
What is a miter?	Both designs on shared inputs with an XOR on each output pair; equivalence is the safety property "the XOR is never 1".
Why sign off synthesis with LEC and not gate-level simulation?	LEC checks every cone for every input value in seconds; simulation samples.
Your LEC run reports a mismatch. What first?	Check whether the counterexample is reachable: inconsistent values at cut points mean a false negative to fix in the setup, not in the design.

Try It

The runner's EQY task. Each file's module is renamed to the task's top before the run.

[gold]
read_verilog -sv design.sv
prep -top hardware_fifo

[gate]
read_verilog -sv gate.sv
prep -top hardware_fifo

[strategy sby]
use sby
depth 1
engine smtbmc yices

How the gate was made: Yosys 0.70+290, the RTL with the A8.1 accept terms.

read_verilog -sv fifo.sv; synth -top hardware_fifo; write_verilog -noattr fifo_net.v

Run it
As loaded: UNKNOWN: equivalence not proven, in about 3.8 s. Open the log and find the one partition that failed.
Line up the key points
In design.sv change used < DEPTH to !full and run again: EQY PASS: every partition proved.
Edit the netlist
In gate.sv find assign aw = write_en & ~(full); and make it assign aw = write_en & ~(full & ~read_en);. Run: UNKNOWN: equivalence not proven. Is this one real? The table above answers it.

Top moduleModeDepthEngine

design.sv

gate.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module hardware_fifo #(parameter int DEPTH=3, WIDTH=8)(input clk, initialize, reset, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  localparam int STORAGE = 1 << $clog2(DEPTH);
  reg [STORAGE*WIDTH-1:0] memory = 0;   // entry i is memory[i*WIDTH +: WIDTH]
  reg [WIDTH-1:0] response = 0;
  reg response_valid = 0;
  reg [1:0] used = 0, wp = 0, rp = 0;
  wire aw = write_en && used < DEPTH;   // a write is accepted
  wire ar = read_en && used > 0;        // a read is accepted
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = response_valid;
  assign read_data = response;
  always @(posedge clk) begin
    if (initialize) begin
      used <= 0; wp <= 0; rp <= 0; response <= 0; response_valid <= 0; memory <= 0;
    end else if (reset) begin
      used <= 0; wp <= 0; rp <= 0; response <= 0; response_valid <= 0;
    end else begin
      response_valid <= ar;
      if (ar) begin response <= memory[rp*WIDTH +: WIDTH]; rp <= rp == DEPTH-1 ? 0 : rp + 1; end
      if (aw) begin memory[wp*WIDTH +: WIDTH] <= write_data; wp <= wp == DEPTH-1 ? 0 : wp + 1; end
      case ({aw, ar}) 2'b10: used <= used + 1; 2'b01: used <= used - 1; default: used <= used; endcase
    end
  end
endmodule

Check Yourself

Predict the outputThe RTL with A8.1's accept terms against its own unedited Yosys netlist, run in this site's EQY mode (default name matching, sby strategy, depth 1, smtbmc yices). The verdict is:

module hardware_fifo #(parameter int DEPTH=3, WIDTH=8)(input clk, initialize, reset, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  localparam int STORAGE = 1 << $clog2(DEPTH);
  reg [STORAGE*WIDTH-1:0] memory = 0;   // entry i is memory[i*WIDTH +: WIDTH]
  reg [WIDTH-1:0] response = 0;
  reg response_valid = 0;
  reg [1:0] used = 0, wp = 0, rp = 0;
  wire aw = write_en && used < DEPTH;   // a write is accepted
  wire ar = read_en && used > 0;        // a read is accepted
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = response_valid;
  assign read_data = response;
  always @(posedge clk) begin
    if (initialize) begin
      used <= 0; wp <= 0; rp <= 0; response <= 0; response_valid <= 0; memory <= 0;
    end else if (reset) begin
      used <= 0; wp <= 0; rp <= 0; response <= 0; response_valid <= 0;
    end else begin
      response_valid <= ar;
      if (ar) begin response <= memory[rp*WIDTH +: WIDTH]; rp <= rp == DEPTH-1 ? 0 : rp + 1; end
      if (aw) begin memory[wp*WIDTH +: WIDTH] <= write_data; wp <= wp == DEPTH-1 ? 0 : wp + 1; end
      case ({aw, ar}) 2'b10: used <= used + 1; 2'b01: used <= used - 1; default: used <= used; endcase
    end
  end
endmodule

Read included file: gate.sv


module hardware_fifo(clk, initialize, reset, write_en, read_en, write_data, full, empty, read_valid, read_data);
  input clk;
  wire clk;
  input initialize;
  wire initialize;
  input reset;
  wire reset;
  input write_en;
  wire write_en;
  input read_en;
  wire read_en;
  input [7:0] write_data;
  wire [7:0] write_data;
  output full;
  wire full;
  output empty;
  wire empty;
  output read_valid;
  wire read_valid;
  output [7:0] read_data;
  wire [7:0] read_data;
  wire _000_;
  wire _001_;
  wire _002_;
  wire _003_;
  wire _004_;
  wire _005_;
  wire _006_;
  wire _007_;
  wire _008_;
  wire _009_;
  wire _010_;
  wire _011_;
  wire _012_;
  wire _013_;
  wire _014_;
  wire _015_;
  wire _016_;
  wire _017_;
  wire _018_;
  wire _019_;
  wire _020_;
  wire _021_;
  wire _022_;
  wire _023_;
  wire _024_;
  wire _025_;
  wire _026_;
  wire _027_;
  wire _028_;
  wire _029_;
  wire _030_;
  wire _031_;
  wire _032_;
  wire _033_;
  wire _034_;
  wire _035_;
  wire _036_;
  wire _037_;
  wire _038_;
  wire _039_;
  wire _040_;
  wire _041_;
  wire _042_;
  wire _043_;
  wire _044_;
  wire _045_;
  wire _046_;
  wire _047_;
  wire _048_;
  wire _049_;
  wire _050_;
  wire _051_;
  wire _052_;
  wire _053_;
  wire _054_;
  wire _055_;
  wire _056_;
  wire _057_;
  wire _058_;
  wire _059_;
  wire _060_;
  wire _061_;
  wire _062_;
  wire _063_;
  wire _064_;
  wire _065_;
  wire _066_;
  wire _067_;
  wire _068_;
  wire _069_;
  wire _070_;
  wire _071_;
  wire _072_;
  wire _073_;
  wire _074_;
  wire _075_;
  wire _076_;
  wire _077_;
  wire _078_;
  wire _079_;
  wire _080_;
  wire _081_;
  wire _082_;
  wire _083_;
  wire _084_;
  wire _085_;
  wire _086_;
  wire _087_;
  wire _088_;
  wire _089_;
  wire _090_;
  wire _091_;
  wire _092_;
  wire _093_;
  wire _094_;
  wire _095_;
  wire _096_;
  wire _097_;
  wire _098_;
  wire _099_;
  wire _100_;
  wire _101_;
  wire _102_;
  wire _103_;
  wire _104_;
  wire _105_;
  wire _106_;
  wire _107_;
  wire _108_;
  wire _109_;
  wire _110_;
  wire _111_;
  wire _112_;
  wire _113_;
  wire _114_;
  wire _115_;
  wire _116_;
  wire _117_;
  wire _118_;
  wire _119_;
  wire _120_;
  wire _121_;
  wire _122_;
  wire _123_;
  wire _124_;
  wire _125_;
  wire _126_;
  wire _127_;
  wire _128_;
  wire _129_;
  wire _130_;
  wire _131_;
  wire _132_;
  wire _133_;
  wire _134_;
  wire _135_;
  wire _136_;
  wire _137_;
  wire _138_;
  wire _139_;
  wire _140_;
  wire _141_;
  wire _142_;
  wire _143_;
  wire _144_;
  wire _145_;
  wire _146_;
  wire _147_;
  wire _148_;
  wire _149_;
  wire _150_;
  wire _151_;
  wire _152_;
  wire _153_;
  wire _154_;
  wire _155_;
  wire _156_;
  wire _157_;
  wire _158_;
  wire _159_;
  wire _160_;
  wire _161_;
  wire _162_;
  wire _163_;
  wire _164_;
  wire _165_;
  wire _166_;
  wire _167_;
  wire _168_;
  wire _169_;
  wire _170_;
  wire _171_;
  wire _172_;
  wire _173_;
  wire _174_;
  wire _175_;
  wire _176_;
  wire _177_;
  wire _178_;
  wire _179_;
  wire _180_;
  wire _181_;
  wire _182_;
  wire _183_;
  wire _184_;
  wire _185_;
  wire _186_;
  wire _187_;
  wire [1:0] _188_;
  wire [1:0] _189_;
  wire [1:0] _190_;
  wire [32:0] _191_;
  wire [32:0] _192_;
  wire ar;
  wire aw;
  reg [31:0] memory = 32'd0;
  reg [7:0] response = 8'h00;
  reg response_valid = 1'h0;
  reg [1:0] rp = 2'h0;
  reg [1:0] used = 2'h0;
  reg [1:0] wp = 2'h0;
  assign _191_[4] = ~wp[1];
  assign _190_[0] = ~wp[0];
  assign _021_ = write_data[1] & _005_;
  assign _003_ = _192_[4] & ~(wp[0]);
  assign _006_ = write_data[0] & _003_;
  assign _029_ = write_data[7] & _003_;
  assign _027_ = write_data[6] & _005_;
  assign _028_ = write_data[7] & _005_;
  assign _023_ = write_data[3] & _005_;
  assign _013_ = write_data[2] & _004_;
  assign _019_ = write_data[7] & _004_;
  assign _017_ = write_data[5] & _004_;
  assign _000_ = reset | initialize;
  assign _020_ = write_data[0] & _005_;
  assign _008_ = write_data[2] & _003_;
  assign _009_ = write_data[3] & _003_;
  assign _010_ = write_data[4] & _003_;
  assign _026_ = write_data[6] & _003_;
  assign _024_ = write_data[4] & _005_;
  assign _007_ = write_data[1] & _003_;
  assign _025_ = write_data[5] & _005_;
  assign _014_ = write_data[3] & _004_;
  assign _018_ = write_data[6] & _004_;
  assign aw = write_en & ~(full);
  assign _011_ = write_data[0] & _004_;
  assign _022_ = write_data[2] & _005_;
  assign _015_ = write_data[5] & _003_;
  assign _002_ = wp[0] & ~(wp[1]);
  assign _001_ = ~(wp[1] | wp[0]);
  assign _004_ = wp[0] & ~(_192_[4]);
  assign _012_ = write_data[1] & _004_;
  assign _005_ = ~(wp[0] | _192_[4]);
  assign _016_ = write_data[4] & _004_;
  assign _188_[0] = ~used[0];
  assign _030_ = ~used[1];
  assign _032_ = aw | ~(ar);
  assign _031_ = ar ^ aw;
  assign full = used[0] & used[1];
  assign empty = ~(used[0] | used[1]);
  assign _033_ = used[0] ^ used[1];
  assign _189_[1] = ~(_032_ ^ _033_);
  assign _045_ = ~(_188_[0] & _030_);
  assign ar = read_en & _045_;
  assign _051_ = ~(rp[1] & _050_);
  assign _052_ = ~(memory[8] & _044_);
  assign _053_ = ~(memory[0] & _043_);
  assign _054_ = _052_ & _053_;
  assign _035_ = ~(_051_ & _054_);
  assign _055_ = rp[0] ? memory[25] : memory[17];
  assign _056_ = ~(rp[1] & _055_);
  assign _057_ = ~(memory[9] & _044_);
  assign _058_ = ~(memory[1] & _043_);
  assign _059_ = _057_ & _058_;
  assign _044_ = rp[0] & ~(rp[1]);
  assign _036_ = ~(_056_ & _059_);
  assign _060_ = rp[0] ? memory[26] : memory[18];
  assign _061_ = ~(rp[1] & _060_);
  assign _062_ = ~(memory[10] & _044_);
  assign _063_ = ~(memory[2] & _043_);
  assign _064_ = _062_ & _063_;
  assign _037_ = ~(_061_ & _064_);
  assign _065_ = rp[0] ? memory[27] : memory[19];
  assign _066_ = ~(rp[1] & _065_);
  assign _067_ = ~(memory[11] & _044_);
  assign _043_ = ~(rp[1] | rp[0]);
  assign _068_ = ~(memory[3] & _043_);
  assign _069_ = _067_ & _068_;
  assign _038_ = ~(_066_ & _069_);
  assign _070_ = rp[0] ? memory[28] : memory[20];
  assign _071_ = ~(rp[1] & _070_);
  assign _072_ = ~(memory[12] & _044_);
  assign _073_ = ~(memory[4] & _043_);
  assign _074_ = _072_ & _073_;
  assign _039_ = ~(_071_ & _074_);
  assign _075_ = rp[0] ? memory[29] : memory[21];
  assign _046_ = ~(memory[7] & _043_);
  assign _076_ = ~(rp[1] & _075_);
  assign _077_ = ~(memory[13] & _044_);
  assign _078_ = ~(memory[5] & _043_);
  assign _079_ = _077_ & _078_;
  assign _040_ = ~(_076_ & _079_);
  assign _080_ = rp[0] ? memory[30] : memory[22];
  assign _081_ = ~(rp[1] & _080_);
  assign _082_ = ~(memory[14] & _044_);
  assign _083_ = ~(memory[6] & _043_);
  assign _084_ = _082_ & _083_;
  assign _047_ = ~(_034_ & rp[1]);
  assign _041_ = ~(_081_ & _084_);
  assign _048_ = ~(memory[15] & _044_);
  assign _049_ = _046_ & _048_;
  assign _042_ = ~(_047_ & _049_);
  assign _050_ = rp[0] ? memory[24] : memory[16];
  assign _085_ = aw & ~(reset);
  assign _118_ = ~(_191_[4] | _190_[0]);
  assign _124_ = ~(memory[30] & _119_);
  assign _185_ = ~(_014_ & _118_);
  assign _105_ = ~(_184_ & _185_);
  assign _186_ = ~(memory[28] & _119_);
  assign _187_ = ~(_016_ & _118_);
  assign _106_ = ~(_186_ & _187_);
  assign _125_ = ~(_018_ & _118_);
  assign _109_ = ~(_124_ & _125_);
  assign _192_[4] = _191_[4] & _190_[0];
  assign _126_ = ~(_003_ & _192_[4]);
  assign _127_ = ~(memory[0] & _126_);
  assign _128_ = ~(_006_ & _192_[4]);
  assign _086_ = ~(_127_ & _128_);
  assign _129_ = ~(memory[1] & _126_);
  assign _130_ = ~(_007_ & _192_[4]);
  assign _119_ = ~(_004_ & _118_);
  assign _097_ = ~(_129_ & _130_);
  assign _131_ = ~(memory[2] & _126_);
  assign _132_ = ~(_008_ & _192_[4]);
  assign _108_ = ~(_131_ & _132_);
  assign _133_ = ~(memory[3] & _126_);
  assign _134_ = ~(_009_ & _192_[4]);
  assign _111_ = ~(_133_ & _134_);
  assign _135_ = ~(memory[4] & _126_);
  assign _136_ = ~(_010_ & _192_[4]);
  assign _112_ = ~(_135_ & _136_);
  assign _120_ = ~(memory[31] & _119_);
  assign _137_ = ~(memory[5] & _126_);
  assign _138_ = ~(_015_ & _192_[4]);
  assign _113_ = ~(_137_ & _138_);
  assign _139_ = ~(memory[6] & _126_);
  assign _140_ = ~(_026_ & _192_[4]);
  assign _114_ = ~(_139_ & _140_);
  assign _141_ = ~(memory[7] & _126_);
  assign _142_ = ~(_029_ & _192_[4]);
  assign _115_ = ~(_141_ & _142_);
  assign _143_ = _191_[4] ^ _190_[0];
  assign _121_ = ~(_019_ & _118_);
  assign _144_ = ~(_004_ & _143_);
  assign _145_ = ~(memory[8] & _144_);
  assign _146_ = ~(_011_ & _143_);
  assign _116_ = ~(_145_ & _146_);
  assign _147_ = ~(memory[9] & _144_);
  assign _148_ = ~(_012_ & _143_);
  assign _117_ = ~(_147_ & _148_);
  assign _149_ = ~(memory[10] & _144_);
  assign _150_ = ~(_013_ & _143_);
  assign _087_ = ~(_149_ & _150_);
  assign _110_ = ~(_120_ & _121_);
  assign _151_ = ~(memory[11] & _144_);
  assign _152_ = ~(_014_ & _143_);
  assign _088_ = ~(_151_ & _152_);
  assign _153_ = ~(memory[12] & _144_);
  assign _154_ = ~(_016_ & _143_);
  assign _089_ = ~(_153_ & _154_);
  assign _155_ = ~(memory[13] & _144_);
  assign _156_ = ~(_017_ & _143_);
  assign _090_ = ~(_155_ & _156_);
  assign _157_ = ~(memory[14] & _144_);
  assign _034_ = rp[0] ? memory[31] : memory[23];
  assign _158_ = ~(_018_ & _143_);
  assign _091_ = ~(_157_ & _158_);
  assign _159_ = ~(memory[15] & _144_);
  assign _160_ = ~(_019_ & _143_);
  assign _092_ = ~(_159_ & _160_);
  assign _161_ = ~(_005_ & _143_);
  assign _162_ = ~(memory[16] & _161_);
  assign _163_ = ~(_020_ & _143_);
  assign _093_ = ~(_162_ & _163_);
  assign _164_ = ~(memory[17] & _161_);
  assign _122_ = ~(memory[29] & _119_);
  assign _165_ = ~(_021_ & _143_);
  assign _094_ = ~(_164_ & _165_);
  assign _166_ = ~(memory[18] & _161_);
  assign _167_ = ~(_022_ & _143_);
  assign _095_ = ~(_166_ & _167_);
  assign _168_ = ~(memory[19] & _161_);
  assign _169_ = ~(_023_ & _143_);
  assign _096_ = ~(_168_ & _169_);
  assign _170_ = ~(memory[20] & _161_);
  assign _171_ = ~(_024_ & _143_);
  assign _123_ = ~(_017_ & _118_);
  assign _098_ = ~(_170_ & _171_);
  assign _172_ = ~(memory[21] & _161_);
  assign _173_ = ~(_025_ & _143_);
  assign _099_ = ~(_172_ & _173_);
  assign _174_ = ~(memory[22] & _161_);
  assign _175_ = ~(_027_ & _143_);
  assign _100_ = ~(_174_ & _175_);
  assign _176_ = ~(memory[23] & _161_);
  assign _177_ = ~(_028_ & _143_);
  assign _101_ = ~(_176_ & _177_);
  assign _107_ = ~(_122_ & _123_);
  assign _178_ = ~(memory[24] & _119_);
  assign _179_ = ~(_011_ & _118_);
  assign _102_ = ~(_178_ & _179_);
  assign _180_ = ~(memory[25] & _119_);
  assign _181_ = ~(_012_ & _118_);
  assign _103_ = ~(_180_ & _181_);
  assign _182_ = ~(memory[26] & _119_);
  assign _183_ = ~(_013_ & _118_);
  assign _104_ = ~(_182_ & _183_);
  assign _184_ = ~(memory[27] & _119_);
  always @(posedge clk)
    if (_000_) wp[0] <= 1'h0;
    else if (aw) wp[0] <= _001_;
  always @(posedge clk)
    if (_000_) wp[1] <= 1'h0;
    else if (aw) wp[1] <= _002_;
  always @(posedge clk)
    if (_000_) rp[0] <= 1'h0;
    else if (ar) rp[0] <= _043_;
  always @(posedge clk)
    if (_000_) rp[1] <= 1'h0;
    else if (ar) rp[1] <= _044_;
  always @(posedge clk)
    if (_000_) used[0] <= 1'h0;
    else if (_031_) used[0] <= _188_[0];
  always @(posedge clk)
    if (_000_) used[1] <= 1'h0;
    else if (_031_) used[1] <= _189_[1];
  always @(posedge clk)
    if (_000_) response_valid <= 1'h0;
    else response_valid <= ar;
  always @(posedge clk)
    if (_000_) response[0] <= 1'h0;
    else if (ar) response[0] <= _035_;
  always @(posedge clk)
    if (_000_) response[1] <= 1'h0;
    else if (ar) response[1] <= _036_;
  always @(posedge clk)
    if (_000_) response[2] <= 1'h0;
    else if (ar) response[2] <= _037_;
  always @(posedge clk)
    if (_000_) response[3] <= 1'h0;
    else if (ar) response[3] <= _038_;
  always @(posedge clk)
    if (_000_) response[4] <= 1'h0;
    else if (ar) response[4] <= _039_;
  always @(posedge clk)
    if (_000_) response[5] <= 1'h0;
    else if (ar) response[5] <= _040_;
  always @(posedge clk)
    if (_000_) response[6] <= 1'h0;
    else if (ar) response[6] <= _041_;
  always @(posedge clk)
    if (_000_) response[7] <= 1'h0;
    else if (ar) response[7] <= _042_;
  always @(posedge clk)
    if (initialize) memory[0] <= 1'h0;
    else if (_085_) memory[0] <= _086_;
  always @(posedge clk)
    if (initialize) memory[1] <= 1'h0;
    else if (_085_) memory[1] <= _097_;
  always @(posedge clk)
    if (initialize) memory[2] <= 1'h0;
    else if (_085_) memory[2] <= _108_;
  always @(posedge clk)
    if (initialize) memory[3] <= 1'h0;
    else if (_085_) memory[3] <= _111_;
  always @(posedge clk)
    if (initialize) memory[4] <= 1'h0;
    else if (_085_) memory[4] <= _112_;
  always @(posedge clk)
    if (initialize) memory[5] <= 1'h0;
    else if (_085_) memory[5] <= _113_;
  always @(posedge clk)
    if (initialize) memory[6] <= 1'h0;
    else if (_085_) memory[6] <= _114_;
  always @(posedge clk)
    if (initialize) memory[7] <= 1'h0;
    else if (_085_) memory[7] <= _115_;
  always @(posedge clk)
    if (initialize) memory[8] <= 1'h0;
    else if (_085_) memory[8] <= _116_;
  always @(posedge clk)
    if (initialize) memory[9] <= 1'h0;
    else if (_085_) memory[9] <= _117_;
  always @(posedge clk)
    if (initialize) memory[10] <= 1'h0;
    else if (_085_) memory[10] <= _087_;
  always @(posedge clk)
    if (initialize) memory[11] <= 1'h0;
    else if (_085_) memory[11] <= _088_;
  always @(posedge clk)
    if (initialize) memory[12] <= 1'h0;
    else if (_085_) memory[12] <= _089_;
  always @(posedge clk)
    if (initialize) memory[13] <= 1'h0;
    else if (_085_) memory[13] <= _090_;
  always @(posedge clk)
    if (initialize) memory[14] <= 1'h0;
    else if (_085_) memory[14] <= _091_;
  always @(posedge clk)
    if (initialize) memory[15] <= 1'h0;
    else if (_085_) memory[15] <= _092_;
  always @(posedge clk)
    if (initialize) memory[16] <= 1'h0;
    else if (_085_) memory[16] <= _093_;
  always @(posedge clk)
    if (initialize) memory[17] <= 1'h0;
    else if (_085_) memory[17] <= _094_;
  always @(posedge clk)
    if (initialize) memory[18] <= 1'h0;
    else if (_085_) memory[18] <= _095_;
  always @(posedge clk)
    if (initialize) memory[19] <= 1'h0;
    else if (_085_) memory[19] <= _096_;
  always @(posedge clk)
    if (initialize) memory[20] <= 1'h0;
    else if (_085_) memory[20] <= _098_;
  always @(posedge clk)
    if (initialize) memory[21] <= 1'h0;
    else if (_085_) memory[21] <= _099_;
  always @(posedge clk)
    if (initialize) memory[22] <= 1'h0;
    else if (_085_) memory[22] <= _100_;
  always @(posedge clk)
    if (initialize) memory[23] <= 1'h0;
    else if (_085_) memory[23] <= _101_;
  always @(posedge clk)
    if (initialize) memory[24] <= 1'h0;
    else if (_085_) memory[24] <= _102_;
  always @(posedge clk)
    if (initialize) memory[25] <= 1'h0;
    else if (_085_) memory[25] <= _103_;
  always @(posedge clk)
    if (initialize) memory[26] <= 1'h0;
    else if (_085_) memory[26] <= _104_;
  always @(posedge clk)
    if (initialize) memory[27] <= 1'h0;
    else if (_085_) memory[27] <= _105_;
  always @(posedge clk)
    if (initialize) memory[28] <= 1'h0;
    else if (_085_) memory[28] <= _106_;
  always @(posedge clk)
    if (initialize) memory[29] <= 1'h0;
    else if (_085_) memory[29] <= _107_;
  always @(posedge clk)
    if (initialize) memory[30] <= 1'h0;
    else if (_085_) memory[30] <= _109_;
  always @(posedge clk)
    if (initialize) memory[31] <= 1'h0;
    else if (_085_) memory[31] <= _110_;
  assign { _192_[32:5], _192_[3:0] } = { _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _192_[4], _190_[0], 3'h7 };
  assign { _191_[32:5], _191_[3:0] } = { 28'hfffffff, _190_[0], 3'h7 };
  assign _190_[1] = wp[1];
  assign _189_[0] = _188_[0];
  assign read_data = response;
  assign read_valid = response_valid;
endmodule

ConceptWhy can LEC run on a whole chip when property checking cannot?

With matched flops every check is one cone of logic, with no unrolling.It skips the datapath entirely and checks only the control logic.It uses a faster kind of solver than property checking does.The netlist is always far smaller than the RTL it was synthesised from.

ConceptA failed partition's counterexample shows full = 0 and used = 3, where full = (used == 3). What is it?

A real bug that simulation missedA false negative from cut pointsA synthesis bug in the full flagA wrong flop pairing by name

ConceptA team says their gate-level regression passed, so LEC is unnecessary. What is wrong with that?

Nothing: a full regression and LEC prove the same thing.LEC is needed only when the synthesis tool has changed.The regression samples; LEC decides every cone for every value.Gate-level simulation cannot read a Yosys netlist at all.

ConceptWhich change makes combinational LEC report unmatched flops even though the design is correct?

Resizing a cell for timingRenaming an input portInverting one gate inside a coneAdding a pipeline stage

Remember

Equivalence is a safety property on a miter: shared inputs, an XOR per output pair, "never 1".
Combinational LEC pairs flops by name and compares one cone per key point, with no unrolling.
Cut points lose the relations between signals; a counterexample with impossible values is a false negative.
A real difference has a consistent, reachable counterexample. Check that before calling it a bug.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.