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.

96 lines
2.2 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. use std.env.all;
  4. package pkg is
  5. component sequencer is
  6. generic (
  7. seq : string
  8. );
  9. port (
  10. clk : in std_logic;
  11. data : out std_logic
  12. );
  13. end component sequencer;
  14. component hex_sequencer is
  15. generic (
  16. seq : string
  17. );
  18. port (
  19. clk : in std_logic;
  20. data : out std_logic_vector(3 downto 0)
  21. );
  22. end component hex_sequencer;
  23. function to_bit (a : in character) return std_logic;
  24. function to_hex (a : in character) return std_logic_vector;
  25. -- synthesis translate_off
  26. procedure stop_sim (signal clk : in std_logic; cycles : in natural; add_cycles : in natural := 2);
  27. -- synthesis translate_on
  28. end package pkg;
  29. package body pkg is
  30. function to_bit (a : in character) return std_logic is
  31. variable ret : std_logic;
  32. begin
  33. case a is
  34. when '0' | '_' => ret := '0';
  35. when '1' | '-' => ret := '1';
  36. when others => ret := 'X';
  37. end case;
  38. return ret;
  39. end function to_bit;
  40. function to_hex (a : in character) return std_logic_vector is
  41. variable ret : std_logic_vector(3 downto 0);
  42. begin
  43. case a is
  44. when '0' | '_' => ret := x"0";
  45. when '1' => ret := x"1";
  46. when '2' => ret := x"2";
  47. when '3' => ret := x"3";
  48. when '4' => ret := x"4";
  49. when '5' => ret := x"5";
  50. when '6' => ret := x"6";
  51. when '7' => ret := x"7";
  52. when '8' => ret := x"8";
  53. when '9' => ret := x"9";
  54. when 'a' | 'A' => ret := x"A";
  55. when 'b' | 'B' => ret := x"B";
  56. when 'c' | 'C' => ret := x"C";
  57. when 'd' | 'D' => ret := x"D";
  58. when 'e' | 'E' => ret := x"E";
  59. when 'f' | 'F' | '-' => ret := x"F";
  60. when others => ret := x"X";
  61. end case;
  62. return ret;
  63. end function to_hex;
  64. -- synthesis translate_off
  65. procedure stop_sim (signal clk : in std_logic; cycles : in natural; add_cycles : in natural := 2) is
  66. variable index : natural := cycles + add_cycles;
  67. begin
  68. loop
  69. wait until rising_edge(clk);
  70. index := index - 1;
  71. if index = 0 then
  72. exit;
  73. end if;
  74. end loop;
  75. finish(0);
  76. end procedure stop_sim;
  77. -- synthesis translate_on
  78. end package body pkg;