| --- Log opened Sat Jul 14 00:00:12 2018 | ||
| --- Day changed Sat Jul 14 2018 | ||
| shorne | I think you showed in your blog post | 00:00 |
|---|---|---|
| ZipCPU | Perhaps on something ridiculously simple? | 00:00 |
| shorne | but either, showing from screen dumps, or a demo of running the command | 00:00 |
| * ZipCPU tugs at his beard | 00:01 | |
| shorne | yeah, either simple, or if you can show what you did for ZipCpu | 00:01 |
| shorne | i.e. the annotations and output that proved your bus interface had a timing issue | 00:01 |
| shorne | just some kind or real world tangible examples | 00:01 |
| ZipCPU | Well, my plan was to show "lessons learned" from what I did with the ZipCPU. That will therefore need to include not only some of the properties, but also how the properties were good or bad | 00:01 |
| ZipCPU | Hehe | 00:01 |
| ZipCPU | Did you read the post about finding bugs in a "working" CPU? ;) | 00:01 |
| shorne | yeah, thats good | 00:02 |
| ZipCPU | That would be real world examples for you. | 00:02 |
| shorne | Yeah, I read most of it | 00:02 |
| shorne | I think that would be good | 00:02 |
| shorne | How long does it take to run now? | 00:03 |
| ZipCPU | So ... the difficult part of running a demo of the proof for the ZipCPU is that, as I recall, it takes about 20 minutes to run. | 00:03 |
| shorne | ok... I was just thinking | 00:03 |
| ZipCPU | As a result, I run it in its pipelined mode, in its non-pipelined mode, with a data cache, without a data cache, etc. | 00:03 |
| shorne | Step 1. run this command 'yosys --args, code.v' | 00:03 |
| ZipCPU | 20 minutes means in an hour or so I can run a lot of configurations. | 00:03 |
| ZipCPU | The command is: sby -f zipcpu.sby | 00:03 |
| ZipCPU | zipcpu.sby is a SymbiYosys configuration file. I keep it in the bench/formal directory of the ZipCPU repository (dev branch currently) | 00:04 |
| shorne | Step 0. create a .sby file | 00:04 |
| shorne | Step 1. | 00:04 |
| shorne | Step 2. wait 20 minutes... | 00:04 |
| ZipCPU | Ahh, I get the question. | 00:04 |
| ZipCPU | Step 1. Add properties to your design. | 00:05 |
| ZipCPU | For example, no more than one execution unit can write to the register file at any given time. | 00:05 |
| ZipCPU | Step 2. Run sby -f zipcpu.sby | 00:05 |
| shorne | Step 3. output looks like ... | 00:05 |
| ZipCPU | Step 3. Look at the bottom of the stuff sby gives you, for PASS, FAIL or UNKNOWN. In all but PASS, there's a VCD file to pull up. | 00:06 |
| shorne | yeah, I guess I dont mean run the example, but just a quick overview. would be cool, I havent seen one before | 00:06 |
| shorne | if you think there already is enough of that out there then cool | 00:06 |
| ZipCPU | Really? That might make a good, quick, and easy blog post then. | 00:06 |
| ZipCPU | For example, I just built and verified a SPI flash controller this evening in the last four hours or so. | 00:07 |
| shorne | yeah, Blog post good, but if you could spend 4-5 minutes on it in the intro of your presentation, it would be a cool youtube video | 00:07 |
| ZipCPU | That's the size of a small fun project. | 00:07 |
| ZipCPU | Ahh, I get it, ok. | 00:07 |
| shorne | I think I got that from your previous blog post, but maybe I didnt see the .sby file | 00:07 |
| ZipCPU | Hmm .... might make more sense, though, as a separate topic. | 00:08 |
| shorne | ok | 00:08 |
| shorne | Blog post is fine too if you think it will be a full presentation | 00:08 |
| shorne | or maybe you can sign up for 2 talks :) | 00:09 |
| ZipCPU | I mean .... that's a brief in itself. When I teach formal methods, I typically spend about half to 3/4 of an hour going over thee basics. | 00:09 |
| ZipCPU | Two talks would work, if you think there would be interest in it. | 00:09 |
| shorne | ok, there maybe lots of info out there already, I haven't really looked | 00:10 |
| shorne | but I would be interested | 00:10 |
| ZipCPU | Tell you what, now that we've had this conversation, let me tweet about the idea of a separate presentation on just the basics of formal verification enabled development, and see if anyone would like the topic. I might find that useful to gauge interest, would you? What would you think about that? | 00:12 |
| shorne | ZipCPU: sounds good, if not we can just discuss it in poland | 02:11 |
| -!- [X-Scale] is now known as X-Scale | 10:24 | |
| -!- ZipCPU_ is now known as ZipCPU | 11:40 | |
| --- Log closed Sun Jul 15 00:00:58 2018 | ||
Generated by irclog2html.py 2.15.2 by Marius Gedminas - find it at mg.pov.lt!