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.

116 lines
2.2 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. use ieee.numeric_std.all;
  38. entity issue is
  39. port (
  40. clk : in std_logic
  41. );
  42. end entity issue;
  43. architecture psl of issue is
  44. signal a, b : std_logic;
  45. begin
  46. -- 012345678
  47. SEQ_A : entity work.sequencer generic map ("_-____-__") port map (clk, a);
  48. SEQ_B : entity work.sequencer generic map ("__-____-_") port map (clk, b);
  49. default clock is rising_edge(clk);
  50. -- This works, but it's not that useful as even a simple negation
  51. -- leads to an error (see seq1)
  52. sequence seq (boolean d0, d1) is {d0; d1};
  53. TEST_0 : cover seq(a, b) report "TEST_0 hit";
  54. -- One could negate the parameter when calling the
  55. -- sequence, but this is not very intuitive
  56. TEST_1 : assert never seq(a, not b);
  57. -- This doesnt work:
  58. -- error: PSL declaration "a" not allowed in an expression
  59. sequence seq1 (boolean d0) is {not d0; d0 = true};
  60. TEST_2 : cover seq1(a) report "TEST_1 hit";
  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 10 cycles
  73. process
  74. variable index : natural := 10;
  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;