Browse Source

Add examples using prev() with 2nd parameter)

master
T. Meissner 5 years ago
parent
commit
7a8545857b
2 changed files with 51 additions and 41 deletions
  1. +32
    -31
      README.md
  2. +19
    -10
      src/psl_prev.vhd

+ 32
- 31
README.md View File

@ -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


+ 19
- 10
src/psl_prev.vhd View File

@ -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


Loading…
Cancel
Save