Implement PSL prev() built-in function

NEWS.md

@@ -8,6 +8,7 @@
 - The Windows installer now bundles the Tcllib library (#1136).
 - Fixed a bug where PSL directives in comments were parsed incorrectly
   when split over multiple lines (#1135).
+- Added support for PSL `prev()` built-in function (#1135).
 
 ## Version 1.15.0 - 2025-01-11
 - `--load` is now a global option and should be placed before the `-r`

src/lower.c

@@ -121,7 +121,6 @@ typedef vcode_reg_t (*resolved_fn_t)(vcode_reg_t, vcode_reg_t);
 typedef A(concat_param_t) concat_list_t;
 
 static vcode_reg_t lower_expr(lower_unit_t *lu, tree_t expr, expr_ctx_t ctx);
-static vcode_type_t lower_bounds(type_t type);
 static void lower_stmt(lower_unit_t *lu, tree_t stmt, loop_stack_t *loops);
 static void lower_func_body(lower_unit_t *lu, object_t *obj);
 static void lower_proc_body(lower_unit_t *lu, object_t *obj);
@@ -130,7 +129,6 @@ static vcode_reg_t lower_record_aggregate(lower_unit_t *lu, tree_t expr,
                                           vcode_reg_t hint);
 static vcode_reg_t lower_aggregate(lower_unit_t *lu, tree_t expr,
                                    vcode_reg_t hint);
-static vcode_type_t lower_type(type_t type);
 static void lower_decls(lower_unit_t *lu, tree_t scope);
 static void lower_check_array_sizes(lower_unit_t *lu, type_t ltype,
                                     type_t rtype, vcode_reg_t lval,
@@ -634,7 +632,7 @@ static vcode_type_t lower_array_type(type_t type)
       return vtype_uarray(dims_for_type(type), elem_type, elem_bounds);
 }
 
-static vcode_type_t lower_type(type_t type)
+vcode_type_t lower_type(type_t type)
 {
    switch (type_kind(type)) {
    case T_SUBTYPE:
@@ -713,7 +711,7 @@ static vcode_type_t lower_type(type_t type)
    }
 }
 
-static vcode_type_t lower_bounds(type_t type)
+vcode_type_t lower_bounds(type_t type)
 {
    if (type_kind(type) == T_SUBTYPE) {
       if (type_is_integer(type) || type_is_enum(type)) {
@@ -5235,6 +5233,8 @@ static vcode_reg_t lower_expr(lower_unit_t *lu, tree_t expr, expr_ctx_t ctx)
    case T_FCALL:
    case T_PROT_FCALL:
       return lower_fcall(lu, expr, VCODE_INVALID_REG);
+   case T_PSL_FCALL:
+      return psl_lower_fcall(lu, tree_psl(expr));
    case T_LITERAL:
       return lower_literal(expr);
    case T_STRING:

src/lower.h

@@ -21,6 +21,7 @@
 #include "prim.h"
 
 typedef int32_t vcode_reg_t;
+typedef int32_t vcode_type_t;
 
 typedef void (*lower_fn_t)(lower_unit_t *, object_t *);
 typedef vcode_unit_t (*emit_fn_t)(ident_t, object_t *, vcode_unit_t);
@@ -51,6 +52,9 @@ cover_scope_t *lower_get_cover_scope(lower_unit_t *lu);
 vcode_reg_t lower_lvalue(lower_unit_t *lu, tree_t expr);
 vcode_reg_t lower_rvalue(lower_unit_t *lu, tree_t expr);
 
+vcode_type_t lower_type(type_t type);
+vcode_type_t lower_bounds(type_t type);
+
 lower_unit_t *lower_instance(unit_registry_t *ur, lower_unit_t *parent,
                              vcode_unit_t shape, driver_set_t *ds,
                              cover_data_t *cover, tree_t block);

src/psl/psl-lower.c

@@ -1,5 +1,5 @@
 //
-//  Copyright (C) 2023  Nick Gasson
+//  Copyright (C) 2023-2025  Nick Gasson
 //
 //  This program is free software: you can redistribute it and/or modify
 //  it under the terms of the GNU General Public License as published by
@@ -31,6 +31,10 @@
 #include <assert.h>
 #include <stdlib.h>
 
+#define PSL_BLOCK_CASE  1
+#define PSL_BLOCK_ABORT 2
+#define PSL_BLOCK_PREV  3
+
 static void psl_wait_cb(tree_t t, void *ctx)
 {
    lower_unit_t *lu = ctx;
@@ -270,6 +274,57 @@ static vcode_reg_t psl_lower_async_abort(unit_registry_t *ur,
    return emit_function_trigger(name, args, ARRAY_LEN(args));
 }
 
+vcode_reg_t psl_lower_fcall(lower_unit_t *lu, psl_node_t p)
+{
+   assert(psl_kind(p) == P_BUILTIN_FCALL);
+
+   if (psl_subkind(p) != PSL_BUILTIN_PREV)
+      fatal_at(psl_loc(p), "sorry, this built-in function is not supported");
+
+   vcode_state_t state;
+   vcode_state_save(&state);
+
+   vcode_select_block(PSL_BLOCK_PREV);
+
+   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");
+   }
+
+   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_reg_t cur_reg = lower_rvalue(lu, expr);
+
+   const bool is_array = type_is_array(type);
+   if (is_array) {
+      int64_t length;
+      if (!folded_length(range_of(type, 0), &length))
+         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);
+   }
+   else
+      emit_store(cur_reg, var);
+
+   vcode_state_restore(&state);
+
+   if (is_array)
+      return emit_index(var, VCODE_INVALID_REG);
+   else
+      return emit_load(var);
+}
+
 void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent,
                          cover_data_t *cover, tree_t wrapper)
 {
@@ -297,8 +352,13 @@ void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent,
    vcode_type_t vint32 = vtype_int(INT32_MIN, INT32_MAX);
    vcode_reg_t state_reg = emit_param(vint32, vint32, ident_new("state"));
 
-   vcode_block_t case_bb = emit_block();   // Must be block 1
+   vcode_block_t case_bb = emit_block();
    vcode_block_t abort_bb = emit_block();
+   vcode_block_t prev_bb = emit_block();
+
+   assert(case_bb == PSL_BLOCK_CASE);
+   assert(abort_bb == PSL_BLOCK_ABORT);
+   assert(prev_bb == PSL_BLOCK_PREV);
 
    // Only handle a single clock for the whole property
    psl_node_t top = psl_value(p);
@@ -330,22 +390,22 @@ void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent,
    }
 
    emit_add_trigger(trigger_reg);
-
-   emit_return(emit_const(vint32, fsm->next_id));
+   emit_jump(prev_bb);
 
    vcode_select_block(case_bb);
 
    vcode_block_t *state_bb LOCAL =
-      xmalloc_array(fsm->next_id, sizeof(vcode_block_t));
+      xmalloc_array(fsm->next_id + 1, sizeof(vcode_block_t));
    vcode_reg_t *state_ids LOCAL =
-      xmalloc_array(fsm->next_id, sizeof(vcode_reg_t));
+      xmalloc_array(fsm->next_id + 1, sizeof(vcode_reg_t));
 
    for (int i = 0; i < fsm->next_id; i++) {
       state_bb[i] = emit_block();
       state_ids[i] = emit_const(vint32, i);
    }
 
-   emit_case(state_reg, abort_bb, state_ids, state_bb, fsm->next_id);
+   state_bb[fsm->next_id] = prev_bb;
+   state_ids[fsm->next_id] = emit_const(vint32, fsm->next_id);
 
    bool strong = false;
    for (fsm_state_t *s = fsm->states; s; s = s->next) {
@@ -368,6 +428,19 @@ void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent,
    else
       emit_unreachable(VCODE_INVALID_REG);
 
+   vcode_select_block(prev_bb);
+
+   const bool has_prev = vcode_count_ops() > 0;
+
+   emit_return(emit_const(vint32, fsm->next_id + 1));
+
+   vcode_select_block(case_bb);
+
+   if (has_prev)
+      emit_enter_state(fsm->next_id, VCODE_INVALID_REG);
+
+   emit_case(state_reg, abort_bb, state_ids, state_bb, fsm->next_id + 1);
+
    unit_registry_finalise(ur, lu);
 
    psl_fsm_free(fsm);

src/psl/psl-phase.h

@@ -1,5 +1,5 @@
 //
-//  Copyright (C) 2022-2023  Nick Gasson
+//  Copyright (C) 2022-2025  Nick Gasson
 //
 //  This program is free software: you can redistribute it and/or modify
 //  it under the terms of the GNU General Public License as published by
@@ -20,6 +20,8 @@
 
 #include "prim.h"
 
+typedef int32_t vcode_reg_t;
+
 // Check PSL statements for errors.
 void psl_check(psl_node_t p, nametab_t *tab);
 
@@ -34,4 +36,7 @@ void psl_lower_directive(unit_registry_t *ur, lower_unit_t *parent,
 void psl_lower_decl(unit_registry_t *ur, lower_unit_t *parent, psl_node_t p,
                     ident_t name);
 
+// Lower embedded PSL function call
+vcode_reg_t psl_lower_fcall(lower_unit_t *lu, psl_node_t p);
+
 #endif  // _PSL_PHASE_H

src/rt/model.c

@@ -993,6 +993,7 @@ static void reset_property(rt_model_t *m, rt_prop_t *prop)
    mask_init(&prop->newstate, results[1].integer);
 
    mask_set(&prop->state, 0);
+   mask_set(&prop->state, results[1].integer - 1);   // Update prev() variables
 
    thread->active_obj = NULL;
    thread->active_scope = NULL;

test/regress/gold/psl18.txt

@@ -0,0 +1,2 @@
+5ns+1: PSL assertion failed
+7ns+1: PSL assertion failed

test/regress/psl18.vhd

@@ -0,0 +1,42 @@
+entity psl18 is
+end entity;
+
+library ieee;
+use ieee.std_logic_1164.all;
+
+architecture test of psl18 is
+    signal clk : std_logic := '0';
+    signal i : integer := 0;
+    signal x : bit_vector(1 to 3) := "101";
+
+    default clock is rising_edge(clk);
+
+    procedure pulse (signal clk : out std_logic) is
+    begin
+        wait for 1 ns;
+        clk <= '1';
+        wait for 1 ns;
+        clk <= '0';
+    end procedure;
+begin
+
+    one: assert always i = prev(i) + 1;  -- Fails at 7ns
+    two: assert always x = not prev(x);  -- Fails at 5ns
+
+    stim: process is
+    begin
+        i <= i + 1;
+        x <= not x;
+        pulse(clk);
+        x <= not x;
+        i <= i + 1;
+        pulse(clk);
+        i <= i + 1;
+        pulse(clk);                     -- Error
+        x <= not x;
+        pulse(clk);                     -- Error
+
+        wait;
+    end process;
+
+end architecture;

test/regress/testlist.txt

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