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

properties.sv 8.1KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324
  1. module properties (
  2. input Reset_n_i,
  3. input Clk_i,
  4. input [7:0] Din_i,
  5. input DinValid_i,
  6. input DinStart_i,
  7. input DinStop_i,
  8. input DinAccept_o,
  9. input [7:0] Dout_o,
  10. input DoutValid_o,
  11. input DoutStart_o,
  12. input DoutStop_o,
  13. input DoutAccept_i,
  14. // Internals
  15. input [2:0] s_fsm_state,
  16. input [7:0] s_header,
  17. input [7:0] s_data,
  18. input s_error,
  19. input [7:0] s_register [0:7]
  20. );
  21. // commands
  22. `define READ 0
  23. `define WRITE 1
  24. // FSM states
  25. `define IDLE 0
  26. `define GET_HEADER 1
  27. `define GET_DATA 2
  28. `define SET_DATA 3
  29. `define SEND_HEADER 4
  30. `define SEND_DATA 5
  31. `define SEND_FOOTER 6
  32. reg init_state = 1;
  33. // Initial reset
  34. always @(*) begin
  35. if (init_state) assume (!Reset_n_i);
  36. if (!init_state) assume (Reset_n_i);
  37. end
  38. always @(posedge Clk_i)
  39. init_state = 0;
  40. // Default clocking & reset
  41. default clocking
  42. @(posedge Clk_i);
  43. endclocking
  44. default disable iff (!Reset_n_i);
  45. // Constraints
  46. assume property (
  47. DinValid_i && !DinAccept_o |=>
  48. $stable(DinValid_i)
  49. );
  50. assume property (
  51. DinValid_i && !DinAccept_o |=>
  52. $stable(Din_i)
  53. );
  54. assume property (
  55. DinValid_i && !DinAccept_o |=>
  56. $stable(DinStart_i)
  57. );
  58. assume property (
  59. DinValid_i && !DinAccept_o |=>
  60. $stable(DinStop_i)
  61. );
  62. // Asserts
  63. fsm_state_valid_a : assert property (
  64. s_fsm_state >= `IDLE && s_fsm_state <= `SEND_FOOTER
  65. );
  66. valid_when_start_a : assert property (
  67. DoutStart_o |->
  68. DoutValid_o
  69. );
  70. start_off_when_acked_a : assert property (
  71. DoutStart_o && DoutAccept_i |=>
  72. !DoutStart_o
  73. );
  74. valid_when_stop_a : assert property (
  75. DoutStop_o |->
  76. DoutValid_o
  77. );
  78. stop_off_when_acked_a : assert property (
  79. DoutStop_o && DoutAccept_i |=>
  80. !DoutStop_o
  81. );
  82. store_header_a : assert property (
  83. s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && DinAccept_o |=>
  84. s_header == $past(Din_i)
  85. );
  86. // State changes
  87. // IDLE -> GET_HEADER
  88. fsm_idle_to_get_header_a : assert property (
  89. s_fsm_state == `IDLE |=>
  90. s_fsm_state == `GET_HEADER
  91. );
  92. // GET_HEADER -> GET_DATA
  93. fsm_get_header_to_get_data_a : assert property (
  94. s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=>
  95. s_fsm_state == `GET_DATA
  96. );
  97. // GET_HEADER -> SET_DATA
  98. fsm_get_header_to_set_data_a : assert property (
  99. s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=>
  100. s_fsm_state == `SET_DATA
  101. );
  102. // GET_DATA -> SEND_HEADER
  103. fsm_get_data_to_send_header_a : assert property (
  104. s_fsm_state == `GET_DATA |=>
  105. s_fsm_state == `SEND_HEADER
  106. );
  107. // SET_DATA -> IDLE
  108. fsm_set_data_to_idle_a : assert property (
  109. s_fsm_state == `SET_DATA && DinValid_i && !DinStop_i |=>
  110. s_fsm_state == `IDLE
  111. );
  112. // SET_DATA -> SEND_HEADER
  113. fsm_set_data_to_send_header_a : assert property (
  114. s_fsm_state == `SET_DATA && DinValid_i && DinStop_i |=> s_fsm_state == `SEND_HEADER
  115. );
  116. // SEND_HEADER -> SEND_DATA
  117. fsm_send_header_to_send_data_a : assert property (
  118. s_fsm_state == `SEND_HEADER && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=>
  119. s_fsm_state == `SEND_DATA
  120. );
  121. // SEND_HEADER -> SEND_FOOTER
  122. fsm_send_header_to_send_footer_a : assert property (
  123. s_fsm_state == `SEND_HEADER && DoutValid_o && DoutAccept_i && s_header[3:0] == `WRITE |=>
  124. s_fsm_state == `SEND_FOOTER
  125. );
  126. // SEND_DATA -> SEND_FOOTER
  127. fsm_send_data_to_send_footer_a : assert property (
  128. s_fsm_state == `SEND_DATA && DoutValid_o && DoutAccept_i |=>
  129. s_fsm_state == `SEND_FOOTER
  130. );
  131. // SEND_FOOTER -> IDLE
  132. fsm_send_footer_to_idle_a : assert property (
  133. s_fsm_state == `SEND_FOOTER && DoutValid_o && DoutAccept_i |=>
  134. s_fsm_state == `IDLE
  135. );
  136. // Protocol checks
  137. header_in_valid_range_a : assert property (
  138. s_fsm_state > `GET_HEADER |->
  139. s_header[3:0] inside {`READ, `WRITE}
  140. );
  141. header_stable_a : assert property (
  142. s_fsm_state > `GET_HEADER |=>
  143. $stable(s_header)
  144. );
  145. header_dout_valid_a : assert property (
  146. DoutStart_o && DoutValid_o |->
  147. Dout_o == s_header
  148. );
  149. error_flag_initial_false_a : assert property (
  150. s_fsm_state inside {`GET_HEADER, `GET_DATA, `SET_DATA} |->
  151. !s_error
  152. );
  153. error_flag_set_invalid_addr_a : assert property (
  154. s_fsm_state >= `SEND_HEADER |->
  155. s_error == !(s_header[7:4] <= 7)
  156. );
  157. footer_dout_valid_a :assert property (
  158. DoutStop_o && DoutValid_o |->
  159. Dout_o == s_error
  160. );
  161. doutvalid_stable_until_acked_a : assert property (
  162. DoutValid_o && !DoutAccept_i |=>
  163. $stable(DoutValid_o)
  164. );
  165. dout_stable_until_acked_a : assert property (
  166. DoutValid_o && !DoutAccept_i |=>
  167. $stable(Dout_o)
  168. );
  169. doutstart_stable_until_acked_a : assert property (
  170. DoutValid_o && !DoutAccept_i |=>
  171. $stable(DoutStart_o)
  172. );
  173. doutstop_stable_until_acked_a : assert property (
  174. DoutValid_o && !DoutAccept_i |=>
  175. $stable(DoutStop_o)
  176. );
  177. onehot_doutstart_doutstop_a : assert property (
  178. DoutValid_o |-> $onehot0({DoutStart_o, DoutStop_o})
  179. );
  180. doutstart_in_valid_fsm_state_a : assert property (
  181. DoutStart_o |->
  182. s_fsm_state == `SEND_HEADER
  183. );
  184. doutstop_in_valid_fsm_state_a : assert property (
  185. DoutStop_o |->
  186. s_fsm_state == `SEND_FOOTER
  187. );
  188. doutvalid_in_valid_fsm_states_a : assert property (
  189. DoutValid_o |->
  190. s_fsm_state inside {`SEND_HEADER, `SEND_DATA, `SEND_FOOTER}
  191. );
  192. // Write ack frame
  193. write_frame_a : assert property (
  194. DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `WRITE |=>
  195. !DoutValid_o ##1
  196. DoutValid_o && DoutStop_o
  197. );
  198. // Read ack frame
  199. read_frame_a : assert property (
  200. DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ |=>
  201. !DoutValid_o ##1
  202. DoutValid_o && !DoutStart_o && !DoutStop_o && !DoutAccept_i [*] ##1
  203. DoutValid_o && !DoutStart_o && !DoutStop_o && DoutAccept_i ##1
  204. !DoutValid_o ##1
  205. DoutValid_o && DoutStop_o
  206. );
  207. // Register read in GET_DATA if valid adress was given
  208. get_data_valid_a : assert property (
  209. s_fsm_state > `GET_DATA && s_header[7:4] <= 7 && s_header[3:0] == `READ |->
  210. s_data == s_register[s_header[7:4]]
  211. );
  212. // Error flag set & no register read in GET_DATA if invalid adress was given
  213. get_data_invalid_a : assert property (
  214. s_fsm_state > `GET_DATA && s_header[7:4] > 7 && s_header[3:0] == `READ |=>
  215. s_data == 0 && s_error
  216. );
  217. // register stable if read request
  218. reg_stable_during_read_a : assert property (
  219. s_fsm_state > `GET_HEADER && s_header[3:0] == `READ |=>
  220. $stable(s_register)
  221. );
  222. // Read ack data correct if address is valid
  223. read_ack_data_valid_a : assert property (
  224. DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ && s_header[7:4] <= 7 |=>
  225. !DoutValid_o ##1
  226. DoutValid_o && !DoutStart_o && !DoutStop_o && Dout_o == s_data
  227. );
  228. // Read ack data zero if address is invalid
  229. read_ack_data_invalid_a : assert property (
  230. DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ && s_header[7:4] > 7 |=>
  231. !DoutValid_o ##1
  232. DoutValid_o && !DoutStart_o && !DoutStop_o && Dout_o == 0
  233. );
  234. // Register write in SET_DATA if valid adress was given
  235. set_data_valid_a : assert property (
  236. s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] <= 7 |=>
  237. s_register[s_header[7:4]] == $past(Din_i)
  238. );
  239. // Error flag set & no register write in SET_DATA if invalid adress was given
  240. set_data_invalid_a : assert property (
  241. s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] > 7 |=>
  242. $stable(s_register) && s_error
  243. );
  244. // No register write in SET_DATA if stop don't active
  245. set_data_discard_a : assert property (
  246. s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && !DinStop_i |=>
  247. $stable(s_register)
  248. );
  249. fsm_read_req_when_get_data_a : assert property (
  250. s_fsm_state == `GET_DATA |-> s_header[3:0] == `READ
  251. );
  252. fsm_write_req_when_set_data_a : assert property (
  253. s_fsm_state == `SET_DATA |-> s_header[3:0] == `WRITE
  254. );
  255. endmodule
  256. bind vai_reg properties properties (.*);