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.

175 lines
3.9 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. entity hex_sequencer is
  38. generic (
  39. seq : string
  40. );
  41. port (
  42. clk : in std_logic;
  43. data : out std_logic_vector(3 downto 0)
  44. );
  45. end entity hex_sequencer;
  46. architecture rtl of hex_sequencer is
  47. signal index : natural := seq'low;
  48. function to_hex (a : in character) return std_logic_vector is
  49. variable ret : std_logic_vector(3 downto 0);
  50. begin
  51. case a is
  52. when '0' | '_' => ret := x"0";
  53. when '1' => ret := x"1";
  54. when '2' => ret := x"2";
  55. when '3' => ret := x"3";
  56. when '4' => ret := x"4";
  57. when '5' => ret := x"5";
  58. when '6' => ret := x"6";
  59. when '7' => ret := x"7";
  60. when '8' => ret := x"8";
  61. when '9' => ret := x"9";
  62. when 'a' | 'A' => ret := x"A";
  63. when 'b' | 'B' => ret := x"B";
  64. when 'c' | 'C' => ret := x"C";
  65. when 'd' | 'D' => ret := x"D";
  66. when 'e' | 'E' => ret := x"E";
  67. when 'f' | 'F' | '-' => ret := x"F";
  68. when others => ret := x"X";
  69. end case;
  70. return ret;
  71. end function to_hex;
  72. begin
  73. process (clk) is
  74. begin
  75. if rising_edge(clk) then
  76. if (index < seq'high) then
  77. index <= index + 1;
  78. end if;
  79. end if;
  80. end process;
  81. data <= to_hex(seq(index));
  82. end architecture rtl;
  83. library ieee;
  84. use ieee.std_logic_1164.all;
  85. use ieee.numeric_std.all;
  86. entity issue is
  87. port (
  88. clk : in std_logic
  89. );
  90. end entity issue;
  91. architecture psl of issue is
  92. component sequencer is
  93. generic (
  94. seq : string
  95. );
  96. port (
  97. clk : in std_logic;
  98. data : out std_logic
  99. );
  100. end component sequencer;
  101. component hex_sequencer is
  102. generic (
  103. seq : string
  104. );
  105. port (
  106. clk : in std_logic;
  107. data : out std_logic_vector(3 downto 0)
  108. );
  109. end component hex_sequencer;
  110. signal req, ack : std_logic;
  111. signal din, dout : std_logic_vector(3 downto 0);
  112. begin
  113. -- 0123456789
  114. SEQ_REQ : sequencer generic map ("_-______-____") port map (clk, req);
  115. SEQ_DIN : hex_sequencer generic map ("4433344774444") port map (clk, din);
  116. SEQ_ACK : sequencer generic map ("___-______-__") port map (clk, ack);
  117. SEQ_DOUT : hex_sequencer generic map ("2244333447744") port map (clk, dout);
  118. -- All is sensitive to rising edge of clk
  119. default clock is rising_edge(clk);
  120. -- Check for two possible values of din/dout
  121. NEXT_EVENT_0_a : assert always ((req and din = x"4") -> next_event(ack)(dout = x"4"));
  122. NEXT_EVENT_1_a : assert always ((req and din = x"7") -> next_event(ack)(dout = x"7"));
  123. -- Check for all possible values of din/dout
  124. check_transfer : for i in 0 to 15 generate
  125. signal i_slv : std_logic_vector(din'range);
  126. begin
  127. i_slv <= std_logic_vector(to_unsigned(i, 4));
  128. -- Without name it works
  129. assert always ((req and din = i_slv) -> next_event(ack)(dout = i_slv));
  130. -- This errors because of similar names of all asserts
  131. -- ERROR: Assert `count_id(cell->name) == 0' failed in kernel/rtlil.cc:1613.
  132. NEXT_EVENT_a : assert always ((req and din = i_slv) -> next_event(ack)(dout = i_slv));
  133. end generate check_transfer;
  134. end architecture psl;