Mastering Memory Abstraction in Formal Verification | Step-by-Step Guide | Part 7 — Transcript

Full transcript

1. 0:00in the intricate world of formal
2. 0:02edification abstractions are not just
3. 0:04helpful they are essential they are the
4. 0:07silent Heroes that transform a complex
5. 0:09design into something far more
6. 0:12manageable imagine a maze with multiple
7. 0:14entry points you want to see if you
8. 0:17constructed your maze correctly you're
9. 0:19letting 20 rats enter the maze from all
10. 0:22possible ports you let them run around
11. 0:25the maze to see if eventually all the
12. 0:28rats are coming out or not
13. 0:30how easy is it going to
14. 0:32be with 20 rats and tracking all
15. 0:35possible paths it's going to be really
16. 0:38difficult what if you could solve the
17. 0:40puzzle with just one imaginary rat who
18. 0:44can arbitrarily enter the maze from any
19. 0:46entrance and still check the correctness
20. 0:48of all paths in the Maze that's
21. 0:52abstraction for you memories are also
22. 0:55similar to this maze you can write into
23. 0:58n address locations and read from all of
24. 1:00them if you let all possibilities in
25. 1:03your formal runs the complexity is going
26. 1:05to
27. 1:07explode imagine taking a vast memory
28. 1:10system and Distilling it down to its
29. 1:12Essence where tracking a single location
30. 1:15or just a few of them unravels the
31. 1:18complexity of the whole that is a power
32. 1:21of
33. 1:21abstraction and that's exactly what I'm
34. 1:24here to help you with I'm your Gade on
35. 1:26this journey through the nuances of
36. 1:27formal verification so if you a blsa
37. 1:30engineer looking to sharpen your skills
38. 1:32and navigate the complexity of formal
39. 1:34verification you are in the right place
40. 1:36join me on my YouTube channel formal
41. 1:38intelligence and let's tackle formal
42. 1:40verification together one step at a time
43. 1:44hit that subscribe button and let's get
44. 1:46started on this journey to
45. 1:49Mastery with this video we will complete
46. 1:53all basic and intermediate techniques
47. 1:55for formal complexity reduction if you
48. 1:57have watched all the videos so far you
49. 1:59are in a real good position to start
50. 2:01implementing these techniques in your
51. 2:02formal venes I encourage you to try them
52. 2:05out and discuss any issues that you
53. 2:07might come
54. 2:09across memory abstraction is a way of
55. 2:13tracking only one or a few locations in
56. 2:15the memory irrespective of the number of
57. 2:18locations in the original memory we will
58. 2:21discuss a case where we'll track only
59. 2:22one location and not three or four
60. 2:25locations which is also another
61. 2:27possibility for
62. 2:28abstraction one simp way to do this is
63. 2:31to create a file with the abstracted
64. 2:33memory model and use it in your formal
65. 2:35runs and ignore the RTL memory
66. 2:38altoe so are there any problems with
67. 2:41these kind of
68. 2:43abstractions yes so if you don't model
69. 2:46the locations other than the ones which
70. 2:47you are tracking you will see false
71. 2:50failures in your property if the
72. 2:52property relies on data from untracked
73. 2:56locations that's
74. 2:58one so is there any other issue there is
75. 3:02another issue with timing so if your
76. 3:05memory has a specific read or write
77. 3:07latency let's say one clock or two
78. 3:09clocks then your abstraction should also
79. 3:11make sure that you maintain that latency
80. 3:13in your
81. 3:15model let's look at an example here's a
82. 3:18memory with n locations with multi-bit
83. 3:21data input address and single bit read
84. 3:24and write control signals and this is
85. 3:27the data out from this let's see can
86. 3:29abstract this memory and track just one
87. 3:32out of these n
88. 3:35locations this is how you can abstract
89. 3:37it the code is as shown here the
90. 3:41strategy is to Define an internal signal
91. 3:44called track M that can store only one
92. 3:46data trag will have the size of data in
93. 3:50the width of the data in just for just
94. 3:52one
95. 3:53data the first red arrow right here
96. 3:56shows how the data is stored the data
97. 4:00data in is stored in the tracker track M
98. 4:03when the address is equal to symbolic
99. 4:05address for a
100. 4:06right and this section shows the read
101. 4:09operation in this read if the address is
102. 4:11equal to symbolic address then the data
103. 4:14out will be the tracked data track
104. 4:18M but what happens to all the other
105. 4:21cases all the other reads where address
106. 4:23is not equal to symbolic address in this
107. 4:25abstraction we don't care about them but
108. 4:27do we tie them to zero no no we just
109. 4:30want to let it take any value so the key
110. 4:33thing about abstraction is that you
111. 4:34abstract only what's essential so you
112. 4:37just want you want to introduce as
113. 4:39minimum over constraints as possible
114. 4:41inal and the strategy is you constraint
115. 4:44something you let everything else take
116. 4:45any value if you see a failure then you
117. 4:49add constraints on the other free
118. 4:51running signals that's usually how we do
119. 4:53things
120. 4:56informal Q time can you think of some
121. 5:00answers for these
122. 5:04questions you can pause the video and
123. 5:06see if you can answer
124. 5:11them will the abstraction work if the
125. 5:13memory read Laten is 2 CL the current
126. 5:17code which I show which I shown in the
127. 5:18previous
128. 5:20slide this will not work because there
129. 5:23is just one latency so if you send a
130. 5:25read and in the next clock cycle you're
131. 5:27getting going to get the data what but
132. 5:30if there is a memory in article which
133. 5:32just saying that you need to get the
134. 5:34data only after two clock Cycles you
135. 5:36need to modify this to ensure that the
136. 5:38timing is so
137. 5:39B and will the abstraction check for all
138. 5:42addresses or will it check just the
139. 5:45address
140. 5:46two which is U symbolic address here so
141. 5:51the thing with symbolic address is that
142. 5:53it's free to choose any value as long as
143. 5:56you very add some over constraints on
144. 5:59that that so in this case it is going to
145. 6:02take all the values 1 to n but in a
146. 6:05single formal run it will take only
147. 6:08single value so it doesn't mean that
148. 6:09it's not going to cover other cases so
149. 6:12it is going to cover other other
150. 6:13addresses as well in fact all the
151. 6:16addresses so the answer is
152. 6:19yes thanks for watching make sure you
153. 6:22subscribe to our Channel and never miss
154. 6:23an update stay tuned for our next video
155. 6:26where we will cover another font formal
156. 6:28verification topic until then bye take
157. 6:31care