Formal Verification of DPRAM and LRU Algorithm of Cache
June 5, 2021
I am delighted to work with the OpenRISC community as part of the FOSSi Foundation as I will contribute to the Mor1kx CPU in its formal verification. I had outlined the tasks of verification stages and my project flow for formal verification, which I have planned to complete in my previous blog. In this blog, I will elaborate on different formal methods that I could use in my project, and a sneak peek of my work.
This project is entirely dependent on Yosys tools, specifically SymbiYosys and Yosys-smtbmc. What does Yosys-smtbmc do? It applies formal methods to our code and mathematically proves that code works. If not, the solvers tell us where the code might fail.
BMC and Induction
Before getting into the tool, it's essential to understand some terminologies like Bounded Model Check (BMC) and Induction. BMC is the first step in Yosys-smtbmc theorem solving. Here, the solver starts with the initial state of the design and explores all the other states that it can encounter during its transitions. This method is bounded because it is time-limited and checks only a finite number of transitions.
To find out additional states, we follow the Induction step. It's just like mathematical Induction, where we first consider base case n=1 and prove that. Later, we check for n states and finally n+1. BMC is like a base case for k-induction.
Formal Declarations
For any formal verification, basic operations like assert, assume, restrict and cover play a vital role. For a design, we need to assert some conditions to check if that holds for the design. If the design fails, it may be because the code fails or a flaw in the assertion. It is recommended to assert statements carefully.
To formally verify, do I need to understand the code? Definitely yes! Without knowing the code, it's impossible to assert conditions. Having an excellent exposure to design and its environment would help declare assertions quickly. We can also add constraints to the design space by including assume statements in the code.
With this basic idea, it's good to move ahead with Yosys formal. I have started my project earlier and have verified tiny modules like simple DPRAM, true DPRAM, and the least recently used algorithm. These modules are part of the instruction cache, data cache, and memory management unit.
Formally Verifying Mor1kx’s DPRAM, LRU Algorithm
Mor1kx cache memory uses DPRAM to store its contents. The Instruction cache/Data cache is simple DPRAM based, and the MMU is true DPRAM based.
Simple DPRAM
To check simple dpram’s correctness, I need to verify a few properties based on its code.
- Data on the output port changes only if read enable is high.
- If bypass is enabled, write data should forward data to the output port, given both write and read addresses are the same
- Verifying read or write operation on memory.
Here, is the complete formal section of simple dpram.
`ifdef SDPRAM
reg f_written;
initial f_written = 0;
//Writing f_data at address f_addr
always @(posedge clk)
if (f_past_valid && $past(we) && $past(waddr) == f_addr && !ENABLE_BYPASS && $past(din) == f_data)
f_written <= 1;
//Read access for address f_addr should return f_data
always @(posedge clk)
if (f_past_valid && $past(re) && $past(raddr) == f_addr && !ENABLE_BYPASS && $rose(f_written))
assert (dout == f_data);
`endif
//Verifying Bypass logic of SDPRAM
always @(posedge clk)
if (f_past_valid && $past(we) && $past(re) && $past(waddr) == f_addr && $past(raddr) == f_addr && ENABLE_BYPASS)
assert (dout == $past(din));
//Output data should remain unchanged if there is no read enable
always @(posedge clk)
if (f_past_valid && !$past(re))
assert ($stable(dout));
//Output data changes only if there is read or write enable
always @(posedge clk)
if (f_past_valid && $changed(dout))
assert ($past(re) | $past(we));
`endif
After adding formal declarations to the source file, the very next step is to configure the SBY file.
Different values for parameters ENABLE_BYPASS can be set using tasks in the SBY file. Under options, the mode of testing has to be specified along with the depth of iterations. Yosys supports solvers like z3, yices, boolector, etc for the smtbmc engine. If not specified, then the smtbmc engine picks any of the above solvers. One last step is to add design files and script specifying the top module. On running the SBY file, one would get to know what's the result of verification.
[tasks]
BYPASS bypass
NO_BYPASS no_bypass
[options]
mode prove
depth 20
wait on
[engines]
smtbmc yices
[script]
read -formal -D SDPRAM mor1kx_simple_dpram_sclk.v
--pycode-begin--
cmd = "hierarchy -top mor1kx_simple_dpram_sclk"
cmd+= " -chparam ENABLE_BYPASS %d" % (1 if "bypass" in tags else 0)
output(cmd)
--pycode-end--
prep -top mor1kx_simple_dpram_sclk
[files]
../../rtl/verilog/mor1kx_simple_dpram_sclk.v
True DPRAM
True DPRAM’s properties are somewhat similar to simple DPRAM but use two clocks, one for each port. I have used a global clock to handle two clocks A and B. At the posedge of clk_a or clk_b read and write operations of that port are verified.
reg f_write_a;
initial f_write_a = 0;
reg f_write_b;
initial f_write_b = 0;
always @(posedge global_clock) begin
if ($rose(clk_a)) begin
//Port A: Writing f_data_a at address f_addr
if ($past(we_a) && $past(addr_a) == f_addr && $past(din_a) == f_data_a && f_past_valid) begin
assert (dout_a == f_data_a);
f_write_a <= 1;
end
//Port A: Reading data from address f_addr
if (!$past(we_a) && $past(addr_a) == f_addr && f_past_valid && $rose(f_write_a))
assert (dout_a == f_data_a);
end
if ($rose(clk_b)) begin
//Port B: Writing f_data_b at address f_addr
if ($past(we_b) && $past(addr_b) == f_addr && $past(din_b) == f_data_b && f_past_valid) begin
assert (dout_b == f_data_b);
f_write_b <= 1;
end
//Port B: Writing f_data_b at address f_addr
if (!$past(we_b) && $past(addr_b) == f_addr && f_past_valid && $rose(f_write_b))
assert (dout_b == f_data_b);
end
end
`endif
//Port A output data changes only if there is read or write access at port A
always @(posedge clk_a)
if (f_past_valid && $changed(dout_a))
assert ($past(we_a) | !$past(we_a));
//Port B output data changes only if there is read or write access at port B
always @(posedge clk_b)
if (f_past_valid && $changed(dout_b))
assert ($past(we_b) | !$past(we_b));
//Port B shouldn't be affected by write signals of port A
always @(posedge global_clock)
if (f_past_valid && $rose(clk_a) && $fell(clk_b) && $past(we_a))
assert ($stable(dout_b));
//Port A shouldn't be affected by write signals of port B
always @(posedge global_clock)
if (f_past_valid && $rose(clk_b) && $fell(clk_a) && $past(we_b))
assert ($stable(dout_a));
`endif
endmodule
LRU algorithm
Having verified DPRAM, I moved onto the least recently used algorithm which is used to replace the least recently used block from cache. This is a fully combinational design module so it's much easier to verify.
First, I assumed that inputs to variable access are one-hot encoded just to avoid random inputs that solvers might consider. Since this is an algorithm, I tried to verify its outcomes and asserted if the lru_pre (before access) and lru_post (after access) are also one-hot encoded.
/*-----Formal Checking-------*/
`ifdef FORMAL
always @(*) begin
assert (NUMWAYS > 1);
assume ($onehot0(access));
assert ($onehot(lru_pre));
assert ($onehot(lru_post));
end
`endif
We have seen that all the properties I have tested on Mor1kx's DPRAM and LRU algorithm are satisfied. Now, I will be moving on to the instruction cache verification. For the upcoming week, I plan to verify the Instruction memory management unit and Instruction fetch modules. I am hoping to find some interesting parts of Mor1kx there.