Static promotion doesn't preserve semantics for shared resource dones on consecutive groups #2349
Open
Description
We found that static promotion doesn't preserve semantics when done signals of shared resources between two sequentially enabled groups are observed.
The below Calyx program has different outputs based on whether static promotion was enabled or not:
import "primitives/core.futil";
import "primitives/memories/comb.futil";
component main(@go go: 1) -> (@done done: 1) {
cells {
@external(1) mem = comb_mem_d1(1, 1, 1);
rr = std_reg(32);
}
wires {
group g1 {
rr.in = 32'd123;
rr.write_en = 1'b1;
g1[done] = rr.done;
}
group g2 {
mem.addr0 = 1'b0;
mem.write_en = 1'b1;
mem.write_data = rr.done;
g2[done] = mem.done;
}
}
control { seq { g1; g2; } }
}
When running with static-promotion.futil.data while enabling static promotion, we get the result
$ fud2 static-promotion.futil --to dat --through verilator -s sim.data=static-promotion.futil.data
{
"cycles": 2,
"memories": {
"mem": [
1
]
}
}
while when we disable static promotion, we get the result
$ fud2 static-promotion.futil --to dat --through verilator -s sim.data=static-promotion.futil.data -s calyx.args="-d static-promotion"
{
"cycles": 4,
"memories": {
"mem": [
0
]
}
}
because there is an extra cycle between g1 and g2, which is when rr.done is 1; rr.done is 0 for the rest of the execution. But in static, there is no such extra cycle because g2 starts on the next cycle after g1.