<ZipCPU>
So the "files" in the image represent separate files composing the ZipCPU.
<ZipCPU>
Those outlined in dashes have been replaced with abstract replacement components
<ZipCPU>
The red lines represent formal properties, normally found at the bottom of the file
<promach2>
$anyconst results ?
<ZipCPU>
Yes
* ZipCPU
steps away
* ZipCPU
returns
<ZipCPU>
The red lines on the top represent the formal properties turned upside down, indicating an invariant relationship
<promach2>
invariant ?
<ZipCPU>
Yes.
<ZipCPU>
It helps the formal methods to *zoom* forward
<promach2>
what does that mean in the context of formal verification ?
<promach2>
huh ? *zoom* ?
<ZipCPU>
It means that if once you prove (A) -> B, you don't need to prove it again.
<ZipCPU>
*zoom*: Move faster
<ZipCPU>
A couple days ago, formally verifying 15 steps of the ZipCPU was taking 4 hrs or so.
<promach2>
I see, there are so many interdependent modules
<ZipCPU>
Yes.
<ZipCPU>
Today, I can do 15 steps in less than 12 minutes.
<promach2>
how do you exactly manage to do this ?
<ZipCPU>
What's the golden rule of formal verification?
<promach2>
in less than 12 minutes
<ZipCPU>
Assume inputs, assert local state and outputs
<ZipCPU>
What would happen, though, if the inputs to a file weren't the inputs to the design?
<ZipCPU>
You can't assume them any more. You'd instead need to assert them.
<ZipCPU>
See where this is going?
<promach2>
you are restricting the inputs to a file to what you will get from other interdependent modules
<ZipCPU>
Not quite.
<ZipCPU>
I assume the inputs have some properties when I test the file alone.
<ZipCPU>
When I test the file as part of a larger system, I then *assert* that the inputs have those properties.
<promach2>
huh ?
<promach2>
I thought that is going to take more steps
<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.
<ZipCPU>
You then prove that the memory module works.
<ZipCPU>
Now, when you place that memory module into the bigger CPU, making assumptions within it will now mask problems.
<ZipCPU>
So you need to change those assumptions into assertions.
<ZipCPU>
The opposite applies to the assertions within a module ... ;)
<promach2>
asserions within a module ? what did you with them ?
<promach2>
did you do*
<ZipCPU>
Well, once you've proved that A -> B, you can then assume that A->B. You don't need to prove it anymore.
<promach2>
wait
<promach2>
but how do you assume A->B ? this does not really make sense
<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.
<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
<promach2>
that is the flow when you are only verifying a single module on its own
<ZipCPU>
When I'm only verifying a single module, I assume (A) and prove that B must then be true.
<promach2>
when you verifying under a big system, you assume(A->B) is true ? but how ?
<ZipCPU>
By ... assuming(A->B) is true. I'm not sure I understand your question.
<promach2>
but B is a set of assertions
<ZipCPU>
Yes.
<promach2>
and A->B is .....
<promach2>
A is a set of assumptions
<ZipCPU>
A is a list of properties, such as assume(i_input), and B is a set of properties such as assert(o_output);
<ZipCPU>
When that module becomes a submodule, you want to replace the assumptions with assertions, as in: assert(i_input)
<ZipCPU>
This works because the module is a submodule and not the parent module where it would be inappropriate.
<promach2>
I see
<promach2>
so, basically changing assume(A) to assert(A)
<ZipCPU>
Yes.
<promach2>
but why is this taking fewer steps on yosys ?
<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.
<promach2>
yeah
<ZipCPU>
On the outputs, you do the opposite, changing assert(o_A) to assume(o_A) ... that's where the dynamite is located.
<promach2>
" changing assert(o_A) to assume(o_A) " <- what ?!
<ZipCPU>
:D
<promach2>
because o_A is inputs to other modules
<ZipCPU>
It only works if you've already proved the assertions hold within the submodule.
<ZipCPU>
Making sense?
<promach2>
yes
<promach2>
you are reducing the number of possible combinations of data/control signals
<ZipCPU>
There 'ya go!
<promach2>
that is why you need fewer steps on yosys
<ZipCPU>
No ... I still need the same number of steps
<ZipCPU>
I just need less time than before
<promach2>
huh ?
<promach2>
i do not get this
<ZipCPU>
Yeah.
<promach2>
same number of steps, but less time ? this does not make sense
<ZipCPU>
Why not? What do you think determines the amount of time per step?
<promach2>
I am not sure
sklv has quit [Remote host closed the connection]
<ZipCPU>
I imagine that it's the number of possibilities the formal engine needs to check.
<ZipCPU>
The number of checks is likely to be a part of this as well ....
<ZipCPU>
If you can reduce the number of possibilities, then things should go faster, right?
sklv has joined #yosys
<promach2>
yeah, ok
<promach2>
What about $anyconst results ?
<ZipCPU>
You haven't been reading my blog, now, have you?
<ZipCPU>
:D
<ZipCPU>
$anyconst is a random number, chosen once at the beginning of time
<ZipCPU>
$anyseq (which probably makes more sense in that conext) is a random number allowed to change from step to step
<ZipCPU>
*context
<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.
<tpb>
Title: Pipelining a Prefetch (at zipcpu.com)
sifpwj has joined #yosys
<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.
<ZipCPU>
That will allow me to test all instructions at once.
sifpwj has quit [K-Lined]
pie__ has quit [Ping timeout: 264 seconds]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<promach2>
ZipCPU: why do you need $anyconst and $anyseq when you will need to do induction check ?
emeb_mac has joined #yosys
<ZipCPU>
Not sure I understand. What does induction have to do with $anyconst or $anyseq?
<ZipCPU>
They are two separate concepts, orthogonal to each other
<promach2>
hmm.. I am confused between the two concepts then
<promach2>
ZipCPU: let me read more
<ZipCPU>
Induction runs the proof while starting all your variables at "random" initial values
<ZipCPU>
$anyconst selects an arbitrary random initial value at the beginning of time.
<ZipCPU>
$anyseq creates an arbitrary random value at every formal step through your logic.
<ZipCPU>
An $anyseq variable is equivalent to an input parameter to your design
<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
<promach2>
what input parameter ?
<ZipCPU>
An $anyseq variable is equivalent to an input parameter to your design
<ZipCPU>
Sorry, input port
<ZipCPU>
not parameter
<ZipCPU>
And not one in particular--any one
<promach2>
I am not really sure why would $anyseq be equivalent to an input port ?
<ZipCPU>
From a formal method standpoint, what is known of any input port?
<ZipCPU>
Only its width.
<ZipCPU>
The value at the port can change from one clock to the next.
<ZipCPU>
You can make assumptions about the input, but otherwise the input can be anything.
<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.
<ZipCPU>
The same is true of an $anyseq variable: wire [3:0] example; assign example = $anyseq;
<ZipCPU>
Yes.
<ZipCPU>
An $anyconst variable is the same, but with the assumption that it will never change throughout the design.
<promach2>
wait
<promach2>
but why do you need $anyseq when BMC machine could try out all possibilities ?
<promach2>
is there any particular advantage if using $anyseq compared to creating another explicit input port ?
AlexDaniel has quit [Ping timeout: 240 seconds]
<ZipCPU>
Yes. The advantage is that your design doesn't then need another explicit input port.
digshadow has quit [Ping timeout: 268 seconds]
<promach2>
ok
<promach2>
I will have to read more on $anyconst to understand its purpose
<ZipCPU>
You might struggle to find material
<ZipCPU>
$anyconst is not standard Verilog, but rather a "feature" of yosys
<promach2>
ok, With a just one simple assumption, $anyseq can be turned into an $anyconst
<ZipCPU>
Sure.
<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 ?
<ZipCPU>
wire example = $anyseq; always @(posedge i_clk) if (f_past_valid) assume($stable(example));
<ZipCPU>
Go ahead and read
<ZipCPU>
I'm finding one bug at a time in the ZipCPU and its formal properties every 40 minutes or so.
<ZipCPU>
I'll probably find another bug therefore in about 35 minutes .... assuming I'm still awake.
<promach2>
sigh, bug-hunting never stop
<ZipCPU>
Yeah ... it's just annoying how slow this particular approach to bug-hunting is.
<ZipCPU>
The good news is that induction seems to be *much* faster than BMC at finding bugs.
* ZipCPU
is not looking forward to taking this "bug-free" code and trying to meet timing with it
<promach2>
that is why I like induction so much
<promach2>
induction helps us to create enough assert() for MC
<promach2>
BMC*
<promach2>
and cover() helps to check if the assert() is valid or not