From fb993953cb3533fda4d405556c336e87ef03d171 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 4 May 2020 22:00:30 +0200 Subject: [PATCH] Minor fixes, beauty care * Minor fixes to README * Add psl_before & psl_eventually to formal test list --- README.md | 2 +- formal/tests.mk | 4 +++- src/psl_before.vhd | 6 +++--- src/psl_eventually.vhd | 3 ++- 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index ccfceed..439884a 100644 --- a/README.md +++ b/README.md @@ -38,4 +38,4 @@ The next two lists will grow during further development ## PSL features supported by GHDL but with wrong behaviour -* before_ operator (Overlapping between left & right side not working, see psl_before.vhd) +* before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd) diff --git a/formal/tests.mk b/formal/tests.mk index 416bff7..270d563 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -5,4 +5,6 @@ psl_next \ psl_next_3 \ psl_next_event \ psl_next_event_4 \ -psl_until +psl_until \ +psl_before \ +psl_eventually diff --git a/src/psl_before.vhd b/src/psl_before.vhd index 58d8dea..94c9016 100644 --- a/src/psl_before.vhd +++ b/src/psl_before.vhd @@ -47,9 +47,9 @@ begin -- This is flawed variant of the former assertion -- because even in cycle 1 the b before a property has - -- to hold, which is clearly what we want + -- to hold, which is clearly not what we want -- This assertion doesn't hold at cycle 1 - -- Furthermore this assertion leads to a GHDL crash with bug report + -- Furthermore this assertion leads to a GHDL synthesis crash with bug report -- BEFORE_3_a : assert always (a -> (b before a)); -- This assertion should hold but does not at cycle 3 @@ -58,7 +58,7 @@ begin -- This assertion should hold but does not at cycle 9 -- Potential GHDL bug? - BEFORE_5_a : assert always (c -> next (d before_ c)); + BEFORE_5_a : assert always (c -> next (d before_ c)); -- This assertion doesn't at cycle 6 BEFORE_6_a : assert always (e -> next (f before_ e)); diff --git a/src/psl_eventually.vhd b/src/psl_eventually.vhd index a5d3a9e..b0002ab 100644 --- a/src/psl_eventually.vhd +++ b/src/psl_eventually.vhd @@ -27,7 +27,8 @@ begin default clock is rising_edge(clk); -- This assertion holds - EVENTUALLY_a : assert always (a -> eventually! b); + -- This assertion leads to a GHDL synthesis crash with bug report + --EVENTUALLY_a : assert always (a -> eventually! b); end architecture psl;