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.

116 lines
2.2 KiB

  1. vunit issue_vunit (issue(psl)) {
  2. -- VHDL declaration seem to be working
  3. signal a_delayed : std_logic := '0';
  4. signal prev_valid : boolean := false;
  5. -- Other VHDL code not
  6. -- results in parser errors
  7. -- during synthesis
  8. -- EDIT: works since fix of ghdl issue #1366
  9. process is
  10. begin
  11. wait until rising_edge(clk);
  12. a_delayed <= a;
  13. prev_valid <= true;
  14. end process;
  15. -- All is sensitive to rising edge of clk
  16. default clock is rising_edge(clk);
  17. -- This assertion holds
  18. CHECK_0_a : assert always (a -> b);
  19. -- You can't do anything with the declared signal
  20. -- Can be synthesized with GHDL, however
  21. -- results in error in ghdl-yosys-plugin:
  22. -- ERROR: Assert `n.id != 0' failed in src/ghdl.cc:172
  23. -- EDIT: works since fix of ghdl issue #1366
  24. CHECK_1_a : assert always prev_valid -> a_delayed = prev(a);
  25. }
  26. library ieee;
  27. use ieee.std_logic_1164.all;
  28. use ieee.numeric_std.all;
  29. entity sequencer is
  30. generic (
  31. seq : string
  32. );
  33. port (
  34. clk : in std_logic;
  35. data : out std_logic
  36. );
  37. end entity sequencer;
  38. architecture rtl of sequencer is
  39. signal index : natural := seq'low;
  40. function to_bit (a : in character) return std_logic is
  41. variable ret : std_logic;
  42. begin
  43. case a is
  44. when '0' | '_' => ret := '0';
  45. when '1' | '-' => ret := '1';
  46. when others => ret := 'X';
  47. end case;
  48. return ret;
  49. end function to_bit;
  50. begin
  51. process (clk) is
  52. begin
  53. if rising_edge(clk) then
  54. if (index < seq'high) then
  55. index <= index + 1;
  56. end if;
  57. end if;
  58. end process;
  59. data <= to_bit(seq(index));
  60. end architecture rtl;
  61. library ieee;
  62. use ieee.std_logic_1164.all;
  63. use ieee.numeric_std.all;
  64. entity issue is
  65. port (
  66. clk : in std_logic
  67. );
  68. end entity issue;
  69. architecture psl of issue is
  70. component sequencer is
  71. generic (
  72. seq : string
  73. );
  74. port (
  75. clk : in std_logic;
  76. data : out std_logic
  77. );
  78. end component sequencer;
  79. signal a, b : std_logic;
  80. begin
  81. -- 0123456789
  82. SEQ_A : sequencer generic map ("__-__-____") port map (clk, a);
  83. SEQ_B : sequencer generic map ("__-__-____") port map (clk, b);
  84. end architecture psl;