Feature request: treat a cell with no Liberty `function` as an uninterpreted function when it appears on both sides, instead of skipping the cone

[ovebryne]

Summary

This is an enhancement request, not a defect — the current behaviour is
sound. When a cell has no function in Liberty, SEC declines to prove the cone
and says exactly why. It is conservative and correctly reported.

It is, however, incomplete in a case that costs us most of our coverage: the
same cell instance on both sides. Its behaviour cannot affect the
comparison, yet the cone is still skipped — so a netlist does not prove
equivalent to itself.

It should not need the cell's behaviour. The same instance drives the same
inputs on both sides, so its outputs are equal by congruence whatever it
computes. Treating it as one shared uninterpreted function is sound and needs no
model from anyone.

Observed on main at 4b6b1bf5cc.

Reproduction

Attached below as a 3 KB archive, and also inline here — two 5-line netlists and
one library, no PDK, seconds to run.

./run.sh /path/to/kepler-formal

Each netlist is compared against itself, so the two runs differ in exactly
one thing — whether the instantiated cell carries a function:

designs/top_opaque.v:

module top(a, y);
  input a;
  output y;
  OPAQUE_BLK u (.a(a), .y(y));
endmodule

designs/top_modelled.v is the same file with MODELLED_BLK substituted, and
blk.lib defines the two cells identically apart from one line:

  cell (OPAQUE_BLK) {
    pin (a) { direction : input; capacitance : 1.0; }
    pin (y) { direction : output; }                      /* no function */
  }
  cell (MODELLED_BLK) {
    pin (a) { direction : input; capacitance : 1.0; }
    pin (y) { direction : output; function : "a"; }      /* <- only difference */
  }

Output:

  opaque        rc=2   coverage: 0.00% (0/1 covered/existing outputs)
      opaque internal cell `u` (model `OPAQUE_BLK`) pin `y[0]`:
      no initialized combinational truth table or usable sequential model
  modelled      rc=0   No binary-defined difference was found

OPAQUE_BLK is shaped like a hardened block's Liberty timing abstract — pins,
no behaviour — which is how an FPU, a memory-compiler macro or third-party IP
arrives in a gate netlist. The same behaviour occurs with real PDK cells; this
stand-in just removes the need to download one.

Why it matters

Any design with a hardened block — an FPU, a memory-compiler macro, externally
supplied IP — ships that block as a Liberty timing abstract: pins, no
function. On our design every gate-side skip traces to exactly one such cell
at a time; removing one only reveals the next.

Because these blocks sit on wide datapaths, a single one of them can cap nearly
every observable output. The behaviour above means that cost is paid even in the
cases where the block provably cannot matter.

Ask

Neither of these is a correctness fix — both trade some of the current
conservatism for coverage, and both are sound.

1. When a cell with no usable model appears on both sides with the same
   interface, treat it as one shared uninterpreted function rather than
   skipping the cone. That alone makes a netlist prove equivalent to itself.

2. A way to request the same abstraction by name, so it also works when the
   two sides describe the block differently — the common case of RTL against a
   synthesised netlist, where design 1 has the block's RTL and design 2 has only
   its Liberty abstract. A pattern form would help, e.g. --blackbox '*_ext'.

One caveat on (2), from having built the wrong version of it. It must be a
shared uninterpreted function, not a free environment input per side: we
prototyped per-side free variables in
#214 and coverage rose
while every answer became a false Difference was found, because the property
being checked degenerates to forall x0, x1. out(x0) == out(x1).

The attached archive contains everything needed to reproduce: both netlists, the
library, a run script, our logs, and the expected output.

repro-opaque-congruence.tar.gz

[ovebryne]

set_as_boundary on main (see #214) gives a working manual route for this:
naming the opaque instance on both sides makes its cone provable, and we
verified it does not mask real differences on either side of the cell.

Two gaps remain against what this issue asked for:

1. It is manual — one pair per instance, rather than the tool treating a cell
   with no function as an uninterpreted function shared by both designs.
2. It requires the instance on both sides, so it does not cover a cell that only
   one design has (our case: a synthesis-inserted clock gate).

Leaving this open for those two points, but the boundary mechanism covers the
part of it we most needed. Close it if you would rather track the remainder
elsewhere.