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.

37 lines
526 B

  1. vunit issue_vunit (issue(psl)) {
  2. -- All is sensitive to rising edge of clk
  3. default clock is rising_edge(clk);
  4. -- GHDL crash if condition evaluates to true
  5. test_g : if true generate
  6. -- This assertion holds
  7. CHECK_0_a : assert always (a -> b);
  8. end generate test_g;
  9. }
  10. library ieee;
  11. use ieee.std_logic_1164.all;
  12. entity issue is
  13. port (
  14. clk : in std_logic
  15. );
  16. end entity issue;
  17. architecture psl of issue is
  18. signal a, b : std_logic := '1';
  19. begin
  20. a <= '1';
  21. b <= a;
  22. end architecture psl;