diff --git a/alu/Makefile b/alu/Makefile index b884e4a..0b56f53 100644 --- a/alu/Makefile +++ b/alu/Makefile @@ -1,6 +1,17 @@ -alu: alu.vhd alu_t.sv alu_f.sby - sby -f -d work alu_f.sby +DUT := alu +.PHONY: cover prove all clean + +all: cover bmc prove + +cover: ${DUT}.vhd symbiyosys.sby + sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@ + +bmc: ${DUT}.vhd symbiyosys.sby + sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@ + +prove: ${DUT}.vhd symbiyosys.sby + sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@ clean: rm -rf work diff --git a/alu/alu.vhd b/alu/alu.vhd index 9ad24b5..e9aac0d 100644 --- a/alu/alu.vhd +++ b/alu/alu.vhd @@ -6,7 +6,8 @@ use ieee.numeric_std.all; entity alu is generic ( - Width : natural := 8 + Width : natural := 8; + Formal : boolean := true ); port ( Reset_n_i : in std_logic; @@ -24,7 +25,7 @@ end entity alu; architecture rtl of alu is - subtype t_opc is std_logic_vector(Opc_i'length-1 downto 0); + subtype t_opc is std_logic_vector(Opc_i'range); constant c_add : t_opc := "00"; constant c_sub : t_opc := "01"; @@ -36,24 +37,61 @@ begin process (Reset_n_i, Clk_i) is + variable v_result : std_logic_vector(Width downto 0); begin if (Reset_n_i = '0') then - Dout_o <= (others => '0'); + v_result := (others => '0'); + Dout_o <= (others => '0'); + OverFlow_o <= '0'; elsif (rising_edge(Clk_i)) then case Opc_i is - when c_add => (OverFlow_o, Dout_o) <= - std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) + - resize(unsigned(DinB_i), Dout_o'length+1)); - when c_sub => (OverFlow_o, Dout_o) <= - std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) - - resize(unsigned(DinB_i), Dout_o'length+1)); - when c_and => Dout_o <= DinA_i and DinB_i; - when c_or => Dout_o <= DinA_i or DinB_i; + when c_add => + v_result := std_logic_vector(unsigned('0' & DinA_i) + + unsigned('0' & DinB_i)); + when c_sub => + v_result := std_logic_vector(unsigned('0' & DinA_i) - + unsigned('0' & DinB_i)); + when c_and => v_result := DinA_i and DinB_i; + when c_or => v_result := DinA_i or DinB_i; when others => null; end case; + Dout_o <= v_result(Width-1 downto 0); + OverFlow_o <= v_result(Width); end if; end process; -end architecture rtl; + FormalG : if Formal generate + + signal s_dina : std_logic_vector(DinA_i'range); + signal s_dinb : std_logic_vector(DinB_i'range); + + begin + + -- VHDL helper logic + process is + begin + wait until rising_edge(Clk_i); + s_dina <= DinA_i; + s_dinb <= DinB_i; + end process; + + + default clock is rising_edge(Clk_i); + + AFTER_RESET : assert always + not Reset_n_i -> Dout_o = x"00" and OverFlow_o = '0'; + + ADD_OP : assert Reset_n_i and Opc_i = c_add -> next unsigned(Dout_o) = unsigned(s_dina) + unsigned(s_dinb) abort not Reset_n_i; + + SUB_OP : assert Reset_n_i and Opc_i = c_sub -> next unsigned(Dout_o) = unsigned(s_dina) - unsigned(s_dinb) abort not Reset_n_i; + + AND_OP : assert Reset_n_i and Opc_i = c_and -> next Dout_o = (s_dina and s_dinb) abort not Reset_n_i; + + OR_OP : assert Reset_n_i and Opc_i = c_or -> next Dout_o = (s_dina or s_dinb) abort not Reset_n_i; + + end generate FormalG; + + +end architecture rtl; diff --git a/alu/alu_f.sby b/alu/alu_f.sby deleted file mode 100644 index 1bc33bc..0000000 --- a/alu/alu_f.sby +++ /dev/null @@ -1,18 +0,0 @@ -[options] -depth 30 -wait on -mode prove -#mode bmc - -[engines] -smtbmc -abc pdr - -[script] -verific -vhdl alu.vhd -verific -formal alu_t.sv -prep -top alu_t - -[files] -alu.vhd -alu_t.sv diff --git a/alu/alu_t.sv b/alu/alu_t.sv deleted file mode 100644 index af8f5c6..0000000 --- a/alu/alu_t.sv +++ /dev/null @@ -1,76 +0,0 @@ -`define WIDTH 8 - - -module alu_t ( - input Reset_n_i, - input Clk_i, - input [1:0] Opc_i, - input [`WIDTH-1:0] DinA_i, - input [`WIDTH-1:0] DinB_i, - output [`WIDTH-1:0] Dout_o, - output OverFlow_o -); - - - - `define OPC_ADD 0 - `define OPC_SUB 1 - `define OPC_AND 2 - `define OPC_OR 3 - - - alu #(.Width(`WIDTH)) alu_i ( - .Reset_n_i(Reset_n_i), - .Clk_i(Clk_i), - .Opc_i(Opc_i), - .DinA_i(DinA_i[`WIDTH-1:0]), - .DinB_i(DinB_i[`WIDTH-1:0]), - .Dout_o(Dout_o[`WIDTH-1:0]), - .OverFlow_o(OverFlow_o) - ); - - - reg init_state = 1; - - // 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; - - default clocking - @(posedge Clk_i); - endclocking - - default disable iff (!Reset_n_i); - - - bit unsigned [`WIDTH:0] dina, dinb; - - assign dina = DinA_i; - assign dinb = DinB_i; - - assert property (Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i))); - assert property (Opc_i == `OPC_ADD && (dina + dinb) > 2**`WIDTH-1 |=> OverFlow_o); - assert property (Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i))); - assert property (Opc_i == `OPC_SUB && (dina - dinb) > 2**`WIDTH-1 |=> OverFlow_o); - assert property (Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i))); - assert property (Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i))); - - - - property cover_opc (opc); - Opc_i == opc; - endproperty - - cover property (cover_opc(`OPC_ADD)); - cover property (cover_opc(`OPC_SUB)); - cover property (cover_opc(`OPC_AND)); - cover property (cover_opc(`OPC_OR)); - - -endmodule - diff --git a/alu/symbiyosys.sby b/alu/symbiyosys.sby new file mode 100644 index 0000000..3aed69d --- /dev/null +++ b/alu/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: abc bmc3 +prove: abc pdr + +[script] +ghdl --std=08 -fpsl alu.vhd -e alu +prep -auto-top + +[files] +alu.vhd