diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd index 28407cb..ae4f87e 100644 --- a/vai_reg/vai_reg.vhd +++ b/vai_reg/vai_reg.vhd @@ -100,7 +100,7 @@ begin when GET_DATA => if (unsigned(a_addr) <= 7) then - -- s_data <= s_register(to_integer(unsigned(a_addr))); + s_data <= s_register(to_integer(unsigned(a_addr))); else s_error <= true; s_data <= (others => '0'); @@ -112,7 +112,7 @@ begin DinAccept_o <= '0'; if (DinStop_i = '1') then if (unsigned(a_addr) <= 7) then - -- s_register(to_integer(unsigned(a_addr))) <= Din_i; + s_register(to_integer(unsigned(a_addr))) <= Din_i; else s_error <= true; end if; @@ -165,11 +165,12 @@ begin FormalG : if Formal generate + signal s_addr : natural range 0 to 15; type t_cmd is (READ, WRITE, NOP); signal s_cmd : t_cmd; - + type t_vai is record Start : std_logic; Stop : std_logic; @@ -177,13 +178,14 @@ begin Valid : std_logic; Accept : std_logic; end record t_vai; - + signal s_job_req : t_vai; signal s_job_ack : t_vai; begin + -- VHDL helper logic process is begin @@ -200,8 +202,8 @@ begin end if; end process; - default clock is rising_edge(Clk_i); + default clock is rising_edge(Clk_i); -- RESTRICTIONS @@ -210,7 +212,7 @@ begin -- CONSTRAINTS - + -- Valid stable until accepted JOB_REQ_VALID_STABLE : assume always DinValid_i and not DinAccept_o -> next (DinValid_i until_ DinAccept_o); @@ -218,11 +220,11 @@ begin -- Start stable until accepted JOB_REQ_START_STABLE : assume always DinValid_i and not DinAccept_o -> next (DinStart_i = s_job_req.Start until_ DinAccept_o); - + -- Stop stable until accepted JOB_REQ_STOP_STABLE : assume always DinValid_i and not DinAccept_o -> next (DinStop_i = s_job_req.Stop until_ DinAccept_o); - + -- Data stable until accepted JOB_REQ_DIN_STABLE : assume always DinValid_i and not DinAccept_o -> next (Din_i = s_job_req.Data until_ DinAccept_o); @@ -230,6 +232,17 @@ begin -- ASSERTIONS + -- Reset values + AFTER_RESET : assert always + not Reset_n_i + -> + s_fsm_state = IDLE and + not DinAccept_o and + not DoutStart_o and + not DoutStop_o and + not DoutValid_o and + s_register = (0 to 7 => x"00"); + -- FSM states in valid range FSM_STATES_VALID : assert always s_fsm_state = IDLE or s_fsm_state = GET_HEADER or @@ -262,34 +275,34 @@ begin -- a job read acknowledge has to follow READ_VALID_ACK : assert always {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and - Din_i(3 downto 0) = x"0" and DinStop_i = '1'} + Din_i(3 downto 0) = x"0" and DinStop_i = '1'} |=> {-- Job ack header cycle - (not DoutValid_o)[*]; - (DoutValid_o and DoutStart_o and not DoutAccept_i)[*]; - (DoutValid_o and DoutStart_o and DoutAccept_i); + not DoutValid_o [*]; + DoutValid_o and DoutStart_o and not DoutAccept_i [*]; + DoutValid_o and DoutStart_o and DoutAccept_i; -- Job ack data cycle - (not DoutValid_o)[*]; - (DoutValid_o and not DoutStart_o and not DoutStop_o and not DoutAccept_i)[*]; - (DoutValid_o and not DoutStart_o and not DoutStop_o and DoutAccept_i); + not DoutValid_o [*]; + DoutValid_o and not DoutStart_o and not DoutStop_o and not DoutAccept_i [*]; + DoutValid_o and not DoutStart_o and not DoutStop_o and DoutAccept_i; -- Job ack footer cycle - (not DoutValid_o)[*]; + not DoutValid_o [*]; DoutValid_o and DoutStop_o}; -- After a valid job write request, -- a job read acknowledge has to follow WRITE_VALID_ACK : assert always {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and - Din_i(3 downto 0) = x"1" and DinStop_i = '0'; - (not DinValid_i)[*]; - DinValid_i and DinStop_i} + Din_i(3 downto 0) = x"1" and DinStop_i = '0'; + not DinValid_i [*]; + DinValid_i and DinStop_i} |=> {-- Job ack header cycle - (not DoutValid_o)[*]; - (DoutValid_o and DoutStart_o and not DoutAccept_i)[*]; - (DoutValid_o and DoutStart_o and DoutAccept_i); + not DoutValid_o [*]; + DoutValid_o and DoutStart_o and not DoutAccept_i [*]; + DoutValid_o and DoutStart_o and DoutAccept_i; -- Job ack footer cycle - (not DoutValid_o)[*]; + not DoutValid_o [*]; DoutValid_o and DoutStop_o}; -- Start & stop flag have to be exclusive @@ -316,9 +329,30 @@ begin JOB_ACK_DOUT_STABLE : assert always DoutValid_o and not DoutAccept_i -> next (Dout_o = s_job_ack.Data until_ DoutAccept_i); --- READ_DATA : assert always --- (DoutValid_o and not DoutStart_o and not DoutStop_o) -> --- (Dout_o = s_register(to_integer(unsigned(a_addr)))); + -- Data from selected address has to be read + READ_DATA : assert always + DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr <= 7 + -> + Dout_o = s_register(s_addr); + + -- 0 has to be read when invalid address is given + READ_DATA_INV_ADDR : assert always + DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr > 7 + -> + Dout_o = x"00"; + + -- Register has to be written at given address with given data + -- when correct job req write occurs + WRITE_DATA : assert always + -- Job req header cycle + {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and + Din_i(3 downto 0) = x"1" and unsigned(Din_i(7 downto 4)) <= 7 and DinStop_i = '0'; + -- Job req data / footer cycle + not DinValid_i [*]; + DinValid_i and not DinStart_i and DinStop_i and not DinAccept_o [*]; + DinValid_i and not DinStart_i and DinStop_i and DinAccept_o} + |=> + {s_register(s_addr) = s_job_req.Data}; -- FUNCTIONAL COVERAGE @@ -326,6 +360,7 @@ begin FOOTER_VALID : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"0"}; FOOTER_ERR : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"1"}; + end generate FormalG;