82 lines
2.1 KiB
VHDL
82 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;
|