IRC logs for #openrisc Saturday, 2018-07-14

--- Log opened Sat Jul 14 00:00:12 2018
--- Day changed Sat Jul 14 2018
shorneI think you showed in your blog post00:00
ZipCPUPerhaps on something ridiculously simple?00:00
shornebut either, showing from screen dumps, or a demo of running the command00:00
* ZipCPU tugs at his beard00:01
shorneyeah, either simple, or if you can show what you did for ZipCpu00:01
shornei.e. the annotations and output that proved your bus interface had a timing issue00:01
shornejust some kind or real world tangible examples00:01
ZipCPUWell, 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 bad00:01
ZipCPUDid you read the post about finding bugs in a "working" CPU?  ;)00:01
shorneyeah, thats good00:02
ZipCPUThat would be real world examples for you.00:02
shorneYeah, I read most of it00:02
shorneI think that would be good00:02
shorneHow long does it take to run now?00:03
ZipCPUSo ... 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
shorneok... I was just thinking00:03
ZipCPUAs 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
shorneStep 1.  run this command 'yosys --args, code.v'00:03
ZipCPU20 minutes means in an hour or so I can run a lot of configurations.00:03
ZipCPUThe command is: sby -f zipcpu.sby00:03
ZipCPUzipcpu.sby is a SymbiYosys configuration file.  I keep it in the bench/formal directory of the ZipCPU repository (dev branch currently)00:04
shorneStep 0. create a .sby file00:04
shorneStep 1.00:04
shorneStep 2. wait 20 minutes...00:04
ZipCPUAhh, I get the question.00:04
ZipCPUStep 1. Add properties to your design.00:05
ZipCPUFor example, no more than one execution unit can write to the register file at any given time.00:05
ZipCPUStep 2. Run sby -f zipcpu.sby00:05
shorneStep 3. output looks like ...00:05
ZipCPUStep 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
shorneyeah, I guess I dont mean run the example, but just a quick overview.  would be cool,  I havent seen one before00:06
shorneif you think there already is enough of that out there then cool00:06
ZipCPUReally?  That might make a good, quick, and easy blog post then.00:06
ZipCPUFor example, I just built and verified a SPI flash controller this evening in the last four hours or so.00:07
shorneyeah,  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 video00:07
ZipCPUThat's the size of a small fun project.00:07
ZipCPUAhh, I get it, ok.00:07
shorneI think I got that from your previous blog post, but maybe I didnt see the .sby file00:07
ZipCPUHmm .... might make more sense, though, as a separate topic.00:08
shorneBlog post is fine too if you think it will be a full presentation00:08
shorneor maybe you can sign up for 2 talks :)00:09
ZipCPUI 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
ZipCPUTwo talks would work, if you think there would be interest in it.00:09
shorneok, there maybe lots of info out there already, I haven't really looked00:10
shornebut I would be interested00:10
ZipCPUTell 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
shorneZipCPU: sounds good, if not we can just discuss it in poland02:11
-!- [X-Scale] is now known as X-Scale10:24
-!- ZipCPU_ is now known as ZipCPU11:40
--- Log closed Sun Jul 15 00:00:58 2018

Generated by 2.15.2 by Marius Gedminas - find it at!