Browse Source

Update PSL sequence, property & vunit examples as #1889 was fixed

* Named sequences & properties for synthesis are also supported in
  PSL vunits (#1889) and inline PSL (#1891) now.
master
T. Meissner 3 years ago
parent
commit
bb50d3436b
4 changed files with 14 additions and 10 deletions
  1. +2
    -3
      README.md
  2. +1
    -4
      src/psl_property.vhd
  3. +0
    -2
      src/psl_sequence.vhd
  4. +11
    -1
      src/psl_vunit.psl

+ 2
- 3
README.md View File

@ -77,8 +77,8 @@ The next lists will grow during further development
### Convenient stuff ### Convenient stuff
* Partial support of PSL vunits (synthesis only) * Partial support of PSL vunits (synthesis only)
* Partial support of named sequences (simulation only)
* Partial support of named properties (simulation only)
* Partial support of named sequences (some parameter types missing)
* Partial support of named properties (some parameter types missing)
* Partial support of PSL `endpoint` (simulation only, in PSL comments) * Partial support of PSL `endpoint` (simulation only, in PSL comments)
### Yosys formal extensions (reference to [Symbiyosys docs](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables)) ### Yosys formal extensions (reference to [Symbiyosys docs](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables))
@ -92,7 +92,6 @@ The next lists will grow during further development
* `for` operator * `for` operator
* Synthesis of built-in functions `countones()`, `isunknown()` * Synthesis of built-in functions `countones()`, `isunknown()`
* Synthesis of strong operator versions * Synthesis of strong operator versions
* Synthesis of named sequences & properties
* Simulation of built-in functions * Simulation of built-in functions
* Simulation of PSL vunits * Simulation of PSL vunits
* PSL macros (`%for`, `%if`) * PSL macros (`%for`, `%if`)


+ 1
- 4
src/psl_property.vhd View File

@ -31,7 +31,6 @@ begin
default clock is rising_edge(clk); default clock is rising_edge(clk);
-- Transfer property -- Transfer property
-- Don't works in synthesis, only in simulation
property transfer_3 is always ( property transfer_3 is always (
{req} |=> {{avalid; busy[->3]; adone}; {data[->3]; ddone}} {req} |=> {{avalid; busy[->3]; adone}; {data[->3]; ddone}}
); );
@ -42,9 +41,7 @@ begin
PROP_0_a : assert transfer_3; PROP_0_a : assert transfer_3;
-- Properties can have parameters -- Properties can have parameters
-- Don't works in synthesis, only in simulation
-- Parameters with repetition operators lead to crash:
-- raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : no field Hash
-- This assertion holds
property transfer_3_p (boolean v, ad, dd) is always ( property transfer_3_p (boolean v, ad, dd) is always (
{req} |=> {{v; busy[->3]; ad}; {data[->3]; dd}} {req} |=> {{v; busy[->3]; ad}; {data[->3]; dd}}
); );


+ 0
- 2
src/psl_sequence.vhd View File

@ -31,12 +31,10 @@ begin
default clock is rising_edge(clk); default clock is rising_edge(clk);
-- Address phase sequence -- Address phase sequence
-- Don't works in synthesis, only in simulation
sequence a_phase is {avalid; busy[->3]; adone}; sequence a_phase is {avalid; busy[->3]; adone};
-- Data phase sequence -- Data phase sequence
-- Sequences can have parameters -- Sequences can have parameters
-- Don't works in synthesis, only in simulation
sequence d_phase (boolean done) is {data[->3]; done}; sequence d_phase (boolean done) is {data[->3]; done};
-- SERE concatenation operator -- SERE concatenation operator


+ 11
- 1
src/psl_vunit.psl View File

@ -32,5 +32,15 @@ vunit psl_vunit_vu (psl_vunit(beh)) {
{c = std_logic_vector(to_unsigned(i + 1, 4))}; {c = std_logic_vector(to_unsigned(i + 1, 4))};
end generate counter_check; end generate counter_check;
-- Using named sequences
sequence s_a is {a; a};
sequence s_b is {b};
}
SERE_5_a : assert always s_a |-> s_b;
-- Using named property
property p_a is always s_a |-> s_b;
PROP_0_a : assert p_a;
}

Loading…
Cancel
Save