diff --git a/vai_reg/Makefile b/vai_reg/Makefile new file mode 100644 index 0000000..8d2a410 --- /dev/null +++ b/vai_reg/Makefile @@ -0,0 +1,6 @@ +vai_reg: vai_reg.vhd properties.sv symbiyosys.sby + sby -f -d work symbiyosys.sby + + +clean: + rm -rf work diff --git a/vai_reg/properties.sv b/vai_reg/properties.sv new file mode 100644 index 0000000..822c78e --- /dev/null +++ b/vai_reg/properties.sv @@ -0,0 +1,167 @@ +module properties ( + input Reset_n_i, + input Clk_i, + input [7:0] Din_i, + input DinValid_i, + input DinStart_i, + input DinStop_i, + input DinAccept_o, + input [7:0] Dout_o, + input DoutValid_o, + input DoutStart_o, + input DoutStop_o, + input DoutAccept_i, + // Internals + input [2:0] s_fsm_state, + input [7:0] s_header +); + + + + `define READ 0 + `define WRITE 1 + + + 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; + + + // Constraints + + assume property (@(posedge Clk_i) + DinValid_i && !DinAccept_o |=> + $stable(Din_i) + ); + + assume property (@(posedge Clk_i) + DinValid_i && !DinAccept_o |=> + $stable(DinStart_i) + ); + + assume property (@(posedge Clk_i) + DinValid_i && !DinAccept_o |=> + $stable(DinStop_i) + ); + + + // Asserts + + assert property (@(posedge Clk_i) + s_fsm_state >= 0 && s_fsm_state <= 6 + ); + + assert property (@(posedge Clk_i) + DoutStart_o |-> + DoutValid_o + ); + + assert property (@(posedge Clk_i) + DoutStart_o && DoutAccept_i |=> + !DoutStart_o + ); + + assert property (@(posedge Clk_i) + DoutStop_o |-> + DoutValid_o + ); + + assert property (@(posedge Clk_i) + DoutStop_o && DoutAccept_i |=> + !DoutStop_o + ); + + assert property (@(posedge Clk_i) + s_fsm_state == 1 && DinValid_i && DinStart_i && DinAccept_o |=> + s_header == $past(Din_i) + ); + + + // State changes + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 0 |=> s_fsm_state == 1 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 1 && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=> + s_fsm_state == 2 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=> + s_fsm_state == 3 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 2 |=> s_fsm_state == 4 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=> s_fsm_state == 5 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] != `READ |=> s_fsm_state == 6 + ); + + assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + s_fsm_state == 6 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 0 + ); + + + // Protocol checks + + assert property (@(posedge Clk_i) + s_fsm_state > 1 |-> + s_header[3:0] == `READ || s_header[3:0] == `WRITE + ); + + assert property (@(posedge Clk_i) + DoutStart_o && DoutValid_o |-> + Dout_o[3:0] == s_header[3:0] + ); + + assert property (@(posedge Clk_i) + DoutValid_o && !DoutAccept_i |=> + $stable(Dout_o) + ); + + assert property (@(posedge Clk_i) + DoutValid_o && !DoutAccept_i |=> + $stable(DoutStart_o) + ); + + assert property (@(posedge Clk_i) + DoutValid_o && !DoutAccept_i |=> + $stable(DoutStop_o) + ); + + assert property (@(posedge Clk_i) + DoutValid_o |-> !(DoutStart_o && DoutStop_o) + ); + + assert property (@(posedge Clk_i) + DoutStart_o |-> s_fsm_state == 4 + ); + + assert property (@(posedge Clk_i) + DoutStop_o |-> s_fsm_state == 6 + ); + + assert property (@(posedge Clk_i) + DoutValid_o |-> s_fsm_state >= 4 && s_fsm_state <= 6 + ); + + +endmodule + + +bind vai_reg properties properties (.*); diff --git a/vai_reg/symbiyosys.sby b/vai_reg/symbiyosys.sby new file mode 100644 index 0000000..c5cca6c --- /dev/null +++ b/vai_reg/symbiyosys.sby @@ -0,0 +1,19 @@ +[options] +depth 30 +wait on +mode prove +#mode bmc + +[engines] +smtbmc +#abc pdr + +[script] +verific -vhdl vai_reg.vhd +verific -formal properties.sv +verific -import -extnets -all vai_reg +prep -top vai_reg + +[files] +vai_reg.vhd +properties.sv diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd new file mode 100644 index 0000000..b07e8f5 --- /dev/null +++ b/vai_reg/vai_reg.vhd @@ -0,0 +1,163 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + + + +entity vai_reg is + port ( + Reset_n_i : in std_logic; + Clk_i : in std_logic; + -- req + Din_i : in std_logic_vector(7 downto 0); + DinValid_i : in std_logic; + DinStart_i : in std_logic; + DinStop_i : in std_logic; + DinAccept_o : out std_logic; + -- ack + Dout_o : out std_logic_vector(7 downto 0); + DoutValid_o : out std_logic; + DoutStart_o : out std_logic; + DoutStop_o : out std_logic; + DoutAccept_i : in std_logic + ); +end entity vai_reg; + + + +architecture rtl of vai_reg is + + + constant C_READ : std_logic_vector(3 downto 0) := x"0"; + constant C_WRITE : std_logic_vector(3 downto 0) := x"1"; + + type t_fsm_state is (IDLE, GET_HEADER, GET_DATA, + SET_DATA, SEND_HEADER, SEND_DATA, SEND_FOOTER); + signal s_fsm_state : t_fsm_state; + + type t_register is array(0 to 7) of std_logic_vector(7 downto 0); + signal s_register : t_register; + + signal s_header : std_logic_vector(7 downto 0); + signal s_data : std_logic_vector(7 downto 0); + + signal s_error : boolean; + + alias a_addr : std_logic_vector(3 downto 0) is s_header(7 downto 4); + + +begin + + + process (Reset_n_i, Clk_i) is + begin + if (Reset_n_i = '0') then + DinAccept_o <= '0'; + DoutStart_o <= '0'; + DoutStop_o <= '0'; + DoutValid_o <= '0'; + Dout_o <= (others => '0'); + s_header <= (others => '0'); + s_data <= (others => '0'); + s_register <= (others => (others => '0')); + s_error <= false; + s_fsm_state <= IDLE; + elsif (rising_edge(Clk_i)) then + case s_fsm_state is + + when IDLE => + DinAccept_o <= '0'; + DoutStart_o <= '0'; + DoutStop_o <= '0'; + DoutValid_o <= '0'; + Dout_o <= (others => '0'); + s_header <= (others => '0'); + s_data <= (others => '0'); + s_error <= false; + s_fsm_state <= GET_HEADER; + + when GET_HEADER => + DinAccept_o <= '1'; + if (DinValid_i = '1' and DinStart_i = '1') then + DinAccept_o <= '0'; + s_header <= Din_i; + if (Din_i(3 downto 0) = C_READ and DinStop_i = '1') then + s_fsm_state <= GET_DATA; + elsif (Din_i(3 downto 0) = C_WRITE and DinStop_i = '0') then + s_fsm_state <= SET_DATA; + else + s_fsm_state <= IDLE; + end if; + end if; + + when GET_DATA => + if (unsigned(a_addr) <= 7) then + s_data <= s_register(to_integer(unsigned(a_addr))); + else + s_error <= true; + s_data <= (others => '0'); + end if; + s_fsm_state <= SEND_HEADER; + + when SET_DATA => + DinAccept_o <= '1'; + if (DinValid_i = '1') then + DinAccept_o <= '0'; + if (DinStop_i = '1') then + if (unsigned(a_addr) <= 7) then + -- Following line results in a Segmentation Fault + s_register(to_integer(unsigned(a_addr))) <= Din_i; + -- Following line results in following error: + -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172. + s_register(0) <= Din_i; + else + s_error <= true; + end if; + s_fsm_state <= SEND_HEADER; + else + s_fsm_state <= IDLE; + end if; + end if; + + when SEND_HEADER => + DoutValid_o <= '1'; + DoutStart_o <= '1'; + Dout_o <= s_header; + if (DoutAccept_i = '1') then + DoutValid_o <= '0'; + DoutStart_o <= '0'; + if (s_header(3 downto 0) = C_WRITE) then + s_fsm_state <= SEND_FOOTER; + else + s_fsm_state <= SEND_DATA; + end if; + end if; + + when SEND_DATA => + DoutValid_o <= '1'; + Dout_o <= s_data; + if (DoutAccept_i = '1') then + DoutValid_o <= '0'; + s_fsm_state <= SEND_FOOTER; + end if; + + when SEND_FOOTER => + DoutValid_o <= '1'; + DoutStop_o <= '1'; + Dout_o <= x"01" when s_error else x"00"; + if (DoutAccept_i = '1') then + Dout_o <= (others => '0'); + DoutValid_o <= '0'; + DoutStop_o <= '0'; + s_fsm_state <= IDLE; + end if; + + when others => null; + + end case; + end if; + end process; + + +end architecture rtl; +