Trying to verify Verilog/VHDL designs with formal methods and tools
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

168 lines
4.6 KiB

  1. library ieee;
  2. use ieee.std_logic_1164.all;
  3. use ieee.numeric_std.all;
  4. entity vai_reg is
  5. port (
  6. Reset_n_i : in std_logic;
  7. Clk_i : in std_logic;
  8. -- req
  9. Din_i : in std_logic_vector(7 downto 0);
  10. DinValid_i : in std_logic;
  11. DinStart_i : in std_logic;
  12. DinStop_i : in std_logic;
  13. DinAccept_o : out std_logic;
  14. -- ack
  15. Dout_o : out std_logic_vector(7 downto 0);
  16. DoutValid_o : out std_logic;
  17. DoutStart_o : out std_logic;
  18. DoutStop_o : out std_logic;
  19. DoutAccept_i : in std_logic
  20. );
  21. end entity vai_reg;
  22. architecture rtl of vai_reg is
  23. constant C_READ : std_logic_vector(3 downto 0) := x"0";
  24. constant C_WRITE : std_logic_vector(3 downto 0) := x"1";
  25. type t_fsm_state is (IDLE, GET_HEADER, GET_DATA,
  26. SET_DATA, SEND_HEADER, SEND_DATA, SEND_FOOTER);
  27. signal s_fsm_state : t_fsm_state;
  28. type t_register is array(0 to 7) of std_logic_vector(7 downto 0);
  29. signal s_register : t_register;
  30. signal s_header : std_logic_vector(7 downto 0);
  31. signal s_data : std_logic_vector(7 downto 0);
  32. signal s_error : boolean;
  33. signal s_dout_accepted : boolean;
  34. alias a_addr : std_logic_vector(3 downto 0) is s_header(7 downto 4);
  35. begin
  36. s_dout_accepted <= true when DoutValid_o = '1' and DoutAccept_i = '1' else
  37. false;
  38. process (Reset_n_i, Clk_i) is
  39. begin
  40. if (Reset_n_i = '0') then
  41. DinAccept_o <= '0';
  42. DoutStart_o <= '0';
  43. DoutStop_o <= '0';
  44. DoutValid_o <= '0';
  45. Dout_o <= (others => '0');
  46. s_header <= (others => '0');
  47. s_data <= (others => '0');
  48. s_register <= (others => (others => '0'));
  49. s_error <= false;
  50. s_fsm_state <= IDLE;
  51. elsif (rising_edge(Clk_i)) then
  52. case s_fsm_state is
  53. when IDLE =>
  54. DinAccept_o <= '0';
  55. DoutStart_o <= '0';
  56. DoutStop_o <= '0';
  57. DoutValid_o <= '0';
  58. Dout_o <= (others => '0');
  59. s_header <= (others => '0');
  60. s_data <= (others => '0');
  61. s_error <= false;
  62. s_fsm_state <= GET_HEADER;
  63. when GET_HEADER =>
  64. DinAccept_o <= '1';
  65. if (DinValid_i = '1' and DinStart_i = '1') then
  66. DinAccept_o <= '0';
  67. s_header <= Din_i;
  68. if (Din_i(3 downto 0) = C_READ and DinStop_i = '1') then
  69. s_fsm_state <= GET_DATA;
  70. elsif (Din_i(3 downto 0) = C_WRITE and DinStop_i = '0') then
  71. s_fsm_state <= SET_DATA;
  72. else
  73. s_fsm_state <= IDLE;
  74. end if;
  75. end if;
  76. when GET_DATA =>
  77. if (unsigned(a_addr) <= 7) then
  78. s_data <= s_register(to_integer(unsigned(a_addr)));
  79. else
  80. s_error <= true;
  81. s_data <= (others => '0');
  82. end if;
  83. s_fsm_state <= SEND_HEADER;
  84. when SET_DATA =>
  85. DinAccept_o <= '1';
  86. if (DinValid_i = '1') then
  87. DinAccept_o <= '0';
  88. if (DinStop_i = '1') then
  89. if (unsigned(a_addr) <= 7) then
  90. -- Following line results in a Segmentation Fault
  91. s_register(to_integer(unsigned(a_addr))) <= Din_i;
  92. -- Following line results in following error:
  93. -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172.
  94. s_register(0) <= Din_i;
  95. else
  96. s_error <= true;
  97. end if;
  98. s_fsm_state <= SEND_HEADER;
  99. else
  100. s_fsm_state <= IDLE;
  101. end if;
  102. end if;
  103. when SEND_HEADER =>
  104. DoutValid_o <= '1';
  105. DoutStart_o <= '1';
  106. Dout_o <= s_header;
  107. if (s_dout_accepted) then
  108. DoutValid_o <= '0';
  109. DoutStart_o <= '0';
  110. if (s_header(3 downto 0) = C_WRITE) then
  111. s_fsm_state <= SEND_FOOTER;
  112. else
  113. s_fsm_state <= SEND_DATA;
  114. end if;
  115. end if;
  116. when SEND_DATA =>
  117. DoutValid_o <= '1';
  118. Dout_o <= s_data;
  119. if (s_dout_accepted) then
  120. DoutValid_o <= '0';
  121. s_fsm_state <= SEND_FOOTER;
  122. end if;
  123. when SEND_FOOTER =>
  124. DoutValid_o <= '1';
  125. DoutStop_o <= '1';
  126. Dout_o <= x"01" when s_error else x"00";
  127. if (s_dout_accepted) then
  128. Dout_o <= (others => '0');
  129. DoutValid_o <= '0';
  130. DoutStop_o <= '0';
  131. s_fsm_state <= IDLE;
  132. end if;
  133. when others => null;
  134. end case;
  135. end if;
  136. end process;
  137. end architecture rtl;