0 00:00:00,000 --> 00:00:30,000 Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/705 Thanks! 1 00:00:15,380 --> 00:00:17,809 I have the tremendous pleasure 2 00:00:17,810 --> 00:00:19,699 and the big honor here to see you, 3 00:00:19,700 --> 00:00:21,769 Clifford, for the most of the guys who 4 00:00:21,770 --> 00:00:24,139 know him and the other guys who don't 5 00:00:24,140 --> 00:00:24,649 know him. 6 00:00:24,650 --> 00:00:26,959 Be warned, because 7 00:00:26,960 --> 00:00:29,149 this man is like a bullet 8 00:00:29,150 --> 00:00:30,229 train. 9 00:00:30,230 --> 00:00:32,389 So the moment we press that button, 10 00:00:32,390 --> 00:00:34,469 start the start 11 00:00:34,470 --> 00:00:36,529 the race and you be 12 00:00:36,530 --> 00:00:36,889 careful. 13 00:00:36,890 --> 00:00:38,179 So fasten seatbelts. 14 00:00:38,180 --> 00:00:39,829 Ladies and gentlemen. 15 00:00:39,830 --> 00:00:40,830 Here is the man. 16 00:00:41,930 --> 00:00:43,549 Thank you. Yes. 17 00:00:43,550 --> 00:00:45,499 If you put it in play. 18 00:00:45,500 --> 00:00:47,749 So, OK, this is my talk about 19 00:00:47,750 --> 00:00:49,999 form verification with yours as SMTP. 20 00:00:50,000 --> 00:00:51,229 See it. 21 00:00:51,230 --> 00:00:52,490 And it's the. 22 00:00:57,260 --> 00:00:59,089 This is my talk about format verification 23 00:00:59,090 --> 00:01:01,279 with your SMTP, BMC, and 24 00:01:01,280 --> 00:01:03,499 it's a shorter version 25 00:01:03,500 --> 00:01:05,719 of my talk, but I still need to 26 00:01:05,720 --> 00:01:07,729 speak very fast. 27 00:01:07,730 --> 00:01:09,799 So if you're interested in the 28 00:01:09,800 --> 00:01:12,319 full flight set, go to this 29 00:01:12,320 --> 00:01:13,639 link. 30 00:01:13,640 --> 00:01:15,469 The link will be also on the last slide 31 00:01:15,470 --> 00:01:17,029 of this presentation. So you don't need 32 00:01:17,030 --> 00:01:19,759 to like, write it down right now. 33 00:01:19,760 --> 00:01:21,529 And you can also download all the 34 00:01:21,530 --> 00:01:23,179 profiles files. For example, as I showed 35 00:01:23,180 --> 00:01:25,339 you during my talk from from this 36 00:01:25,340 --> 00:01:27,499 page. And my 37 00:01:27,500 --> 00:01:29,689 my goal is really to just 38 00:01:29,690 --> 00:01:31,819 give you a 39 00:01:31,820 --> 00:01:33,889 rough idea of what you can do 40 00:01:33,890 --> 00:01:36,199 with the refusers sometimes here 41 00:01:36,200 --> 00:01:38,269 and then you can download the sample 42 00:01:38,270 --> 00:01:40,729 files, reproduce the stuff that I can. 43 00:01:40,730 --> 00:01:43,129 I will be talking here and then modify 44 00:01:43,130 --> 00:01:45,379 this examples to fit your 45 00:01:45,380 --> 00:01:47,269 verification needs, whatever, whatever 46 00:01:47,270 --> 00:01:48,270 you need to do. 47 00:01:49,670 --> 00:01:51,979 OK, but really 48 00:01:51,980 --> 00:01:54,019 quickly, if just a little bit about the 49 00:01:54,020 --> 00:01:56,299 users as a whole, because 50 00:01:56,300 --> 00:01:57,819 there are a lot of things you can do with 51 00:01:57,820 --> 00:02:01,399 users besides formal verification. 52 00:02:01,400 --> 00:02:03,769 So there are a lot of syntheses, flaws 53 00:02:03,770 --> 00:02:05,269 that are available in users. 54 00:02:05,270 --> 00:02:07,369 So most prominently we can do synthesis 55 00:02:07,370 --> 00:02:09,478 for for the future is I had 56 00:02:09,479 --> 00:02:11,539 the talk last year at CES 57 00:02:11,540 --> 00:02:13,909 about that and I had to reverse engineer 58 00:02:13,910 --> 00:02:16,159 this for the bitstream format in order to 59 00:02:16,160 --> 00:02:17,160 enable this flow. 60 00:02:18,230 --> 00:02:20,459 But there is also a synthesis Flarf 61 00:02:20,460 --> 00:02:22,400 exciting seven series features 62 00:02:23,510 --> 00:02:25,579 here. You need to use sailing's we've of 63 00:02:25,580 --> 00:02:26,959 a place and throughout, but the synthesis 64 00:02:26,960 --> 00:02:29,419 part can be done by users. 65 00:02:29,420 --> 00:02:31,549 There are also a couple of async flows 66 00:02:31,550 --> 00:02:33,049 that are enabled by users. 67 00:02:33,050 --> 00:02:35,179 You can also do your custom synthesis 68 00:02:35,180 --> 00:02:36,709 flows, which is something that some 69 00:02:36,710 --> 00:02:39,379 people do on the formal verification 70 00:02:39,380 --> 00:02:40,309 site. 71 00:02:40,310 --> 00:02:41,479 We have users S.A. 72 00:02:41,480 --> 00:02:43,009 BMC, which is the thing that I will be 73 00:02:43,010 --> 00:02:45,229 talking about today. 74 00:02:45,230 --> 00:02:46,849 But there are also some other 75 00:02:46,850 --> 00:02:48,949 verification flows available in 76 00:02:48,950 --> 00:02:50,059 the also's. 77 00:02:50,060 --> 00:02:51,849 For example, there are a couple of built 78 00:02:51,850 --> 00:02:54,019 in comments in users directive that can 79 00:02:54,020 --> 00:02:56,839 be used for certain verification 80 00:02:56,840 --> 00:02:59,029 tasks. There's a built in sub 81 00:02:59,030 --> 00:03:00,949 so that you can use for some things. 82 00:03:00,950 --> 00:03:02,239 There is an equivalence checking 83 00:03:02,240 --> 00:03:05,029 framework or you can use 84 00:03:05,030 --> 00:03:07,219 your source just as a front end to 85 00:03:07,220 --> 00:03:09,949 convert your design into something 86 00:03:09,950 --> 00:03:11,839 that can be understood by other tools. 87 00:03:11,840 --> 00:03:13,909 For example, you could use users 88 00:03:13,910 --> 00:03:16,249 as a front end and combine it with ABC 89 00:03:16,250 --> 00:03:19,249 and to verification in the ABC. 90 00:03:19,250 --> 00:03:20,719 But the thing I'll be talking about is 91 00:03:20,720 --> 00:03:22,910 the first one uses some key here, 92 00:03:23,930 --> 00:03:26,349 a framework for bounded model check 93 00:03:26,350 --> 00:03:29,029 or induction enabled by users. 94 00:03:29,030 --> 00:03:30,979 It can be combined with any existing 95 00:03:30,980 --> 00:03:33,199 SMPTE to solving 96 00:03:33,200 --> 00:03:35,029 so that there is not a lock in here to 97 00:03:35,030 --> 00:03:36,319 one specific Soulsville. 98 00:03:36,320 --> 00:03:38,329 You can combine it with anyone because 99 00:03:38,330 --> 00:03:40,459 I'm using the Asanti Liberta language to 100 00:03:40,460 --> 00:03:43,399 communicate with that soever. 101 00:03:43,400 --> 00:03:45,499 Um, and there are a couple of servers 102 00:03:45,500 --> 00:03:47,299 that will test tested. 103 00:03:47,300 --> 00:03:49,429 So usually when you read here, support 104 00:03:49,430 --> 00:03:50,839 that Tolliver's, it means well tested 105 00:03:50,840 --> 00:03:52,969 saurus because in principle with 106 00:03:52,970 --> 00:03:55,399 any source that supports this file format 107 00:03:55,400 --> 00:03:57,589 and those will test it, all of us are, 108 00:03:57,590 --> 00:04:00,139 for example, said freakier 109 00:04:00,140 --> 00:04:01,610 for ICS and so on. 110 00:04:04,060 --> 00:04:06,459 Good, but before we 111 00:04:06,460 --> 00:04:09,009 dove into a formal verification of 112 00:04:09,010 --> 00:04:11,349 this slide and this is my 113 00:04:11,350 --> 00:04:13,479 way, you should be excited about this 114 00:04:13,480 --> 00:04:14,480 slide. 115 00:04:15,430 --> 00:04:17,619 So I have 116 00:04:17,620 --> 00:04:20,199 some thoughts here about the availability 117 00:04:20,200 --> 00:04:22,749 of other tools for students, 118 00:04:22,750 --> 00:04:25,029 for hobbyists, for enthusiasts 119 00:04:25,030 --> 00:04:26,739 who just would like to experiment with 120 00:04:26,740 --> 00:04:28,899 the technology or that kind 121 00:04:28,900 --> 00:04:31,299 of stuff. And on the FPGA synthesis 122 00:04:31,300 --> 00:04:33,549 site, there are a couple of free to use 123 00:04:33,550 --> 00:04:35,289 tools. So if you're interested in playing 124 00:04:35,290 --> 00:04:37,149 with this kind of technologies, you can 125 00:04:37,150 --> 00:04:39,639 just download the free stuff from filings 126 00:04:39,640 --> 00:04:41,919 or other 127 00:04:41,920 --> 00:04:43,989 vendor and install it. 128 00:04:43,990 --> 00:04:46,209 And maybe within an hour or two, 129 00:04:46,210 --> 00:04:47,439 if the installation 130 00:04:49,000 --> 00:04:52,449 goes goes without any major difficulties, 131 00:04:52,450 --> 00:04:54,549 you you can play around with it 132 00:04:54,550 --> 00:04:56,829 and you can start making 133 00:04:56,830 --> 00:04:58,479 your experiences with this kind of 134 00:04:58,480 --> 00:05:00,759 technology and with FPGA 135 00:05:00,760 --> 00:05:02,979 synthesis, even some 136 00:05:02,980 --> 00:05:04,479 free and open source options. 137 00:05:04,480 --> 00:05:06,639 So there is the orses 138 00:05:06,640 --> 00:05:08,859 floor with Project Isong on 540, for 139 00:05:08,860 --> 00:05:10,329 example. 140 00:05:10,330 --> 00:05:11,599 But this is not the only one. 141 00:05:11,600 --> 00:05:13,699 There is also Vitara within two or 142 00:05:13,700 --> 00:05:14,599 three frameworks. 143 00:05:14,600 --> 00:05:15,600 So there are a couple of options. 144 00:05:16,870 --> 00:05:18,999 The same thing for HGL simulation. 145 00:05:19,000 --> 00:05:20,949 If you would like to simulate a circuit, 146 00:05:20,950 --> 00:05:23,289 I would like to to make 147 00:05:23,290 --> 00:05:25,569 your own experiences with FPGA. 148 00:05:25,570 --> 00:05:27,759 By HGL simulation, you can 149 00:05:27,760 --> 00:05:29,889 download some free to use tools like 150 00:05:29,890 --> 00:05:32,109 Xilinx, XM and 151 00:05:32,110 --> 00:05:33,879 even some open source tools that you can 152 00:05:33,880 --> 00:05:36,189 download and start learning about 153 00:05:36,190 --> 00:05:38,259 this kind of stuff just within 154 00:05:39,280 --> 00:05:41,349 minutes. However, take how 155 00:05:41,350 --> 00:05:42,769 long it takes to install. 156 00:05:42,770 --> 00:05:44,499 We are not using up get something like 157 00:05:44,500 --> 00:05:45,500 this. 158 00:05:45,850 --> 00:05:48,009 However, on the formal verification 159 00:05:48,010 --> 00:05:49,599 side, we have a completely different 160 00:05:49,600 --> 00:05:52,089 picture. There's practically no 161 00:05:52,090 --> 00:05:54,579 free to use tool that is. 162 00:05:54,580 --> 00:05:56,949 Besides the things I showed you today 163 00:05:56,950 --> 00:05:59,109 know are free and open 164 00:05:59,110 --> 00:06:01,329 source told that you could use to do 165 00:06:01,330 --> 00:06:02,850 and format verification. 166 00:06:04,480 --> 00:06:06,069 And interestingly, at the same time, 167 00:06:06,070 --> 00:06:07,659 people in the industry are complaining 168 00:06:07,660 --> 00:06:09,099 they can't hire anyone who has 169 00:06:09,100 --> 00:06:11,199 experienced performer verification. 170 00:06:11,200 --> 00:06:13,359 And I really wonder why why this is 171 00:06:13,360 --> 00:06:15,279 so why there are no people with formal 172 00:06:15,280 --> 00:06:17,469 verification even though the industry 173 00:06:17,470 --> 00:06:19,029 demands them. 174 00:06:19,030 --> 00:06:21,579 So I think this should be 175 00:06:21,580 --> 00:06:24,189 the the focus of that. 176 00:06:24,190 --> 00:06:26,319 I can't really tell you stuff like how 177 00:06:26,320 --> 00:06:28,419 fast is my floor compared with the 178 00:06:28,420 --> 00:06:30,489 commercial floors because I don't have 179 00:06:30,490 --> 00:06:32,109 access to those commercial floors. 180 00:06:32,110 --> 00:06:32,899 I have. 181 00:06:32,900 --> 00:06:35,049 I had no way so far to compare 182 00:06:35,050 --> 00:06:37,359 my stuff with the commercially available 183 00:06:37,360 --> 00:06:39,639 stuff, because even so, 184 00:06:39,640 --> 00:06:40,640 I, 185 00:06:41,910 --> 00:06:43,659 I do some research at the University 186 00:06:43,660 --> 00:06:45,399 Institute and I have some commercial 187 00:06:45,400 --> 00:06:47,229 software that I have nothing that's 188 00:06:47,230 --> 00:06:49,089 comparable on the farmer verification 189 00:06:49,090 --> 00:06:50,259 front. 190 00:06:50,260 --> 00:06:52,509 So I think it doesn't really matter that 191 00:06:52,510 --> 00:06:54,579 much if my tool is 192 00:06:54,580 --> 00:06:56,769 faster than the commercial 193 00:06:56,770 --> 00:06:58,779 tool, if it supports exactly the same 194 00:06:58,780 --> 00:07:00,279 features, that the really important thing 195 00:07:00,280 --> 00:07:02,439 is that this is something that enables 196 00:07:02,440 --> 00:07:05,259 you to to make experiences 197 00:07:05,260 --> 00:07:06,759 with this kind of technology. 198 00:07:06,760 --> 00:07:08,979 And hopefully one day 199 00:07:08,980 --> 00:07:11,049 I will be able to compare my work 200 00:07:11,050 --> 00:07:13,119 with the commercial tools and then I 201 00:07:13,120 --> 00:07:15,489 will know if I'm better 202 00:07:15,490 --> 00:07:18,129 or if they are better or if they're 203 00:07:18,130 --> 00:07:19,130 about equal. 204 00:07:21,650 --> 00:07:23,989 OK, so when we're talking about farmer 205 00:07:23,990 --> 00:07:25,699 verification, what are we actually 206 00:07:25,700 --> 00:07:27,949 talking about? And in almost 207 00:07:27,950 --> 00:07:29,809 all representations about this kind of 208 00:07:29,810 --> 00:07:31,759 stuff, you will find a slide that looks 209 00:07:31,760 --> 00:07:33,919 more like like this one 210 00:07:33,920 --> 00:07:36,049 that have a couple of 211 00:07:36,050 --> 00:07:38,239 of of states Yazaki it can be 212 00:07:38,240 --> 00:07:39,169 in. 213 00:07:39,170 --> 00:07:41,299 And the couple of simulation traces of 214 00:07:41,300 --> 00:07:43,609 the simulation traces are there. 215 00:07:43,610 --> 00:07:45,799 I don't know what what color 216 00:07:45,800 --> 00:07:48,019 this is, but this here is 217 00:07:48,020 --> 00:07:49,649 a simulation race. 218 00:07:49,650 --> 00:07:50,690 Oh you don't see it. 219 00:07:55,250 --> 00:07:57,339 This here is one of those simulation 220 00:07:57,340 --> 00:07:58,340 traces, 221 00:07:59,720 --> 00:08:01,709 and you see we have three simulation 222 00:08:01,710 --> 00:08:03,889 cases here and they cover a 223 00:08:03,890 --> 00:08:06,079 subset of all the states, 224 00:08:06,080 --> 00:08:07,849 interestingly, that don't cover this red 225 00:08:07,850 --> 00:08:09,829 state. And the red state is a red state 226 00:08:09,830 --> 00:08:11,509 that violates an association. 227 00:08:11,510 --> 00:08:13,459 So when we would like to verify it this 228 00:08:13,460 --> 00:08:15,649 second, we would like to be sure 229 00:08:15,650 --> 00:08:17,749 that we have caught this red state that 230 00:08:17,750 --> 00:08:20,029 we have shown that this state is actually 231 00:08:20,030 --> 00:08:21,030 reachable. 232 00:08:21,800 --> 00:08:24,199 One one way to improve 233 00:08:24,200 --> 00:08:26,269 the coverage here would be just 234 00:08:26,270 --> 00:08:28,129 to run more and more random simulations. 235 00:08:29,360 --> 00:08:31,409 However, if you look at this example 236 00:08:31,410 --> 00:08:33,739 really carefully, you will see 237 00:08:33,740 --> 00:08:36,048 that there is only one possible path 238 00:08:36,049 --> 00:08:38,569 that goes to this one, one red state. 239 00:08:38,570 --> 00:08:40,668 And one of those traces almost got 240 00:08:40,669 --> 00:08:43,369 there. But the last minute 241 00:08:43,370 --> 00:08:45,199 decided to go a different route within 242 00:08:45,200 --> 00:08:47,239 the states diagram. 243 00:08:47,240 --> 00:08:49,549 And if you just multiply it, the choices 244 00:08:49,550 --> 00:08:51,679 you have at each node on this path, 245 00:08:51,680 --> 00:08:54,409 you will realize that you could run 246 00:08:54,410 --> 00:08:56,329 a thousand simulation traces on this 247 00:08:56,330 --> 00:08:57,859 really, really small example. 248 00:08:57,860 --> 00:09:00,139 And you still only have about 50 249 00:09:00,140 --> 00:09:02,609 percent chance to to 250 00:09:02,610 --> 00:09:05,179 to get to this one red state 251 00:09:05,180 --> 00:09:07,249 that violates your assumptions. 252 00:09:07,250 --> 00:09:09,319 So random simulation is not really 253 00:09:09,320 --> 00:09:11,599 a solution if you would like to make sure 254 00:09:11,600 --> 00:09:14,089 if an invalid state is reachable 255 00:09:14,090 --> 00:09:16,669 or not, you have to use former methods 256 00:09:16,670 --> 00:09:18,440 and the former methods actually 257 00:09:19,730 --> 00:09:21,949 like look at the whole state 258 00:09:21,950 --> 00:09:24,289 diagram as as 259 00:09:24,290 --> 00:09:26,509 a whole. So it's not simulating many, 260 00:09:26,510 --> 00:09:28,789 many individual places. 261 00:09:28,790 --> 00:09:30,799 Instead, it will give you a definite 262 00:09:30,800 --> 00:09:33,019 answer if this state, this red 263 00:09:33,020 --> 00:09:35,239 state is rich or not 264 00:09:35,240 --> 00:09:36,559 in this situation. 265 00:09:37,700 --> 00:09:39,769 And then you simulate that a 266 00:09:39,770 --> 00:09:42,109 lot, you can be 267 00:09:42,110 --> 00:09:43,189 fairly certain. 268 00:09:43,190 --> 00:09:45,049 You can be more certain if assimilate for 269 00:09:45,050 --> 00:09:47,389 many, many hours, but only 270 00:09:47,390 --> 00:09:48,589 with formal verification. 271 00:09:48,590 --> 00:09:50,689 You can absolutely be sure that no 272 00:09:50,690 --> 00:09:53,089 assertion can be violated in your 273 00:09:53,090 --> 00:09:54,949 design. So that's that's what they're 274 00:09:54,950 --> 00:09:56,359 talking about. And we're talking about 275 00:09:56,360 --> 00:09:58,609 far more verification. 276 00:09:58,610 --> 00:10:00,709 So why would we do this? 277 00:10:00,710 --> 00:10:02,809 Why would we want formal verification? 278 00:10:02,810 --> 00:10:04,909 And in almost all 279 00:10:04,910 --> 00:10:06,499 cases where people use formal 280 00:10:06,500 --> 00:10:08,659 verification, they have to first 281 00:10:08,660 --> 00:10:10,759 use case. They would like to prove 282 00:10:10,760 --> 00:10:13,039 that at the sign is correct. 283 00:10:13,040 --> 00:10:15,139 And in many cases, this this is 284 00:10:15,140 --> 00:10:16,429 a really good reason to do formal 285 00:10:16,430 --> 00:10:18,739 verification. I just told you, when 286 00:10:18,740 --> 00:10:21,019 you have to be sure this is the only way 287 00:10:22,070 --> 00:10:23,250 you can can achieve them. 288 00:10:24,350 --> 00:10:26,489 However, proving that the 289 00:10:26,490 --> 00:10:28,249 design is correct, even if you have a 290 00:10:28,250 --> 00:10:30,499 formal verification tool, is a pretty 291 00:10:30,500 --> 00:10:31,500 hard thing. 292 00:10:32,150 --> 00:10:33,150 So first of all, 293 00:10:34,610 --> 00:10:36,619 you need a formal specification of the 294 00:10:36,620 --> 00:10:38,299 correct behavior if you don't have a 295 00:10:38,300 --> 00:10:39,829 formal verification of the correct 296 00:10:39,830 --> 00:10:42,139 behavior. How can the tool know which 297 00:10:42,140 --> 00:10:43,669 is the right behavior and which just the 298 00:10:43,670 --> 00:10:45,919 wrong behavior and 299 00:10:45,920 --> 00:10:48,229 usually just this one step, 300 00:10:48,230 --> 00:10:50,389 creating a formal specification 301 00:10:50,390 --> 00:10:52,189 of the right behavior can already be a 302 00:10:52,190 --> 00:10:53,299 showstopper. 303 00:10:53,300 --> 00:10:55,399 This could be a project so that 304 00:10:55,400 --> 00:10:57,649 you you wouldn't think it's worth 305 00:10:57,650 --> 00:10:59,929 your your wine in 306 00:10:59,930 --> 00:11:00,979 many applications. 307 00:11:00,980 --> 00:11:03,469 So maybe if you are in 308 00:11:03,470 --> 00:11:05,569 some space applications, 309 00:11:05,570 --> 00:11:07,489 you can get around it. 310 00:11:07,490 --> 00:11:09,619 But in many other cases, people 311 00:11:09,620 --> 00:11:11,899 might say, well, if there is a problem 312 00:11:11,900 --> 00:11:14,329 in the field, I'll just create a new FPGA 313 00:11:14,330 --> 00:11:16,339 image and we will figure out how to how 314 00:11:16,340 --> 00:11:19,009 to update the devices in the field. 315 00:11:19,010 --> 00:11:21,379 However, there are two other big, big 316 00:11:21,380 --> 00:11:23,119 application domains for formal 317 00:11:23,120 --> 00:11:24,739 verification. 318 00:11:24,740 --> 00:11:26,239 There is back hunting and there is 319 00:11:26,240 --> 00:11:27,799 optimization. 320 00:11:27,800 --> 00:11:29,989 And I think usually we don't 321 00:11:29,990 --> 00:11:32,119 talk about this to that much. 322 00:11:32,120 --> 00:11:34,099 And I think the reason is that the 323 00:11:34,100 --> 00:11:35,899 pricing on the commercial tours is 324 00:11:35,900 --> 00:11:36,859 prohibitive. 325 00:11:36,860 --> 00:11:39,199 So you only buy 326 00:11:39,200 --> 00:11:41,509 those commercial tools if you really, 327 00:11:41,510 --> 00:11:42,709 really have to. 328 00:11:42,710 --> 00:11:44,749 And the only case where you really have 329 00:11:44,750 --> 00:11:46,869 to is if you have the first case, if 330 00:11:46,870 --> 00:11:49,759 you need proof that the design is correct 331 00:11:49,760 --> 00:11:52,339 and many projects might benefit 332 00:11:52,340 --> 00:11:54,199 from having formal verification around 333 00:11:54,200 --> 00:11:56,479 for background hunting optimization, 334 00:11:56,480 --> 00:11:58,399 but they don't do it because it's not on 335 00:11:58,400 --> 00:11:59,400 the radar. 336 00:12:00,830 --> 00:12:02,999 So what is the difference between 337 00:12:03,000 --> 00:12:04,909 counting and proving that the design is 338 00:12:04,910 --> 00:12:07,459 correct? So first of all, for accounting, 339 00:12:07,460 --> 00:12:10,679 you only need a partial specification. 340 00:12:10,680 --> 00:12:12,829 If you just have specified some part 341 00:12:12,830 --> 00:12:14,929 of the circuit, you can use the former 342 00:12:14,930 --> 00:12:17,389 tools to figure out if the socket 343 00:12:17,390 --> 00:12:19,189 at least conforms to this partial 344 00:12:19,190 --> 00:12:20,269 specification. 345 00:12:20,270 --> 00:12:22,519 Maybe there is other stuff that is not 346 00:12:22,520 --> 00:12:24,409 specified with this partial 347 00:12:24,410 --> 00:12:27,109 specification, but if there is a back 348 00:12:27,110 --> 00:12:30,589 that is somewhere within the specified 349 00:12:30,590 --> 00:12:32,849 domain, then then you can use this. 350 00:12:34,100 --> 00:12:35,100 The other thing is 351 00:12:36,170 --> 00:12:39,169 when you do back hunting, you can do 352 00:12:39,170 --> 00:12:41,299 many different checks 353 00:12:41,300 --> 00:12:43,639 with different overlapping 354 00:12:43,640 --> 00:12:46,249 partial specifications. 355 00:12:46,250 --> 00:12:48,319 And you only need to have a 356 00:12:48,320 --> 00:12:49,989 really good feeling about that. 357 00:12:49,990 --> 00:12:52,159 All this overlapping specifications 358 00:12:52,160 --> 00:12:54,579 really cover the entire. 359 00:12:54,580 --> 00:12:56,799 Havey off the sacket, that's when 360 00:12:56,800 --> 00:12:58,719 you want like to prove that the design is 361 00:12:58,720 --> 00:13:00,609 correct and you would like to fracture 362 00:13:00,610 --> 00:13:03,039 into individual small checks, 363 00:13:03,040 --> 00:13:05,679 that you have to have a second proof 364 00:13:05,680 --> 00:13:07,389 that proof that you haven't left and the 365 00:13:07,390 --> 00:13:09,549 gaps with this partial 366 00:13:09,550 --> 00:13:10,869 specifications. 367 00:13:10,870 --> 00:13:12,999 And there are cases where people do 368 00:13:13,000 --> 00:13:15,519 that and they claim that the first thing. 369 00:13:15,520 --> 00:13:17,859 But actually they don't because this 370 00:13:17,860 --> 00:13:19,959 this are questions that are left open 371 00:13:19,960 --> 00:13:21,429 if you do that. So this is just one 372 00:13:21,430 --> 00:13:24,009 thing, but it can be really beneficial 373 00:13:24,010 --> 00:13:26,229 to have those tools for back hunting. 374 00:13:26,230 --> 00:13:28,299 Usually they will find 375 00:13:28,300 --> 00:13:30,849 Besar a box really, really obscure 376 00:13:30,850 --> 00:13:33,519 box packs that you would never find 377 00:13:33,520 --> 00:13:35,619 using handwritten test 378 00:13:35,620 --> 00:13:37,779 benches because nobody comes up with 379 00:13:37,780 --> 00:13:40,029 the crazy things they do with 380 00:13:40,030 --> 00:13:42,909 your design in order to trigger 381 00:13:42,910 --> 00:13:43,910 an assertion. 382 00:13:45,220 --> 00:13:47,619 So not only will it find 383 00:13:47,620 --> 00:13:49,869 bugs, it will find those sparks 384 00:13:49,870 --> 00:13:51,459 that are really, really, really hard to 385 00:13:51,460 --> 00:13:52,630 find in the field. 386 00:13:53,800 --> 00:13:56,259 That box there you have a processor 387 00:13:56,260 --> 00:13:57,819 and that works really fine. 388 00:13:57,820 --> 00:14:00,009 And after a year that is in the field, 389 00:14:00,010 --> 00:14:02,289 someone comes to you and says, well, 390 00:14:02,290 --> 00:14:04,089 there is this one plug in. 391 00:14:04,090 --> 00:14:06,299 And if you use this binary for the Skemp 392 00:14:06,300 --> 00:14:08,769 plugin and you run it an entire day, 393 00:14:08,770 --> 00:14:10,839 then it will somehow crash the 394 00:14:10,840 --> 00:14:12,129 process. So at one point 395 00:14:13,330 --> 00:14:15,489 and this is like the thing you get as 396 00:14:15,490 --> 00:14:17,499 a back report and then you have to figure 397 00:14:17,500 --> 00:14:20,139 out how to go from there to 398 00:14:20,140 --> 00:14:22,209 the one obscure thing in your 399 00:14:22,210 --> 00:14:24,189 instruction cache that went wrong. 400 00:14:24,190 --> 00:14:26,169 And that was triggered by this one 401 00:14:26,170 --> 00:14:27,579 scenario. 402 00:14:27,580 --> 00:14:30,639 Um, so the R 403 00:14:30,640 --> 00:14:32,949 but if you find the same back here, 404 00:14:32,950 --> 00:14:35,029 the will give you a counterexample. 405 00:14:35,030 --> 00:14:36,220 It will tell you. Well if I, 406 00:14:37,890 --> 00:14:40,239 if I, if I use the inputs of your socket 407 00:14:40,240 --> 00:14:42,129 in this way, then the socket will go into 408 00:14:42,130 --> 00:14:43,939 the estate. And here you have said the 409 00:14:43,940 --> 00:14:46,089 state is an invalid state that should 410 00:14:46,090 --> 00:14:48,159 not read it. So you're in a much, much 411 00:14:48,160 --> 00:14:50,229 better position to have to 412 00:14:50,230 --> 00:14:52,269 figure out what's actually going wrong. 413 00:14:52,270 --> 00:14:54,129 Even if you could already reproduce the 414 00:14:54,130 --> 00:14:56,199 bug in hardware, 415 00:14:56,200 --> 00:14:57,639 you would be on the very different 416 00:14:57,640 --> 00:14:58,659 standing here. 417 00:14:58,660 --> 00:14:59,959 So so be the hunter. 418 00:14:59,960 --> 00:15:01,539 Don't be the hunted. 419 00:15:01,540 --> 00:15:02,860 When it comes to the box 420 00:15:05,440 --> 00:15:07,539 with optimization, 421 00:15:07,540 --> 00:15:09,070 we essentially do 422 00:15:10,660 --> 00:15:12,789 the same thing as we would do when the 423 00:15:12,790 --> 00:15:14,499 proof of design is correct. 424 00:15:14,500 --> 00:15:16,779 But we just use the an optimized design 425 00:15:16,780 --> 00:15:17,919 like a spec. 426 00:15:17,920 --> 00:15:20,049 So we have already a design that works 427 00:15:20,050 --> 00:15:22,149 and we know this is that this behavior we 428 00:15:22,150 --> 00:15:24,249 want and that we would like to optimize 429 00:15:24,250 --> 00:15:25,999 the kind usually of any optimized call 430 00:15:26,000 --> 00:15:27,789 your make it a little bit more complex. 431 00:15:27,790 --> 00:15:29,949 So if you would like to optimize 432 00:15:29,950 --> 00:15:32,289 for power, for example, you would add 433 00:15:32,290 --> 00:15:34,959 are allocating in certain cases 434 00:15:34,960 --> 00:15:37,299 and then you have to put 435 00:15:37,300 --> 00:15:39,459 additional thought into which 436 00:15:39,460 --> 00:15:41,949 flipflop stage can be 437 00:15:41,950 --> 00:15:44,109 located in a cycle. 438 00:15:44,110 --> 00:15:46,299 And if this if there 439 00:15:46,300 --> 00:15:48,939 is a problem somewhere, then you would 440 00:15:48,940 --> 00:15:51,039 find this by formally verifying you 441 00:15:51,040 --> 00:15:53,259 optimized design using the, um, optimized 442 00:15:53,260 --> 00:15:55,330 design specification. 443 00:15:56,770 --> 00:15:58,659 In this case, this would be very, very 444 00:15:58,660 --> 00:16:00,699 similar to farmers formal equivalents. 445 00:16:00,700 --> 00:16:03,429 Checking, however, there are cases 446 00:16:03,430 --> 00:16:05,529 where your optimization reduces the 447 00:16:05,530 --> 00:16:08,049 number of cycles needed to produce 448 00:16:08,050 --> 00:16:09,459 the same result. 449 00:16:09,460 --> 00:16:11,709 And then we are already beyond what 450 00:16:11,710 --> 00:16:13,359 formula equivalents checking would do, 451 00:16:13,360 --> 00:16:15,489 because now we have two circuits 452 00:16:15,490 --> 00:16:17,649 that are formally not 453 00:16:17,650 --> 00:16:19,749 equivalent, because once this 454 00:16:19,750 --> 00:16:21,849 circuit is producing the result one cycle 455 00:16:21,850 --> 00:16:23,709 earlier than the other one, but we could 456 00:16:23,710 --> 00:16:26,769 still construct a farmer proof using 457 00:16:26,770 --> 00:16:28,839 property checking to make sure that the 458 00:16:28,840 --> 00:16:31,659 result both circuits produce 459 00:16:31,660 --> 00:16:32,660 the same. 460 00:16:34,420 --> 00:16:36,549 OK, I'm not really going to talk 461 00:16:36,550 --> 00:16:38,769 about the things on the slide here. 462 00:16:38,770 --> 00:16:41,019 This is just to 463 00:16:41,020 --> 00:16:43,149 to show you it's really easy to install 464 00:16:43,150 --> 00:16:45,399 this on an open to 465 00:16:45,400 --> 00:16:46,869 anything beyond those of other 466 00:16:46,870 --> 00:16:47,950 distributions, of course. 467 00:16:49,450 --> 00:16:52,299 So you really have no excuse 468 00:16:52,300 --> 00:16:53,799 for not trying this out. 469 00:16:53,800 --> 00:16:55,239 If you do anything about formal 470 00:16:55,240 --> 00:16:57,429 verification, could be could 471 00:16:57,430 --> 00:16:59,439 be useful. It's not like you have to 472 00:16:59,440 --> 00:17:01,869 spend an afternoon compiling for tangoed 473 00:17:01,870 --> 00:17:03,749 from the 70s in 474 00:17:05,780 --> 00:17:07,868 in instead you just 475 00:17:07,869 --> 00:17:09,879 get some prerequisites and then you build 476 00:17:09,880 --> 00:17:12,459 your source and then you build a set 477 00:17:12,460 --> 00:17:14,379 and something solid. 478 00:17:14,380 --> 00:17:16,659 And after 20 minutes of 479 00:17:16,660 --> 00:17:17,679 however fast 480 00:17:18,810 --> 00:17:21,368 your computer can be large C++ 481 00:17:21,369 --> 00:17:23,739 projects, you have everything in start 482 00:17:23,740 --> 00:17:25,899 and you can playing around with 483 00:17:25,900 --> 00:17:28,420 the examples in this presentation. 484 00:17:30,490 --> 00:17:32,619 So the first 485 00:17:32,620 --> 00:17:34,119 link is the same link you had on the 486 00:17:34,120 --> 00:17:35,199 first slide. 487 00:17:35,200 --> 00:17:37,089 This is where I can download the slides 488 00:17:37,090 --> 00:17:39,159 and also some examplar files, 489 00:17:39,160 --> 00:17:41,349 some example files that can 490 00:17:41,350 --> 00:17:43,959 also be interesting are the examples 491 00:17:43,960 --> 00:17:46,329 in example, slash SMTP E.M.S. 492 00:17:46,330 --> 00:17:48,579 within the order source code. 493 00:17:48,580 --> 00:17:50,829 And if you know my pick of 494 00:17:50,830 --> 00:17:52,150 the two project, that's a 495 00:17:53,200 --> 00:17:55,749 five implementation. 496 00:17:55,750 --> 00:17:58,029 There's is a couple of former staff there 497 00:17:58,030 --> 00:17:58,449 as well. 498 00:17:58,450 --> 00:18:00,849 And it could also look 499 00:18:00,850 --> 00:18:02,799 look, they are far more examples and 500 00:18:02,800 --> 00:18:05,049 crazy things you can do with this form 501 00:18:05,050 --> 00:18:06,050 verification. 502 00:18:07,600 --> 00:18:10,329 OK, let's let's get right into it. 503 00:18:10,330 --> 00:18:11,330 Some code. 504 00:18:13,420 --> 00:18:15,999 This is simple HelloWallet example. 505 00:18:16,000 --> 00:18:17,919 So if you have accountably initialized 506 00:18:17,920 --> 00:18:20,200 the counter to to zero in this case 507 00:18:21,250 --> 00:18:23,329 and then we have a clock block and we say 508 00:18:23,330 --> 00:18:25,719 whenever we get a rising clock, that's 509 00:18:25,720 --> 00:18:27,909 when the reset is higher than 510 00:18:27,910 --> 00:18:29,619 countervail to zero. 511 00:18:29,620 --> 00:18:31,389 And then reset is not high. 512 00:18:31,390 --> 00:18:32,950 Then we will increment the content. 513 00:18:34,060 --> 00:18:36,099 And then we have some farmer statements 514 00:18:36,100 --> 00:18:37,989 at the at the end of this input. 515 00:18:37,990 --> 00:18:40,089 So we assume that the counter 516 00:18:40,090 --> 00:18:42,189 will never reach the value of ten 517 00:18:42,190 --> 00:18:44,289 and then the Assad, that the counter 518 00:18:44,290 --> 00:18:46,179 will never reach the value of 15. 519 00:18:46,180 --> 00:18:48,279 And since we are incrementing and 520 00:18:48,280 --> 00:18:50,649 steps of one, we never can go 521 00:18:50,650 --> 00:18:53,289 to 15 without going over 10. 522 00:18:53,290 --> 00:18:55,449 So indeed, this should 523 00:18:55,450 --> 00:18:57,909 hold to verify 524 00:18:57,910 --> 00:19:00,059 this. We call this three 525 00:19:00,060 --> 00:19:02,919 commands on the lower right. 526 00:19:02,920 --> 00:19:04,510 The first command is. 527 00:19:05,560 --> 00:19:07,929 So if you use your for a synthesis 528 00:19:07,930 --> 00:19:09,639 of this circuit, but they don't 529 00:19:09,640 --> 00:19:11,829 synthesizers for an FHA 530 00:19:11,830 --> 00:19:13,729 or an async architecture, instead they 531 00:19:13,730 --> 00:19:15,939 synthesize it into an essential to 532 00:19:15,940 --> 00:19:18,369 description of this circuit. 533 00:19:18,370 --> 00:19:20,529 And then we use users, SMTP, 534 00:19:20,530 --> 00:19:23,919 E.M.S. to check if 535 00:19:23,920 --> 00:19:25,689 the assumptions are right. 536 00:19:25,690 --> 00:19:27,429 And we have two calls here. 537 00:19:27,430 --> 00:19:29,829 The first one does a bounded model check. 538 00:19:29,830 --> 00:19:32,079 So we check if the 539 00:19:32,080 --> 00:19:33,080 socket 540 00:19:35,620 --> 00:19:37,719 if all the assumptions hold within 541 00:19:37,720 --> 00:19:39,909 the first and cycles, the default 542 00:19:39,910 --> 00:19:42,129 value is 20 at the second call 543 00:19:42,130 --> 00:19:44,619 tries to perform an induction step 544 00:19:44,620 --> 00:19:46,659 to prove that. In fact, that doesn't only 545 00:19:46,660 --> 00:19:48,459 hold for the first end cycles. 546 00:19:48,460 --> 00:19:50,859 It holds for infinitely many cycles. 547 00:19:50,860 --> 00:19:52,029 It holds forever. 548 00:19:52,030 --> 00:19:53,379 This is what we would like to do. 549 00:19:53,380 --> 00:19:54,909 In most cases. We would like to do that. 550 00:19:54,910 --> 00:19:56,769 Something holds forever. 551 00:19:56,770 --> 00:19:58,839 However, in some cases with very 552 00:19:58,840 --> 00:20:01,149 complex designs, this can be hard 553 00:20:01,150 --> 00:20:02,469 to achieve. 554 00:20:02,470 --> 00:20:04,449 Then you are in trouble if you would like 555 00:20:04,450 --> 00:20:06,249 to prove that your design is correct 556 00:20:06,250 --> 00:20:07,989 under all circumstances. 557 00:20:07,990 --> 00:20:09,289 But if you are, for example, back 558 00:20:09,290 --> 00:20:11,379 hunting, you could still save Allahpundit 559 00:20:11,380 --> 00:20:13,119 model check for 100 cycles. 560 00:20:13,120 --> 00:20:15,399 Gives me enough competence, confidence 561 00:20:15,400 --> 00:20:17,469 that that actually this 562 00:20:17,470 --> 00:20:20,319 design is correct and works as expected 563 00:20:20,320 --> 00:20:22,509 because of my understanding of 564 00:20:22,510 --> 00:20:24,609 my design. I know within hundred 565 00:20:24,610 --> 00:20:26,829 cycles that should reach all the richer 566 00:20:26,830 --> 00:20:27,830 states anyways. 567 00:20:29,760 --> 00:20:31,859 So when you run it, you you get 568 00:20:31,860 --> 00:20:34,259 this output and 569 00:20:34,260 --> 00:20:36,179 the first one is for the bounded model 570 00:20:36,180 --> 00:20:38,399 checks of it, just check 571 00:20:38,400 --> 00:20:40,589 the assertions, hold assertions 572 00:20:40,590 --> 00:20:42,689 in timestep zero, then after 573 00:20:42,690 --> 00:20:44,759 one state transition, do they 574 00:20:44,760 --> 00:20:47,009 hold in state one and so on until 575 00:20:47,010 --> 00:20:49,199 we reached state 19. 576 00:20:49,200 --> 00:20:51,749 And the other one is the induction 577 00:20:51,750 --> 00:20:53,999 step at the induction step count 578 00:20:54,000 --> 00:20:55,529 backwards from 120. 579 00:20:55,530 --> 00:20:57,779 And if it's very easy to prove something 580 00:20:57,780 --> 00:20:59,429 by induction, we will talk a little bit 581 00:20:59,430 --> 00:21:00,659 more about this later in the 582 00:21:00,660 --> 00:21:01,619 presentation. 583 00:21:01,620 --> 00:21:03,809 Then this will maybe try to 584 00:21:03,810 --> 00:21:05,939 improve induction and step 20 and 585 00:21:05,940 --> 00:21:08,489 then step 19 and say, well, 586 00:21:08,490 --> 00:21:10,589 it's passed, everything is OK in this 587 00:21:10,590 --> 00:21:12,749 case is a little bit harder 588 00:21:12,750 --> 00:21:14,849 and we need to go down all the way 589 00:21:14,850 --> 00:21:16,949 to step 15 before the 590 00:21:16,950 --> 00:21:18,929 induction vox. 591 00:21:18,930 --> 00:21:20,719 And then we'll see a little bit later of 592 00:21:20,720 --> 00:21:21,720 why this is. 593 00:21:23,530 --> 00:21:24,530 OK, 594 00:21:25,780 --> 00:21:28,119 so who here knows 595 00:21:28,120 --> 00:21:29,490 a little bit of relock? 596 00:21:31,780 --> 00:21:34,569 Oh, that's good. It's at least at least 597 00:21:34,570 --> 00:21:36,549 maybe maybe maybe 30 percent, maybe maybe 598 00:21:36,550 --> 00:21:37,750 half of that. That's correct. 599 00:21:38,800 --> 00:21:41,139 So for formal verification, you need to 600 00:21:41,140 --> 00:21:43,329 have some additional statements 601 00:21:43,330 --> 00:21:44,589 in the language. 602 00:21:45,730 --> 00:21:47,799 Namely, you need to have a way 603 00:21:47,800 --> 00:21:49,899 to create assertions and you need a 604 00:21:49,900 --> 00:21:51,369 way to create assumptions. 605 00:21:51,370 --> 00:21:53,979 And we've seen those assert and assume 606 00:21:53,980 --> 00:21:55,929 statements already in the world. 607 00:21:55,930 --> 00:21:58,430 Example I just showed you before. 608 00:21:59,530 --> 00:22:02,319 So when you have a stop, some expression, 609 00:22:02,320 --> 00:22:04,689 it just says we say 610 00:22:04,690 --> 00:22:07,299 this expression must always be true. 611 00:22:07,300 --> 00:22:09,489 And if there is a way to make 612 00:22:09,490 --> 00:22:11,649 this and this expression of forest, then 613 00:22:11,650 --> 00:22:13,659 this is a back. And the tool should tell 614 00:22:13,660 --> 00:22:15,439 us how to get into the state to 615 00:22:15,440 --> 00:22:17,499 demonstrate the readability of 616 00:22:17,500 --> 00:22:18,730 this back to us 617 00:22:19,900 --> 00:22:22,029 and assume we also say 618 00:22:22,030 --> 00:22:23,979 this expression is always true, but we 619 00:22:23,980 --> 00:22:25,839 don't say it's an inherent property of 620 00:22:25,840 --> 00:22:28,299 the design. We say this is something 621 00:22:28,300 --> 00:22:29,300 we 622 00:22:30,760 --> 00:22:32,829 we restrict our proof to. 623 00:22:32,830 --> 00:22:34,929 So in some cases, you might say 624 00:22:34,930 --> 00:22:37,329 we assume that this input 625 00:22:37,330 --> 00:22:39,549 signal is only always low or 626 00:22:39,550 --> 00:22:42,039 we assume that those two inputs 627 00:22:42,040 --> 00:22:44,199 are never high at the same time, maybe 628 00:22:44,200 --> 00:22:45,939 because this is some kind of a protocol 629 00:22:45,940 --> 00:22:48,339 and we assume that the the other side 630 00:22:48,340 --> 00:22:50,619 of the the product might appear to talk. 631 00:22:50,620 --> 00:22:53,209 This protocol to this 632 00:22:53,210 --> 00:22:54,759 is using the protocol correctly. 633 00:22:54,760 --> 00:22:56,529 And maybe in this protocol, those two 634 00:22:56,530 --> 00:22:58,719 signals can't be asserted at the same 635 00:22:58,720 --> 00:23:01,059 time, restrict 636 00:23:01,060 --> 00:23:03,189 for verification, essentially does 637 00:23:03,190 --> 00:23:05,439 the same thing with, say, we don't want 638 00:23:05,440 --> 00:23:07,569 to consider traces that 639 00:23:07,570 --> 00:23:09,739 this expression is false. 640 00:23:09,740 --> 00:23:11,319 We only want to conceal the traces. 641 00:23:11,320 --> 00:23:13,599 What this expression is true. 642 00:23:13,600 --> 00:23:16,089 However, there is a little 643 00:23:16,090 --> 00:23:18,759 difference in the circumstances 644 00:23:18,760 --> 00:23:21,009 when you use assume and then you use 645 00:23:21,010 --> 00:23:23,289 restrict and 646 00:23:23,290 --> 00:23:25,479 assume you use, then your 647 00:23:25,480 --> 00:23:27,409 assertions depend on it. 648 00:23:27,410 --> 00:23:29,229 When you say, well, if this assumption 649 00:23:29,230 --> 00:23:31,059 doesn't hold and they really don't care 650 00:23:31,060 --> 00:23:33,339 about this, because I know if, 651 00:23:33,340 --> 00:23:35,619 for example, it is two lines 652 00:23:35,620 --> 00:23:37,929 that both at the same time, 653 00:23:37,930 --> 00:23:39,999 then my car will go into some crazy 654 00:23:40,000 --> 00:23:42,159 state because I 655 00:23:42,160 --> 00:23:44,269 brought my car under the assumption that 656 00:23:44,270 --> 00:23:46,599 the I'm talking this protocol to Will 657 00:23:46,600 --> 00:23:49,329 Will actually the product specification 658 00:23:49,330 --> 00:23:51,529 with restriction V, 659 00:23:51,530 --> 00:23:54,669 v, v essentially say 660 00:23:54,670 --> 00:23:57,369 this makes the proof easier 661 00:23:57,370 --> 00:23:59,559 if you assume this expression, but 662 00:23:59,560 --> 00:24:02,469 it's not really necessary for our 663 00:24:02,470 --> 00:24:04,119 assertions to hold. 664 00:24:05,140 --> 00:24:07,689 And because of that, then an assumption 665 00:24:07,690 --> 00:24:08,739 is violated. 666 00:24:08,740 --> 00:24:11,139 Simulation will also produce an error, 667 00:24:11,140 --> 00:24:13,839 but even a restriction is violated 668 00:24:13,840 --> 00:24:15,789 in simulation. Then they don't care 669 00:24:15,790 --> 00:24:18,069 because we've set assassins' don't 670 00:24:18,070 --> 00:24:19,029 really depend on it. 671 00:24:19,030 --> 00:24:20,919 It's just an additional thing for formal 672 00:24:20,920 --> 00:24:21,920 verification 673 00:24:23,330 --> 00:24:24,999 that makes the proof a little bit easier. 674 00:24:28,570 --> 00:24:30,729 There are immediate assertions 675 00:24:30,730 --> 00:24:33,219 and concurrent assertions in the Haluk, 676 00:24:33,220 --> 00:24:35,349 so immediate assertions 677 00:24:35,350 --> 00:24:37,269 are within the behavioral block like 678 00:24:37,270 --> 00:24:39,429 initial always and 679 00:24:39,430 --> 00:24:41,589 the we can use, assume and sound 680 00:24:41,590 --> 00:24:43,089 like like a normal statement. 681 00:24:44,200 --> 00:24:46,359 Concurrent assertions are used 682 00:24:46,360 --> 00:24:48,609 in your context 683 00:24:48,610 --> 00:24:51,459 and essentially assume or assert 684 00:24:51,460 --> 00:24:53,919 that something will hold forever 685 00:24:53,920 --> 00:24:55,179 in our state. 686 00:24:55,180 --> 00:24:56,829 That is in the behavior of our part. 687 00:24:56,830 --> 00:24:59,629 We could use an if statement to 688 00:24:59,630 --> 00:25:02,139 try to add an additional a condition 689 00:25:02,140 --> 00:25:05,229 to discussion or an assumption. 690 00:25:05,230 --> 00:25:07,089 And then this assumption assumption would 691 00:25:07,090 --> 00:25:08,799 only need to be true. 692 00:25:08,800 --> 00:25:11,739 Then the if statement Audiovox 693 00:25:11,740 --> 00:25:13,789 usually the concurrent assertions and 694 00:25:13,790 --> 00:25:15,969 they are used with system 695 00:25:15,970 --> 00:25:18,189 of properties that 696 00:25:18,190 --> 00:25:19,959 can be temporal properties. 697 00:25:19,960 --> 00:25:21,549 But right now your source doesn't support 698 00:25:21,550 --> 00:25:22,789 any of that. 699 00:25:22,790 --> 00:25:24,999 So and because of that, 700 00:25:25,000 --> 00:25:26,000 we could say 701 00:25:27,760 --> 00:25:29,499 when we're using users, when they're 702 00:25:29,500 --> 00:25:31,689 using this flow, then usually we 703 00:25:31,690 --> 00:25:33,849 will use immediate assassins', but 704 00:25:33,850 --> 00:25:36,159 between within and behave a block like 705 00:25:36,160 --> 00:25:37,529 initial olelbis. 706 00:25:39,830 --> 00:25:40,830 OK. 707 00:25:41,820 --> 00:25:43,529 Former test benchers, 708 00:25:45,670 --> 00:25:47,949 so in simulation, we usually have a test 709 00:25:47,950 --> 00:25:50,019 bench that creates input 710 00:25:50,020 --> 00:25:51,789 signal as far as I could and stuff like 711 00:25:51,790 --> 00:25:52,790 that. 712 00:25:54,100 --> 00:25:56,439 With formal verification, 713 00:25:56,440 --> 00:25:59,179 you also sometimes use test benches, 714 00:25:59,180 --> 00:26:01,509 however, those test benches don't 715 00:26:05,410 --> 00:26:07,689 play through one possible 716 00:26:07,690 --> 00:26:09,759 path with our circus like a 717 00:26:09,760 --> 00:26:11,829 normal simulation test against us. 718 00:26:11,830 --> 00:26:13,540 Instead, we 719 00:26:15,920 --> 00:26:18,399 would just add some external restrictions 720 00:26:18,400 --> 00:26:20,499 or assumptions for stuff 721 00:26:20,500 --> 00:26:22,809 like well researched below 722 00:26:22,810 --> 00:26:25,239 and the far sighted things like that. 723 00:26:25,240 --> 00:26:27,459 But other than that, we believe a lot 724 00:26:27,460 --> 00:26:30,069 of our free room for the verification 725 00:26:30,070 --> 00:26:32,139 tour to actually explore 726 00:26:32,140 --> 00:26:34,419 different different parts and 727 00:26:34,420 --> 00:26:36,579 and and see if 728 00:26:36,580 --> 00:26:39,309 using the thing in the former 729 00:26:39,310 --> 00:26:41,529 test bench it can can reach 730 00:26:41,530 --> 00:26:42,699 an invalid state. 731 00:26:42,700 --> 00:26:44,829 So this is a variation 732 00:26:44,830 --> 00:26:47,169 of of the science 733 00:26:47,170 --> 00:26:49,509 we had before the HelloWallet design. 734 00:26:49,510 --> 00:26:51,009 But now we're using your former test 735 00:26:51,010 --> 00:26:53,619 bench. You see, I've removed 736 00:26:53,620 --> 00:26:55,689 the initialization for the counter. 737 00:26:55,690 --> 00:26:58,019 So now we only have there's always blocks 738 00:26:58,020 --> 00:26:59,049 traversable. 739 00:26:59,050 --> 00:27:01,269 If reset is higher than the set, count 740 00:27:01,270 --> 00:27:04,689 to zero. Otherwise we increment count. 741 00:27:04,690 --> 00:27:06,729 And then our former test bench on the 742 00:27:06,730 --> 00:27:08,949 right, we assume that the reset 743 00:27:08,950 --> 00:27:11,079 signal will be higher initially 744 00:27:11,080 --> 00:27:12,459 and the first cycler. 745 00:27:12,460 --> 00:27:14,619 So because of that, we we 746 00:27:14,620 --> 00:27:17,169 we've reset the design from outside, 747 00:27:17,170 --> 00:27:19,019 from the test bench in the first cycle. 748 00:27:20,200 --> 00:27:22,269 And then you have the same assumption and 749 00:27:22,270 --> 00:27:24,429 the same combination you had before, 750 00:27:24,430 --> 00:27:26,589 but now with a condition around it 751 00:27:26,590 --> 00:27:28,929 that we don't check it in in the initial 752 00:27:28,930 --> 00:27:30,219 state. 753 00:27:30,220 --> 00:27:32,019 So in the initial state, they don't care 754 00:27:32,020 --> 00:27:33,489 what the count is because it can be 755 00:27:33,490 --> 00:27:34,490 anything. 756 00:27:35,110 --> 00:27:37,209 They just paid for the reset to complete. 757 00:27:37,210 --> 00:27:39,969 And after the reset has completed, 758 00:27:39,970 --> 00:27:41,859 then we are not in the initial state 759 00:27:41,860 --> 00:27:44,169 anymore. Then we actually apply 760 00:27:44,170 --> 00:27:45,249 our assumption in the. 761 00:27:49,900 --> 00:27:50,900 OK. 762 00:27:52,670 --> 00:27:54,680 This is a slide I thought I removed. 763 00:27:58,430 --> 00:27:59,430 Oh, 764 00:28:01,280 --> 00:28:02,280 yeah, 765 00:28:03,920 --> 00:28:06,009 so bounded and unbounded methods. 766 00:28:06,010 --> 00:28:08,299 This is this is terminology you will hear 767 00:28:08,300 --> 00:28:10,609 a lot when when when I'm 768 00:28:10,610 --> 00:28:11,269 reading. 769 00:28:11,270 --> 00:28:13,789 I'm talking about a former method, 770 00:28:13,790 --> 00:28:16,399 a bounded method, essentially says 771 00:28:16,400 --> 00:28:18,169 we check that the property holds within 772 00:28:18,170 --> 00:28:20,689 the first End-Time steps. 773 00:28:20,690 --> 00:28:22,789 And we had this before here and I just 774 00:28:22,790 --> 00:28:25,399 call yours SMTP mce without 775 00:28:25,400 --> 00:28:28,399 a parameter then given the bounded 776 00:28:28,400 --> 00:28:30,619 model check for 20 777 00:28:30,620 --> 00:28:33,079 cycles and then inbounded method 778 00:28:33,080 --> 00:28:34,489 is we would like to prove that the 779 00:28:34,490 --> 00:28:36,919 property holds forever and not only 780 00:28:36,920 --> 00:28:39,049 for a limited number of 781 00:28:39,050 --> 00:28:40,940 cycles after the initial state. 782 00:28:42,170 --> 00:28:44,509 So PMC, which is part 783 00:28:44,510 --> 00:28:46,819 of the user Stasch assumptive 784 00:28:46,820 --> 00:28:49,129 BMC name is bounded 785 00:28:49,130 --> 00:28:51,859 model check. That's a bounded method 786 00:28:51,860 --> 00:28:54,319 and temporal induction is a mechanism 787 00:28:54,320 --> 00:28:56,399 that that builds in a 788 00:28:56,400 --> 00:28:59,269 way on a bounded model check 789 00:28:59,270 --> 00:29:01,429 and extends the 790 00:29:01,430 --> 00:29:03,589 validity of the of the check 791 00:29:03,590 --> 00:29:05,680 for Fiverr. 792 00:29:08,480 --> 00:29:10,969 Let's have a look how we can do that. 793 00:29:10,970 --> 00:29:13,159 That's the bounded model check. 794 00:29:13,160 --> 00:29:14,930 So we create 795 00:29:16,730 --> 00:29:19,129 a former circuit within our tool that 796 00:29:19,130 --> 00:29:21,949 more or less looks like the example 797 00:29:21,950 --> 00:29:23,039 at the top here. 798 00:29:23,040 --> 00:29:25,519 If you have an initial state in yellow 799 00:29:25,520 --> 00:29:27,140 and then three 800 00:29:28,370 --> 00:29:30,949 states that follow the initial state 801 00:29:30,950 --> 00:29:32,509 does that the green states here. 802 00:29:32,510 --> 00:29:34,639 And for each of those four states, 803 00:29:34,640 --> 00:29:37,279 we check if all the assumptions 804 00:29:37,280 --> 00:29:39,619 hold. So this is the 805 00:29:39,620 --> 00:29:42,109 way of creating a bounded model check. 806 00:29:42,110 --> 00:29:44,329 Remember this now 807 00:29:44,330 --> 00:29:46,489 I like former states like very obvious. 808 00:29:46,490 --> 00:29:48,199 They're like placeholders for all the 809 00:29:48,200 --> 00:29:49,549 states that are possible. 810 00:29:49,550 --> 00:29:51,199 The only thing that they constrain as the 811 00:29:51,200 --> 00:29:52,849 first one should be a yellow one. 812 00:29:52,850 --> 00:29:55,309 It should be an initial state. 813 00:29:55,310 --> 00:29:57,469 And the others don't need to be initial 814 00:29:57,470 --> 00:29:59,119 states. Their only constraint that there 815 00:29:59,120 --> 00:30:01,309 must be a valid state that can 816 00:30:01,310 --> 00:30:02,630 follow after 817 00:30:03,710 --> 00:30:05,929 the initial state in case of the second 818 00:30:05,930 --> 00:30:06,930 and so on. 819 00:30:08,310 --> 00:30:09,559 And this works. 820 00:30:09,560 --> 00:30:11,269 So this is a correct way of making 821 00:30:11,270 --> 00:30:13,669 inbounded model check for four and equals 822 00:30:13,670 --> 00:30:16,129 the three time steps. 823 00:30:16,130 --> 00:30:17,539 But it's not very efficient. 824 00:30:17,540 --> 00:30:19,609 And in practice, it turns out it's 825 00:30:19,610 --> 00:30:21,799 much more efficient to use the scheme 826 00:30:21,800 --> 00:30:23,659 on the bottom half of the slide. 827 00:30:23,660 --> 00:30:26,239 The first just create a symbolic 828 00:30:26,240 --> 00:30:28,189 initial state. So as symbolic state that 829 00:30:28,190 --> 00:30:30,919 can represent any initial state 830 00:30:30,920 --> 00:30:33,079 and the check is there and the initial 831 00:30:33,080 --> 00:30:35,239 state that violates one 832 00:30:35,240 --> 00:30:36,439 of my assertions. 833 00:30:36,440 --> 00:30:38,089 And if there is such an additional state, 834 00:30:38,090 --> 00:30:40,189 then we are done. I just output the state 835 00:30:40,190 --> 00:30:42,589 and say, well, obviously this initial 836 00:30:42,590 --> 00:30:44,929 state violates our sanctions. 837 00:30:44,930 --> 00:30:46,250 So this is your counter example. 838 00:30:47,330 --> 00:30:49,669 If this 839 00:30:49,670 --> 00:30:51,829 does not succeed in 840 00:30:51,830 --> 00:30:53,209 the way for the tool we've got, the tool 841 00:30:53,210 --> 00:30:55,489 would like to find the back so it doesn't 842 00:30:55,490 --> 00:30:56,599 find it back here. 843 00:30:56,600 --> 00:30:58,939 We figure out that already 844 00:30:58,940 --> 00:31:01,579 initial states actually conform 845 00:31:01,580 --> 00:31:02,809 to the assertions. 846 00:31:02,810 --> 00:31:04,969 Then we create a former 847 00:31:04,970 --> 00:31:06,500 model for two states. 848 00:31:07,610 --> 00:31:10,489 And now we can we can assume 849 00:31:10,490 --> 00:31:12,259 that all the assertions in the first 850 00:31:12,260 --> 00:31:14,269 state will hold because that's what we 851 00:31:14,270 --> 00:31:16,010 just proved in the first state. 852 00:31:21,110 --> 00:31:22,110 Uh. 853 00:31:23,960 --> 00:31:25,939 Yeah, and so on, so if I find something 854 00:31:25,940 --> 00:31:28,249 here, but a counterexample that's too 855 00:31:28,250 --> 00:31:29,959 steep, if it doesn't count. 856 00:31:29,960 --> 00:31:32,029 Well, we move on to the to the next 857 00:31:32,030 --> 00:31:34,219 state, our next step and make 858 00:31:34,220 --> 00:31:35,390 it prove that the three 859 00:31:37,190 --> 00:31:39,109 cycliste and so forth. 860 00:31:39,110 --> 00:31:40,849 And in practice, this turns out to be 861 00:31:40,850 --> 00:31:42,919 much, much more efficient than the 862 00:31:42,920 --> 00:31:44,039 naive approach. 863 00:31:44,040 --> 00:31:46,189 I would like to prove like everything 864 00:31:46,190 --> 00:31:48,259 at once, especially if you would like 865 00:31:48,260 --> 00:31:50,509 to do a deep founded model check like 100 866 00:31:50,510 --> 00:31:51,740 cycliste or something like that. 867 00:31:53,120 --> 00:31:55,429 So tentpole induction now 868 00:31:55,430 --> 00:31:57,559 takes one of those bounded model checks 869 00:31:57,560 --> 00:31:59,749 of now we have one of those founded model 870 00:31:59,750 --> 00:32:01,339 checks above. 871 00:32:01,340 --> 00:32:03,499 It's then the implementation that really 872 00:32:03,500 --> 00:32:04,500 doesn't matter. 873 00:32:05,300 --> 00:32:07,159 And then they create the proof that you 874 00:32:07,160 --> 00:32:09,200 see in the middle of the slide here. 875 00:32:10,520 --> 00:32:12,589 So initially we say there 876 00:32:12,590 --> 00:32:14,989 is an initial state followed 877 00:32:14,990 --> 00:32:17,389 by three other states and none 878 00:32:17,390 --> 00:32:19,219 of them violates any assertions and they 879 00:32:19,220 --> 00:32:20,509 have proven that. 880 00:32:20,510 --> 00:32:22,709 And now we would like to prove that. 881 00:32:22,710 --> 00:32:25,130 Then there are three states. 882 00:32:26,140 --> 00:32:28,599 Consecutive that don't violate 883 00:32:28,600 --> 00:32:30,969 assassin, then there is no way 884 00:32:30,970 --> 00:32:33,199 for a first date to violate 885 00:32:33,200 --> 00:32:34,329 the session. 886 00:32:34,330 --> 00:32:36,459 And if this if this works, if 887 00:32:36,460 --> 00:32:38,559 we can prove this, we have obviously 888 00:32:38,560 --> 00:32:41,349 proven that this option will hold forever 889 00:32:41,350 --> 00:32:42,350 because. 890 00:32:43,550 --> 00:32:45,679 This here kind of fits together, so 891 00:32:45,680 --> 00:32:47,719 they can just say, well, we have proven 892 00:32:47,720 --> 00:32:51,169 one, two, three noninsured states, 893 00:32:51,170 --> 00:32:53,419 so this exists and if this 894 00:32:53,420 --> 00:32:55,639 proof holds, we know every 895 00:32:55,640 --> 00:32:57,679 state that follows the failed state here 896 00:32:57,680 --> 00:32:58,680 must also 897 00:33:00,830 --> 00:33:02,749 conform with our assumptions. 898 00:33:02,750 --> 00:33:04,939 And then I just take this 899 00:33:04,940 --> 00:33:06,799 proof that I have made and I don't need 900 00:33:06,800 --> 00:33:07,849 to change this proof. 901 00:33:07,850 --> 00:33:09,679 I don't need to rerun this proof. 902 00:33:09,680 --> 00:33:11,809 Just think of moving this one 903 00:33:11,810 --> 00:33:13,579 step to the right and I can apply the 904 00:33:13,580 --> 00:33:15,769 same argument again and again and again. 905 00:33:15,770 --> 00:33:17,299 And therefore I have proven that my 906 00:33:17,300 --> 00:33:18,769 properties will hold forever. 907 00:33:18,770 --> 00:33:19,849 So this is great. 908 00:33:19,850 --> 00:33:21,529 However, it doesn't always work. 909 00:33:22,850 --> 00:33:25,249 So if if this kind of thing 910 00:33:25,250 --> 00:33:27,409 works and tells us, well, the 911 00:33:27,410 --> 00:33:28,410 science seems to be fine, 912 00:33:29,840 --> 00:33:30,840 then 913 00:33:32,960 --> 00:33:34,039 then everything is good. 914 00:33:34,040 --> 00:33:36,229 But this might tell us I can't 915 00:33:36,230 --> 00:33:37,549 I can't do this. 916 00:33:37,550 --> 00:33:38,659 I can't do this proof. 917 00:33:38,660 --> 00:33:40,459 I find a counterexample. 918 00:33:40,460 --> 00:33:42,619 And now this counterexample can 919 00:33:42,620 --> 00:33:45,049 mean, well, maybe my assertions 920 00:33:45,050 --> 00:33:47,269 are violated somewhere deeper in 921 00:33:47,270 --> 00:33:49,519 the state space or it can mean 922 00:33:49,520 --> 00:33:50,520 well, maybe, 923 00:33:54,320 --> 00:33:55,849 maybe everything is correct. 924 00:33:55,850 --> 00:33:58,039 But I just need a deeper induction 925 00:33:58,040 --> 00:34:00,139 proof. Maybe it doesn't work with three 926 00:34:00,140 --> 00:34:02,449 time steps. Maybe it only works with 20 927 00:34:02,450 --> 00:34:04,549 or 100, or maybe it doesn't work 928 00:34:04,550 --> 00:34:05,809 at all. 929 00:34:05,810 --> 00:34:08,299 And that's what we see in this picture. 930 00:34:08,300 --> 00:34:09,300 So. 931 00:34:13,570 --> 00:34:16,149 Here again, we have the states 932 00:34:16,150 --> 00:34:18,908 that violate assertions and that 933 00:34:18,909 --> 00:34:21,129 then we have all the states in 934 00:34:21,130 --> 00:34:23,349 this area. So if you look 935 00:34:23,350 --> 00:34:25,089 at the direction of the arrows, you see 936 00:34:25,090 --> 00:34:27,009 there is no arrow going out from this 937 00:34:27,010 --> 00:34:28,718 either barber to the barber. 938 00:34:28,719 --> 00:34:30,729 So there's actually are the regional 939 00:34:30,730 --> 00:34:31,959 states and the systems. 940 00:34:31,960 --> 00:34:34,059 However, usually we don't have an 941 00:34:34,060 --> 00:34:36,428 explicit representation of an explicit 942 00:34:36,429 --> 00:34:38,709 picture like this of all the states. 943 00:34:40,540 --> 00:34:42,849 And then we have this this 944 00:34:42,850 --> 00:34:44,439 intermediate zone here 945 00:34:45,969 --> 00:34:48,759 where there are states 946 00:34:48,760 --> 00:34:50,919 that are OK with our sessions, 947 00:34:50,920 --> 00:34:53,198 but nevertheless unreachable. 948 00:34:53,199 --> 00:34:55,419 And when we look at this proof 949 00:34:55,420 --> 00:34:57,519 that we are trying to do this here, 950 00:34:57,520 --> 00:34:59,499 we don't we don't know if these states 951 00:34:59,500 --> 00:35:01,119 are very chipper or not. 952 00:35:02,320 --> 00:35:04,419 So we could, for example, 953 00:35:04,420 --> 00:35:06,849 find here one, two, three 954 00:35:06,850 --> 00:35:09,219 states that are OK with our assertions, 955 00:35:09,220 --> 00:35:11,439 followed by a state that's not OK with 956 00:35:11,440 --> 00:35:12,489 our assumptions. 957 00:35:12,490 --> 00:35:15,579 So if you find something like that are 958 00:35:15,580 --> 00:35:17,079 the easiest thing we can do, we can 959 00:35:17,080 --> 00:35:18,909 increment the index length. 960 00:35:18,910 --> 00:35:21,609 So here we need at least five 961 00:35:21,610 --> 00:35:23,509 consecutive states because they are. 962 00:35:23,510 --> 00:35:25,749 But if you say we have proven for five 963 00:35:25,750 --> 00:35:27,579 consecutive states that are OK with our 964 00:35:27,580 --> 00:35:29,769 sessions, then 965 00:35:29,770 --> 00:35:31,839 then we won't get a counterexample 966 00:35:31,840 --> 00:35:33,969 here. However, we might get 967 00:35:33,970 --> 00:35:35,349 a counter example here. 968 00:35:35,350 --> 00:35:35,979 Why? 969 00:35:35,980 --> 00:35:38,229 Because there is a loop and 970 00:35:38,230 --> 00:35:41,079 in this loop I can fit and arbitrarily 971 00:35:41,080 --> 00:35:43,239 long sequence of states that are 972 00:35:43,240 --> 00:35:44,709 OK with my assertions. 973 00:35:44,710 --> 00:35:47,259 And then in the end I break out and 974 00:35:47,260 --> 00:35:48,909 reach this state here. 975 00:35:48,910 --> 00:35:51,309 So here I can't just make the induction 976 00:35:51,310 --> 00:35:53,379 longer, have to use something 977 00:35:53,380 --> 00:35:55,569 else. For example, I have to add 978 00:35:55,570 --> 00:35:58,059 an additional assertion to my design 979 00:35:58,060 --> 00:36:00,129 that invalidates one of those four 980 00:36:00,130 --> 00:36:01,360 states that built the loop. 981 00:36:02,520 --> 00:36:05,009 And if I do this, 982 00:36:05,010 --> 00:36:07,109 then I can can prove this example 983 00:36:07,110 --> 00:36:08,849 by induction, because I don't have this 984 00:36:08,850 --> 00:36:10,219 this this loop there anymore. 985 00:36:11,740 --> 00:36:12,740 I'm. 986 00:36:15,220 --> 00:36:17,379 So when 987 00:36:17,380 --> 00:36:18,699 you would like to do this one, you would 988 00:36:18,700 --> 00:36:20,979 like to make such a proof of 989 00:36:20,980 --> 00:36:23,109 this is the entire floor, you'd be 990 00:36:23,110 --> 00:36:25,399 using you you'd use you take 991 00:36:25,400 --> 00:36:27,489 your lock designed your assertions, you 992 00:36:27,490 --> 00:36:28,759 put them through your source. 993 00:36:28,760 --> 00:36:31,479 You also generate some key tulip model. 994 00:36:31,480 --> 00:36:34,029 Then we put this into yours as SMTP, 995 00:36:34,030 --> 00:36:36,579 BMC, together with an external 996 00:36:36,580 --> 00:36:37,600 constraints. Fine, 997 00:36:38,980 --> 00:36:41,259 pass it to the server and 998 00:36:41,260 --> 00:36:43,809 then I get a pass fail information. 999 00:36:43,810 --> 00:36:46,269 And if it fails, I get a counterexample 1000 00:36:46,270 --> 00:36:48,669 with if you file or a 1001 00:36:48,670 --> 00:36:50,289 test bench that reproduces the 1002 00:36:50,290 --> 00:36:52,599 counterexample, why are constraints filed 1003 00:36:52,600 --> 00:36:55,179 that I could put back in on 1004 00:36:55,180 --> 00:36:56,709 the left side? 1005 00:36:56,710 --> 00:36:58,539 For example, if I would like to just 1006 00:36:58,540 --> 00:37:01,239 easily reproduce 1007 00:37:01,240 --> 00:37:02,560 a thing that I found before. 1008 00:37:05,050 --> 00:37:07,269 So the typical backflow would be 1009 00:37:07,270 --> 00:37:09,149 the fast run abounded model check. 1010 00:37:09,150 --> 00:37:11,289 That's the easy part, we say 1011 00:37:11,290 --> 00:37:13,389 for 10 steps, for 20 steps. 1012 00:37:13,390 --> 00:37:15,519 See if you can find a violation of my 1013 00:37:15,520 --> 00:37:17,260 assertions within 10 or 20 steps. 1014 00:37:18,610 --> 00:37:19,810 And if this is 1015 00:37:20,980 --> 00:37:22,569 if this fails, then we know we have it 1016 00:37:22,570 --> 00:37:23,529 back. 1017 00:37:23,530 --> 00:37:25,479 We know we either have it back or one of 1018 00:37:25,480 --> 00:37:27,039 our suggestions is bogus. 1019 00:37:27,040 --> 00:37:29,289 This is, of course, also an 1020 00:37:29,290 --> 00:37:30,519 option. 1021 00:37:30,520 --> 00:37:33,609 So the solution is either fix the back 1022 00:37:33,610 --> 00:37:36,459 or add additional assumptions 1023 00:37:36,460 --> 00:37:38,559 or loosen the sanctions 1024 00:37:38,560 --> 00:37:39,869 so that everything is fine. 1025 00:37:41,170 --> 00:37:43,299 If this passes, then we move on to 1026 00:37:43,300 --> 00:37:44,529 step two. 1027 00:37:44,530 --> 00:37:46,269 And step two is this this temple 1028 00:37:46,270 --> 00:37:48,039 induction step. 1029 00:37:48,040 --> 00:37:50,919 And if that fails, 1030 00:37:50,920 --> 00:37:52,899 then we have to investigate the 1031 00:37:52,900 --> 00:37:54,579 counterexample we get and make a 1032 00:37:54,580 --> 00:37:56,739 decision. Is this remember what 1033 00:37:56,740 --> 00:37:59,019 the soldier is showing us or is this not 1034 00:37:59,020 --> 00:38:00,369 reachable? 1035 00:38:00,370 --> 00:38:02,769 This is our judgment call, essentially. 1036 00:38:02,770 --> 00:38:04,929 And if it's Cheverton the same 1037 00:38:04,930 --> 00:38:06,339 thing as before, we have to fix the 1038 00:38:06,340 --> 00:38:08,439 design. We have to add assumption 1039 00:38:08,440 --> 00:38:10,659 all. We have to do some assertions. 1040 00:38:10,660 --> 00:38:12,789 However, if it's unreachable, 1041 00:38:12,790 --> 00:38:15,069 then you have to add additional 1042 00:38:15,070 --> 00:38:17,309 assertions usually to tell 1043 00:38:17,310 --> 00:38:19,149 the story about that. This is actually an 1044 00:38:19,150 --> 00:38:20,260 unreachable state. 1045 00:38:21,670 --> 00:38:24,099 And that's that's the kind of dialog 1046 00:38:24,100 --> 00:38:25,389 you have with this tour. 1047 00:38:25,390 --> 00:38:27,549 While formally verifying something, 1048 00:38:27,550 --> 00:38:29,049 the soldier is giving you a 1049 00:38:29,050 --> 00:38:31,029 counterexample and you have to explain to 1050 00:38:31,030 --> 00:38:33,159 the soldier, well, that's actually not 1051 00:38:33,160 --> 00:38:35,469 reachable because this condition 1052 00:38:35,470 --> 00:38:37,539 will never become true and then the 1053 00:38:37,540 --> 00:38:39,609 sort of give you another counterexample 1054 00:38:39,610 --> 00:38:40,610 and so forth. 1055 00:38:41,620 --> 00:38:43,210 The nice thing about this is 1056 00:38:44,600 --> 00:38:46,929 when it passes, 1057 00:38:46,930 --> 00:38:49,059 we know everything is right, but 1058 00:38:49,060 --> 00:38:50,829 we still have two options. 1059 00:38:50,830 --> 00:38:53,379 We can say we'd be 1060 00:38:53,380 --> 00:38:55,449 fine with the thing we have have we have 1061 00:38:55,450 --> 00:38:57,789 proven that our design process 1062 00:38:57,790 --> 00:38:59,319 verification get done. 1063 00:38:59,320 --> 00:39:01,299 But we could also say I would like to 1064 00:39:01,300 --> 00:39:03,459 have more assassins in my 1065 00:39:03,460 --> 00:39:05,739 design and then I just reduce 1066 00:39:05,740 --> 00:39:07,869 the length and I will get another 1067 00:39:07,870 --> 00:39:10,449 counterexample now for induction 1068 00:39:10,450 --> 00:39:12,669 with with a small 1069 00:39:12,670 --> 00:39:13,899 inducts length. 1070 00:39:13,900 --> 00:39:16,029 But now I will know that 1071 00:39:16,030 --> 00:39:18,699 every counterexample I get is unreachable 1072 00:39:18,700 --> 00:39:21,249 and it's much, much easier to 1073 00:39:21,250 --> 00:39:23,049 track with this. 1074 00:39:23,050 --> 00:39:25,629 And if I make a mistake 1075 00:39:25,630 --> 00:39:27,819 and then add an assertion 1076 00:39:27,820 --> 00:39:30,039 while of telling 1077 00:39:30,040 --> 00:39:32,259 the whole that something is unreachable, 1078 00:39:32,260 --> 00:39:34,509 well, the soldier will then tell us 1079 00:39:34,510 --> 00:39:35,949 he isn't the sergeant that can be 1080 00:39:35,950 --> 00:39:38,259 violated using this at this path. 1081 00:39:38,260 --> 00:39:40,059 So there is really nothing you can 1082 00:39:40,060 --> 00:39:42,159 inherently to do wrong. 1083 00:39:43,510 --> 00:39:46,389 Um, yeah, the 1084 00:39:46,390 --> 00:39:48,189 idea would be to talk about this floor 1085 00:39:48,190 --> 00:39:49,779 again with this graphics, but I will skip 1086 00:39:49,780 --> 00:39:50,780 it. 1087 00:39:53,110 --> 00:39:55,209 So we 1088 00:39:55,210 --> 00:39:57,279 have a variation of the design 1089 00:39:57,280 --> 00:39:59,260 we had before. We have to count again. 1090 00:40:00,460 --> 00:40:02,589 But this this time we 1091 00:40:02,590 --> 00:40:04,839 have a most important remote input, 1092 00:40:04,840 --> 00:40:06,759 tells us if it should count up or if it 1093 00:40:06,760 --> 00:40:07,760 should count down. 1094 00:40:09,010 --> 00:40:11,109 And we 1095 00:40:11,110 --> 00:40:13,389 assume that initially count is five 1096 00:40:13,390 --> 00:40:16,179 and viasat that it can never be 200. 1097 00:40:16,180 --> 00:40:17,619 And if you stare at us for a little 1098 00:40:17,620 --> 00:40:19,929 while, we see this is true because 1099 00:40:19,930 --> 00:40:22,029 when it's the count is ninety nine, 1100 00:40:22,030 --> 00:40:24,039 we will not increment it any further. 1101 00:40:24,040 --> 00:40:26,109 So there is no way to go from 1102 00:40:26,110 --> 00:40:28,389 four and five to 200 1103 00:40:28,390 --> 00:40:30,069 or so. There is no way to do it with 1104 00:40:30,070 --> 00:40:31,749 another floor on the floor because it 1105 00:40:31,750 --> 00:40:32,709 count to zero. 1106 00:40:32,710 --> 00:40:34,420 We also don't incremented anymore. 1107 00:40:36,160 --> 00:40:39,099 And if we run this, uh, 1108 00:40:39,100 --> 00:40:41,169 the bounded model check 1109 00:40:41,170 --> 00:40:42,009 will work. 1110 00:40:42,010 --> 00:40:44,469 However, temple induction will not work. 1111 00:40:44,470 --> 00:40:46,329 It will give us a counterexample like 1112 00:40:46,330 --> 00:40:48,519 this that starts with one 1113 00:40:48,520 --> 00:40:50,769 hundred ninety four and 1114 00:40:50,770 --> 00:40:52,929 then increment and increment an 1115 00:40:52,930 --> 00:40:55,059 incremental decremental that will 1116 00:40:56,320 --> 00:40:58,029 do some things here really, really close 1117 00:40:58,030 --> 00:40:59,409 to two hundred. And at the end of the 1118 00:40:59,410 --> 00:41:01,809 count example and then I can increment 1119 00:41:01,810 --> 00:41:03,219 from one hundred ninety nine to two 1120 00:41:03,220 --> 00:41:04,329 hundred. 1121 00:41:04,330 --> 00:41:05,949 Of course the thing is, 1122 00:41:07,300 --> 00:41:09,469 the reason why we get the counterexample 1123 00:41:09,470 --> 00:41:11,499 like this is because we haven't really 1124 00:41:11,500 --> 00:41:13,959 told the server that count 1125 00:41:13,960 --> 00:41:16,059 equals one hundred and ninety 1126 00:41:16,060 --> 00:41:18,310 four is not reachable either. 1127 00:41:19,790 --> 00:41:22,099 So if we modify our design like this 1128 00:41:22,100 --> 00:41:24,209 and we add an additional insertion of a 1129 00:41:24,210 --> 00:41:26,569 say count is always smaller 1130 00:41:26,570 --> 00:41:28,939 than 100, then 1131 00:41:28,940 --> 00:41:31,249 the proof will work and we will 1132 00:41:31,250 --> 00:41:33,799 have proven that all this assassins' 1133 00:41:33,800 --> 00:41:36,209 actually put. 1134 00:41:36,210 --> 00:41:38,609 And because in the example I had first 1135 00:41:38,610 --> 00:41:40,139 I was only incrementing 1136 00:41:41,250 --> 00:41:43,529 and I was saying, we can't reach step 1137 00:41:43,530 --> 00:41:46,049 10 but the Assad 1138 00:41:46,050 --> 00:41:48,089 so we assume we don't reach Lieutenant 1139 00:41:48,090 --> 00:41:50,309 ViaSat, they never reach 15 1140 00:41:50,310 --> 00:41:52,379 because of that. I had to have 15 1141 00:41:52,380 --> 00:41:54,689 steps in my temper and five 1142 00:41:54,690 --> 00:41:56,789 steps in my temple and proof 1143 00:41:56,790 --> 00:41:58,919 from 15 1144 00:41:58,920 --> 00:42:01,319 to 20 in order to prove that now 1145 00:42:01,320 --> 00:42:03,629 that we have correctly described 1146 00:42:03,630 --> 00:42:06,419 the entirety of our state of our design, 1147 00:42:06,420 --> 00:42:08,759 we can actually complete temporal 1148 00:42:08,760 --> 00:42:10,409 induction with just within just one 1149 00:42:10,410 --> 00:42:11,410 second. 1150 00:42:12,780 --> 00:42:15,089 OK, I have some some some other examples 1151 00:42:15,090 --> 00:42:16,739 that I just would like to mention 1152 00:42:16,740 --> 00:42:17,940 quickly. Now, 1153 00:42:19,560 --> 00:42:22,079 there is a special command 1154 00:42:22,080 --> 00:42:24,329 called SRP Mook's 1155 00:42:24,330 --> 00:42:26,579 that adds additional assassins 1156 00:42:26,580 --> 00:42:28,709 to your design whenever there is 1157 00:42:28,710 --> 00:42:30,389 a parallel case statement. 1158 00:42:31,560 --> 00:42:33,719 And then this this example, we have 1159 00:42:33,720 --> 00:42:35,909 a parallel statement in the analog. 1160 00:42:35,910 --> 00:42:38,909 So we as a designer tell the tour 1161 00:42:38,910 --> 00:42:41,009 that those two cases and the parallel 1162 00:42:41,010 --> 00:42:43,109 case statement are exclusive and 1163 00:42:43,110 --> 00:42:45,359 that we might use this information 1164 00:42:45,360 --> 00:42:47,280 to do any optimizations. 1165 00:42:48,450 --> 00:42:51,719 And if if we are wrong about this, 1166 00:42:51,720 --> 00:42:53,849 this thing that we say well, is the case 1167 00:42:53,850 --> 00:42:56,429 statement is parallel, then we 1168 00:42:56,430 --> 00:42:57,430 might run into. 1169 00:42:58,840 --> 00:43:01,089 Even more problems 1170 00:43:01,090 --> 00:43:03,429 because we might, for example, test 1171 00:43:03,430 --> 00:43:05,649 our design and FPGA for many, 1172 00:43:05,650 --> 00:43:08,469 many hours and everything, that's fine. 1173 00:43:08,470 --> 00:43:10,299 And it turns out the reason is because 1174 00:43:10,300 --> 00:43:12,939 maybe this FPGA tool in this instance 1175 00:43:12,940 --> 00:43:15,519 has ignored the parallel case. 1176 00:43:15,520 --> 00:43:17,679 But then we go to an for example, 1177 00:43:17,680 --> 00:43:19,389 and we synthesize the same thing with the 1178 00:43:19,390 --> 00:43:21,699 AC tool and maybe the AC 1179 00:43:21,700 --> 00:43:23,469 will actually use this parallel case to 1180 00:43:23,470 --> 00:43:24,759 do an optimization. 1181 00:43:24,760 --> 00:43:26,979 And then all these hours of testing we've 1182 00:43:26,980 --> 00:43:30,009 done on FPGA is completely worthless. 1183 00:43:30,010 --> 00:43:32,139 But with a formal verification tool, we 1184 00:43:32,140 --> 00:43:34,459 can, of course, prove stuff like that. 1185 00:43:34,460 --> 00:43:36,789 Um, that's another 1186 00:43:36,790 --> 00:43:38,949 example. I have a memory design 1187 00:43:38,950 --> 00:43:41,259 here and I have another memory design 1188 00:43:41,260 --> 00:43:43,059 that's kind of convoluted, but sometimes 1189 00:43:43,060 --> 00:43:44,229 called looks like this. 1190 00:43:44,230 --> 00:43:46,269 And it would like to force synthesized 1191 00:43:46,270 --> 00:43:48,849 water into a 1192 00:43:48,850 --> 00:43:51,369 special form of of the resource. 1193 00:43:51,370 --> 00:43:53,199 It would like to prove that these two 1194 00:43:53,200 --> 00:43:55,269 memories are equal. 1195 00:43:55,270 --> 00:43:57,369 And if we if we do that, we 1196 00:43:57,370 --> 00:43:59,589 create this kind of formal test 1197 00:43:59,590 --> 00:44:01,509 bench that just instantiates both 1198 00:44:01,510 --> 00:44:03,009 memories in parallel. 1199 00:44:03,010 --> 00:44:04,329 And then we add this additional 1200 00:44:04,330 --> 00:44:06,849 constraint file on the upper right 1201 00:44:06,850 --> 00:44:09,199 that we assume that in the initial 1202 00:44:09,200 --> 00:44:11,319 state, the the memories in 1203 00:44:11,320 --> 00:44:13,359 those two instances are actually the 1204 00:44:13,360 --> 00:44:14,589 same. 1205 00:44:14,590 --> 00:44:17,259 And then for all the other states, 1206 00:44:17,260 --> 00:44:19,269 we assert that they are still the same. 1207 00:44:19,270 --> 00:44:21,039 And we also assert that the output, the 1208 00:44:21,040 --> 00:44:23,619 same value for the same 1209 00:44:23,620 --> 00:44:25,119 input and the input will be the same 1210 00:44:25,120 --> 00:44:27,309 because the input parts are connected to 1211 00:44:27,310 --> 00:44:28,810 the same top level input. 1212 00:44:31,360 --> 00:44:33,639 This is an example for using 1213 00:44:33,640 --> 00:44:35,439 multiple domains with yours. 1214 00:44:35,440 --> 00:44:38,349 SMP BMC is just to 1215 00:44:38,350 --> 00:44:39,909 show you that this is something that's 1216 00:44:39,910 --> 00:44:40,929 also possible. 1217 00:44:40,930 --> 00:44:42,999 So here we have a 1218 00:44:43,000 --> 00:44:45,069 counter, but we implement this 1219 00:44:45,070 --> 00:44:48,009 counter just by using the 1220 00:44:48,010 --> 00:44:50,169 the lower bid we've just created as 1221 00:44:50,170 --> 00:44:52,359 a clock input, another Pockley flipflop 1222 00:44:52,360 --> 00:44:53,679 and then we go on. 1223 00:44:53,680 --> 00:44:55,809 So if you're building 1224 00:44:55,810 --> 00:44:58,959 acounter from like Title 1225 00:44:58,960 --> 00:45:01,209 IX, then this would be a possible 1226 00:45:01,210 --> 00:45:02,269 way to build account counter. 1227 00:45:02,270 --> 00:45:03,519 Usually don't do this on a chip 1228 00:45:04,600 --> 00:45:06,939 because now we have one, two, 1229 00:45:06,940 --> 00:45:09,429 three, four different Tuckerman's here. 1230 00:45:09,430 --> 00:45:11,319 So the first Orvis block is like the 1231 00:45:11,320 --> 00:45:13,449 regular counter and then the other 1232 00:45:13,450 --> 00:45:16,359 four Orvis blocks are 1233 00:45:16,360 --> 00:45:18,279 the bits for our other counter. 1234 00:45:18,280 --> 00:45:20,979 And then we assert this two counters. 1235 00:45:20,980 --> 00:45:22,989 They must always have the same value. 1236 00:45:22,990 --> 00:45:25,539 And indeed I can, 1237 00:45:25,540 --> 00:45:27,039 I can prove this. 1238 00:45:27,040 --> 00:45:29,169 I need the special command clock to f 1239 00:45:29,170 --> 00:45:31,239 logic to enable this, 1240 00:45:31,240 --> 00:45:33,759 but then this can be done 1241 00:45:33,760 --> 00:45:36,669 similarly. This is another design 1242 00:45:36,670 --> 00:45:39,100 that I have a set reset flipflop. 1243 00:45:40,240 --> 00:45:41,979 Never use something like that in the real 1244 00:45:41,980 --> 00:45:43,119 design. It's horrible. 1245 00:45:43,120 --> 00:45:45,369 But if, if you have 1246 00:45:45,370 --> 00:45:47,469 to use it for some reason, we 1247 00:45:47,470 --> 00:45:49,629 can we can actually check 1248 00:45:49,630 --> 00:45:50,630 in. 1249 00:45:51,500 --> 00:45:53,779 And of course, and 1250 00:45:53,780 --> 00:45:55,579 this is actually what exciting stories do 1251 00:45:55,580 --> 00:45:57,079 for us, we said flip flop because they 1252 00:45:57,080 --> 00:45:59,179 don't have the resources to create 1253 00:45:59,180 --> 00:46:01,189 this weird thing with two flip flops on 1254 00:46:01,190 --> 00:46:02,839 the latch and them. 1255 00:46:02,840 --> 00:46:04,759 And we can actually prove that this is 1256 00:46:04,760 --> 00:46:07,219 the right thing to do, that this is a 1257 00:46:07,220 --> 00:46:09,559 flip flop like this can also 1258 00:46:09,560 --> 00:46:11,329 cost them things. 1259 00:46:11,330 --> 00:46:12,980 I'm not going to talk about them. 1260 00:46:14,930 --> 00:46:17,089 There is a larger project going on right 1261 00:46:17,090 --> 00:46:19,369 now trying to do end to end farmer 1262 00:46:19,370 --> 00:46:21,619 verification of his 1263 00:46:21,620 --> 00:46:22,620 five processors. 1264 00:46:23,660 --> 00:46:25,959 It's called Risk five former US. 1265 00:46:25,960 --> 00:46:27,349 I'm working on that right now. 1266 00:46:27,350 --> 00:46:29,479 And this is also, of course, using 1267 00:46:29,480 --> 00:46:31,759 a lot of this infrastructure 1268 00:46:31,760 --> 00:46:33,559 to do this kind of verifications. 1269 00:46:33,560 --> 00:46:35,719 If I would like to look into a more 1270 00:46:35,720 --> 00:46:37,939 complex thing that can be done 1271 00:46:37,940 --> 00:46:39,589 with farmer verification and with this 1272 00:46:39,590 --> 00:46:41,239 farmer verification floor, that this 1273 00:46:41,240 --> 00:46:43,819 would probably be worth a look 1274 00:46:43,820 --> 00:46:46,009 at future work. 1275 00:46:46,010 --> 00:46:48,829 Well, I would like to add more 1276 00:46:48,830 --> 00:46:51,259 system lock assertion, 1277 00:46:51,260 --> 00:46:52,260 property support. 1278 00:46:53,300 --> 00:46:54,919 This is just something that you will find 1279 00:46:54,920 --> 00:46:57,049 a lot of existing code for farmer 1280 00:46:57,050 --> 00:46:58,129 verification tools. 1281 00:46:58,130 --> 00:47:00,199 And it would be interesting to be 1282 00:47:00,200 --> 00:47:02,269 able to use some of that with this flow 1283 00:47:02,270 --> 00:47:03,469 as well. 1284 00:47:03,470 --> 00:47:05,659 Then there is improved support for the 1285 00:47:05,660 --> 00:47:06,589 propagation. 1286 00:47:06,590 --> 00:47:08,239 So in some of my other farmer 1287 00:47:08,240 --> 00:47:11,269 verification flows, I can actually 1288 00:47:11,270 --> 00:47:14,119 model the propagation 1289 00:47:14,120 --> 00:47:16,189 exactly the way the way 1290 00:47:16,190 --> 00:47:18,199 I like LRM is specifying. 1291 00:47:18,200 --> 00:47:20,329 It would be interesting to also 1292 00:47:20,330 --> 00:47:21,919 be able to do that with this flow. 1293 00:47:23,120 --> 00:47:25,699 I have on my to do list 1294 00:47:25,700 --> 00:47:27,869 C backend for users so 1295 00:47:27,870 --> 00:47:30,049 you can take a circuit and 1296 00:47:30,050 --> 00:47:32,209 convert it to a flavor of C 1297 00:47:32,210 --> 00:47:34,639 that is is good for farmer 1298 00:47:34,640 --> 00:47:37,039 verification with see farmer verification 1299 00:47:37,040 --> 00:47:38,979 tools like, like C bruv. 1300 00:47:38,980 --> 00:47:40,640 Yes. BMC, stuff like that. 1301 00:47:44,360 --> 00:47:46,219 And also there is a project going on 1302 00:47:46,220 --> 00:47:48,499 called Symbiosis, which is like 1303 00:47:48,500 --> 00:47:50,689 a big front to, to 1304 00:47:50,690 --> 00:47:53,419 use all is userspace 1305 00:47:53,420 --> 00:47:55,819 farmer verification flows 1306 00:47:55,820 --> 00:47:57,259 without having to land. 1307 00:47:57,260 --> 00:47:59,449 And you think whenever you switch 1308 00:47:59,450 --> 00:48:01,219 from one floor to another, 1309 00:48:02,240 --> 00:48:03,240 that's it. 1310 00:48:13,090 --> 00:48:15,670 So what did we learn today, Clifford? 1311 00:48:17,380 --> 00:48:18,819 What did we learn today? 1312 00:48:18,820 --> 00:48:21,219 What did I learn today that I can speak 1313 00:48:21,220 --> 00:48:22,610 very fast? No, no, you were really 1314 00:48:24,190 --> 00:48:25,869 something you do in the normally in half 1315 00:48:25,870 --> 00:48:27,219 day. You did in the hours. 1316 00:48:27,220 --> 00:48:28,959 Yeah, yeah, yeah. 1317 00:48:28,960 --> 00:48:30,429 We have some questions at the audience. 1318 00:48:30,430 --> 00:48:31,659 I know there's one on the web. 1319 00:48:31,660 --> 00:48:33,879 I will take this right now. 1320 00:48:33,880 --> 00:48:34,880 No. 1321 00:48:35,820 --> 00:48:37,529 That's disappointing, but we have some 1322 00:48:37,530 --> 00:48:39,519 others. This man, please. 1323 00:48:39,520 --> 00:48:42,029 I did not yet understand what 1324 00:48:42,030 --> 00:48:44,309 is the difference between Yosses and just 1325 00:48:44,310 --> 00:48:46,499 using, like, any 1326 00:48:46,500 --> 00:48:48,719 kind of very simulator? 1327 00:48:48,720 --> 00:48:50,939 I mean, the simulators also 1328 00:48:50,940 --> 00:48:53,639 react on assaults and whatnot. 1329 00:48:53,640 --> 00:48:55,889 Yeah, but you have to write a test 1330 00:48:55,890 --> 00:48:59,189 bench that triggers discussion 1331 00:48:59,190 --> 00:49:01,409 and with formal verification, you don't 1332 00:49:01,410 --> 00:49:03,449 have to do that. You can't just say this 1333 00:49:03,450 --> 00:49:05,909 is the set of valid inputs 1334 00:49:05,910 --> 00:49:07,269 and are. 1335 00:49:09,560 --> 00:49:10,630 There is a better way to do that. 1336 00:49:15,320 --> 00:49:16,320 So 1337 00:49:17,650 --> 00:49:19,789 when I go to that simulation, 1338 00:49:19,790 --> 00:49:22,129 you just have individual places that may 1339 00:49:22,130 --> 00:49:24,409 or may not trigger your assertion, but 1340 00:49:24,410 --> 00:49:25,759 this form of verification. 1341 00:49:25,760 --> 00:49:28,009 Can I have a tool kit for you? 1342 00:49:28,010 --> 00:49:29,899 Looks at the big picture because it can't 1343 00:49:29,900 --> 00:49:31,249 paint the big picture. I mean, this is a 1344 00:49:31,250 --> 00:49:33,409 comic, but the state 1345 00:49:33,410 --> 00:49:35,569 graph for real, VITAC it would probably 1346 00:49:35,570 --> 00:49:37,459 have more states than the photons in the 1347 00:49:37,460 --> 00:49:38,629 universe. 1348 00:49:38,630 --> 00:49:39,749 The country. 1349 00:49:39,750 --> 00:49:40,750 Yeah. 1350 00:49:42,230 --> 00:49:44,989 Someone else this 1351 00:49:44,990 --> 00:49:47,239 I'm wondering if in your experiments 1352 00:49:47,240 --> 00:49:49,219 you have actually run into problems with 1353 00:49:49,220 --> 00:49:50,220 Vorkuta 1354 00:49:52,400 --> 00:49:54,169 that your solutions hold because you have 1355 00:49:54,170 --> 00:49:56,359 restricted, artificially restricted 1356 00:49:56,360 --> 00:49:58,099 the state space too far. 1357 00:49:58,100 --> 00:49:59,839 Yeah, I mean, this is possible whenever 1358 00:49:59,840 --> 00:50:02,369 you use restrict, I assume 1359 00:50:02,370 --> 00:50:04,509 you have this risk that 1360 00:50:04,510 --> 00:50:06,799 you restricted it in a way 1361 00:50:06,800 --> 00:50:08,599 so it doesn't really work anymore. 1362 00:50:08,600 --> 00:50:10,849 So in the usual backflow, you 1363 00:50:10,850 --> 00:50:12,919 often have some vehicle 1364 00:50:12,920 --> 00:50:14,989 of defiance or whatever in your design 1365 00:50:14,990 --> 00:50:17,839 that you can use to to artificially 1366 00:50:17,840 --> 00:50:18,949 add bugs. 1367 00:50:18,950 --> 00:50:21,059 And then you always check that at least 1368 00:50:21,060 --> 00:50:22,579 you still can find those parts, of 1369 00:50:22,580 --> 00:50:24,739 course. This is not a guarantee, but 1370 00:50:24,740 --> 00:50:26,449 at least that improves the situation a 1371 00:50:26,450 --> 00:50:27,450 little bit. 1372 00:50:28,530 --> 00:50:31,259 OK, a question there from outer space, 1373 00:50:31,260 --> 00:50:33,749 yes. So what kind of expressions 1374 00:50:33,750 --> 00:50:35,760 does he also support in these assertions? 1375 00:50:36,930 --> 00:50:39,089 Because essentially I only 1376 00:50:39,090 --> 00:50:41,249 support immediate assertions you 1377 00:50:41,250 --> 00:50:43,739 can use like any violent expression, 1378 00:50:43,740 --> 00:50:46,329 but it's not the system of property 1379 00:50:46,330 --> 00:50:48,449 syntax that you could use 1380 00:50:48,450 --> 00:50:50,969 to to express temporal 1381 00:50:50,970 --> 00:50:52,679 properties, insisting that all of those 1382 00:50:52,680 --> 00:50:54,170 are not supported right now. 1383 00:50:55,540 --> 00:50:57,130 One last question, yes, sir, 1384 00:50:58,600 --> 00:51:00,879 can you give me a rough idea of 1385 00:51:00,880 --> 00:51:04,359 how long the of verification 1386 00:51:04,360 --> 00:51:05,949 needs? 1387 00:51:05,950 --> 00:51:08,199 It really, really depends on the kind 1388 00:51:08,200 --> 00:51:11,109 of problem on the soldier you have 1389 00:51:11,110 --> 00:51:13,349 on many other parameters. 1390 00:51:13,350 --> 00:51:15,729 So here I have a couple of soldiers, 1391 00:51:15,730 --> 00:51:16,809 three different benchmarks. 1392 00:51:16,810 --> 00:51:19,059 And you see there is quite, quite 1393 00:51:19,060 --> 00:51:21,489 a span and always 1394 00:51:22,570 --> 00:51:24,729 maybe this is not the can can be seen 1395 00:51:24,730 --> 00:51:26,919 here. But but often you 1396 00:51:26,920 --> 00:51:29,049 have an example of really, 1397 00:51:29,050 --> 00:51:30,279 really well with one soldier. 1398 00:51:30,280 --> 00:51:31,869 But it takes a long time with another 1399 00:51:31,870 --> 00:51:33,809 soldier, but with a different problem, 1400 00:51:33,810 --> 00:51:35,469 just vice versa. 1401 00:51:35,470 --> 00:51:37,149 And because of that, it's really good 1402 00:51:37,150 --> 00:51:39,189 that we can use the that some people see 1403 00:51:39,190 --> 00:51:41,169 with almost every assembly to deliver. 1404 00:51:41,170 --> 00:51:42,170 Thank you. 1405 00:51:42,680 --> 00:51:43,899 OK, thank you, Clifford. 1406 00:51:43,900 --> 00:51:45,609 It's really fantastic to have you here. 1407 00:51:45,610 --> 00:51:47,529 And really the will that you're sharing, 1408 00:51:47,530 --> 00:51:49,629 your knowledge, your explorations 1409 00:51:49,630 --> 00:51:52,119 with all these people that 1410 00:51:52,120 --> 00:51:53,479 give him another applause, please. 1411 00:51:53,480 --> 00:51:54,480 Thank you.