aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authortmeissner <programming@goodcleanfun.de>2020-06-07 09:26:28 +0200
committertgingold <tgingold@users.noreply.github.com>2020-06-07 18:32:39 +0200
commitdcc6dc4eccea56104bbea43e4407ce8b82dbdab2 (patch)
tree398042851c94fa22eb3868100e878385a55d57cb
parent75c74b4745bfcca3fa86366b9f95c66635ee9316 (diff)
downloadghdl-dcc6dc4eccea56104bbea43e4407ce8b82dbdab2.tar.gz
ghdl-dcc6dc4eccea56104bbea43e4407ce8b82dbdab2.tar.bz2
ghdl-dcc6dc4eccea56104bbea43e4407ce8b82dbdab2.zip
Adjust use of PSL prev() in fell(), rose() & stable() testcases
-rw-r--r--testsuite/synth/issue662/psl_fell.vhdl2
-rw-r--r--testsuite/synth/issue662/psl_rose.vhdl2
-rw-r--r--testsuite/synth/issue662/psl_stable.vhdl8
3 files changed, 9 insertions, 3 deletions
diff --git a/testsuite/synth/issue662/psl_fell.vhdl b/testsuite/synth/issue662/psl_fell.vhdl
index a3261a923..ae2c40c59 100644
--- a/testsuite/synth/issue662/psl_fell.vhdl
+++ b/testsuite/synth/issue662/psl_fell.vhdl
@@ -17,7 +17,7 @@ begin
FELL_0_a : assert always {a; not a} |-> fell(a);
-- This assertion holds
- FELL_1_a : assert always (fell(a) -> (prev(a) = '1' and a = '0'));
+ FELL_1_a : assert always (fell(a) -> (prev(a) and not a));
-- This assertion should fail at cycle 11
FELL_2_a : assert always fell(a) -> b;
diff --git a/testsuite/synth/issue662/psl_rose.vhdl b/testsuite/synth/issue662/psl_rose.vhdl
index 83e9a6c04..f4ea37179 100644
--- a/testsuite/synth/issue662/psl_rose.vhdl
+++ b/testsuite/synth/issue662/psl_rose.vhdl
@@ -17,7 +17,7 @@ begin
ROSE_0_a : assert always {not a; a} |-> rose(a);
-- This assertion holds
- ROSE_1_a : assert always (rose(a) -> (prev(a) = '0' and a = '1'));
+ ROSE_1_a : assert always (rose(a) -> (not prev(a) and a));
-- This assertion should fail at cycle 11
ROSE_2_a : assert always rose(a) -> b;
diff --git a/testsuite/synth/issue662/psl_stable.vhdl b/testsuite/synth/issue662/psl_stable.vhdl
index 675cdbd56..36d0011f6 100644
--- a/testsuite/synth/issue662/psl_stable.vhdl
+++ b/testsuite/synth/issue662/psl_stable.vhdl
@@ -14,10 +14,16 @@ begin
-- All is sensitive to rising edge of clk
default clock is rising_edge(clk);
- -- This assertion holds
+ -- This assertion should fail at cycle 13
STABLE_0_a : assert always {not a; a} |=> (stable(c) until_ b);
-- This assertion holds
STABLE_1_a : assert always {not a; a} |=> (stable(d) until_ b);
+ -- This assertion should fail at cycle 13
+ STABLE_2_a : assert always {not a; a} |=> (c = prev(c) until_ b);
+
+ -- This assertion holds
+ STABLE_3_a : assert always {not a; a} |=> (d = prev(d) until_ b);
+
end architecture psl;