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.
 
 

86 lines
3.0 KiB

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;