dipl/sections/soc/alu_formal.vhd

81 lines
2.1 KiB
VHDL

formal: block
signal prev_a : MATH_WORD;
signal prev_b : MATH_WORD;
signal prev_operation : alu_operation_t;
signal expected_result : MATH_WORD;
signal has_run : std_logic := '0';
signal prev_enable_math : std_logic;
begin
default clock is rising_edge(clk);
process(clk)
begin
if rising_edge(clk) then
prev_a <= a;
prev_b <= b;
prev_operation <= operation;
prev_enable_math <= enable_math;
end if;
end process;
-- assume inputs won't change while calculation is ongoing
assume always not valid -> (
a = prev_a and
b = prev_b and
operation = prev_operation
);
-- assume the "run" input is active at least until the result is valid
assume always prev_enable_math -> (enable_math or valid);
process(clk)
begin
if rising_edge(clk) and enable_math = '1' and valid = '1' then
has_run <= '1';
expected_result <= (others => '0');
case operation is
when ALU_AND =>
expected_result <= a and b;
when ALU_OR =>
expected_result <= a or b;
when ALU_XOR =>
expected_result <= a xor b;
when ALU_SHIFTL =>
expected_result <= std_logic_vector(shift_left(
unsigned(a),
to_integer(unsigned(b(4 downto 0)))
));
when ALU_SHIFTR_L =>
expected_result <= std_logic_vector(shift_right(
unsigned(a),
to_integer(unsigned(b(4 downto 0)))
));
when ALU_SHIFTR_A =>
expected_result <= std_logic_vector(shift_right(
signed(a),
to_integer(unsigned(b(4 downto 0)))
));
when ALU_ADD =>
expected_result <= std_logic_vector(signed(a) + signed(b));
when ALU_SUB =>
expected_result <= std_logic_vector(signed(a) - signed(b));
end case;
end if;
end process;
-- When a result has been computed, it must be correct
assert always valid and has_run -> math_result = expected_result;
-- Eventually, a result will always be available
assert always enable_math -> eventually! valid;
-- Hints for induction
assert always not valid -> enable_math;
assert always not valid and (
operation = ALU_SHIFTL or
operation = ALU_SHIFTR_L or
operation = ALU_SHIFTR_A) -> not (or current_b(current_b'left downto 5));
end block;