The question

Two details decide whether a RAM behaves in silicon the way it simulated. The write mask selects which lanes change, so a partial-word write becomes one masked access instead of a read-modify-write around it. Read-during-write decides what a read of the just-written address returns: a synchronous read is one cycle late, so without a bypass path the data is stale. This lesson records both on three 8-entry 16-bit forms: a plain whole-word write, a per-byte split enable, and a bypass that forwards write data when the addresses match. Every form runs the same flow with the same assertions: one memory cell after collection, none after mapping.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

read_verilog <<VERILOG
module plain16 (input clk, input we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output reg [15:0] rdata);
  reg [15:0] mem [0:7];
  always @(posedge clk) begin
    if (we) mem[waddr] <= wdata;
    rdata <= mem[raddr];
  end
endmodule
VERILOG
hierarchy -check -top plain16
proc
memory -nomap
select -assert-count 1 t:$mem*
tee -o dump_plain.txt dump
memory_map
select -assert-none t:$mem*
tee -o gen_plain.txt stat
techmap
opt
dfflibmap -liberty course.lib
tee -o abc_plain.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_plain.txt stat -liberty course.lib
design -reset
read_verilog <<VERILOG
module be16 (input clk, input [1:0] we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output reg [15:0] rdata);
  reg [15:0] mem [0:7];
  always @(posedge clk) begin
    if (we[0]) mem[waddr][7:0] <= wdata[7:0];
    if (we[1]) mem[waddr][15:8] <= wdata[15:8];
    rdata <= mem[raddr];
  end
endmodule
VERILOG
hierarchy -check -top be16
proc
memory -nomap
select -assert-count 1 t:$mem*
tee -o dump_be.txt dump
memory_map
select -assert-none t:$mem*
tee -o gen_be.txt stat
techmap
opt
dfflibmap -liberty course.lib
tee -o abc_be.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_be.txt stat -liberty course.lib
design -reset
read_verilog <<VERILOG
module bypass16 (input clk, input we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output reg [15:0] rdata);
  reg [15:0] mem [0:7];
  always @(posedge clk) begin
    if (we) mem[waddr] <= wdata;
    if (we && (waddr == raddr)) rdata <= wdata;
    else rdata <= mem[raddr];
  end
endmodule
VERILOG
hierarchy -check -top bypass16
proc
memory -nomap
select -assert-count 1 t:$mem*
tee -o dump_bypass.txt dump
memory_map
select -assert-none t:$mem*
tee -o gen_bypass.txt stat
techmap
opt
dfflibmap -liberty course.lib
tee -o abc_bypass.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_bypass.txt stat -liberty course.lib
log PASS: plain byte-enabled and bypass forms collect and map with recorded counts

All three collect to a single $mem_v2 cell with WIDTH 16 and SIZE 8, so masked writes and forwarding still infer one memory. The differences sit in the write enables and the transparency mask, listed next to the mapped cost below.

Write masks per byte

Read the write side first. In $mem_v2, WR_EN is always WIDTH bits wide, so count distinct enable signals, not bits: the plain dump drives all 16 WR_EN bits from 1 shared signal, one enable fanned out across the whole word. The byte-enabled dump drives WR_EN from 16 distinct signals, one per data bit, with the byte selects steering which lanes take new data. That steering is the structural price of masking: the generic cells move from 293 to 326 and the muxes from 138 to 155, while the word flops stay put at 9. No read-modify-write is needed, because the mask does the keeping lane by lane inside one write.

Generic counts are pre-techmap while chip area is post-mapping, so the two can move in opposite directions. The byte-enabled steering absorbs into the same mapped skeleton, 144 DFFs and 240 MUX2s in both, with a cheaper surrounding gate mix: 424 mapped cells against 436, and area 2437 against 2476. More generic cells yet slightly less area is normal here: the pre-map count prices structure, the mapped total prices gates.

A macro without a per-byte mask cannot do this natively. Around such a macro the wrapper performs the avoided read-modify-write: read the word, merge the new bytes, write it back, costing an extra read cycle plus merge muxes. How enables map decides the wrapper: per-bit enables absorb the mask, a whole-word enable pushes the merge into the wrapper or the cycle budget.

Read during write and the transparency mask

The read side tells the second half. The plain and byte-enabled forms record RD_TRANSPARENCY_MASK 1'0: a same-cycle same-address read returns the previous contents, with RD_COLLISION_X_MASK 1'0 marking no undefined bits. The bypass form records 1'1: the tool recognised the forwarding and folded it into the port semantics. The counts confirm it: 293 generic cells with 138 muxes, indistinguishable from plain, because the forwarding became a port attribute instead of extra gates. The dump backs that reading: the bypass port keeps RD_CLK connected with RD_CLK_ENABLE 1'1 while only the transparency mask flips, so the forwarding lives in the clocked port's semantics with no added generic cells.

The area still drops to 2371 against 2476 from an identical generic structure: with transparency recorded, the mapped netlist holds 131 DFFs against 144 DFFs for plain, so identical pre-map counts map to different areas. Judge structure from generic counts and cost from mapped area, never one from the other.

That folding is an inference convenience, not a macro property. A macro without transparency still returns stale data on a collision, so around it the wrapper rebuilds in silicon what the tool folded away: a comparator, a write gate, and a forwarding mux. The calc block prices that wrapper from teaching-library areas, hand-derived and labelled so.

hand-derived wrapper estimate, not a recording (course.lib teaching areas: XNOR2 = 5, AND2 = 3, MUX2 = 5)
3-bit address compare: 3 x XNOR2 + 2 x AND2 = 3 x 5 + 2 x 3 = 21 units
write gate (we AND match): 1 x AND2 = 3 units
16-bit 2:1 forwarding mux: 16 x MUX2 = 80 units
wrapper total = 21 + 3 + 80 = 104 units

The wrapper costs about a hundred units against a memory of a few thousand: cheap insurance, and exactly the logic a missing transparency forces every design around that macro to carry. Skipping it corrupts every read-after-write, which is why the proof below checks behaviour, not structure.

Proving the bypass with sat

The second script builds a clocked miter: the plain read-old RAM and the bypass RAM side by side on the same inputs, with the previous cycle's write, addresses, and data delayed into registers. Two properties cover write-first behaviour: the outputs agree in every cycle except after a same-address collision, and after a collision the bypass output equals the colliding write data. Each runs as its own sat -prove with four sequential steps from a zeroed initial state, and -verify turns any counterexample into a run failure.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

read_verilog <<VERILOG
module plain16 (input clk, input we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output reg [15:0] rdata);
  reg [15:0] mem [0:7];
  always @(posedge clk) begin
    if (we) mem[waddr] <= wdata;
    rdata <= mem[raddr];
  end
endmodule
module bypass16 (input clk, input we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output reg [15:0] rdata);
  reg [15:0] mem [0:7];
  always @(posedge clk) begin
    if (we) mem[waddr] <= wdata;
    if (we && (waddr == raddr)) rdata <= wdata;
    else rdata <= mem[raddr];
  end
endmodule
module miter (input clk, input we, input [2:0] waddr, input [2:0] raddr, input [15:0] wdata, output ok, output ok2);
  wire [15:0] ro_old, ro_new;
  plain16 a (.clk(clk), .we(we), .waddr(waddr), .raddr(raddr), .wdata(wdata), .rdata(ro_old));
  bypass16 b (.clk(clk), .we(we), .waddr(waddr), .raddr(raddr), .wdata(wdata), .rdata(ro_new));
  reg p_we;
  reg [2:0] p_waddr, p_raddr;
  reg [15:0] p_wdata;
  always @(posedge clk) begin
    p_we <= we; p_waddr <= waddr; p_raddr <= raddr; p_wdata <= wdata;
  end
  wire coll = p_we && (p_waddr == p_raddr);
  assign ok = ((ro_old == ro_new) || coll);
  assign ok2 = (!coll || (ro_new == p_wdata));
endmodule
VERILOG
hierarchy -check -top miter
proc
memory
opt_clean
flatten
tee -o sat_ok.txt sat -prove ok 1 -seq 4 -verify -set-init-zero
tee -o sat_ok2.txt sat -prove ok2 1 -seq 4 -verify -set-init-zero
log PASS: bypass wrapper matches write-first behavior on collision cycles

Both proofs hold: the first sat file records 1 SUCCESS line and the second records 1 SUCCESS line, each reading "SAT proof finished - no model found: SUCCESS!". No model means no counterexample in four steps from reset: the bypass matches the plain RAM everywhere except after a collision, and after a collision it carries exactly the write data. That is write-first behaviour at the output, proved for every pattern the solver could try.

Break it: add the bypass

The third form in the first script is the break-it: the same whole-word memory with the forwarding branch added and nothing else changed. The mask flips from 1'0 to 1'1 while the generic structure is unchanged from plain. The macro lesson is the contrapositive: with no transparency to absorb the forwarding, the same behaviour costs the hundred-odd wrapper units from the calc block on every instance.

Common mistakes

Related topics

• Next: Compilers, Macros and Wrappers

• Register files

• Retiming and Pipelining