From 7a8545857b6db038d6bb509ae6dc6376466328eb Mon Sep 17 00:00:00 2001 From: tmeissner Date: Tue, 2 Jun 2020 16:36:12 +0200 Subject: [PATCH] Add examples using prev() with 2nd parameter) --- README.md | 63 ++++++++++++++++++++++++------------------------ src/psl_prev.vhd | 29 ++++++++++++++-------- 2 files changed, 51 insertions(+), 41 deletions(-) diff --git a/README.md b/README.md index b614afc..d90bf20 100644 --- a/README.md +++ b/README.md @@ -21,54 +21,55 @@ The next lists will grow during further development ### Directives -* assert directive -* cover directive -* assume directive (synthesis) -* restrict directive (synthesis) +* `assert` directive +* `cover` directive +* `assume` directive (synthesis) +* `restrict` directive (synthesis) ### Temporal operators (LTL style) -* always operator -* never operator -* logical implication operator (->) -* next operator -* next[n] operator -* next_a[i to j] operator -* next_e[i to j] operator -* next_event operator -* next_event[n] operator -* next_event_e[i to j] operator -* until operator -* until_ operator -* before operator (GHDL crash with a specific invalid property, see [PSL before example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_before.vhd#L53)) -* eventually! operator +* `always` operator +* `never` operator +* logical implication operator (`->`) +* `next` operator +* `next[n]` operator +* `next_a[i to j]` operator +* `next_e[i to j]` operator +* `next_event` operator +* `next_event[n]` operator +* `next_event_e[i to j]` operator +* `until` operator +* `until_` operator +* `before` operator (GHDL crash with a specific invalid property, see [PSL before example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_before.vhd#L53)) +* `eventually!` operator ### Sequential Extended Regular Expressions (SERE style) * Simple SERE -* Overlapping suffix implication operator (|->) -* Non overlapping suffix implication operator (|=>) -* Consecutive repetition operator ([*], [+], [*n], [*i to j]) -* Non consecutive repetition operator ([=n], [=i to j]) -* Non consecutive goto repetition operator ([->], [->n], [->i to j]) -* Length-matching and operator (&&) -* or operator (|) -* within operator +* Overlapping suffix implication operator (`|->`) +* Non overlapping suffix implication operator (`|=>`) +* Consecutive repetition operator (`[*]`, `[+]`, `[*n]`, `[*i to j]`) +* Non consecutive repetition operator (`[=n]`, `[=i to j]`) +* Non consecutive goto repetition operator (`[->]`, `[->n]`, `[->i to j]`) +* Length-matching and operator (`&&`) +* or operator (`|`) +* `within` operator ### Functions -* prev() (Synthesis & boolean parameter only, see [prev() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_prev.vhd)) +* `prev()` function (Synthesis & boolean parameter only, see [prev() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_prev.vhd)) ## Not yet supported by GHDL: -* forall statement +* `forall` statement * Synthesis of strong operator versions +* PSL functions (`prev()` partially implemented) ## Under investigation -* before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd) -* next_event_a[i to j] operator -* eventually! behaviour with (un)bounded proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345) +* `before_` operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd) +* `next_event_a[i to j]` operator +* `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345) ## Further Ressources diff --git a/src/psl_prev.vhd b/src/psl_prev.vhd index ece883b..3a7afc6 100644 --- a/src/psl_prev.vhd +++ b/src/psl_prev.vhd @@ -20,10 +20,10 @@ architecture psl of psl_prev is begin - -- 0123456789012 - SEQ_VALID : sequencer generic map ("_-_-_-_-_-_-_") port map (clk, valid); - SEQ_A : sequencer generic map ("__--__--__--_") port map (clk, a); - SEQ_D : hex_sequencer generic map ("0011223344556") port map (clk, d); + -- 01234567890123 + SEQ_VALID : sequencer generic map ("____-_-_-_-_-_") port map (clk, valid); + SEQ_A : sequencer generic map ("-__--__--__--_") port map (clk, a); + SEQ_D : hex_sequencer generic map ("00011223344556") port map (clk, d); -- All is sensitive to rising edge of clk @@ -34,13 +34,13 @@ begin -- This assertion should hold -- prev() with vector parameter isn't supported yet - -- Workaround: VHDL glue logic + -- Workaround: VHDL glue logic and simple compare -- PREV_1_a : assert always (valid -> d = prev(d)); -- Workaround with VHDL glue logic generating the - -- previous value of d + -- previous value of d and simple comparing the two values d_reg : block is - signal d_prev : std_logic_vector(3 downto 0); + signal d_prev : std_logic_vector(d'range); begin process (clk) is begin @@ -48,15 +48,24 @@ begin d_prev <= d; end if; end process; - PREV_2_a : assert always (valid -> d = d_prev); - end block d_reg; + -- Using prev() with additional parameter i, should return + -- the value of the expression in the i-th previous cycle + -- prev(a) = prev(a, 1) + -- This assertion holds + PREV_3_a : assert always (valid -> a = prev(a, 1)); + + -- Using prev() with additional parameter i, should return + -- the value of the expression in the i-th previous cycle + -- This assertion holds + PREV_4_a : assert always (valid -> a = prev(a, 4)); + -- Stop simulation after longest running sequencer is finished -- Simulation only code by using pragmas -- synthesis translate_off - stop_sim(clk, 13); + stop_sim(clk, 14); -- synthesis translate_on