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.

61 lines
2.1 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. use work.pkg.all;
  4. entity psl_sere_non_consecutive_repeat_repetition is
  5. port (
  6. clk : in std_logic
  7. );
  8. end entity psl_sere_non_consecutive_repeat_repetition;
  9. architecture psl of psl_sere_non_consecutive_repeat_repetition is
  10. signal req, busy, done : std_logic;
  11. begin
  12. -- 0123456789
  13. SEQ_REQ : sequencer generic map ("_-________") port map (clk, req);
  14. SEQ_BUSY : sequencer generic map ("__-_-_-___") port map (clk, busy);
  15. SEQ_DONE : sequencer generic map ("________-_") port map (clk, done);
  16. -- All is sensitive to rising edge of clk
  17. default clock is rising_edge(clk);
  18. -- Non consecutive repetition of 3 cycles with possible padding
  19. -- busy has to hold on 3 cycles between req & done
  20. -- This assertion holds
  21. SERE_0_a : assert always {req} |=> {busy[=3]; done};
  22. -- Non consecutive repetition of 2 to 4 cycles with possible padding
  23. -- busy has to hold on 2 to 4 cycles between req & done
  24. -- This assertion holds
  25. SERE_1_a : assert always {req} |=> {busy[=2 to 4]; done};
  26. -- Non consecutive repetition of 5 cycles with possible padding
  27. -- busy has to hold on 5 cycles between req & done
  28. -- This assertion holds -> possible PITFALL!
  29. -- RHS is underspecified, nothing prevents done to hold between or together
  30. -- with holding busy. For intentioned behaviour, the behaviour of done
  31. -- has to be described more specificly (see SERE_3_a)
  32. SERE_2_a : assert always {req} |=> {busy[=5]; done};
  33. -- Non consecutive repetition of 3 cycles with possible padding
  34. -- busy has to hold on exactly 3 cycles between req & and the first done
  35. -- This is a more exact version of the assertions before using
  36. -- the length-matching and SERE operator &&
  37. -- This assertion holds
  38. SERE_3_a : assert always {req} |=> {{{busy[=3]} && {not done[+]}}; done};
  39. -- Non consecutive repetition of 4 cycles with possible padding
  40. -- busy has to hold on exactly 4 cycles between req & and the first done
  41. -- This assertion doesn't hold at cycle 8
  42. SERE_4_a : assert always {req} |=> {{{busy[=4]} && {not done[+]}}; done};
  43. end architecture psl;