VHDL formal verification tryout

unary_counter.psl

vunit unary_counter_prop(unary_counter(unary_counter_arch)) {
  constant all_zeros : std_logic_vector(LENGTH-1 downto 0) := (others => '0');
  constant all_ones : std_logic_vector(LENGTH-1 downto 0) := (others => '1');

  default clock is rising_edge(clk);

  --
  -- Check for counter code is a unary code
  --
  signal f_check_out: std_logic_vector(LENGTH-1 downto 0) := all_zeros;

  p_check_out: process(clk)
    variable check_out: std_logic_vector(LENGTH-1 downto 0);
  begin
    if rising_edge(clk) then
      check_out := counter;
      for n in 0 to LENGTH-1 loop
        if check_out(0) = '1' then
          check_out := check_out srl 1; -- '0' & check_out(LENGTH-1 downto 1);
        end if;
      end loop;

      f_check_out <= check_out;
    end if;
  end process p_check_out;

  prop_is_unary: assert always f_check_out = all_zeros;

  --
  -- Check for up/down count
  --
  pure function countones(x: std_logic_vector(LENGTH-1 downto 0)) return integer is
    variable co: integer;
  begin
    co := 0;
    for n in 0 to LENGTH-1 loop
      if x(n) = '1' then
        co := co + 1;
      end if;
    end loop;

    return co;
  end function;

  signal f_diff: integer := 0;
  signal f_counter_prev: std_logic_vector(LENGTH-1 downto 0) := all_zeros;

  p_check_updown: process(clk)
  begin
    if rising_edge(clk) then
      f_counter_prev <= counter;
    end if;
  end process p_check_updown;

  f_diff <= countones(counter) - countones(f_counter_prev);

  prop_count_dn: assert always ((i_up = '0' and (counter /= all_zeros) and rst = '0') -> next (f_diff = -1));
  prop_count_up: assert always ((i_up = '1' and (counter /= all_ones) and rst = '0') -> next (f_diff = 1));
}

unary_counter.sby

#
# Run: sby --yosys "yosys -m ghdl" -f unary_counter.sby
#
[tasks]
do_bmc
do_prove

[options]
do_bmc: mode bmc
do_prove: mode prove

[engines]
smtbmc yices

[script]
ghdl --std=08 -fsynopsys -gLENGTH=8 unary_counter.vhdl unary_counter.psl -e unary_counter
prep -top unary_counter

[files]
unary_counter.vhdl
unary_counter.psl

unary_counter.vhdl

library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_unsigned.all;

entity unary_counter is
  generic (LENGTH: integer := 8);
  port (clk, rst: in std_logic;
        i_up: in std_logic;
        o_out: out std_logic_vector(LENGTH-1 downto 0));
end unary_counter;

architecture unary_counter_arch of unary_counter is
  signal counter: std_logic_vector(LENGTH-1 downto 0) := (others => '0');
begin
  o_out <= counter;

  process(clk)
  begin
    if rising_edge(clk) then
      if rst = '1' then
        counter <= (others => '0');
      else
        if i_up = '1' then
          counter <= counter(LENGTH-2 downto 0) & '1';
        else
          counter <= '0' & counter(LENGTH-1 downto 1);
        end if;
      end if;
    end if;
  end process;
end unary_counter_arch;