Files for discussion

File dut.vhdl:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity dut is
	port(
		behaviour_in: in std_logic_vector(15 downto 0);
		
		clk_in: in std_logic;
		
		en_in: in std_logic;
		cnt_out: out std_logic_vector(1 downto 0)
	);
end;

architecture fs of dut is
	-- correct answer:
	constant beh_ref: std_logic_vector(15 downto 0) := "0011111010010100";

	-- DUT signals =>
	type state_table_t is array(0 to 7) of std_logic_vector(1 downto 0);

	function beh2table_f(a: std_logic_vector) return state_table_t is
		variable r: state_table_t;
	begin
		for i in r'range loop
			r(i) := a(i*2+1 downto i*2); 
		end loop;
		return r;
	end;
	
	signal state_table: state_table_t;

	signal state: std_logic_vector(1 downto 0) := "00";
	signal next_state: std_logic_vector(1 downto 0);
	
	signal state_inputs: std_logic_vector(2 downto 0);
	
	-- Verification signals =>
	signal prev_state: std_logic_vector(1 downto 0) := "00";
	signal cnt_incremented: std_logic;
begin
	-- DUT code =>
	
	state_table <= beh2table_f(behaviour_in);
	
	state_inputs(0) <= en_in;
	state_inputs(1) <= state(0);
	state_inputs(2) <= state(1);

	state_async_pr: process(all)
	begin
		next_state <= state_table(to_integer(unsigned(state_inputs)));
	end process;
	
	state_sync_pr: process(clk_in)
	begin
		if rising_edge(clk_in) then
			state <= next_state;
		end if;
	end process;
	
	cnt_out <= state;
	
	-- <= DUT code ends here.
	
	-- Verification part, included in the same file on purpose =>
	
	process(all)
	begin
		cnt_incremented <= '0';
		if unsigned(prev_state) + 1 = unsigned(state) then
			cnt_incremented <= '1';
		end if;
	end process;
	
	process(clk_in)
	begin
		if rising_edge(clk_in) then
			prev_state <= state;
		end if;
	end process;
	
	-- <= Verification part, included in the same file on purpose.
	
	-- PSL:
	
	-- The intention is to have binary counter (0 to 3) with clock enable input.
	
	default clock is rising_edge(clk_in);
	
	beh_const_a: assume always {stable(behaviour_in)};
	
	-- Replace all asserts with assumes =>
	--cnt_a: assert always {en_in} |=> {cnt_incremented};
	--en_a: assert always {not en_in} |=> {stable(cnt_out)};
	cnt_a: assume always {en_in} |=> {cnt_incremented};
	en_a: assume always {not en_in} |=> {stable(cnt_out)};
	
	test: assume always {en_in} |=> {not en_in};
	test2: assume always {not en_in} |=> {en_in};
	
	cover {[*10]};
end;

File dut.sby

[tasks]
cover

[options]
cover: mode cover
cover: depth 50

[engines]
cover: smtbmc

[script]
ghdl --std=08 dut.vhdl -e dut
prep -top dut

[files]
dut.vhdl

Running the code:

docker run --rm -it -v $PWD:/root registry.hub.docker.com/hdlc/formal:all bash -c 'cd /root; sby --yosys "yosys -m ghdl" -f dut.sby'