Browse Source

Add example for named properties

master
T. Meissner 4 years ago
parent
commit
29ff43dcb2
4 changed files with 85 additions and 1 deletions
  1. +1
    -0
      README.md
  2. +18
    -0
      formal/psl_property.sby
  3. +2
    -1
      sim/tests.mk
  4. +64
    -0
      src/psl_property.vhd

+ 1
- 0
README.md View File

@ -70,6 +70,7 @@ The next lists will grow during further development
* Partial support of PSL vunits (synthesis only)
* Partial support of named sequences (simulation only)
* Partial support of named properties (simulation only)
## Not yet supported by GHDL:


+ 18
- 0
formal/psl_property.sby View File

@ -0,0 +1,18 @@
[tasks]
bmc
[options]
depth 25
bmc: mode bmc
[engines]
bmc: smtbmc z3
[script]
bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_property.vhd -e psl_property
prep -top psl_property
[files]
../src/pkg.vhd
../src/sequencer.vhd
../src/psl_property.vhd

+ 2
- 1
sim/tests.mk View File

@ -26,4 +26,5 @@ psl_sere_len_matching_and \
psl_sere_non_len_matching_and \
psl_sere_concat \
psl_sere_fusion \
psl_sequence
psl_sequence \
psl_property

+ 64
- 0
src/psl_property.vhd View File

@ -0,0 +1,64 @@
library ieee;
use ieee.std_logic_1164.all;
use work.pkg.all;
entity psl_property is
port (
clk : in std_logic
);
end entity psl_property;
architecture psl of psl_property is
signal req, avalid, busy, adone, data, ddone : std_logic;
begin
-- 01234567890123
SEQ_REQ : sequencer generic map ("_-____________") port map (clk, req);
SEQ_AVALID : sequencer generic map ("__-___________") port map (clk, avalid);
SEQ_BUSY : sequencer generic map ("___-_--_______") port map (clk, busy);
SEQ_ADONE : sequencer generic map ("_______-______") port map (clk, adone);
SEQ_DATA : sequencer generic map ("________---___") port map (clk, data);
SEQ_DDONE : sequencer generic map ("___________-__") port map (clk, ddone);
-- All is sensitive to rising edge of clk
default clock is rising_edge(clk);
-- Transfer property
-- Don't works in synthesis, only in simulation
property transfer_3 is always (
{req} |=> {{avalid; busy[->3]; adone}; {data[->3]; ddone}}
);
-- SERE concatenation operator
-- RHS starts at one cycle cycle that the LHS ends
-- This assertion holds
PROP_0_a : assert transfer_3;
-- 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
property transfer_3_p (boolean v, ad, dd) is always (
{req} |=> {{v; busy[->3]; ad}; {data[->3]; dd}}
);
-- SERE concatenation operator
-- RHS starts at one cycle cycle that the LHS ends
-- This assertion holds
PROP_1_a : assert transfer_3_p(avalid, adone, ddone);
-- Stop simulation after longest running sequencer is finished
-- Simulation only code by using pragmas
-- synthesis translate_off
stop_sim(clk, 13);
-- synthesis translate_on
end architecture psl;

Loading…
Cancel
Save