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.

40 lines
792 B

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. use ieee.numeric_std.all;
  4. use work.pkg.all;
  5. entity psl_vunit is
  6. generic (
  7. formal : string := "ALL"
  8. );
  9. port (
  10. clk : in std_logic
  11. );
  12. end entity psl_vunit;
  13. architecture beh of psl_vunit is
  14. signal a, b : std_logic;
  15. signal c : std_logic_vector(3 downto 0);
  16. begin
  17. -- 012345
  18. SEQ_A : sequencer generic map ("--____") port map (clk, a);
  19. SEQ_B : sequencer generic map ("_-____") port map (clk, b);
  20. --
  21. SEQ_C : hex_sequencer generic map ("0123456789ABCDEF") port map (clk, c);
  22. -- Stop simulation after longest running sequencer is finished
  23. -- Simulation only code by using pragmas
  24. -- synthesis translate_off
  25. stop_sim(clk, 18);
  26. -- synthesis translate_on
  27. end architecture beh;