Is your feature request related to a problem? Please describe.
Maybe you have following code:

Pipeline : process (clk) is
begin
  if rising_edge(clk) then
    if Wen_i = '1' then
      Data_o <= Data_i;
    end if;
    Wen_o <= Wen_i;
  end if;
end process Pipeline;

If you want to check that Data_o is valid in a write cycle, you need the content of Data_i in the cycle before, for example by using the PSL function prev():

-- psl default clock is rising_edge(clk);

-- psl assert always Wen_o -> Data_o = prev(Data_i);

Describe the solution you'd like
There are various functions defined in the PSL specification which GHDL doesn't implement. For example the prev() function, which returns the value of a signal in the previous cycle (useful in the above example). The stable() function is also very useful to check if signals are stable during a range of clock cycles.

A list of PSL functions in order of usefulness:

Hint: All marked functions are implemented now, but for synthesis only. Useful for formal verification.

Would be really useful:

• prev() (Synthesis)
• stable() (Synthesis)
• ended() (In non VHDL-08 simulation code, PSL endpoint can used instead, see Support to evaluate PSL endpoints in VHDL code #45)

Not so important, can be relatively easy implemented is VHDL functions instead:

• rose() (Synthesis)
• fell() (Synthesis)
• isunknown()
• countones()
• onehot() (Synthesis)
• onehot0() (Synthesis)

Don't know if these functions are useful or valid in the simple subset:

• nondet()
• nondet_vector()
• next()

You can find the functions defined by the PSL standard in the 1850-2005 IEEE Standard for PSL document in section 5.2.3:

Built_In_Function_Call ::=
    prev ( Any_Type [ , Number [ , Clock_Expression ]] )
  | next ( Any_Type )
  | stable ( Any_Type [ , Clock_Expression ] )
  | rose ( Bit [ , Clock_Expression ] )
  | fell ( Bit [ , Clock_Expression ] )
  | ended ( Sequence [ , Clock_Expression ] )
  | isunknown ( BitVector )
  | countones ( BitVector )
  | onehot ( BitVector )
  | onehot0 ( BitVector )
  | nondet ( Value_Set )
  | nondet_vector ( Number, Value_Set )

Describe alternatives you've considered
Some of these function could be emulated by using (a lot of) VHDL code which implement their behaviour.