Stability check is too strict #1732
Description
Currently the stability check requires static ifs to only accept values produced directly by registers. This requirement is fall too strict for many real design, where it is common for guard conditions to be made up for several register results combined together through simple combinational operations (and, not, or, etc). We should figure out a way to modify the stability checks to allow for this use case. I have attached an example calyx file that demonstrates the issue here (as well as an associated data file).
Running this command produces a correct design and data result:
fud e dyn-dot.futil -s verilog.data dot.data --from calyx --to dat --through icarus-verilog -v -s calyx.flags '-d well-formed'
and running this command causes a failure in the well-formed check:
fud e dyn-dot.futil -s verilog.data dot.data --from calyx --to dat --through icarus-verilog -v
dot.futil
import "primitives/core.futil";
import "primitives/pipelined.futil";
import "primitives/stallable.futil";
import "primitives/memories.futil";
extern "ram_1rw.sv" {
primitive ram_1rw[WIDTH, SIZE, IDX_SIZE](addr0: IDX_SIZE, @clk clk: 1, @go(2) @static(1) read_en: 1, write_data: WIDTH, @go @static(1) write_en: 1) -> (@stable read_data: WIDTH, @done(2) read_done: 1, @done write_done: 1);
}
extern "arbiter_2_to_1_rw_dims1.sv" {
primitive arbiter_2_to_1_rw_dims1[WIDTH, PORT0_SIZE, PORT0_IDX_SIZE, PORT1_SIZE, PORT1_IDX_SIZE, PORT2_SIZE, PORT2_IDX_SIZE](@clk clk: 1, @reset reset: 1, port0_addr0: PORT0_IDX_SIZE, @go(2) port0_read_en: 1, port0_write_data: WIDTH, @go port0_write_en: 1, port1_addr0: PORT1_IDX_SIZE, @go(4) port1_read_en: 1, port1_write_data: WIDTH, @go(3) port1_write_en: 1, port2_read_data: WIDTH, port2_read_done: 1, port2_write_done: 1) -> (@stable port0_read_data: WIDTH, @done(2) port0_read_done: 1, @done port0_write_done: 1, @stable port1_read_data: WIDTH, @done(4) port1_read_done: 1, @done(3) port1_write_done: 1, port2_addr0: PORT2_IDX_SIZE, port2_read_en: 1, port2_write_data: WIDTH, port2_write_en: 1);
}
component mem_0_comp(@clk clk: 1, port0_addr0: 4, @go(2) port0_read_en: 1, port0_write_data: 32, @go port0_write_en: 1, port1_addr0: 4, @go(4) port1_read_en: 1, port1_write_data: 32, @go(3) port1_write_en: 1, @reset reset: 1) -> (@stable port0_read_data: 32, @done(2) port0_read_done: 1, @done port0_write_done: 1, @stable port1_read_data: 32, @done(4) port1_read_done: 1, @done(3) port1_write_done: 1, @stable no_stall: 1) {
cells {
arbiter_2_to_1_rw_dims1_inst0 = arbiter_2_to_1_rw_dims1(32, 10, 4, 10, 4, 10, 4);
mem_0_comp_bank_0 = ram_1rw(32, 10, 4);
stall_reg = std_reg(1);
and0 = std_and(1);
not0 = std_not(1);
}
wires {
arbiter_2_to_1_rw_dims1_inst0.clk = clk;
mem_0_comp_bank_0.clk = clk;
arbiter_2_to_1_rw_dims1_inst0.port0_write_data = port0_write_data;
arbiter_2_to_1_rw_dims1_inst0.port0_write_en = port0_write_en;
port0_write_done = arbiter_2_to_1_rw_dims1_inst0.port0_write_done;
port0_read_data = arbiter_2_to_1_rw_dims1_inst0.port0_read_data;
arbiter_2_to_1_rw_dims1_inst0.port0_read_en = port0_read_en;
port0_read_done = arbiter_2_to_1_rw_dims1_inst0.port0_read_done;
arbiter_2_to_1_rw_dims1_inst0.port0_addr0 = port0_addr0;
arbiter_2_to_1_rw_dims1_inst0.port1_write_data = port1_write_data;
arbiter_2_to_1_rw_dims1_inst0.port1_write_en = port1_write_en;
port1_write_done = arbiter_2_to_1_rw_dims1_inst0.port1_write_done;
port1_read_data = arbiter_2_to_1_rw_dims1_inst0.port1_read_data;
arbiter_2_to_1_rw_dims1_inst0.port1_read_en = port1_read_en;
port1_read_done = arbiter_2_to_1_rw_dims1_inst0.port1_read_done;
arbiter_2_to_1_rw_dims1_inst0.port1_addr0 = port1_addr0;
mem_0_comp_bank_0.write_data = arbiter_2_to_1_rw_dims1_inst0.port2_write_data;
mem_0_comp_bank_0.write_en = arbiter_2_to_1_rw_dims1_inst0.port2_write_en;
arbiter_2_to_1_rw_dims1_inst0.port2_write_done = mem_0_comp_bank_0.write_done;
arbiter_2_to_1_rw_dims1_inst0.port2_read_data = mem_0_comp_bank_0.read_data;
mem_0_comp_bank_0.read_en = arbiter_2_to_1_rw_dims1_inst0.port2_read_en;
arbiter_2_to_1_rw_dims1_inst0.port2_read_done = mem_0_comp_bank_0.read_done;
mem_0_comp_bank_0.addr0 = arbiter_2_to_1_rw_dims1_inst0.port2_addr0;
and0.left = port0_read_en;
and0.right = port1_read_en;
not0.in = and0.out;
stall_reg.in = not0.out;
stall_reg.write_en = 1'd1;
no_stall = stall_reg.out;
}
control {
}
}
component dot<"toplevel"=1>(@clk clk: 1, @reset reset: 1, @go go: 1) -> (@done done: 1) {
cells {
std_slice_8 = std_slice(32, 4);
std_slice_7 = std_slice(32, 4);
std_slice_6 = std_slice(32, 4);
std_slice_5 = std_slice(32, 4);
std_slice_4 = std_slice(32, 4);
std_slice_3 = std_slice(32, 4);
std_slice_2 = std_slice(32, 4);
std_slice_1 = std_slice(32, 4);
std_slice_0 = std_slice(32, 1);
std_and_1 = std_and(1);
guard_reg_5_reg = std_reg(1);
std_ge_1 = std_ge(32);
std_lt_7 = std_lt(32);
std_and_0 = std_and(1);
guard_reg_4_reg = std_reg(1);
std_ge_0 = std_ge(32);
std_lt_6 = std_lt(32);
guard_reg_3_reg = std_reg(1);
std_lt_5 = std_lt(32);
guard_reg_2_reg = std_reg(1);
std_lt_4 = std_lt(32);
guard_reg_1_reg = std_reg(1);
std_lt_3 = std_lt(32);
guard_reg_0_reg = std_reg(1);
std_lt_2 = std_lt(32);
loop_1_stage_2_register_0_reg = std_reg(32);
loop_0_stage_0_register_2_reg = std_reg(32);
std_add_5 = std_add(32);
idx_1_reg = std_reg(32);
loop_1_arg1_reg = std_reg(32);
loop_1_arg0_reg = std_reg(32);
std_add_4 = std_add(32);
std_add_3 = std_add(32);
pipelined_mult_1 = pipe_stall_mult(32);
pipelined_mult_0 = pipe_stall_mult(32);
std_add_2 = std_add(32);
std_lt_1 = std_lt(32);
std_add_1 = std_add(32);
idx_0_reg = std_reg(32);
loop_0_arg0_reg = std_reg(32);
std_add_0 = std_add(32);
std_lt_0 = std_lt(32);
std_lt_8 = std_lt(32);
cond_reg_0 = std_reg(1);
no_stall = std_and(1);
stall = std_not(1);
b = mem_0_comp();
a = mem_0_comp();
@external(1) ext_mem_0 = seq_mem_d1(32, 10, 4);
@external(1) ext_mem_1 = seq_mem_d1(32, 10, 4);
@external(1) ext_mem_2 = seq_mem_d1(32, 1, 1);
}
wires {
no_stall.left = a.no_stall;
no_stall.right = b.no_stall;
a.port1_write_en = 1'd0;
b.port1_write_en = 1'd0;
stall.in = no_stall.out;
pipelined_mult_0.stall = stall.out;
pipelined_mult_1.stall = stall.out;
static<1> group load_0 {
std_slice_8.in = loop_0_arg0_reg.out;
ext_mem_0.addr0 = std_slice_8.out;
ext_mem_0.read_en = 1'd1;
}
static<1> group load_1 {
std_slice_7.in = loop_0_arg0_reg.out;
ext_mem_1.addr0 = std_slice_7.out;
ext_mem_1.read_en = 1'd1;
}
static<1> group store_0 {
std_slice_6.in = loop_0_stage_0_register_2_reg.out;
a.port0_addr0 = std_slice_6.out;
a.port0_write_data = ext_mem_0.read_data;
a.port0_write_en = 1'd1;
}
static<1> group store_1 {
std_slice_5.in = loop_0_stage_0_register_2_reg.out;
b.port0_addr0 = std_slice_5.out;
b.port0_write_data = ext_mem_1.read_data;
b.port0_write_en = 1'd1;
}
static<1> group assign_loop_0_init_0 {
loop_0_arg0_reg.in = 32'd0;
loop_0_arg0_reg.write_en = 1'd1;
}
static<1> group incr_0 {
std_add_1.left = idx_0_reg.out;
std_add_1.right = 32'd1;
idx_0_reg.in = std_add_1.out;
idx_0_reg.write_en = 1'd1;
std_lt_2.left = std_add_1.out;
std_lt_2.right = 32'd10;
guard_reg_0_reg.in = std_lt_2.out;
guard_reg_0_reg.write_en = 1'd1;
std_lt_3.left = std_add_1.out;
std_lt_3.right = 32'd11;
guard_reg_1_reg.in = std_lt_3.out;
guard_reg_1_reg.write_en = 1'd1;
}
static<1> group incr_init_0 {
idx_0_reg.in = 32'd0;
idx_0_reg.write_en = 1'd1;
}
static<1> group load_2 {
std_slice_4.in = loop_1_arg0_reg.out;
a.port0_addr0 = std_slice_4.out;
a.port0_read_en = 1'd1;
}
static<1> group load_3 {
std_slice_3.in = loop_1_arg0_reg.out;
b.port0_addr0 = std_slice_3.out;
b.port0_read_en = 1'd1;
}
static<1> group load_4 {
std_slice_2.in = loop_1_arg0_reg.out;
a.port1_addr0 = std_slice_2.out;
a.port1_read_en = 1'd1;
}
static<1> group load_5 {
std_slice_1.in = loop_1_arg0_reg.out;
b.port1_addr0 = std_slice_1.out;
b.port1_read_en = 1'd1;
}
static<1> group muli_0 {
pipelined_mult_0.left = a.port0_read_data;
pipelined_mult_0.right = b.port0_read_data;
}
static<1> group muli_1 {
pipelined_mult_1.left = a.port1_read_data;
pipelined_mult_1.right = b.port1_read_data;
}
static<1> group assign_loop_1_init_0 {
loop_1_arg0_reg.in = 32'd0;
loop_1_arg0_reg.write_en = 1'd1;
}
static<1> group assign_loop_1_init_1 {
loop_1_arg1_reg.in = 32'd0;
loop_1_arg1_reg.write_en = 1'd1;
}
static<1> group incr_1 {
std_add_5.left = idx_1_reg.out;
std_add_5.right = 32'd1;
idx_1_reg.in = std_add_5.out;
idx_1_reg.write_en = 1'd1;
std_lt_4.left = std_add_5.out;
std_lt_4.right = 32'd10;
guard_reg_2_reg.in = std_lt_4.out;
guard_reg_2_reg.write_en = 1'd1;
std_lt_5.left = std_add_5.out;
std_lt_5.right = 32'd11;
guard_reg_3_reg.in = std_lt_5.out;
guard_reg_3_reg.write_en = 1'd1;
std_lt_6.left = std_add_5.out;
std_lt_6.right = 32'd15;
std_ge_0.left = std_add_5.out;
std_ge_0.right = 32'd5;
std_and_0.left = std_ge_0.out;
std_and_0.right = std_lt_6.out;
guard_reg_4_reg.in = std_and_0.out;
guard_reg_4_reg.write_en = 1'd1;
std_lt_7.left = std_add_5.out;
std_lt_7.right = 32'd16;
std_ge_1.left = std_add_5.out;
std_ge_1.right = 32'd6;
std_and_1.left = std_ge_1.out;
std_and_1.right = std_lt_7.out;
guard_reg_5_reg.in = std_and_1.out;
guard_reg_5_reg.write_en = 1'd1;
std_lt_8.left = idx_1_reg.out;
std_lt_8.right = 32'd16;
cond_reg_0.in = std_lt_8.out;
cond_reg_0.write_en = 1'd1;
}
static<1> group incr_init_1 {
idx_1_reg.in = 32'd0;
idx_1_reg.write_en = 1'd1;
cond_reg_0.in = 1'd1;
cond_reg_0.write_en = 1'd1;
}
static<1> group store_2 {
std_slice_0.in = 32'd0;
ext_mem_2.addr0 = std_slice_0.out;
ext_mem_2.write_data = loop_1_arg1_reg.out;
ext_mem_2.write_en = 1'd1;
}
static<1> group guard_init_0 {
guard_reg_0_reg.in = 1'd1;
guard_reg_0_reg.write_en = 1'd1;
}
static<1> group phase_reg_3 {
loop_0_stage_0_register_2_reg.in = loop_0_arg0_reg.out;
loop_0_stage_0_register_2_reg.write_en = 1'd1;
}
static<1> group phase_reg_4 {
loop_0_arg0_reg.in = std_add_0.out;
loop_0_arg0_reg.write_en = 1'd1;
std_add_0.left = loop_0_arg0_reg.out;
std_add_0.right = 32'd1;
}
static<1> group guard_init_1 {
guard_reg_1_reg.in = 1'd0;
guard_reg_1_reg.write_en = 1'd1;
}
static<1> group guard_init_2 {
guard_reg_2_reg.in = 1'd1;
guard_reg_2_reg.write_en = 1'd1;
}
static<1> group phase_reg_9 {
loop_1_arg0_reg.in = std_add_2.out;
loop_1_arg0_reg.write_en = 1'd1;
std_add_2.left = loop_1_arg0_reg.out;
std_add_2.right = 32'd1;
}
static<1> group guard_init_3 {
guard_reg_3_reg.in = 1'd0;
guard_reg_3_reg.write_en = 1'd1;
}
static<1> group guard_init_4 {
guard_reg_4_reg.in = 1'd0;
guard_reg_4_reg.write_en = 1'd1;
}
static<1> group phase_reg_12 {
loop_1_stage_2_register_0_reg.in = std_add_3.out;
loop_1_stage_2_register_0_reg.write_en = 1'd1;
std_add_3.left = pipelined_mult_0.out;
std_add_3.right = pipelined_mult_1.out;
}
static<1> group guard_init_5 {
guard_reg_5_reg.in = 1'd0;
guard_reg_5_reg.write_en = 1'd1;
}
static<1> group phase_reg_13 {
loop_1_arg1_reg.in = std_add_4.out;
loop_1_arg1_reg.write_en = 1'd1;
std_add_4.left = loop_1_arg1_reg.out;
std_add_4.right = loop_1_stage_2_register_0_reg.out;
}
}
control {
seq {
static par {
assign_loop_0_init_0;
incr_init_0;
guard_init_0;
guard_init_1;
}
static repeat 11 {
static par {
incr_0;
static if guard_reg_0_reg.out {
static par {
load_0;
load_1;
phase_reg_3;
phase_reg_4;
}
}
static if guard_reg_1_reg.out {
static par {
store_0;
store_1;
}
}
}
}
static par {
assign_loop_1_init_0;
assign_loop_1_init_1;
incr_init_1;
guard_init_2;
guard_init_3;
guard_init_4;
guard_init_5;
}
while cond_reg_0.out {
static if no_stall.out {
static par {
incr_1;
static if guard_reg_2_reg.out {
static par {
load_2;
load_3;
load_4;
load_5;
phase_reg_9;
}
}
static if guard_reg_3_reg.out {
static par {
muli_0;
muli_1;
}
}
static if guard_reg_4_reg.out {
phase_reg_12;
}
static if guard_reg_5_reg.out {
phase_reg_13;
}
}
}
}
store_2;
}
}
}
dot.data
{
"ext_mem_0": {
"data": [
1,
2,
3,
4,
5,
6,
7,
8,
9,
10
],
"format": {
"numeric_type": "bitnum",
"is_signed": false,
"width": 32
}
},
"ext_mem_1": {
"data": [
1,
1,
1,
1,
1,
1,
1,
1,
1,
1
],
"format": {
"numeric_type": "bitnum",
"is_signed": false,
"width": 32
}
},
"ext_mem_2": {
"data": [
0
],
"format": {
"numeric_type": "bitnum",
"is_signed": false,
"width": 32
}
}
}