But how can the formal model checker do its job?

Formal model checking is a tool which verifies your RTL model against zillions of input combinations, and tells you if any of them violate your specification.

We would like to verify this simple module

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity bin_to_7seg is
	port(
		clk_in: in std_logic;
		bin_in: in unsigned(3 downto 0);
		segs_out: out std_logic_vector(6 downto 0)
	);
end;

architecture rtl of bin_to_7seg is
	type seg_a is array(0 to 15) of std_logic_vector(6 downto 0);
	constant seg_c: seg_a := (
		"1111110", -- 0
		"0110000", -- 1
		"1101101", -- 2
		"1111001", -- 3
		"0110011", -- 4
		"1011011", -- 5
		"1011111", -- 6
		"1110000", -- 7
		"1111111", -- 8
		"1111011", -- 9
		"1110111", -- A
		"0011111", -- B
		"1001110", -- C
		"0111101", -- D
		"1001111", -- E
		"1000111" -- F
	);
	
	signal cnt: integer range 0 to 6 := 6;
begin
	process(clk_in)
		variable s: std_logic_vector(6 downto 0);
	begin
		if rising_edge(clk_in) then
			if cnt < 6 then
				cnt <= cnt + 1;
			end if;
			if cnt = 6 then
				cnt <= 0;
			end if;

			segs_out <= (others => '0');
			s := seg_c(to_integer(bin_in)); -- Needs to use variable to circumvet a bug in GHDL.
			segs_out(cnt) <= s(cnt);
		end if;
	end process;
end;

This module converts binary input to single digit hex output to be displayed on 7-segment LED display, and as a special feature it lights up maximum of one segment at any time.

The module can be converted to a schematic representation of asynchronous logic blocks (drawn as clouds) and DFFs (D-Flip-Flops).

This module is simple. For each clock cycle, it takes 4 bits of inputs and produces 7 bits of output. It has counter inside, which works as a simple state machine.

Now the schematic is simplified: All async clouds are combined as one, and all DFFs are combined as one (multibit) DFF.
Also a checker of our requirement is added. A cloud which detects if its seven input bits have at most one bit high, and produces zero if the rule is violated.

Let’s focus on the first 10 clock cycles after starting this module.
Each clock cycle we can select 1 or 0 to all of the four input bits.
During 10 clock cycles, we have 40 bits, which each needs to be selected to either 1 or 0.
The total number of combinations is about 1 trillion. We want to ensure that all of these combinations satisfy our requirement.
It is not enough to verify it by looking at source code for 15 minutes without interruption, but actually being sure that the requirement doesn’t break up in the first 10 clock cycles.

The trick needed at this moment, is to remove all DFFs from the design without changing its behaviour.

Now, instead of having one input, and clock driving the transition from one time to the next, we have separated each clock cycle’s input as a separate input, and also output at each clock cycle is separated to several outputs.
This module, when extended to 10 bin_in clock cycles, and 11 segs_out clock cycles, is an asynchronous logic representation of our original design for the first 10 clock cycles. It behaves exactly the same way as the original, but has no DFFs.
All the yellow boxes are inputs that should be permuted for all possible combinations.
All the red boxes are outputs to our model checking environment.
If all red boxes receive ones in each and every of the input permutations, then our module passes the requirement test. If not, then we have a design error.

And the catch being, asynchronous-only logic can be perfectly represented by boolean arithmetics.

Now we could (no need to do manually, as tools do the same) write an equation asking if any of these assert blocks receive zero. And if we did solve the equation, we would see which input combination (ones and zeroes in yellow boxes) indeed produce failing result.

And only by looking at the yellow boxes driving the initial values, we see that segs_out initial value can drive the $assert in the clock cycle #0 to any possible 7-bit combination. To avoid this, we need to fix the initial value of the output register in the design file.

Formal tool doing the same

Formal tool does the process almost the same way.

First it is given the VHDL RTL file of the module to be checked.
Then the requirement specification needs to specified.
For this we use PSL language.

PSL (subset of it) is synthesizable language, which is human readable description of the requirements for the design. This file is converted to a netlist of logic gates and DFFs, and a special cell named $assert.

Then the netlist is converted to internal representation where all DFFs are removed, and each clock cycle has its own version of inputs and $asserts.
This is then converted to a set of boolean equations (one for each $assert), trying to find if the $assert is receiving zero.
And these boolean equations are then converted to an industry standard boolean solver file format (SAT), which is sent to a SAT solver (there are several open source solvers).

If the solver cannot find solution to any of the equations, then we know our model behaves as expected for the first 10 (or whatever the tool is instructed to check) clock cycles.

PSL checker

VHDL-2008 standard allows PSL to be embedded within VHDL file.
We add the following lines after the process, and before the last end.

	default clock is rising_edge(clk_in);
	f_1: assert always {onehot0(segs_out)};

The first line states that every PSL checker is using clk_in as a clock unless otherwise specified.

The second line generates a violation checker (assert) stating that for every clock cycle (always) the condition (everything after always) needs to be true.

onehot0() is a function which returns false if the parameter vector has more than one bit high.

And this line is then synthesized to asynchronous checker logic and an $assert cell.

PSL language is rich in expression, and it has concept of clock cycles built it.
It can be used to create quite complicated checkers with very simple code.
And if something cannot be easily checked with PSL, then the checking can be extended by using synthesizable VHDL which provides helper signals to the PSL part.

Running open source formal checker in Docker

Symbiyosys is a collection of open source tools which allows you to verify your VHDL module using PSL language.

Copy the following code to a file named bin_to_7seg.vhdl

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity bin_to_7seg is
	port(
		clk_in: in std_logic;
		bin_in: in unsigned(3 downto 0);
		segs_out: out std_logic_vector(6 downto 0)
	);
end;

architecture rtl of bin_to_7seg is
	type seg_a is array(0 to 15) of std_logic_vector(6 downto 0);
	constant seg_c: seg_a := (
		"1111110", -- 0
		"0110000", -- 1
		"1101101", -- 2
		"1111001", -- 3
		"0110011", -- 4
		"1011011", -- 5
		"1011111", -- 6
		"1110000", -- 7
		"1111111", -- 8
		"1111011", -- 9
		"1110111", -- A
		"0011111", -- B
		"1001110", -- C
		"0111101", -- D
		"1001111", -- E
		"1000111" -- F
	);
	
	signal cnt: integer range 0 to 6 := 6;
begin
	process(clk_in)
		variable s: std_logic_vector(6 downto 0);
	begin
		if rising_edge(clk_in) then
			if cnt < 6 then
				cnt <= cnt + 1;
			end if;
			if cnt = 6 then
				cnt <= 0;
			end if;

			segs_out <= (others => '0');
			s := seg_c(to_integer(bin_in)); -- Needs to use variable to circumvent a bug in GHDL.
			segs_out(cnt) <= s(cnt);
		end if;
	end process;
	
	default clock is rising_edge(clk_in);
	f_1: assert always {onehot0(segs_out)};
end;

Copy the following code to a file named bin_to_7seg.sby

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 10

[engines]
bmc: smtbmc

[script]
ghdl --std=08 bin_to_7seg.vhdl -e bin_to_7seg
prep -top bin_to_7seg

[files]
bin_to_7seg.vhdl

Copy the following code to a file named bin_to_7seg.sh

#!/bin/bash

docker run -v $PWD:/formal -w /formal --rm -it --pull always hdlc/formal:all sby --yosys "yosys -m ghdl" -f bin_to_7seg.sby $@

Now open a terminal (WSL with Docker support or Linux with Docker installed) and run:

. bin_to_7seg.sh

You should get a result close to this:

$ . bin_to_7seg.sh
all: Pulling from hdlc/formal
Digest: sha256:ba97f107812547c0a1cc1ade30cdbcd0d6c42c33725d77d50187a3fe1eb015c1
Status: Image is up to date for hdlc/formal:all
SBY 18:52:52 [bin_to_7seg_bmc] Removing directory '/formal/bin_to_7seg_bmc'.
SBY 18:52:52 [bin_to_7seg_bmc] Copy '/formal/bin_to_7seg.vhdl' to '/formal/bin_to_7seg_bmc/src/bin_to_7seg.vhdl'.
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: smtbmc
SBY 18:52:52 [bin_to_7seg_bmc] base: starting process "cd bin_to_7seg_bmc/src; yosys -m ghdl -ql ../model/design.log ../model/design.ys"
SBY 18:52:52 [bin_to_7seg_bmc] base: bin_to_7seg.vhdl:48:35:note: found ROM "n23", width: 7 bits, depth: 16
SBY 18:52:52 [bin_to_7seg_bmc] base: s := seg_c(to_integer(bin_in)); -- Needs to use variable to circumvet a bug in GHDL.
SBY 18:52:52 [bin_to_7seg_bmc] base: ^
SBY 18:52:52 [bin_to_7seg_bmc] base: finished (returncode=0)
SBY 18:52:52 [bin_to_7seg_bmc] prep: starting process "cd bin_to_7seg_bmc/model; yosys -m ghdl -ql design_prep.log design_prep.ys"
SBY 18:52:52 [bin_to_7seg_bmc] prep: finished (returncode=0)
SBY 18:52:52 [bin_to_7seg_bmc] smt2: starting process "cd bin_to_7seg_bmc/model; yosys -m ghdl -ql design_smt2.log design_smt2.ys"
SBY 18:52:52 [bin_to_7seg_bmc] smt2: finished (returncode=0)
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: starting process "cd bin_to_7seg_bmc; yosys-smtbmc --presat --unroll --noprogress -t 250  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Solver: yices
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Assert failed in bin_to_7seg: f_1
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: ##   0:00:00  Status: failed
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: finished (returncode=1)
SBY 18:52:52 [bin_to_7seg_bmc] engine_0: Status returned by engine: FAIL
SBY 18:52:52 [bin_to_7seg_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:52:52 [bin_to_7seg_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:52:52 [bin_to_7seg_bmc] summary: engine_0 (smtbmc) returned FAIL
SBY 18:52:52 [bin_to_7seg_bmc] summary: counterexample trace: bin_to_7seg_bmc/engine_0/trace.vcd
SBY 18:52:52 [bin_to_7seg_bmc] summary:   failed assertion bin_to_7seg.f_1 at  in step 0
SBY 18:52:52 [bin_to_7seg_bmc] DONE (FAIL, rc=2)
SBY 18:52:52 The following tasks failed: ['bmc']

The checker is telling that the test failed on the first clock cycle (“BMC failed!” after “Checking assertions in step 0”).
This is the initial value on the segs_out register being uninitialized, which is violating our requirement on assert line.

You can open the waveform file to see what actually happened

gtkwave bin_to_7seg_bmc/engine_0/trace.vcd

We can see that the segs_out[6] and segs_out[5] were both high at the same time (your output might be different, but you can see at least two bits of segs_out being high).

Change the segs_out declaration to:

	segs_out: out std_logic_vector(6 downto 0) := (others => '0')

and run the checker again. Now it tests the design for the first 10 clock cycles and says “DONE (PASS, rc=0)” on the last line.

Now you should understand how the formal checker does its job.
Understanding is the key to success. Without it, you start guessing and in difficult subjects will guess the wrong way.

There is another design error in the module. Try to make a checker to find it.
Hint: as an assert you can write

f_2: assert always {cond_1 |=> cond_2};

Which synthesizes a checker to fail if cond_1 is seen as true in any clock cycle, but cond_2 is seen as false on the very next clock cycle. This is interpreted as an implication: cond_2 (being true) must follow (on next clock cycle) cond_1 (being true).