Unlocking Complexity: Advanced Techniques in Formal Verification | Part 8 — Transcript

Full transcript

1. 0:01hey everyone welcome back if you have
2. 0:04been following us you know we have been
3. 0:06figuring out how to address the design
4. 0:08complexity in formal verification we
5. 0:10have looked at ways to do parameter
6. 0:12reductions abstractions case splitting
7. 0:15and so on but honestly when we are
8. 0:17dealing with really tricky designs just
9. 0:20doing the basics isn't enough the good
10. 0:23news is the cat tools we use to do
11. 0:25formal are getting better and smarter
12. 0:28all the time helping us out in new ways
13. 0:31today we are going to talk about some
14. 0:33really cool new methods that are on
15. 0:36another level so get your pen and paper
16. 0:39ready and let's make sense of all this
17. 0:41complicated stuff
18. 0:43together recapping our progress we have
19. 0:46already covered all the items in the
20. 0:48green uh which are shown on the left
21. 0:50hand side which are basic and
22. 0:51intermediate complexity reduction
23. 0:53techniques today we will delve into the
24. 0:56blue ones which are the first two points
25. 0:58in the advanced complexity reduction
26. 1:00part the check decomposition and the
27. 1:03assume
28. 1:06guarantees imagine a whimsicle race
29. 1:09between a rabbit and a Toto it's a timed
30. 1:12event so here's the twist if neither
31. 1:15participant reaches the Finish Line
32. 1:17before the timer expires nobody is going
33. 1:20to win however if someone does cross the
34. 1:23finish line within the alloted time the
35. 1:25clock
36. 1:26stops now how can we formally verify
37. 1:29this this
38. 1:30race one straightforward check is to
39. 1:33consider what we see on the left hand
40. 1:36side that's what um it says race started
41. 1:41and eventually either timeout happened
42. 1:43or somebody
43. 1:44won now in the formal runs let's say
44. 1:48this is taking hours to
45. 1:49converge and we want to decompose it
46. 1:52into multiple smaller
47. 1:55checks how can we do that
48. 2:06I have broken down this check into two
49. 2:08smaller ones as you see on the right
50. 2:10hand side the number one and number two
51. 2:13the idea is to split the check in such a
52. 2:15way that each of these subjects covers
53. 2:18more specific scenarios compared to the
54. 2:21original case which we see on the left
55. 2:23hand
56. 2:24side the motivation is to reduce the
57. 2:26state space for each of the smaller
58. 2:29checks
59. 2:30the focus checks are expect this this
60. 2:32smaller Focus checks are expected to
61. 2:34reach deeper bounds compared to the
62. 2:37original check and if we can prove both
63. 2:40of the smaller checks individually then
64. 2:42it's equalent to proving the original
65. 2:45check so in the first smaller check it's
66. 2:48saying that the race started and the
67. 2:50timeout did not happen then somebody has
68. 2:52to
69. 2:53win and in the second scenario we are
70. 2:56seeing that the race started and nobody
71. 2:58won then time out must happen
72. 3:02eventually now how does it look uh look
73. 3:06like in the real life scenarios that we
74. 3:08deal with let's consider a small f with
75. 3:12n
76. 3:14elements and consider a case where the
77. 3:18F4 has only one entry left in it and the
78. 3:21right happens at this
79. 3:23point so the read pointer is all the way
80. 3:26up here in zero and right pointer is in
81. 3:322 so if a write happens at this point
82. 3:36and then there is no read simultaneous
83. 3:38read happening at that cycle then in the
84. 3:40next cycle the 54 is supposed to become
85. 3:43full the property that I'm going to
86. 3:46verify is shown here there is only one
87. 3:49entry left in the F4 underscore 1 d
88. 3:52means one cycle before and there was a
89. 3:56right one cycle before that implies
90. 3:59either the fif is going to be full in
91. 4:01the current cycle or there was a read in
92. 4:04the previous
93. 4:05cycle assume that for the time being
94. 4:08that this is going to take a long time
95. 4:10to converge and we want to decompose it
96. 4:12into two smaller ones this is how you
97. 4:14can do it let's split the consant into
98. 4:17two sections two properties one says
99. 4:21there was a read there there is one free
100. 4:23entry one cycle before and a right
101. 4:26happened at that point one cycle before
102. 4:29and there was no read one cycle before
103. 4:32that means the 54 is going to be full
104. 4:35has to be full at the current
105. 4:37cycle so what's the second
106. 4:39scenario one free entry one cycle before
107. 4:42right is happening one cycle before and
108. 4:45in the current cycle it's still not
109. 4:47full what does that mean it means that
110. 4:50there was a read one cycle
111. 4:54before that's all about decomposing
112. 4:58checks let look at the second Advanced
113. 5:01technique assume
114. 5:03guarantee it is a way to ignore the cor
115. 5:06of influence of a particular signal or
116. 5:08signals and let those signals choose any
117. 5:12value based on certain constraints that
118. 5:14we
119. 5:16provide let's consider a case with uh
120. 5:19with a F4 and an
121. 5:21FSM the FSM transitions from start to
122. 5:25State one when the F4 is empty and state
123. 5:29one to state two and the 54 is
124. 5:32full the main property that we are
125. 5:34interested in is
126. 5:37this uh if you look at the antient of
127. 5:40this
128. 5:41property it says that the state has to
129. 5:44be in state
130. 5:46two so when does this chick become
131. 5:49active so out of reset it will wait for
132. 5:53the 54 to become full first empty and
133. 5:56then full which is going to take at
134. 5:58least 10 Cycles
135. 6:00then this property will be evaluated but
136. 6:03the interesting thing to not here is
137. 6:05that for those n Cycles when the Fifer
138. 6:07is getting full do we really care about
139. 6:10those end Cycles as far as this property
140. 6:12is
141. 6:13concerned if if the answer is no then
142. 6:16you're essentially wasting those end
143. 6:19Cycles how about getting rid of those
144. 6:22end
145. 6:23Cycles we can use assume guarantee to do
146. 6:25that
147. 6:31we can tell the tool to ignore the
148. 6:34driving logic of the full and empty
149. 6:36signals the signals that matter for this
150. 6:38FS some of interest to take any
151. 6:42value but when we say any value it might
152. 6:46introduce some illegal combination of
153. 6:48signals or illegal values in this case U
154. 6:51if it it's free to choose empty and full
155. 6:54uh one at the same time but that's
156. 6:56that's incorrect so we want to add some
157. 6:58constraints like
158. 7:00full means no
159. 7:02empty that means full and empty should
160. 7:04not be coming together and things like
161. 7:07that based on the nature of the signals
162. 7:08and the understanding you have of the
163. 7:11design now why do we call it assume
164. 7:14guarantee it's because first we need to
165. 7:17verify this
166. 7:18assumption and that part is called
167. 7:20guaranteeing the Assumption so we run
168. 7:23this property as an assertion and then
169. 7:25we verify it first make sure that this
170. 7:27passes then after that we ask for
171. 7:31running this property we will ask the
172. 7:34tool to consider this as an assumption
173. 7:37not as an assertion assertion is a check
174. 7:39assumption is a
175. 7:41constraint or some kind of restriction
176. 7:43on whatever signals we are adding
177. 7:46assumption
178. 7:48on so initially we prove the property or
179. 7:53guarantee the property then we assume
180. 7:55the property for checking another
181. 7:58property that's the key concept of
182. 7:59assume guarantee so there are multiple
183. 8:02ways to do this um one of the major
184. 8:05tools in the industry has something like
185. 8:07proof structure which lets you keep
186. 8:11nested assumptions and guarantees and
187. 8:15initially you can assume um you can have
188. 8:18one property that you can guarantee then
189. 8:20assume that and prove this property then
190. 8:23repeat the process assume this one and
191. 8:25prove another property which is a bigger
192. 8:27one so if you Nest it like that then
193. 8:29you're going to have a uh
194. 8:32really uh good advantage in terms of
195. 8:34producing the complexity it's one of the
196. 8:37really powerful techniques that have
197. 8:38come come across I really encourage you
198. 8:40to try it out and see how it
199. 8:43helps I really hope you enjoyed the
200. 8:45video thanks a lot again for watching
201. 8:48make sure you subscribe to the channel
202. 8:49and never miss an update stay tuned for
203. 8:52the next video where I'll cover another
204. 8:55fun formication topic see you next time
205. 8:58thank you and bye