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.

128 lines
2.6 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. entity hex_sequencer is
  4. generic (
  5. seq : string
  6. );
  7. port (
  8. clk : in std_logic;
  9. data : out std_logic_vector(3 downto 0)
  10. );
  11. end entity hex_sequencer;
  12. architecture rtl of hex_sequencer is
  13. signal index : natural := seq'low;
  14. function to_hex (a : in character) return std_logic_vector is
  15. variable ret : std_logic_vector(3 downto 0);
  16. begin
  17. case a is
  18. when '0' | '_' => ret := x"0";
  19. when '1' => ret := x"1";
  20. when '2' => ret := x"2";
  21. when '3' => ret := x"3";
  22. when '4' => ret := x"4";
  23. when '5' => ret := x"5";
  24. when '6' => ret := x"6";
  25. when '7' => ret := x"7";
  26. when '8' => ret := x"8";
  27. when '9' => ret := x"9";
  28. when 'a' | 'A' => ret := x"A";
  29. when 'b' | 'B' => ret := x"B";
  30. when 'c' | 'C' => ret := x"C";
  31. when 'd' | 'D' => ret := x"D";
  32. when 'e' | 'E' => ret := x"E";
  33. when 'f' | 'F' | '-' => ret := x"F";
  34. when others => ret := x"X";
  35. end case;
  36. return ret;
  37. end function to_hex;
  38. begin
  39. process (clk) is
  40. begin
  41. if rising_edge(clk) then
  42. if (index < seq'high) then
  43. index <= index + 1;
  44. end if;
  45. end if;
  46. end process;
  47. data <= to_hex(seq(index));
  48. end architecture rtl;
  49. library ieee;
  50. use ieee.std_logic_1164.all;
  51. use ieee.numeric_std.all;
  52. entity issue is
  53. port (
  54. clk : in std_logic
  55. );
  56. end entity issue;
  57. architecture psl of issue is
  58. signal a : std_logic_vector(3 downto 0);
  59. begin
  60. SEQ_C : entity work.hex_sequencer generic map ("0123456789ABCDEF") port map (clk, a);
  61. end architecture psl;
  62. library ieee;
  63. use ieee.std_logic_1164.all;
  64. use std.env.all;
  65. entity test_issue is
  66. end entity test_issue;
  67. architecture sim of test_issue is
  68. signal clk : std_logic := '1';
  69. begin
  70. clk <= not clk after 500 ps;
  71. DUT : entity work.issue(psl) port map (clk);
  72. -- stop simulation after 30 cycles
  73. process
  74. variable index : natural := 29;
  75. begin
  76. loop
  77. wait until rising_edge(clk);
  78. index := index - 1;
  79. exit when index = 0;
  80. end loop;
  81. stop(0);
  82. end process;
  83. end architecture sim;
  84. vunit issue_1850_vu (issue(psl)) {
  85. -- All is sensitive to rising edge of clk
  86. default clock is rising_edge(clk);
  87. -- A simple check for counter increasing
  88. -- Nested generate leads to a crash
  89. test : if true generate
  90. counter_check : for i in 0 to 14 generate
  91. SERE_4_a : assert always
  92. {a = std_logic_vector(to_unsigned(i, 4))}
  93. |=>
  94. {a = std_logic_vector(to_unsigned(i + 1, 4))};
  95. end generate counter_check;
  96. end generate test;
  97. }