Sanity check: interpreting synth_xilinx BRAM/LUT/FF counts in a memory-topology comparison

Title: Sanity check: interpreting synth_xilinx BRAM/LUT/FF counts in a memory-topology comparison

Hi,

I’m looking for a narrow Yosys methodology sanity check on PB-HW-04, a small structural comparison of four organizations for fetching four 64-bit evidence records:

  1. one synchronous 1024×64 memory;
  2. four synchronous 256×64 banks;
  3. four replicated 1024×64 memories plus a 16-entry direct-mapped cache;
  4. a ProofBit-labelled wrapper around exactly the same cached core as (3).

The fourth design is intentionally a control: equality with (3) is expected by construction and is not presented as an independent ProofBit advantage.

Each top was synthesized independently with Yosys 0.33:

read_verilog -sv rtl/pb_hw_04.v
hierarchy -check -top <top>
flatten
synth_xilinx -family xc7 -top <top>
ltp -noff
write_json <top>.json

I count mapped top-level LUT1–LUT6, FDRE/FDSE/FDCE/FDPE, RAMB18*, and RAMB36* cells from the JSON output.

The post-fix result was:

Organization RAMB36 LUT FF ltp -noff
Single-port 2 6,966 1,286 36
Four-bank 4 7,645 1,335 59
Conventional cached/replicated 8 10,213 2,148 100
Same cached core, ProofBit wrapper 8 10,213 2,148 100

Icarus simulation also completed 52 checks with 0 failures. The cached designs measured 2 cycles cold and 1 cycle warm; the banked design exposed a 5-cycle same-bank case.

One important history point: an earlier RTL version had multiple syntactic read sites that caused unintended BRAM replication. I rewrote the final version to use explicit synchronous physical read ports and treat only the post-fix run as evidence.

My question is:

Are these memory-inference and resource-accounting choices credible for a narrow structural comparison, or is there a Yosys-specific issue that makes any of the following interpretations misleading?

  • treating the RAMB36 counts as the mapped cost of these inferred memory organizations;
  • comparing LUT/FF counts after flatten and synth_xilinx;
  • comparing ltp -noff values across designs containing synchronous BRAM and cache/control logic, even when described only as a logic-depth proxy.

I am not interpreting ltp as timing, and I am not claiming placed/routed FPGA utilization, board performance, ASIC PPA, power, or a general ProofBit advantage.

Artifacts:

Even a brief pointer to the most important Yosys-specific caveat would be very helpful.

The RAMB36 counts are not a complete representation of the memory cost, as-per Memory handling - YosysHQ Yosys 0.68-dev documentation, additional logic may be added to ensure hardware behavior matches the design (e.g. adding passthrough registers if the design uses a write-before-read pattern but hardware memory is read-before-write), as well as logic necessary for controlling replication and such.

I’m not entirely clear on what you’re actually doing here, but Yosys doesn’t always play nicely with redundancy and may try to duplicates away if it can tell they’re the same. We have a whole blog post about a masters thesis trying to add triple-modular-redundancy with Yosys.