From d94585cad811ac0f55d4ce499f09b1a1f07134e7 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Tue, 24 Mar 2020 14:32:54 +0100 Subject: [PATCH] Making counter design work with GHDL synthesis * Remove unused SVA properties file * Makefile optimizations * Use prep auto-top option to prevent error with not founded top-level module when using generics * Add some simple PSL assertions --- README.md | 2 +- counter/Makefile | 12 ++++++--- counter/counter.vhd | 37 ++++++++++++++++++++++++- counter/counter_f.sby | 17 ------------ counter/counter_t.sv | 61 ------------------------------------------ counter/symbiyosys.sby | 22 +++++++++++++++ 6 files changed, 67 insertions(+), 84 deletions(-) delete mode 100644 counter/counter_f.sby delete mode 100644 counter/counter_t.sv create mode 100644 counter/symbiyosys.sby diff --git a/README.md b/README.md index a369fbd..3e584a8 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ It is mirrored to github with every push, so both should be in sync. Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog frontend plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. -There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/ghdlsynth-beta) as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. Only the vai_reg design can be verified in this branch at the moment. +There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/ghdlsynth-beta) as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. The alu, counter & vai_reg designs can be verified in this branch at the moment. ### alu A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool. diff --git a/counter/Makefile b/counter/Makefile index f7c4eba..17c6e5c 100644 --- a/counter/Makefile +++ b/counter/Makefile @@ -1,7 +1,11 @@ -.PHONY: counter -counter: counter.vhd counter_t.sv counter_f.sby - sby -f -d work counter_f.sby +DUT := counter + +.PHONY: cover bmc prove all clean + +all: cover bmc prove + +cover bmc prove: ${DUT}.vhd symbiyosys.sby + sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@ -.PHONY: clean clean: rm -rf work diff --git a/counter/counter.vhd b/counter/counter.vhd index 7169ad2..1f7ef49 100644 --- a/counter/counter.vhd +++ b/counter/counter.vhd @@ -7,7 +7,8 @@ use ieee.numeric_std.all; entity counter is generic ( InitVal : natural := 0; - EndVal : natural := 64 + EndVal : natural := 16; + Formal : boolean := true ); port ( Reset_n_i : in std_logic; @@ -36,5 +37,39 @@ begin end process; + FormalG : if Formal generate + + signal s_data : unsigned(Data_o'range); + + begin + + -- VHDL helper logic + process is + begin + wait until rising_edge(Clk_i); + s_data <= unsigned(Data_o); + end process; + + default clock is rising_edge(Clk_i); + + -- Initial reset + INITIAL_RESET : restrict {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1]; + + AFTER_RESET : assert always + not Reset_n_i -> Data_o = (Data_o'range => '0'); + + COUNT_UP : assert always + Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data + 1; + + END_VALUE : assert always + unsigned(Data_o) = to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data; + + VALID_RANGE : assert always + unsigned(Data_o) >= to_unsigned(InitVal, 32) and + unsigned(Data_o) <= to_unsigned(EndVal, 32); + + end generate FormalG; + + end architecture rtl; diff --git a/counter/counter_f.sby b/counter/counter_f.sby deleted file mode 100644 index 6179f6e..0000000 --- a/counter/counter_f.sby +++ /dev/null @@ -1,17 +0,0 @@ -[options] -mode prove -depth 30 -wait on - -[engines] -smtbmc -abc pdr - -[script] -verific -vhdl counter.vhd -verific -formal counter_t.sv -prep -top counter_t - -[files] -counter.vhd -counter_t.sv diff --git a/counter/counter_t.sv b/counter/counter_t.sv deleted file mode 100644 index c62b76a..0000000 --- a/counter/counter_t.sv +++ /dev/null @@ -1,61 +0,0 @@ -module counter_t ( - input Reset_n_i, - input Clk_i, - output [31:0] Data_o -); - - - `define INITVAL 8 - `define ENDVAL 64 - - - counter #( - .InitVal(`INITVAL), - .EndVal(`ENDVAL) - ) counter_i ( - .Reset_n_i(Reset_n_i), - .Clk_i(Clk_i), - .Data_o(Data_o) - ); - - - reg init_state = 1; - (* gclk *) wire gbl_clk; - - // Initial reset - always @(*) begin - if (init_state) assume (!Reset_n_i); - if (!init_state) assume (Reset_n_i); - end - - always @(posedge Clk_i) - init_state = 0; - - // Generate global clock - global clocking - @(posedge gbl_clk); - endclocking - - // Use global clock to constrain the DUT clock - always @($global_clock) begin - assume (Clk_i != $past(Clk_i)); - end - - default clocking - @(posedge Clk_i); - endclocking - - default disable iff (!Reset_n_i); - - // Immediate assertions - always @(*) - if (!Reset_n_i) assert (Data_o == `INITVAL); - - // Concurrent assertions - assert property (Data_o < `ENDVAL |=> Data_o == $past(Data_o) + 1); - assert property (Data_o == `ENDVAL |=> $stable(Data_o)); - assert property (Data_o >= `INITVAL && Data_o <= `ENDVAL); - - -endmodule - diff --git a/counter/symbiyosys.sby b/counter/symbiyosys.sby new file mode 100644 index 0000000..b05f40b --- /dev/null +++ b/counter/symbiyosys.sby @@ -0,0 +1,22 @@ +[tasks] +cover +bmc +prove + +[options] +depth 25 +cover: mode cover +bmc: mode bmc +prove: mode prove + +[engines] +cover: smtbmc z3 +bmc: smtbmc z3 +prove: smtbmc z3 + +[script] +ghdl --std=08 -fpsl counter.vhd -e counter +prep -auto-top + +[files] +counter.vhd