First Attempt at Formal Verification
My first proper attempt to use formal verification on an integer division operation.
I've recently been annoyed by the number of black box debug situations I have got myself into. Essentially problems where the testbench setup did not mimic real life closely enough in simulation. I do like to use OSVVM for constrained randomised testing, and find it quite brutal. But that testing still is not sufficient to catch all issues, evidently.
I've noted that formal verification was the chosen solution to Intel's FDIV bug in 1997. I had wondered about trying to recreate the lookup table based floating-point division issue that beset the radix-4 SRT division implementation Intel changed to when this bug was introduced to their processors (see jokes). i.e. Make the algorithm work, then setup formal verification, then degrade the lookup tables to show how formal verification identifies the bug. Perhaps one day I still will, but for now I think it ambitious enough to attempt to get something simpler working since I still need to learn how to specify the expected behaviour and work with the tools, all without a budget for commercial tools.
- Starting Point
- Why PSL?
- Training
- Lessons Learned
- Did It Find Any Flaws?
- Final Solution
- VHDL
- PSL
- Conclusions
- References
Starting Point
My initial reference is the excellent VHDL Whiz blog post Formal verification in VHDL using PSL. It provides:
- An initial introduction to formal verification in VHDL using PSL,
- Open Source tools (Yosys, GHDL and GTKwave) to use in the development process,
- Scripts to use them to get started,
- A worked AXI example1.
So my first task was to use their code as my "Hello World" example for formal verification and check I could install and use the tools. Being a Windows user at home, I had to install a virtual machine to run Linux on for the tools as part of this setup. This also necessitated setting up Samba for a Windows share to pass files between the host and the virtual machine.
Why PSL?
Property Specification Language (PSL) is a formal verification language that allows designers to specify properties of their hardware designs in a precise and unambiguous manner, e.g. using Sequential Extended Regular Expressions (SERE). Its a big topic and there's a standard for it, IEEE 1850-2010, with the active definition being IEC 62531:2012. With VHDL-2008, PSL is integrated into the language rather than being something of an add-on.
Training
I asked Doulos about the availability of training for PSL with VHDL for formal verification given they have some on-line resources, The Structure of PSL. They replied that there is no demand for the courses and they offer SystemVerilog Assertions instead. Whilst learning formal verification and PSL adds to the training burden, moving to SVA feels like a much bigger diversification in total. I have found some paid training resources available on EDA Academy. Otherwise you will be left gleaning what you can from volunteered resources found by your favourite search engine as I have done here.
Lessons Learned
So the first lesson learned is that VHDL-2008's use of PSL might be struggling for widespread adoption!
Simulation with test benches remains essential, or the function you are creating will not get developed. You also need it for debuging formal verification results.
Assertion-based verification is a helpful way to develop the initial PSL code. The assertion signals created can usefully be added to the wave window to see how the PSL is being evaluated.
I spent an age learning how to specify PSL and trying to understand how the traces in GTKwave had been crafted by the FV checker. I dropped the exercise several times and returned at a much later date. I started in December 2024 with Assertion-based Verification in Intel's Free QuestaSim, wrote the division VHDL in November 2025, and finally got the PSL to work with bounded model checking (BMC) and induction by August 2026.
A reset signal adds complication.
Keeping the PSL code separate to the RTL code feels like a good way to proceed as it separates concerns and avoids distractions.
BMC is easier to satisfy than induction. The Internet reports that induction often fails due to unreachable states, and you might start up in one. The problem now shifts to figuring out which PSL to specify to resolve the issue, coupled with finding a subset of PSL that also works with assertion based verification. QuestaSim seems to have a limit here. This led to a significant amount of searching around for different ways to specify that the finished output was assert n clock cycles after the start input was asserted.
| PSL keyword | GHDL | QuestaSim 2023.3 |
|---|---|---|
| assert | Y | Y |
| assume | Y | Y |
| restrict | Y | N2 |
| cover | Y | Y |
2 Might be a version issue as Gemini AI says it is supported, but I can't find a reference. Might be VHDL's flavour of PSL is a limit?
Did It Find Any Flaws?
Yes. The testbench made an assumption about the inputs not changing after start being asserted as follows:
Formal verification found this flaw in the testing.
As a consequence, the following RTL code change became necessary:
if dividend(dividend'high) /= divisor(divisor'high) then
quotient <= resize(signed('0' & quotientu) * to_signed(-1, 2), quotient'length);
else
quotient <= signed('0' & quotientu);
end if;
if dividend(dividend'high) = '1' then
remainder <= resize(signed('0' & remainderu) * to_signed(-1, 2), remainder'length);
else
remainder <= signed('0' & remainderu);
end if;
The sign bits needed to be save from when start was asserted.
-- Need to remember these in case the inputs change after start asserted
if start = '1' then
negq <= dividend(dividend'high) xor divisor(divisor'high);
negd <= dividend(dividend'high);
end if;
if negq = '1' then
quotient <= resize(signed('0' & quotientu) * to_signed(-1, 2), quotient'length);
else
quotient <= signed('0' & quotientu);
end if;
if negd = '1' then
remainder <= resize(signed('0' & remainderu) * to_signed(-1, 2), remainder'length);
else
remainder <= signed('0' & remainderu);
end if;
Final Solution
VHDL
--
-- {quotient, remainder}
-- -----------
-- divisor ) dividend
--
-- NB. remainder = dividend - (divisor x quotient)
--
-- Worked example:
-- Reference: https://web.ece.ucsb.edu/~parhami/pres_folder/f31-book-arith-pres-pt4.pdf
--
-- 117 / 10 = 11 rem 7
-- +10 = 01010
-- -10 = 10110
--
-- SDDDD
-- 01110101 117
-- ---------------
-- 01110101 2x
-- + 10110 -10
-- ---------------
-- x00100101 +ve => q(3) <= '1'
-- ---------------
-- 01001010 2x
-- + 10110 -10
-- ---------------
-- x1111101 -ve => q(2) <= '0'
-- ---------------
-- 111101 2x
-- + 01010 +10
-- ---------------
-- x010001 +ve => q(1) <= '1'
-- ---------------
-- 10001 2x
-- + 10110 -10
-- ---------------
-- 00111 +ve => q(0) <= '1' + remainder = 7
-- q = "1011" quotient = 11
--
--
-- Re-worked example:
--
-- 117 / 10 = 11 rem 7
-- +10 = 01010
-- -10 = 10110
--
-- 01110101 117
-- + 10110 -10
-- ---------------
-- x00100101 +ve => q(3) <= '1'
-- ---------------
-- 0100101
-- + 10110 -10
-- ---------------
-- x1111101 -ve => q(2) <= '0'
-- ---------------
-- 111101
-- + 01010 +10
-- ---------------
-- x010001 +ve => q(1) <= '1'
-- ---------------
-- 10001
-- + 10110 -10
-- ---------------
-- 00111 +ve => q(0) <= '1' + remainder = 7
-- q = "1011" quotient = 11
--
-- Note this requires the arithmetic to be 8-bits instead of 5-bits.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity unsigned_division is
generic (
dividend_width_g : positive;
divisor_width_g : positive
);
port (
clk : in std_logic;
reset : in std_logic;
dividend : in unsigned(dividend_width_g-1 downto 0); -- numerator
divisor : in unsigned(divisor_width_g-1 downto 0); -- denominator
start : in std_logic;
quotient : out unsigned(dividend_width_g-1 downto 0); -- result
remainder : out unsigned(divisor_width_g-1 downto 0);
finished : out std_logic
);
end entity;
architecture rtl of unsigned_division is
constant zeros : unsigned(dividend_width_g-1 downto 0) := (others => '0');
signal enable : std_logic;
signal count : natural range 0 to dividend_width_g-1;
signal divisor_r : unsigned(divisor_width_g-1 downto 0);
begin
process(clk)
variable temp : unsigned(divisor_width_g+dividend_width_g downto 0);
begin
if rising_edge(clk) then
if reset = '1' then
enable <= '0';
finished <= '0';
count <= 0;
quotient <= (others => '0');
remainder <= (others => '0');
else
-- Default values
finished <= '0';
if enable = '0' then
if start = '1' then
count <= dividend_width_g-1;
remainder <= (others => '0');
quotient <= dividend;
enable <= '1';
divisor_r <= divisor;
end if;
else
-- Trial subtraction
temp := (remainder(remainder'high downto 0) & quotient & '0') - ('0' & divisor_r & zeros);
if temp(temp'high) = '1' then -- < 0
-- Just shift left
(remainder, quotient) <= remainder(remainder'high-1 downto 0) & quotient & '0';
else
-- Shift left and subtract, the top bit will be '0'.
(remainder, quotient) <= temp(temp'high-1 downto 1) & '1';
end if;
if count = 0 then
enable <= '0';
finished <= '1';
else
count <= count - 1;
end if;
end if;
end if;
end if;
end process;
end architecture;
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity signed_division is
generic (
dividend_width_g : positive;
divisor_width_g : positive
);
port (
clk : in std_logic;
reset : in std_logic;
dividend : in signed(dividend_width_g-1 downto 0); -- numerator
divisor : in signed(divisor_width_g-1 downto 0); -- denominator
start : in std_logic;
quotient : out signed(dividend_width_g-1 downto 0); -- result
remainder : out signed(divisor_width_g-1 downto 0);
finished : out std_logic
);
end entity;
architecture rtl of signed_division is
signal dividendu : signed(dividend_width_g-1 downto 0);
signal divisoru : signed(divisor_width_g-1 downto 0);
signal quotientu : unsigned(dividend_width_g-2 downto 0);
signal remainderu : unsigned(divisor_width_g-2 downto 0);
signal finishedu : std_logic;
signal negq : std_logic;
signal negd : std_logic;
begin
-- "10..00" => "0..00" when converted to unsigned as it has one less value in the natural range.
assert to_integer(dividend) /= -2**(dividend_width_g-1)
report "signed_division: No unsigned natural to match dividend = " & to_string(to_integer(dividend))
severity error;
assert to_integer(divisor) /= -2**(divisor_width_g-1)
report "signed_division: No unsigned natural to match divisor = " & to_string(to_integer(divisor))
severity error;
dividendu <= abs(dividend);
divisoru <= abs(divisor);
unsigned_division_i : entity work.unsigned_division
generic map (
dividend_width_g => dividend_width_g-1,
divisor_width_g => divisor_width_g-1
)
port map (
clk => clk,
reset => reset,
dividend => unsigned(dividendu(dividend'high-1 downto 0)),
divisor => unsigned(divisoru(divisor'high-1 downto 0)),
start => start,
quotient => quotientu,
remainder => remainderu,
finished => finishedu
);
process(clk)
begin
if rising_edge(clk) then
if reset = '1' then
quotient <= (others => '0');
remainder <= (others => '0');
finished <= '0';
negq <= '0';
negd <= '0';
else
finished <= finishedu;
-- Need to remember these in case the inputs change after start asserted
if start = '1' then
negq <= dividend(dividend'high) xor divisor(divisor'high);
negd <= dividend(dividend'high);
end if;
if negq = '1' then
quotient <= resize(signed('0' & quotientu) * to_signed(-1, 2), quotient'length);
else
quotient <= signed('0' & quotientu);
end if;
if negd = '1' then
remainder <= resize(signed('0' & remainderu) * to_signed(-1, 2), remainder'length);
else
remainder <= signed('0' & remainderu);
end if;
end if;
end if;
end process;
end architecture;
PSL
vunit i_signed_division(signed_division(rtl)) {
-- Set all declarations to run on clk
default clock is rising_edge(clk);
----------------------------------------------------
-- Reset
----------------------------------------------------
-- Assume reset at startup only. NB. Cannot use 'restrict' here for tool support reasons.
initial_reset : assume {reset[+];not reset[+]};
reset_start : assume (reset -> not start);
o_reset : assert (always {reset} |=> {
(to_integer(quotient) = 0) and
(to_integer(remainder) = 0) and
(finished = '0')
});
----------------------------------------------------
-- Division
----------------------------------------------------
signal quotient_psl : integer := 0;
signal remainder_psl : integer := 0;
process(clk)
begin
if rising_edge(clk) then
if start = '1' then
quotient_psl <= to_integer(dividend) / to_integer(divisor);
remainder_psl <= to_integer(dividend) rem to_integer(divisor);
end if;
end if;
end process;
-- A start pulse should be only one clock cycle long, and stay low until finished
-- dividend'length+1 clock cycles later.
start_pulse : assume (always {start and not reset} |=> {
((not start) and (not finished))[*7];
(not start) and finished
});
-- Never divide by zero
divide_by_zero : assume (never ((to_integer(divisor) = 0) and (start = '1') and (reset = '0')));
-- "10..00" => "0..00" when converted to unsigned as it has one less value in the natural range.
maxneg_dividend : assume (never (to_integer(dividend) = -2**(dividend_width_g-1)));
maxneg_divisor : assume (never (to_integer(divisor) = -2**(divisor_width_g-1)));
-- Get the right answer when finished
o_div : assert always (finished and not reset -> {
(to_integer(quotient) = quotient_psl) and
(to_integer(remainder) = remainder_psl)
});
}
Conclusions
Formal verification is hard work, well perhaps when getting started and learning it? It does find flaws. With initial experiments it found a flaw in some AXI signalling that OSVVM did not find. As I previous mentioned, I thought OSVVM could be brutal. I also tried formal verification on some of my son's early floating point arithmetic code. The code did work as expected, but the RTL had not yet been amended to cope with the rounding required for the IEEE 754 standard. Formal verification found the mathematical differences and I was impressed given the search space. So formal verification feels like something worth investing in, but the steep learning curve and expensive commercial tools might be a barrier to adoption in the work place.
References
- Github Source Code - Coming soon!
- Formal verification in VHDL using PSL by VHDL Whiz.
- The Structure of PSL by Doulos.
- The implication operators in PSL and SVA by Liam McSherry.
- My Personal Journey in Verification by Gisselquist Technology.