Your first example
Let’s do our first example!
We will explain some things as we go, so let’s dive in :)
The design: a simple VHDL counter
We want to formally verify a simple VHDL counter, whose code is as follows:
library IEEE;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity counter is
generic ( MAX_COUNT : integer := 128 );
port ( clk: in std_logic;
rst: in std_logic;
Q: out unsigned(7 downto 0)
);
end counter;
architecture behavioral of counter is
signal count: unsigned(7 downto 0);
signal n_count: unsigned(7 downto 0);
begin
sinc: process(clk, rst)
begin
if (rst='1') then
count <= (others=>'0');
elsif (rising_edge(clk)) then
count <= n_count;
end if;
end process;
comb: process(count)
begin
if (count = MAX_COUNT) then
n_count <= (others => '0');
else
n_count <= count + 1;
end if;
end process;
Q <= count;
end behavioral;
Save this file as counter.vhd
Writing the formal.py script
Now, let’s write the formal.py script for the FVM framework!
We write the first version of the script before having the properties, this way we can start leveraging the automatic formal tools even when we haven’t written a single PSL line.
from fvm import FvmFramework
fvm = FvmFramework()
fvm.add_vhdl_source("counter.vhd")
fvm.set_toplevel("counter")
fvm.run()
Running the formal tools
Running the FVM steps using the FVM Framework is as easy as running the
formal.py script:
python3 formal.py
Note
Make sure you have the FVM installed and the venv, if needed, activated.
See the Installation section for details.
Since we haven’t written any properties, we will just see the results of running the automated tools over our design. For each of the FVM steps you will see any warnings and errors given by the relevant tool and a summary of the step. After all the steps run you will see a final summary that will look like this:
FVM Summary: counter ┏━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━┳━━━━━━━━━━━━━━┓ ┃ status ┃ step ┃ results ┃ elapsed time ┃ ┡━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━╇━━━━━━━━━━━━━━┩ │ pass │ lint │ ok │ 10 seconds │ │ pass │ friendliness │ 99.30% │ 10 seconds │ │ pass │ rulecheck │ ok │ 15 seconds │ │ pass │ xverify │ 2I │ 11 seconds │ │ pass │ reachability │ 100.0% │ 14 seconds │ │ pass │ resets │ ok │ 14 seconds │ │ pass │ clocks │ ok │ 20 seconds │ │ pass │ prove │ │ 18 seconds │ │ │ Assumes │ 0 │ │ │ │ Asserts │ 0 │ │ │ │ Covers │ 0 │ │ │ fail │ prove.formalcover │ N/A │ 5 seconds │ │ pass │ prove.simcover │ N/A │ N/A │ └────────┴───────────────────────────┴─────────┴──────────────┘ pass 9 of 10 fail 1 of 10 ─────────────────────────────────────────────────────────────── Total time: 2 minutes, 1 seconds
Let’s explain the results:
lint: Result isok, no issues detected.friendliness: The design has a very high formal-friendliness score, which makes it very suitable for formal verification.rulecheck:ok, no issues detected.xverify: Result is2I. If we scroll up to see the summary of the step, we’ll notice thatImeans Incorruptible in this case, which is equivalent to a warning and means thatXvalues can appear in a signal, but they will not propagate. The user can always consult the documentation of the relevant tool (in this case Questa X-Check) for more detailed information.reachability: 100% of the design is reachable, which is good news.resets:ok, no Reset Domain Crossing issues detected.clocks:ok, no Clock Domain Crossing issues detected.prove: Since we haven’t written any properties yet, there are no assumptions, no assertions and no cover statements.prove.formalcover: This post-step fails, since formal coverage cannot be computed if there are no properties. That is the reason why its result is alsoN/A. If we scroll up to see the results of the post-step, we will see the following error message:ERROR detected in step='prove.formalcover', tool='propcheck', line='# Fatal : No proven/inconclusive properties found for formal coverage computation. [formal-414]'
prove.simcover: This post-step doesn’t run any simulation since there are neither falling assertions nor reached cover directives. Its result is alsoN/A
So, everything seems to work fine but, as expected, we need some properties to
correctly run the prove steps and its sub-steps.
Writing the properties
Now that we know how to run the FVM, let’s write the properties for the counter!
We will write the following to a file named counter_properties.psl
See also
In formal verification, we use three main keywords when writing properties:
assume, assert and cover. See the Assert/assume/cover section for
more information.
In PSL, we write Verification Units, and we do that using the vunit keyword
(not to be confused with the VUnit test framework). These vunits are binded
to either an VHDL entity (if we only need to work with the ports of the entity)
or to an VHDL entity and architecture pair (when we also need to work with the
internal signals of the entity). In this case, we can just bind the vunit
with the properties, named counter_properties, to the entity counter:
vunit counter_properties (counter) {
The first step is to specify the default clock domain to use, to avoid having to include the clock domain in every property. This is highly recommended for designs with a single clock:
-- Default clock for PSL assertions
default clock is rising_edge(clk);
Now, let’s write our first assumption. In formal verification, a reset is
usually required in the first cycle to limit the number of possible initial
states. Although many tools automatically infer this, it is good practice to
explicitly write it for portability between toolchains. So, we will assume
that, on the first clock cycle, our counter is being reset:
-- Force a reset in the first clock cycle
-- Since we don't have an 'always', this assumption only applies to the
-- first clock cycle
assume_initial_reset: assume rst = '1';
Since no assumptions are needed for the rest of the counter inputs, we can start writing assertions.
The following property will assert that the counter output will never
exceed the counter’s maximum count, i.e. the property will fail if overflows
occur. This property is similar to firewall assertions in simulation: it is
not checking for the full expected correct functionality but is checking for
error conditions instead. These kind of properties are very useful for quickly
finding counterexamples when there is an error in the design:
-- Assert we do not go over the maximum
never_go_over_the_maximum: assert always (Q <= MAX_COUNT);
Now we’ll write 3 properties that do actually check the functionality of the
design. The first one will assert that a reset clears the count, the
second one will assert that if the count has not reached the maximum, it
increases by 1 (provided there has not been a reset, due to abort rst) and
the third one will assert that if it has reached the maximum, it returns to
0 (provided there has not been a reset).
-- Assert the count is cleared on reset
reset_clears_count: assert always ({rst = '1'} |=> {Q = 0});
-- Assert the count increments when not at maximum
-- Note that `abort rst` at the end of the assertion avoids checking
-- the property when reset is active
count_increments: assert always ({Q /= MAX_COUNT} |=> {Q = prev(Q) + 1}) abort rst;
-- Assert the count overflows when at maximum
count_overflow: assert always ({Q = MAX_COUNT} |=> {Q = 0}) abort rst;
To complement the assertions, it’s always helpful to have cover directives:
each one will generate a trace of the design covering the specified scenario,
or will result in a proof that it cannot be covered. For this design, covering
the overflow to zero is enough; this way, we’ll see how the counter reaches the
maximum count without having to write any simulation testbench. Additionally,
we can also cover the case when the design is reset, to see its behavior
when suddenly reset:
-- Cover the overflow -> zero case
-- What we write here has to be a sequence inside curly braces {}, even if
-- we only have one element, for example, { Q = MAX_COUNT }
cover_overflow_to_zero: cover {Q = MAX_COUNT ; Q = 0};
-- Same as above but adding reset behavior.
cover_overflow_to_zero_and_reset: cover {Q = MAX_COUNT ; Q = 0; [*]; rst = '1'; [*]; Q = MAX_COUNT ; Q = 0};
Since we have finished writing the properties, we must just make sure that we
are closing the vunit:
}
The full counter_properties.psl should look like this:
vunit counter_properties (counter) {
-- Default clock for PSL assertions
default clock is rising_edge(clk);
-- Assert we do not go over the maximum
never_go_over_the_maximum: assert always (Q <= MAX_COUNT);
-- Assert the count is cleared on reset
reset_clears_count: assert always ({rst = '1'} |=> {Q = 0});
-- Assert the count increments when not at maximum
-- Note that `abort rst` at the end of the assertion avoids checking
-- the property when reset is active
count_increments: assert always ({Q /= MAX_COUNT} |=> {Q = prev(Q) + 1}) abort rst;
-- Assert the count overflows when at maximum
count_overflow: assert always ({Q = MAX_COUNT} |=> {Q = 0}) abort rst;
-- Cover the overflow -> zero case
-- What we write here has to be a sequence inside curly braces {}, even if
-- we only have one element (for example, { Q = MAX_COUNT }
cover_overflow_to_zero: cover {Q = MAX_COUNT ; Q = 0};
cover_overflow_to_zero_and_reset: cover {Q = MAX_COUNT ; Q = 0; [*]; rst = '1'; [*]; Q = MAX_COUNT ; Q = 0};
-- Force a reset in the first clock cycle
-- Since we don't have an 'always', this assumption only applies to the
-- first clock cycle
assume_initial_reset: assume rst = '1';
}
Adding the properties to formal.py
By just adding a line to formal.py, we can add the properties and start using the steps with non-automated formal tools.
from fvm import FvmFramework
fvm = FvmFramework()
fvm.add_vhdl_source("counter.vhd")
fvm.add_psl_source("counter_properties.psl", flavor="vhdl")
fvm.set_toplevel("counter")
fvm.run()
Running the formal tools again
Finally, let’s run our formal.py script again!
python3 formal.py
Now, our results are better:
FVM Summary: counter ┏━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━┳━━━━━━━━━━━━━━┓ ┃ status ┃ step ┃ results ┃ elapsed time ┃ ┡━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━╇━━━━━━━━━━━━━━┩ │ pass │ lint │ ok │ 13 seconds │ │ pass │ friendliness │ 99.30% │ 11 seconds │ │ pass │ rulecheck │ ok │ 15 seconds │ │ pass │ xverify │ 2I │ 13 seconds │ │ pass │ reachability │ 100.0% │ 16 seconds │ │ pass │ resets │ ok │ 19 seconds │ │ pass │ clocks │ ok │ 20 seconds │ │ pass │ prove │ │ 17 seconds │ │ │ Assumes │ 1 │ │ │ │ Asserts │ 4 │ │ │ │ └ Proven │ 4/4 │ │ │ │ Covers │ 2 │ │ │ │ └ Covered │ 2/2 │ │ │ pass │ prove.formalcover │ 100.0% │ 5 seconds │ │ pass │ prove.simcover │ 100.0% │ 14 seconds │ └────────┴───────────────────────────┴─────────┴──────────────┘ pass 10 of 10 ─────────────────────────────────────────────────────────────── Total time: 2 minutes, 27 seconds
In the prove step we can see that, as we have written, we have 1
assumption, 4 assertions which have been proven, and 2 covers that have been
covered.
Also, our formal code coverage (code observed by our properties) and our
simulation code coverage (code executing by simulating the covered cover
statements) are both 100%
With a small number of lines of code we have fully formally verified an 8-bit counter, which testifies to how powerful formal verification is. Formal verification can tackle even bigger designs, so continue reading to learn more!