Add information about formal verification

This commit is contained in:
Xiretza 2020-03-29 19:03:49 +02:00
parent e891568008
commit 3b65229eae
Signed by: xiretza
GPG key ID: E51A6C6A1EB378ED
4 changed files with 106 additions and 0 deletions

View file

@ -83,3 +83,9 @@
title = {RISC-V Compliance Task Group}, title = {RISC-V Compliance Task Group},
url = {https://github.com/riscv/riscv-compliance}, url = {https://github.com/riscv/riscv-compliance},
} }
@online{symbiyosys-slides,
author = {Clifford Wolf},
title = {Formal Verification withSymbiYosys and Yosys-SMTBMC},
url = {http://www.clifford.at/papers/2017/smtbmc-sby/slides.pdf},
}

View file

@ -50,6 +50,7 @@ The decoder receives an instruction and interprets it. Among others, it determin
The registers store the 32 general-purpose values required by \instrset{} (each 32-bit wide). They are accessible through two read ports and one write port. As specified by the RISC-V standard, the first register (\icode{x0}) is hard-wired to 0, and any writes to it are ignored. The registers store the 32 general-purpose values required by \instrset{} (each 32-bit wide). They are accessible through two read ports and one write port. As specified by the RISC-V standard, the first register (\icode{x0}) is hard-wired to 0, and any writes to it are ignored.
\section{Arithmetic and Logic Unit (ALU)} \section{Arithmetic and Logic Unit (ALU)}
\label{sec:core-alu}
\entityheader{alu} \entityheader{alu}

View file

@ -0,0 +1,81 @@
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;

View file

@ -181,4 +181,22 @@ The initial implementation of the compliance tests uncovered several bugs in the
\end{itemize} \end{itemize}
Since these tests are easily automated, they were added to the GitLab Continuous Integration (CI) configuration. Whenever a new git commit is pushed to GitLab, the tests are run automatically, and any failures are reported to the responsible committer via email. Since these tests are easily automated, they were added to the GitLab Continuous Integration (CI) configuration. Whenever a new git commit is pushed to GitLab, the tests are run automatically, and any failures are reported to the responsible committer via email.
\subsection{Formal Verification}
While carefully selected simulation is useful to uncover bugs and to ensure they can't happen again (regression testing), it never offers complete certainty - it is simply impossible to manually cover all possibilities of inputs. With formal verification, the circuit under test is expressed using a mathematical model and an algorithm (a \emph{SAT solver}) ensures that certain manually-selected criteria are always fulfilled. A detailed explanation of the algorithm can be found in~\cite{symbiyosys-slides}.
As an example of formal verification, the core's ALU (\autoref{sec:core-alu}) has been extended with a formal verification definition, which can be seen in \autoref{lst:alu-formal}. Skipping over some helper logic in the beginning, the first statements add assumptions about the entity's input signals. These are rules that must be obeyed by designs using the component, otherwise the correct function cannot be guaranteed (and is indeed unproven).
Below these assumptions, a process is used to calculate the expected result whenever a calculation is requested. While most operations are implemented the same as in the main entity and thus have little value as a known-good comparison value, the bit-shift operations are implemented incrementally in the main ALU and directly in the verification; thus, the less resource-intensive ALU implementation can be confirmed to function exactly like this more expensive method.
Afterwards, the first assertions actually happen: these are the theorems that the formal verification suite will prove to be correct. The only two proven statements that are actually relevant to users are that when a result has been computed, it will equal the value computed using the aformentioned process, and that a computation will always finish eventually.
Finally, two more assertions are used to give hints to the formal verification algorithm, specifically the induction step. It is sometimes very difficult or even impossible to arrive at a successful induction; these assertions can be proven trivially, eliminating a number of potential scenarios that would otherwise make a successful complete proof impossible.
\lstinputlisting[
style=vhdlstyle,
label={lst:alu-formal},
caption={Formal verification block for ALU},
]{alu_formal.vhd}
\end{document} \end{document}