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.

70 lines
1.3 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. entity issue is
  4. port (
  5. clk : in std_logic
  6. );
  7. end entity issue;
  8. architecture psl of issue is
  9. signal a : boolean := true;
  10. begin
  11. testG : if true generate
  12. signal b : boolean := true;
  13. signal c : boolean := false;
  14. begin
  15. c <= true;
  16. -- All is sensitive to rising edge of clk
  17. default clock is rising_edge(clk);
  18. -- This assertion works
  19. INITIAL_0_a : assert always a;
  20. -- This assertion generates an ghdl-yosys-plugin error
  21. -- ERROR: Assert `n.id != 0' failed in src/ghdl.cc:204.
  22. INITIAL_1_a : assert always b;
  23. -- This assertion works
  24. INITIAL_2_a : assert always c;
  25. end generate testG;
  26. -- Same error occurs when using a block instead of a generate
  27. -- statement
  28. testB : block is
  29. signal b : boolean := true;
  30. signal c : boolean := false;
  31. begin
  32. c <= true;
  33. -- All is sensitive to rising edge of clk
  34. default clock is rising_edge(clk);
  35. -- This assertion works
  36. INITIAL_0_a : assert always a;
  37. -- This assertion generates an ghdl-yosys-plugin error
  38. -- ERROR: Assert `n.id != 0' failed in src/ghdl.cc:204.
  39. INITIAL_1_a : assert always b;
  40. -- This assertion works
  41. INITIAL_2_a : assert always c;
  42. end block testB;
  43. end architecture psl;