Saturday, 2018-04-14

*** tpb has joined #yosys00:00
*** ssvb has joined #yosys00:05
*** cemerick has joined #yosys00:18
*** AlexDaniel has quit IRC00:31
*** AlexDaniel has joined #yosys00:31
*** promach2 has joined #yosys00:52
*** dys has quit IRC00:58
promach2ZipCPU: hi01:04
promach2ZipCPU: I supppose SymbiYosys does not like me typing "  ../ " in the [files] section01:04
ZipCPUThat's not the problem.01:05
promach2good evening to you01:05
ZipCPUThe 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
ZipCPUIf you use "../" in your filenames, the copy might adjust a file not in your design.01:05
ZipCPUThat was the emergency bug fix of SymbiYosys01:05
ZipCPUYou should only put one filename on a line at a time.01:06
promach2there is further commit after I went to sleep yesterday ?01:06
ZipCPUNo, that was the one01:06
ZipCPUHey!  15 steps of formal for the CPU pass in less than 11 minutes!  Yay!01:06
*** cemerick has quit IRC01:07
promach2you mean for your zipcpu coding ?01:07
ZipCPUI'm trying to formally prove the entire CPU.01:07
ZipCPUI've now proven all the components, it's time to do the CPU.01:07
promach2I hope I could do something like what you have bbeen doing01:08
promach2including the UART ?01:08
ZipCPUNo, just the CPU.01:08
ZipCPUDid you see the picture I tweeted some time back?01:08
ZipCPUI can post it to imgur if you didn't01:08
ZipCPUTry this link:
tpbTitle: Imgur: The magic of the Internet (at
promach2 Apr 901:10
ZipCPUYou found it, huh?01:10
ZipCPUSo the "files" in the image represent separate files composing the ZipCPU.01:11
ZipCPUThose outlined in dashes have been replaced with abstract replacement components01:11
ZipCPUThe red lines represent formal properties, normally found at the bottom of the file01:12
promach2$anyconst results ?01:12
* ZipCPU steps away01:12
* ZipCPU returns01:18
ZipCPUThe red lines on the top represent the formal properties turned upside down, indicating an invariant relationship01:19
promach2invariant ?01:22
ZipCPUIt helps the formal methods to *zoom* forward01:23
promach2what does that mean in the context of formal verification ?01:23
promach2huh ? *zoom* ?01:23
ZipCPUIt means that if once you prove (A) -> B, you don't need to prove it again.01:23
ZipCPU*zoom*: Move faster01:24
ZipCPUA couple days ago, formally verifying 15 steps of the ZipCPU was taking 4 hrs or so.01:24
promach2I see, there are so many interdependent modules01:24
ZipCPUToday, I can do 15 steps in less than 12 minutes.01:24
promach2how do you exactly manage to do this ?01:24
ZipCPUWhat's the golden rule of formal verification?01:25
promach2in less than 12 minutes01:25
ZipCPUAssume inputs, assert local state and outputs01:25
ZipCPUWhat would happen, though, if the inputs to a file weren't the inputs to the design?01:25
ZipCPUYou can't assume them any more.  You'd instead need to assert them.01:25
ZipCPUSee where this is going?01:26
promach2you are restricting the inputs to a file to what you will get from other interdependent modules01:26
ZipCPUNot quite.01:26
ZipCPUI assume the inputs have some properties when I test the file alone.01:26
ZipCPUWhen I test the file as part of a larger system, I then *assert* that the inputs have those properties.01:26
promach2huh ?01:27
promach2I thought that is going to take more steps01:27
ZipCPUOk, 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
ZipCPUYou then prove that the memory module works.01:28
ZipCPUNow, when you place that memory module into the bigger CPU, making assumptions within it will now mask problems.01:28
ZipCPUSo you need to change those assumptions into assertions.01:28
ZipCPUThe opposite applies to the assertions within a module ... ;)01:29
promach2asserions within a module ? what did you with them ?01:30
promach2did you do*01:30
ZipCPUWell, once you've proved that A -> B, you can then assume that A->B.  You don't need to prove it anymore.01:30
promach2but how do you assume A->B ? this does not really make sense01:31
ZipCPUImagine 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
ZipCPUNow 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)->B01:32
promach2that is the flow when you are only verifying a single module on its own01:32
ZipCPUWhen I'm only verifying a single module, I assume (A) and prove that B must then be true.01:33
promach2when you verifying under a big system, you assume(A->B) is true ? but how ?01:33
ZipCPUBy ... assuming(A->B) is true.  I'm not sure I understand your question.01:34
promach2but B is a set of assertions01:34
promach2and A->B is .....01:35
promach2A is a set of assumptions01:35
ZipCPUA is a list of properties, such as assume(i_input), and B is a set of properties such as assert(o_output);01:35
ZipCPUWhen that module becomes a submodule, you want to replace the assumptions with assertions, as in: assert(i_input)01:36
ZipCPUThis works because the module is a submodule and not the parent module where it would be inappropriate.01:36
promach2I see01:37
promach2so, basically changing assume(A) to assert(A)01:37
promach2but why is this taking fewer steps on yosys ?01:38
ZipCPUWell .... 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
ZipCPUOn 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
promach2because o_A is inputs to other modules01:40
ZipCPUIt only works if you've already proved the assertions  hold within the submodule.01:40
ZipCPUMaking sense?01:41
promach2you are reducing the number of possible combinations of data/control signals01:43
ZipCPUThere 'ya go!01:43
promach2that is why you need fewer steps on yosys01:43
ZipCPUNo ... I still need the same number of steps01:44
ZipCPUI just need less time than before01:44
promach2huh ?01:44
promach2i do not get this01:44
promach2same number of steps, but less time ? this does not make sense01:46
ZipCPUWhy not?  What do you think determines the amount of time per step?01:46
promach2I am not sure01:49
*** sklv has quit IRC01:50
ZipCPUI imagine that it's the number of possibilities the formal engine needs to check.01:50
ZipCPUThe number of checks is likely to be a part of this as well ....01:50
ZipCPUIf you can reduce the number of possibilities, then things should go faster, right?01:50
*** sklv has joined #yosys01:50
promach2yeah, ok01:51
promach2What about $anyconst results ?01:56
ZipCPUYou haven't been reading my blog, now, have you?01:57
ZipCPU$anyconst is a random number, chosen once at the beginning of time01:57
ZipCPU$anyseq (which probably makes more sense in that conext) is a random number allowed to change from step to step01:58
ZipCPUAnd 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
promach2hmm... let me read first01:59
tpbTitle: Pipelining a Prefetch (at
*** sifpwj has joined #yosys02:05
ZipCPUI 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
ZipCPUThat will allow me to test all instructions at once.02:06
*** sifpwj has quit IRC02:08
*** pie__ has quit IRC02:11
*** sklv has quit IRC02:14
*** sklv has joined #yosys02:21
promach2ZipCPU: why do you need $anyconst and $anyseq when you will need to do induction check ?02:33
*** emeb_mac has joined #yosys02:36
ZipCPUNot sure I understand.  What does induction have to do with $anyconst or $anyseq?02:37
ZipCPUThey are two separate concepts, orthogonal to each other02:37
promach2hmm.. I am confused between the two concepts then02:54
promach2ZipCPU: let me read more02:55
ZipCPUInduction runs the proof while starting all your variables at "random" initial values02: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
ZipCPUAn $anyseq variable is equivalent to an input parameter to your design02:56
ZipCPUBy 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 had02:57
promach2what input parameter ?02:58
ZipCPUAn $anyseq variable is equivalent to an input parameter to your design03:00
ZipCPUSorry, input port03:00
ZipCPUnot parameter03:00
ZipCPUAnd not one in particular--any one03:00
promach2I am not really sure why would $anyseq be equivalent to an input port ?03:12
ZipCPUFrom a formal method standpoint, what is known of any input port?03:13
ZipCPUOnly its width.03:13
ZipCPUThe value at the port can change from one clock to the next.03:13
ZipCPUYou can make assumptions about the input, but otherwise the input can be anything.03:14
promach2equivalent 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
ZipCPUThe same is true of an $anyseq variable: wire [3:0] example; assign example = $anyseq;03:14
ZipCPUAn $anyconst variable is the same, but with the assumption that it will never change throughout the design.03:15
promach2but why do you need $anyseq when BMC machine could try out all possibilities ?03:15
promach2is there any particular advantage if using $anyseq compared to creating another explicit input port ?03:16
*** AlexDaniel has quit IRC03:20
ZipCPUYes.  The advantage is that your design doesn't then need another explicit input port.03:23
*** digshadow has quit IRC03:23
promach2I will have to read more on $anyconst to understand its purpose03:26
ZipCPUYou might struggle to find material03:26
ZipCPU$anyconst is not standard Verilog, but rather a "feature" of yosys03:26
promach2ok, With a just one simple assumption, $anyseq can be turned into an $anyconst03:27
promach2ZipCPU: 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
ZipCPUwire example = $anyseq;  always @(posedge i_clk) if (f_past_valid) assume($stable(example));03:28
ZipCPUGo ahead and read03:28
ZipCPUI'm finding one bug at a time in the ZipCPU and its formal properties every 40 minutes or so.03:29
ZipCPUI'll probably find another bug therefore in about 35 minutes .... assuming I'm still awake.03:30
promach2sigh, bug-hunting never stop03:30
ZipCPUYeah ... it's just annoying how slow this particular approach to bug-hunting is.03:30
ZipCPUThe 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 it03:31
promach2that is why I like induction so much03:32
promach2induction helps us to create enough assert() for MC03:33
promach2and cover() helps to check if the assert() is valid or not03:33
*** digshadow has joined #yosys03:42
*** kmehall has joined #yosys03:52
tpbTitle: The Designer's Guide Community Forum - Math functions in Cadence NCVerilog (at
*** xrexeon has joined #yosys04:49
*** xrexeon has quit IRC05:08
*** xrexeon has joined #yosys05:09
*** xrexeon has joined #yosys05:48
*** indy has quit IRC06:22
*** indy has joined #yosys06:23
*** dys has joined #yosys06:31
*** GuzTech has joined #yosys06:48
*** emeb_mac has quit IRC07:07
*** emeb has quit IRC07:08
*** xerpi has joined #yosys07:14
*** proteusguy has quit IRC07:18
*** proteusguy has joined #yosys07:18
*** proteusguy has quit IRC07:19
*** proteusguy has joined #yosys07:20
*** proteusguy has quit IRC07:22
*** proteusguy has joined #yosys07:39
*** xrexeon has quit IRC07:40
*** dmin7 has joined #yosys08:40
*** promach2 has quit IRC08:47
*** promach2 has joined #yosys08:47
*** kraiskil has joined #yosys08:49
*** AlexDaniel has joined #yosys08:56
*** cemerick has joined #yosys09:50
*** xrexeon has joined #yosys11:02
*** X-Scale has quit IRC11:04
*** xrexeon has quit IRC11:20
*** proteusguy has quit IRC11:38
*** ralu_ is now known as ralu12:48
*** dys has quit IRC12:58
*** quigonjinn has quit IRC13:05
*** pie__ has joined #yosys13:08
*** cemerick has quit IRC13:40
*** leviathan has joined #yosys13:49
*** X-Scale has joined #yosys14:01
*** leviathan has quit IRC14:05
*** leviathan has joined #yosys14:05
*** eduardo has joined #yosys14:12
*** proteusguy has joined #yosys14:25
*** leviathan has quit IRC14:36
*** GuzTech has quit IRC14:55
*** dys has joined #yosys14:56
*** xrexeon has joined #yosys15:04
*** xerpi has quit IRC15:29
*** ZipCPU has quit IRC15:48
*** ZipCPU has joined #yosys15:51
*** leviathan has joined #yosys15:57
*** promach2 has quit IRC16:42
*** cemerick has joined #yosys17:45
*** goosenphil has joined #yosys19:11
*** proteusguy has quit IRC19:13
*** goosenphil has quit IRC19:15
*** goosenphil has joined #yosys19:17
*** cemerick has quit IRC19:20
*** proteusguy has joined #yosys19:24
*** proteusguy has quit IRC19:30
*** proteusguy has joined #yosys19:41
*** janrinze has joined #yosys19:42
*** goosenphil has quit IRC19:56
*** proteusguy has quit IRC20:13
*** proteusguy has joined #yosys20:14
*** proteusguy has quit IRC20:36
*** leviathan has quit IRC20:39
*** sandeepkr has quit IRC20:56
*** sandeepkr has joined #yosys20:56
*** dmin7 has quit IRC21:05
*** cemerick has joined #yosys21:29
*** cemerick has quit IRC21:38
*** cemerick has joined #yosys22:11
*** cemerick has quit IRC22:57
*** emeb_mac has joined #yosys23:17
*** emeb_mac has quit IRC23:20
*** pie__ has quit IRC23:51
*** pie_ has joined #yosys23:51

Generated by 2.13.1 by Marius Gedminas - find it at!