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.

112 lines
2.0 KiB

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