Extend PSL prev with configurable cycle count.

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,

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;

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

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;

test/regress/testlist.txt

@@ -1095,3 +1095,4 @@ issue1125       normal,2008
 issue1137       normal
 tcl3            tcl,fail,gold
 psl18           fail,gold,2008
+psl19           gold,psl

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);

www/features.html.in

@@ -478,7 +478,7 @@ table below.
   <tr>
     <td>5.2.3.1</td>
     <td>prev()</td>
-    <td class="feature-missing"></td>
+    <td class="feature-partial"></td>
   </tr>
   <tr>
     <td>5.2.3.2</td>