Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

85 lines
1.5 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. entity sequencer is
  4. generic (
  5. seq : string
  6. );
  7. port (
  8. clk : in std_logic;
  9. data : out std_logic
  10. );
  11. end entity sequencer;
  12. architecture rtl of sequencer is
  13. signal index : natural := seq'low;
  14. function to_bit (a : in character) return std_logic is
  15. variable ret : std_logic;
  16. begin
  17. case a is
  18. when '0' | '_' => ret := '0';
  19. when '1' | '-' => ret := '1';
  20. when others => ret := 'X';
  21. end case;
  22. return ret;
  23. end function to_bit;
  24. begin
  25. process (clk) is
  26. begin
  27. if rising_edge(clk) then
  28. if (index < seq'high) then
  29. index <= index + 1;
  30. end if;
  31. end if;
  32. end process;
  33. data <= to_bit(seq(index));
  34. end architecture rtl;
  35. library ieee;
  36. use ieee.std_logic_1164.all;
  37. use ieee.numeric_std.all;
  38. entity issue is
  39. port (
  40. clk : in std_logic
  41. );
  42. end entity issue;
  43. architecture psl of issue is
  44. signal a, b : std_logic;
  45. begin
  46. -- 012345
  47. SEQ_A : entity work.sequencer generic map ("--____") port map (clk, a);
  48. SEQ_B : entity work.sequencer generic map ("_-____") port map (clk, b);
  49. end architecture psl;
  50. vunit issue_1899_vu0 {
  51. -- Using named sequences
  52. sequence s_a (boolean a) is {a; a};
  53. sequence s_b (boolean b) is {b};
  54. }
  55. vunit issue_1899_vu1 (issue(psl)) {
  56. inherit issue_1899_vu0;
  57. -- All is sensitive to rising edge of clk
  58. default clock is rising_edge(clk);
  59. SERE_0_a : assert always s_a(a) |-> s_b(b);
  60. }