Trying to verify Verilog/VHDL designs with formal methods and tools
vhdl
verilog
systemverilog
sva
assertions
formal
yosys

vai_reg.vhd 4.3KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163
  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 <= (DoutValid_o and DoutAccept_i) = '1';
  37. process (Reset_n_i, Clk_i) is
  38. begin
  39. if (Reset_n_i = '0') then
  40. DinAccept_o <= '0';
  41. DoutStart_o <= '0';
  42. DoutStop_o <= '0';
  43. DoutValid_o <= '0';
  44. Dout_o <= (others => '0');
  45. s_header <= (others => '0');
  46. s_data <= (others => '0');
  47. s_register <= (others => (others => '0'));
  48. s_error <= false;
  49. s_fsm_state <= IDLE;
  50. elsif (rising_edge(Clk_i)) then
  51. case s_fsm_state is
  52. when IDLE =>
  53. DinAccept_o <= '0';
  54. DoutStart_o <= '0';
  55. DoutStop_o <= '0';
  56. DoutValid_o <= '0';
  57. Dout_o <= (others => '0');
  58. s_header <= (others => '0');
  59. s_data <= (others => '0');
  60. s_error <= false;
  61. DinAccept_o <= '1';
  62. s_fsm_state <= GET_HEADER;
  63. when GET_HEADER =>
  64. if (DinValid_i = '1' and DinStart_i = '1') then
  65. s_header <= Din_i;
  66. if (Din_i(3 downto 0) = C_READ and DinStop_i = '1') then
  67. DinAccept_o <= '0';
  68. s_fsm_state <= GET_DATA;
  69. elsif (Din_i(3 downto 0) = C_WRITE and DinStop_i = '0') then
  70. s_fsm_state <= SET_DATA;
  71. else
  72. DinAccept_o <= '0';
  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. if (DinValid_i = '1') then
  86. DinAccept_o <= '0';
  87. if (DinStop_i = '1') then
  88. if (unsigned(a_addr) <= 7) then
  89. s_register(to_integer(unsigned(a_addr))) <= Din_i;
  90. else
  91. s_error <= true;
  92. end if;
  93. s_fsm_state <= SEND_HEADER;
  94. else
  95. s_fsm_state <= IDLE;
  96. end if;
  97. end if;
  98. when SEND_HEADER =>
  99. DoutValid_o <= '1';
  100. DoutStart_o <= '1';
  101. Dout_o <= s_header;
  102. if (s_dout_accepted) then
  103. DoutValid_o <= '0';
  104. DoutStart_o <= '0';
  105. if (s_header(3 downto 0) = C_WRITE) then
  106. s_fsm_state <= SEND_FOOTER;
  107. else
  108. s_fsm_state <= SEND_DATA;
  109. end if;
  110. end if;
  111. when SEND_DATA =>
  112. DoutValid_o <= '1';
  113. Dout_o <= s_data;
  114. if (s_dout_accepted) then
  115. DoutValid_o <= '0';
  116. s_fsm_state <= SEND_FOOTER;
  117. end if;
  118. when SEND_FOOTER =>
  119. DoutValid_o <= '1';
  120. DoutStop_o <= '1';
  121. Dout_o <= x"01" when s_error else x"00";
  122. if (s_dout_accepted) then
  123. Dout_o <= (others => '0');
  124. DoutValid_o <= '0';
  125. DoutStop_o <= '0';
  126. s_fsm_state <= IDLE;
  127. end if;
  128. when others => null;
  129. end case;
  130. end if;
  131. end process;
  132. end architecture rtl;