| *** tpb has joined #yosys | 00:00 | |
| *** ssvb has joined #yosys | 00:05 | |
| *** cemerick has joined #yosys | 00:18 | |
| *** AlexDaniel has quit IRC | 00:31 | |
| *** AlexDaniel has joined #yosys | 00:31 | |
| *** promach2 has joined #yosys | 00:52 | |
| *** dys has quit IRC | 00:58 | |
| promach2 | ZipCPU: hi | 01:04 |
|---|---|---|
| promach2 | ZipCPU: I supppose SymbiYosys does not like me typing " ../ " in the [files] section | 01:04 |
| ZipCPU | Evening! | 01:05 |
| ZipCPU | That's not the problem. | 01:05 |
| promach2 | good evening to you | 01:05 |
| ZipCPU | The problem is that if you put two file names on the same line, SymbiYosys will try to copy the second on top of the first. | 01:05 |
| ZipCPU | If you use "../" in your filenames, the copy might adjust a file not in your design. | 01:05 |
| ZipCPU | That was the emergency bug fix of SymbiYosys | 01:05 |
| ZipCPU | You should only put one filename on a line at a time. | 01:06 |
| promach2 | there is further commit after I went to sleep yesterday ? | 01:06 |
| ZipCPU | No, that was the one | 01:06 |
| ZipCPU | Hey! 15 steps of formal for the CPU pass in less than 11 minutes! Yay! | 01:06 |
| *** cemerick has quit IRC | 01:07 | |
| promach2 | you mean for your zipcpu coding ? | 01:07 |
| ZipCPU | I'm trying to formally prove the entire CPU. | 01:07 |
| promach2 | cool | 01:07 |
| ZipCPU | I've now proven all the components, it's time to do the CPU. | 01:07 |
| promach2 | I hope I could do something like what you have bbeen doing | 01:08 |
| promach2 | including the UART ? | 01:08 |
| ZipCPU | No, just the CPU. | 01:08 |
| ZipCPU | Did you see the picture I tweeted some time back? | 01:08 |
| ZipCPU | I can post it to imgur if you didn't | 01:08 |
| ZipCPU | Try this link: https://imgur.com/HLKbSKZ | 01:09 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 01:09 |
| promach2 | https://twitter.com/zipcpu Apr 9 | 01:10 |
| ZipCPU | You found it, huh? | 01:10 |
| ZipCPU | So the "files" in the image represent separate files composing the ZipCPU. | 01:11 |
| ZipCPU | Those outlined in dashes have been replaced with abstract replacement components | 01:11 |
| ZipCPU | The red lines represent formal properties, normally found at the bottom of the file | 01:12 |
| promach2 | $anyconst results ? | 01:12 |
| ZipCPU | Yes | 01:12 |
| * ZipCPU steps away | 01:12 | |
| * ZipCPU returns | 01:18 | |
| ZipCPU | The red lines on the top represent the formal properties turned upside down, indicating an invariant relationship | 01:19 |
| promach2 | invariant ? | 01:22 |
| ZipCPU | Yes. | 01:23 |
| ZipCPU | It helps the formal methods to *zoom* forward | 01:23 |
| promach2 | what does that mean in the context of formal verification ? | 01:23 |
| promach2 | huh ? *zoom* ? | 01:23 |
| ZipCPU | It means that if once you prove (A) -> B, you don't need to prove it again. | 01:23 |
| ZipCPU | *zoom*: Move faster | 01:24 |
| ZipCPU | A couple days ago, formally verifying 15 steps of the ZipCPU was taking 4 hrs or so. | 01:24 |
| promach2 | I see, there are so many interdependent modules | 01:24 |
| ZipCPU | Yes. | 01:24 |
| ZipCPU | Today, I can do 15 steps in less than 12 minutes. | 01:24 |
| promach2 | how do you exactly manage to do this ? | 01:24 |
| ZipCPU | What's the golden rule of formal verification? | 01:25 |
| promach2 | in less than 12 minutes | 01:25 |
| ZipCPU | Assume inputs, assert local state and outputs | 01:25 |
| ZipCPU | What would happen, though, if the inputs to a file weren't the inputs to the design? | 01:25 |
| ZipCPU | You can't assume them any more. You'd instead need to assert them. | 01:25 |
| ZipCPU | See where this is going? | 01:26 |
| promach2 | you are restricting the inputs to a file to what you will get from other interdependent modules | 01:26 |
| ZipCPU | Not quite. | 01:26 |
| ZipCPU | I assume the inputs have some properties when I test the file alone. | 01:26 |
| ZipCPU | When I test the file as part of a larger system, I then *assert* that the inputs have those properties. | 01:26 |
| promach2 | huh ? | 01:27 |
| promach2 | I thought that is going to take more steps | 01:27 |
| ZipCPU | Ok, consider an example. Imagine you have a memory module. You want to assume that this module will never be given a task if it is busy. | 01:27 |
| ZipCPU | You then prove that the memory module works. | 01:28 |
| ZipCPU | Now, when you place that memory module into the bigger CPU, making assumptions within it will now mask problems. | 01:28 |
| ZipCPU | So you need to change those assumptions into assertions. | 01:28 |
| ZipCPU | The opposite applies to the assertions within a module ... ;) | 01:29 |
| promach2 | asserions within a module ? what did you with them ? | 01:30 |
| promach2 | did you do* | 01:30 |
| ZipCPU | Well, once you've proved that A -> B, you can then assume that A->B. You don't need to prove it anymore. | 01:30 |
| promach2 | wait | 01:31 |
| promach2 | but how do you assume A->B ? this does not really make sense | 01:31 |
| ZipCPU | Imagine if you will that (A) is the set of assumptions within a module, and B is the set of assertions. Within that module, you prove that if (A) is true, then B must be true. | 01:32 |
| ZipCPU | Now when you expand out, you want to prove instead that (A) is true. Once you've proved (A) is true, you already know that B must be true since you've already proven that (A)->B | 01:32 |
| promach2 | that is the flow when you are only verifying a single module on its own | 01:32 |
| ZipCPU | When I'm only verifying a single module, I assume (A) and prove that B must then be true. | 01:33 |
| promach2 | when you verifying under a big system, you assume(A->B) is true ? but how ? | 01:33 |
| ZipCPU | By ... assuming(A->B) is true. I'm not sure I understand your question. | 01:34 |
| promach2 | but B is a set of assertions | 01:34 |
| ZipCPU | Yes. | 01:34 |
| promach2 | and A->B is ..... | 01:35 |
| promach2 | A is a set of assumptions | 01:35 |
| ZipCPU | A is a list of properties, such as assume(i_input), and B is a set of properties such as assert(o_output); | 01:35 |
| ZipCPU | When that module becomes a submodule, you want to replace the assumptions with assertions, as in: assert(i_input) | 01:36 |
| ZipCPU | This works because the module is a submodule and not the parent module where it would be inappropriate. | 01:36 |
| promach2 | I see | 01:37 |
| promach2 | so, basically changing assume(A) to assert(A) | 01:37 |
| ZipCPU | Yes. | 01:38 |
| promach2 | but why is this taking fewer steps on yosys ? | 01:38 |
| ZipCPU | Well .... let's be more explicit. You are changing assume(i_A) to assert(i_A)--this is what takes place on the inputs. | 01:38 |
| promach2 | yeah | 01:38 |
| ZipCPU | On the outputs, you do the opposite, changing assert(o_A) to assume(o_A) ... that's where the dynamite is located. | 01:39 |
| promach2 | " changing assert(o_A) to assume(o_A) " <- what ?! | 01:39 |
| ZipCPU | :D | 01:39 |
| promach2 | because o_A is inputs to other modules | 01:40 |
| ZipCPU | It only works if you've already proved the assertions hold within the submodule. | 01:40 |
| ZipCPU | Making sense? | 01:41 |
| promach2 | yes | 01:43 |
| promach2 | you are reducing the number of possible combinations of data/control signals | 01:43 |
| ZipCPU | There 'ya go! | 01:43 |
| promach2 | that is why you need fewer steps on yosys | 01:43 |
| ZipCPU | No ... I still need the same number of steps | 01:44 |
| ZipCPU | I just need less time than before | 01:44 |
| promach2 | huh ? | 01:44 |
| promach2 | i do not get this | 01:44 |
| ZipCPU | Yeah. | 01:46 |
| promach2 | same number of steps, but less time ? this does not make sense | 01:46 |
| ZipCPU | Why not? What do you think determines the amount of time per step? | 01:46 |
| promach2 | I am not sure | 01:49 |
| *** sklv has quit IRC | 01:50 | |
| ZipCPU | I imagine that it's the number of possibilities the formal engine needs to check. | 01:50 |
| ZipCPU | The number of checks is likely to be a part of this as well .... | 01:50 |
| ZipCPU | If you can reduce the number of possibilities, then things should go faster, right? | 01:50 |
| *** sklv has joined #yosys | 01:50 | |
| promach2 | yeah, ok | 01:51 |
| promach2 | What about $anyconst results ? | 01:56 |
| ZipCPU | You haven't been reading my blog, now, have you? | 01:57 |
| ZipCPU | :D | 01:57 |
| ZipCPU | $anyconst is a random number, chosen once at the beginning of time | 01:57 |
| ZipCPU | $anyseq (which probably makes more sense in that conext) is a random number allowed to change from step to step | 01:58 |
| ZipCPU | *context | 01:58 |
| ZipCPU | And by "random" I mean that the formal engine gets to pick the number however it wants in order to try to make things fail. | 01:58 |
| promach2 | hmm... let me read http://zipcpu.com/zipcpu/2018/03/21/dblfetch.html first | 01:59 |
| tpb | Title: Pipelining a Prefetch (at zipcpu.com) | 01:59 |
| *** sifpwj has joined #yosys | 02:05 | |
| ZipCPU | I should mention, my next step is to you $anyconst heavily within the CPU proof. I'll pick an address and an instruction at that address, both set by $anyconst. Then anytime the address of an instruction working through the CPU matches the address, it must have the features of the instruction. | 02:06 |
| ZipCPU | That will allow me to test all instructions at once. | 02:06 |
| *** sifpwj has quit IRC | 02:08 | |
| *** pie__ has quit IRC | 02:11 | |
| *** sklv has quit IRC | 02:14 | |
| *** sklv has joined #yosys | 02:21 | |
| promach2 | ZipCPU: why do you need $anyconst and $anyseq when you will need to do induction check ? | 02:33 |
| *** emeb_mac has joined #yosys | 02:36 | |
| ZipCPU | Not sure I understand. What does induction have to do with $anyconst or $anyseq? | 02:37 |
| ZipCPU | They are two separate concepts, orthogonal to each other | 02:37 |
| promach2 | hmm.. I am confused between the two concepts then | 02:54 |
| promach2 | ZipCPU: let me read more | 02:55 |
| ZipCPU | Induction runs the proof while starting all your variables at "random" initial values | 02:55 |
| ZipCPU | $anyconst selects an arbitrary random initial value at the beginning of time. | 02:56 |
| ZipCPU | $anyseq creates an arbitrary random value at every formal step through your logic. | 02:56 |
| ZipCPU | An $anyseq variable is equivalent to an input parameter to your design | 02:56 |
| ZipCPU | By using these two, however, the formal methods don't need to change the port list of your design, and yet you can still get the benefits as though you had | 02:57 |
| promach2 | what input parameter ? | 02:58 |
| ZipCPU | An $anyseq variable is equivalent to an input parameter to your design | 03:00 |
| ZipCPU | Sorry, input port | 03:00 |
| ZipCPU | not parameter | 03:00 |
| ZipCPU | And not one in particular--any one | 03:00 |
| promach2 | I am not really sure why would $anyseq be equivalent to an input port ? | 03:12 |
| ZipCPU | From a formal method standpoint, what is known of any input port? | 03:13 |
| ZipCPU | Only its width. | 03:13 |
| ZipCPU | The value at the port can change from one clock to the next. | 03:13 |
| ZipCPU | You can make assumptions about the input, but otherwise the input can be anything. | 03:14 |
| promach2 | equivalent to having an unconstrained input (i.e. a “free variable”) to your module, but doesn’t require you to actually create such an input. | 03:14 |
| ZipCPU | The same is true of an $anyseq variable: wire [3:0] example; assign example = $anyseq; | 03:14 |
| ZipCPU | Yes. | 03:14 |
| ZipCPU | An $anyconst variable is the same, but with the assumption that it will never change throughout the design. | 03:15 |
| promach2 | wait | 03:15 |
| promach2 | but why do you need $anyseq when BMC machine could try out all possibilities ? | 03:15 |
| promach2 | is there any particular advantage if using $anyseq compared to creating another explicit input port ? | 03:16 |
| *** AlexDaniel has quit IRC | 03:20 | |
| ZipCPU | Yes. The advantage is that your design doesn't then need another explicit input port. | 03:23 |
| *** digshadow has quit IRC | 03:23 | |
| promach2 | ok | 03:24 |
| promach2 | I will have to read more on $anyconst to understand its purpose | 03:26 |
| ZipCPU | You might struggle to find material | 03:26 |
| ZipCPU | $anyconst is not standard Verilog, but rather a "feature" of yosys | 03:26 |
| promach2 | ok, With a just one simple assumption, $anyseq can be turned into an $anyconst | 03:27 |
| ZipCPU | Sure. | 03:28 |
| promach2 | ZipCPU: it is quite late for you. Would you mind if you have some rest while I spend some time reading your blog on $anyseq / $anyconst ? | 03:28 |
| ZipCPU | wire example = $anyseq; always @(posedge i_clk) if (f_past_valid) assume($stable(example)); | 03:28 |
| ZipCPU | Go ahead and read | 03:28 |
| ZipCPU | I'm finding one bug at a time in the ZipCPU and its formal properties every 40 minutes or so. | 03:29 |
| ZipCPU | I'll probably find another bug therefore in about 35 minutes .... assuming I'm still awake. | 03:30 |
| promach2 | sigh, bug-hunting never stop | 03:30 |
| ZipCPU | Yeah ... it's just annoying how slow this particular approach to bug-hunting is. | 03:30 |
| ZipCPU | The good news is that induction seems to be *much* faster than BMC at finding bugs. | 03:30 |
| * ZipCPU is not looking forward to taking this "bug-free" code and trying to meet timing with it | 03:31 | |
| promach2 | that is why I like induction so much | 03:32 |
| promach2 | induction helps us to create enough assert() for MC | 03:33 |
| promach2 | BMC* | 03:33 |
| promach2 | and cover() helps to check if the assert() is valid or not | 03:33 |
| *** digshadow has joined #yosys | 03:42 | |
| *** kmehall has joined #yosys | 03:52 | |
| promach2 | ZipCPU: http://www.designers-guide.org/Forum/YaBB.pl?num=1411555911 | 04:02 |
| tpb | Title: The Designer's Guide Community Forum - Math functions in Cadence NCVerilog (at www.designers-guide.org) | 04:02 |
| *** xrexeon has joined #yosys | 04:49 | |
| *** xrexeon has quit IRC | 05:08 | |
| *** xrexeon has joined #yosys | 05:09 | |
| *** xrexeon has joined #yosys | 05:48 | |
| *** indy has quit IRC | 06:22 | |
| *** indy has joined #yosys | 06:23 | |
| *** dys has joined #yosys | 06:31 | |
| *** GuzTech has joined #yosys | 06:48 | |
| *** emeb_mac has quit IRC | 07:07 | |
| *** emeb has quit IRC | 07:08 | |
| *** xerpi has joined #yosys | 07:14 | |
| *** proteusguy has quit IRC | 07:18 | |
| *** proteusguy has joined #yosys | 07:18 | |
| *** proteusguy has quit IRC | 07:19 | |
| *** proteusguy has joined #yosys | 07:20 | |
| *** proteusguy has quit IRC | 07:22 | |
| *** proteusguy has joined #yosys | 07:39 | |
| *** xrexeon has quit IRC | 07:40 | |
| *** dmin7 has joined #yosys | 08:40 | |
| *** promach2 has quit IRC | 08:47 | |
| *** promach2 has joined #yosys | 08:47 | |
| *** kraiskil has joined #yosys | 08:49 | |
| *** AlexDaniel has joined #yosys | 08:56 | |
| *** cemerick has joined #yosys | 09:50 | |
| *** xrexeon has joined #yosys | 11:02 | |
| *** X-Scale has quit IRC | 11:04 | |
| *** xrexeon has quit IRC | 11:20 | |
| *** proteusguy has quit IRC | 11:38 | |
| *** ralu_ is now known as ralu | 12:48 | |
| *** dys has quit IRC | 12:58 | |
| *** quigonjinn has quit IRC | 13:05 | |
| *** pie__ has joined #yosys | 13:08 | |
| *** cemerick has quit IRC | 13:40 | |
| *** leviathan has joined #yosys | 13:49 | |
| *** X-Scale has joined #yosys | 14:01 | |
| *** leviathan has quit IRC | 14:05 | |
| *** leviathan has joined #yosys | 14:05 | |
| *** eduardo has joined #yosys | 14:12 | |
| *** proteusguy has joined #yosys | 14:25 | |
| *** leviathan has quit IRC | 14:36 | |
| *** GuzTech has quit IRC | 14:55 | |
| *** dys has joined #yosys | 14:56 | |
| *** xrexeon has joined #yosys | 15:04 | |
| *** xerpi has quit IRC | 15:29 | |
| *** ZipCPU has quit IRC | 15:48 | |
| *** ZipCPU has joined #yosys | 15:51 | |
| *** leviathan has joined #yosys | 15:57 | |
| *** promach2 has quit IRC | 16:42 | |
| *** cemerick has joined #yosys | 17:45 | |
| *** goosenphil has joined #yosys | 19:11 | |
| *** proteusguy has quit IRC | 19:13 | |
| *** goosenphil has quit IRC | 19:15 | |
| *** goosenphil has joined #yosys | 19:17 | |
| *** cemerick has quit IRC | 19:20 | |
| *** proteusguy has joined #yosys | 19:24 | |
| *** proteusguy has quit IRC | 19:30 | |
| *** proteusguy has joined #yosys | 19:41 | |
| *** janrinze has joined #yosys | 19:42 | |
| *** goosenphil has quit IRC | 19:56 | |
| *** proteusguy has quit IRC | 20:13 | |
| *** proteusguy has joined #yosys | 20:14 | |
| *** proteusguy has quit IRC | 20:36 | |
| *** leviathan has quit IRC | 20:39 | |
| *** sandeepkr has quit IRC | 20:56 | |
| *** sandeepkr has joined #yosys | 20:56 | |
| *** dmin7 has quit IRC | 21:05 | |
| *** cemerick has joined #yosys | 21:29 | |
| *** cemerick has quit IRC | 21:38 | |
| *** cemerick has joined #yosys | 22:11 | |
| *** cemerick has quit IRC | 22:57 | |
| *** emeb_mac has joined #yosys | 23:17 | |
| *** emeb_mac has quit IRC | 23:20 | |
| *** pie__ has quit IRC | 23:51 | |
| *** pie_ has joined #yosys | 23:51 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!