From 721add5b428dcec2b7d84b2d651c28cff5ef72b7 Mon Sep 17 00:00:00 2001 From: Ondrej Ille Date: Sun, 19 Jan 2025 20:56:23 +0100 Subject: [PATCH 1/2] Extend PSL prev with configurable cycle count. --- src/psl/psl-lower.c | 41 ++++++++++++++++++--------- test/psl/sem2.vhd | 1 + test/regress/gold/psl19.txt | 5 ++++ test/regress/psl19.vhd | 55 +++++++++++++++++++++++++++++++++++++ test/regress/testlist.txt | 1 + test/test_psl.c | 1 + www/features.html.in | 2 +- 7 files changed, 92 insertions(+), 14 deletions(-) create mode 100644 test/regress/gold/psl19.txt create mode 100644 test/regress/psl19.vhd diff --git a/src/psl/psl-lower.c b/src/psl/psl-lower.c index eb08f8378..d4900a107 100644 --- a/src/psl/psl-lower.c +++ b/src/psl/psl-lower.c @@ -289,19 +289,19 @@ vcode_reg_t psl_lower_fcall(lower_unit_t *lu, psl_node_t p) tree_t expr = psl_tree(psl_operand(p, 0)); type_t type = tree_type(expr); - if (psl_operands(p) > 1) { - const int num = assume_int(psl_tree(psl_operand(p, 1))); - if (num != 1) - fatal_at(psl_loc(p), "sorry, cycle counts other than 1 are " - "not supported"); - } + int num = 1; + if (psl_operands(p) > 1) + num = assume_int(psl_tree(psl_operand(p, 1))); vcode_type_t vtype = lower_type(type); vcode_type_t vbounds = lower_bounds(type); - vcode_var_t var = emit_var(vtype, vbounds, ident_uniq("prev"), 0); + vcode_var_t vars[num]; + for (int i = 0; i < num; i++) + vars[i] = emit_var(vtype, vbounds, ident_uniq("prev"), 0); vcode_reg_t cur_reg = lower_rvalue(lu, expr); + vcode_reg_t count_reg = VCODE_INVALID_REG; const bool is_array = type_is_array(type); if (is_array) { @@ -310,19 +310,34 @@ vcode_reg_t psl_lower_fcall(lower_unit_t *lu, psl_node_t p) fatal_at(psl_loc(p), "sorry, only constant length arrays " "are supported"); - vcode_reg_t dst_reg = emit_index(var, VCODE_INVALID_REG); - vcode_reg_t count_reg = emit_const(vtype_offset(), length); - emit_copy(dst_reg, cur_reg, count_reg); + count_reg = emit_const(vtype_offset(), length); + } + + for (int i = 0; i < num - 1; i++) { + if (is_array) { + vcode_reg_t src_ptr = emit_index(vars[i + 1], VCODE_INVALID_REG); + vcode_reg_t dst_ptr = emit_index(vars[i], VCODE_INVALID_REG); + emit_copy(dst_ptr, src_ptr, count_reg); + } + else { + vcode_reg_t tmp = emit_load(vars[i + 1]); + emit_store(tmp, vars[i]); + } + } + + if (is_array) { + vcode_reg_t dst_ptr = emit_index(vars[num - 1], VCODE_INVALID_REG); + emit_copy(dst_ptr, cur_reg, count_reg); } else - emit_store(cur_reg, var); + emit_store(cur_reg, vars[num - 1]); vcode_state_restore(&state); if (is_array) - return emit_index(var, VCODE_INVALID_REG); + return emit_index(vars[0], VCODE_INVALID_REG); else - return emit_load(var); + return emit_load(vars[0]); } void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent, diff --git a/test/psl/sem2.vhd b/test/psl/sem2.vhd index f7a46a015..c68b9136c 100644 --- a/test/psl/sem2.vhd +++ b/test/psl/sem2.vhd @@ -13,5 +13,6 @@ begin -- psl assert rose(i); -- Error -- psl assert rose(x); -- OK -- psl assert ended({x;y}); -- OK + -- psl cover prev(x, i); -- Error end architecture; diff --git a/test/regress/gold/psl19.txt b/test/regress/gold/psl19.txt new file mode 100644 index 000000000..a5c0598fd --- /dev/null +++ b/test/regress/gold/psl19.txt @@ -0,0 +1,5 @@ +** Note: 2ns+1: one +** Note: 3ns+1: one +** Note: 4ns+1: two +** Note: 6ns+1: three +** Note: 7ns+1: four \ No newline at end of file diff --git a/test/regress/psl19.vhd b/test/regress/psl19.vhd new file mode 100644 index 000000000..457fd7a3a --- /dev/null +++ b/test/regress/psl19.vhd @@ -0,0 +1,55 @@ +entity psl19 is +end entity; + +architecture tb of psl19 is + + signal clk : natural; + signal a,b,c : bit; + signal v : bit_vector(15 downto 0); + + constant seq_a : bit_vector := "01110000"; + constant seq_b : bit_vector := "01101000"; + constant seq_c : bit_vector := "01000010"; + + type t_matrix is array (0 to 7) of bit_vector(15 downto 0); + constant seq_v : t_matrix := + ( + (x"0000"), + (x"0000"), + (x"0000"), + (x"EEEE"), + (x"DDDD"), + (x"CCCC"), + (x"BBBB"), + (x"AAAA") + ); + +begin + + clkgen: clk <= clk + 1 after 1 ns when clk < 7; + + agen: a <= seq_a(clk); + bgen: b <= seq_b(clk); + cgen: c <= seq_c(clk); + + vgen: v <= seq_v(clk); + + -- psl default clock is clk'delayed(0 ns)'event; + + -- Covered at 2 ns and 3 ns + -- psl one: cover {a and prev(a)} report "one"; + + -- Covered at 4 ns + -- psl two: cover {b and prev(b,2)} report "two"; + + -- Covered at 6 ns + -- psl three: cover {c and prev(c,5)} report "three"; + + -- Covered at 7 ns + -- psl four: cover { v = x"AAAA" and + -- prev(v ) = x"BBBB" and + -- prev(v,2) = x"CCCC" and + -- prev(v,3) = x"DDDD" and + -- prev(v,4) = x"EEEE"} report "four"; + +end architecture; diff --git a/test/regress/testlist.txt b/test/regress/testlist.txt index ec404e672..611364577 100644 --- a/test/regress/testlist.txt +++ b/test/regress/testlist.txt @@ -1095,3 +1095,4 @@ issue1125 normal,2008 issue1137 normal tcl3 tcl,fail,gold psl18 fail,gold,2008 +psl19 gold,psl diff --git a/test/test_psl.c b/test/test_psl.c index 6f4f956b8..0c6db5f3e 100644 --- a/test/test_psl.c +++ b/test/test_psl.c @@ -388,6 +388,7 @@ START_TEST(test_sem2) const error_t expect[] = { { 13, "expression must be a PSL Bit but have type INTEGER" }, + { 16, "expression must be static" }, { -1, NULL } }; expect_errors(expect); diff --git a/www/features.html.in b/www/features.html.in index d7f8569ec..c9fb15ffa 100644 --- a/www/features.html.in +++ b/www/features.html.in @@ -478,7 +478,7 @@ table below. 5.2.3.1 prev() - + 5.2.3.2 From 17ed3d7b4bc9776dc5ff25a884b6bb22e60861cb Mon Sep 17 00:00:00 2001 From: "ondrej.ille" Date: Mon, 20 Jan 2025 08:53:27 +0100 Subject: [PATCH 2/2] allocate var array dynamically rather than on stack. --- src/psl/psl-lower.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/psl/psl-lower.c b/src/psl/psl-lower.c index d4900a107..e5bed1914 100644 --- a/src/psl/psl-lower.c +++ b/src/psl/psl-lower.c @@ -293,10 +293,13 @@ vcode_reg_t psl_lower_fcall(lower_unit_t *lu, psl_node_t p) if (psl_operands(p) > 1) num = assume_int(psl_tree(psl_operand(p, 1))); + if (num > 512) + fatal_at(psl_loc(p), "sorry, Number higher than 512 is not supported"); + vcode_type_t vtype = lower_type(type); vcode_type_t vbounds = lower_bounds(type); - vcode_var_t vars[num]; + vcode_var_t *vars LOCAL = xmalloc_array(num, sizeof(vcode_var_t)); for (int i = 0; i < num; i++) vars[i] = emit_var(vtype, vbounds, ident_uniq("prev"), 0);