Update prev() & stable() examples after ghdl/ghdl#1366 & ghdl/ghdl#1367 were fixed

issues/issue_1366.vhd

@@ -1,29 +1,33 @@
 vunit issue_vunit (issue(psl)) {
-  
+
   -- VHDL declaration seem to be working
-  signal a_delayed : std_logic := '0';
+  signal a_delayed  : std_logic := '0';
+  signal prev_valid : boolean   := false;
 
   -- Other VHDL code not
   -- results in parser errors
   -- during synthesis
+  -- EDIT: works since fix of ghdl issue #1366
   process is
   begin
     wait until rising_edge(clk);
     a_delayed <= a;
-  end process;  
+    prev_valid <= true;
+  end process;
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
   -- This assertion holds
-  CHECK_a : assert always (a -> b);
+  CHECK_0_a : assert always (a -> b);
 
   -- You can't do anything with the declared signal
   -- Can be synthesized with GHDL, however
   -- results in error in ghdl-yosys-plugin:
   -- ERROR: Assert `n.id != 0' failed in src/ghdl.cc:172
-  assert always a_delayed = prev(a);
+  -- EDIT: works since fix of ghdl issue #1366
+  CHECK_1_a : assert always prev_valid -> a_delayed = prev(a);
 
 }
 

issues/issue_1367.vhd

@@ -83,10 +83,17 @@ architecture psl of issue is
   end component hex_sequencer;
 
   signal a, b : std_logic_vector(3 downto 0);
+  signal prev_valid : boolean := false;
 
 begin
 
 
+  process is
+  begin
+    wait until rising_edge(clk);
+    prev_valid <= true;
+  end process;
+
   --                                  0123456789
   SEQ_A : hex_sequencer generic map ("4444444444") port map (clk, a);
   SEQ_B : hex_sequencer generic map ("4444544444") port map (clk, b);
@@ -96,24 +103,36 @@ begin
   default clock is rising_edge(clk);
 
   -- Holds
-  STABLE_0 : assert always stable(a);
+  STABLE_0 : assert always prev_valid -> stable(a);
 
   -- Doesn't hold at cycle 4
-  STABLE_1 : assert always stable(b);
+  STABLE_1 : assert always prev_valid -> stable(b);
 
   -- Triggers GHDL bug
-  STABLE_2 : assert always stable(a(1 downto 0));
-  STABLE_3 : assert always stable(b(1 downto 0));
+  -- EDIT: works since fix of ghdl issue #1367
+  -- Holds
+  STABLE_2 : assert always prev_valid -> stable(a(1 downto 0));
+
+  -- Triggers GHDL bug
+  -- EDIT: works since fix of ghdl issue #1367
+  -- Doesn't hold at cycle 4
+  STABLE_3 : assert always prev_valid -> stable(b(1 downto 0));
 
   -- Holds
-  PREV_0 : assert always a = prev(a);
+  PREV_0 : assert always prev_valid -> a = prev(a);
 
   -- Doesn't hold at cycle 4
-  PREV_1 : assert always b = prev(b);
+  PREV_1 : assert always prev_valid -> b = prev(b);
 
   -- Triggers GHDL bug
-  PREV_2 : assert always always a(1 downto 0) = prev(a(1 downto 0));
-  PREV_3 : assert always always b(1 downto 0) = prev(b(1 downto 0));
+  -- EDIT: works since fix of ghdl issue #1367
+  -- Holds
+  PREV_2 : assert always always prev_valid -> a(1 downto 0) = prev(a(1 downto 0));
+
+  -- Triggers GHDL bug
+  -- EDIT: works since fix of ghdl issue #1367
+  -- Doesn't hold at cycle 4
+  PREV_3 : assert always always prev_valid -> b(1 downto 0) = prev(b(1 downto 0));
 
 
 end architecture psl;

issues/tests.mk

@@ -4,4 +4,6 @@ issue_1292 \
 issue_1314 \
 issue_1321 \
 issue_1322 \
-issue_1345
+issue_1345 \
+issue_1366 \
+issue_1367

src/psl_prev.vhd

@@ -76,6 +76,10 @@ begin
   -- This assertion holds
   PREV_6_a : assert always ((cnt /= x"F") -> next (unsigned(cnt) = unsigned(prev(cnt)) + 1));
 
+  -- Check parts of a vector
+  -- This assertion should hold
+  PREV_7_a : assert always (valid -> di(1 downto 0) = prev(di(1 downto 0)));
+
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas
   -- synthesis translate_off

src/psl_stable.vhd

@@ -33,7 +33,7 @@ begin
   STABLE_0_a : assert always {not valid; valid} |=> (stable(a) until_ ack);
 
   -- This assertion holds
-  STABLE_1_a : assert always {not valid; valid} |=> (stable(b) until_ ack);
+  STABLE_1_a : assert always rose(valid) -> next (stable(b) until_ ack);
 
   -- Workaround needed before stable() was implemented
   -- With VHDL glue logic generating the
@@ -53,6 +53,10 @@ begin
     STABLE_3_a : assert always {not valid; valid} |=> (b = b_prev until_ ack);
   end block a_reg;
 
+  -- Check parts of a vector
+  -- This assertion holds
+  STABLE_4_a : assert always rose(valid) -> next (stable(b(1 downto 0)) until_ ack);
+
 
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas