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.

130 lines
2.1 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. library ieee;
  38. use ieee.std_logic_1164.all;
  39. use ieee.numeric_std.all;
  40. entity issue is
  41. port (
  42. clk : in std_logic
  43. );
  44. end entity issue;
  45. architecture psl of issue is
  46. component sequencer is
  47. generic (
  48. seq : string
  49. );
  50. port (
  51. clk : in std_logic;
  52. data : out std_logic
  53. );
  54. end component sequencer;
  55. signal a, b : std_logic;
  56. begin
  57. -- 0123456789012345
  58. SEQ_A : sequencer generic map ("__-__-____-_____") port map (clk, a);
  59. SEQ_B : sequencer generic map ("_______-________") port map (clk, b);
  60. -- All is sensitive to rising edge of clk
  61. default clock is rising_edge(clk);
  62. -- This assertion should fail
  63. EVENTUALLY_a : assert always (a -> eventually! b);
  64. end architecture psl;
  65. library ieee;
  66. use ieee.std_logic_1164.all;
  67. use std.env.all;
  68. entity test_issue is
  69. end entity test_issue;
  70. architecture sim of test_issue is
  71. signal clk : std_logic := '1';
  72. begin
  73. clk <= not clk after 500 ps;
  74. DUT : entity work.issue(psl) port map (clk);
  75. -- stop simulation after 30 cycles
  76. process
  77. variable index : natural := 29;
  78. begin
  79. loop
  80. wait until rising_edge(clk);
  81. index := index - 1;
  82. exit when index = 0;
  83. end loop;
  84. stop(0);
  85. -- finish(0);
  86. end process;
  87. end architecture sim;