tmeissner
/
psl_with_ghdl


								library ieee;

								  use ieee.std_logic_1164.all;


								use work.pkg.all;


								entity psl_cover is

								  port (

								    clk : in std_logic

								  );

								end entity psl_cover;


								architecture psl of psl_cover is


								  signal req, busy, done : std_logic;


								begin


								  --                                 0123456789

								  SEQ_REQ  : sequencer generic map ("_-________") port map (clk, req);

								  SEQ_BUSY : sequencer generic map ("__-_-_-___") port map (clk, busy);

								  SEQ_DONE : sequencer generic map ("________-_") port map (clk, done);


								  -- All is sensitive to rising edge of clk

								  default clock is rising_edge(clk);


								  -- Covers a transfer request

								  -- This cover directive holds at cycle 1

								  COVER_0_c : cover {req}

								    report "Transfer requested";


								  -- Covers started processing of transfers

								  -- This cover directive holds at cycle 2

								  COVER_1_c : cover {req; {{busy[=1]} && {not done[+]}}}

								    report "Transfer in progress";


								  -- Covers each transfer with length in range 1 to 8

								  -- This cover directive holds at cycle 8

								  COVER_2_c : cover {req; {{busy[=1 to 8]} && {not done[+]}}; done}

								    report "Transfer done";


								  -- Cover transfers with length in range 1 to 8 separately

								  cover_transfer_lengths : for i in 1 to 8 generate

								  begin

								    -- Don't works with GHDL, but should? Is a defined as static in the

								    -- generate body?

								    --COVER_TRANSFER_LENGTH_c : cover {req; {{busy[=i]} && {not done[+]}}; done};

								  end generate cover_transfer_lengths;


								  -- Workaround: writing separate cover directives for

								  -- each length, very tedious

								  -- Only length 3 holds at cycle 8, all others not

								  COVER_LENGTH_1_c : cover {req; {{busy[=1]} && {not done[+]}}; done};

								  COVER_LENGTH_2_c : cover {req; {{busy[=2]} && {not done[+]}}; done};

								  COVER_LENGTH_3_c : cover {req; {{busy[=3]} && {not done[+]}}; done};

								  COVER_LENGTH_4_c : cover {req; {{busy[=4]} && {not done[+]}}; done};

								  COVER_LENGTH_5_c : cover {req; {{busy[=5]} && {not done[+]}}; done};

								  COVER_LENGTH_6_c : cover {req; {{busy[=6]} && {not done[+]}}; done};

								  COVER_LENGTH_7_c : cover {req; {{busy[=7]} && {not done[+]}}; done};

								  COVER_LENGTH_8_c : cover {req; {{busy[=8]} && {not done[+]}}; done};


								  -- BTW: GHDL synthesis creates a cover directive for each assert directive

								  -- which is really nice. So you can run SymbiYosys in cover mode

								  -- to see if your assertions can actually be active.

								  -- This assertion checks for the final done at the end of transfer.

								  -- In cover mode, the LHS side of the property has to hold.

								  -- This cover directive holds at cycle 7

								  ASSERT_a : assert always {req; {{busy[=3]} && {not done[+]}}; not done} |=> {done};


								  -- For simulation, you have to write a separate cover directive when

								  -- you want to check if your assertion can be active

								  -- Simply use the LHS of the asserts property

								  COVER_A : cover {req; {{busy[=3]} && {not done[+]}}; not done}

								    report "Transfer of length 3";


								  -- Stop simulation after longest running sequencer is finished

								  -- Simulation only code by using pragmas

								  -- synthesis translate_off

								  stop_sim(clk, 10);

								  -- synthesis translate_on


								end architecture psl;