<promach_>
do you think I should go down to multiclock induction of 50 ?
<ZipCPU>
How/why would that make things better?
maartenBE has quit [Ping timeout: 240 seconds]
<ZipCPU>
A lower depth doesn't mean you have a better proof, neither does it necessarily demonstrate any better skill of the engineer. It could just be that the problem needs a longer depth. In that case, why suffer through the problems associated with a shorter depth?
maartenBE has joined #yosys
<promach_>
ok, I will stick with induction depth 200
<ZipCPU>
There's a rule for when to go lower ..../
<ZipCPU>
If your design passes before the induction length gets to zero, then choose a shorter depth
<promach_>
passes before the induction length gets to zero ???
<ZipCPU>
Yes.
<promach_>
I am a bit confused
<ZipCPU>
This afternoon, I was working with HDMI. If you give SymbiYosys a "mode prove" with the default depth of 20, the TMDS encoder would pass with about 12 steps of induction.
<ZipCPU>
You can then reduce the depth.
<ZipCPU>
Until it passes, though .... you sort of have to work with your problem to know what the right answer is.
<ZipCPU>
Sometimes it makes sense to set the depth to the length of the entire operation. That's certainly the simplest initial depth.
<promach_>
I see
<ZipCPU>
That doesn't always work. Classic example: video. There's no way you'd verify a full frame without induction.
<ZipCPU>
Incidentally, 20 time-steps was plenty for my HDMI transmitter to pass. ;)
<ZipCPU>
20 was not sufficient for my UART.
<ZipCPU>
In many ways, it's just the nature of the problem.
<promach_>
HDMI is also multiclock, right ?
<ZipCPU>
No.
<ZipCPU>
The components I'm doing are all synchronous with the pixel clock.
<ZipCPU>
The memory fetch uses a separate clock, but I'm moving through my design one piece at a time.
<ZipCPU>
Right now, my next step is to get the HDMI simulation running
<promach_>
:)
<ZipCPU>
Have you seen my FFT-Demo? That's the project I'm working on. I need to switch from VGA to HDMI, and from (simulated) block RAM to DDR3 SDRAM.
<promach_>
DDR3 ? that is so...
<ZipCPU>
Necessary?
<promach_>
I have not tried the FFT-Demo
<ZipCPU>
There's a lot to be learned from it from the stand point of process.
<promach_>
I have SBY 20:54:40 [UART] engine_0: ## 0:00:04 Unreached cover statement at test_UART.v:114.
<ZipCPU>
It simply means that yosys is unable to find any path that would make your cover statement true, after exhausting all paths through your logic for the first 20 formal verification cycles..
<ZipCPU>
Debugging a failed cover statement is ... different from debugging a failed assertion.
<ZipCPU>
In the case of a failed assertion, you have a trace showing you what went wrong.
<ZipCPU>
In the case of the failed cover, you won't get any traces.
<promach_>
TRUE
<ZipCPU>
If I need to debug a cover statement, I'll typically walk backwards. If there's a chain of events, A->B->C->D, and cover(D) fails, I'll cover (C). If that fails I'll cover (B), etc.
<promach_>
ok
<ZipCPU>
Perhaps a better strategy would be to bisect A->B->C->D and cover(B) before (C) or (A).
<promach_>
YES
<promach_>
strange, I incremented TX_CLK_THRESHOLD to 4 but cover(!tx_clk) still fail
<promach_>
does "mode cover" actually take into account "assume()" ?
<ZipCPU>
Yes. assert() too,
maikmerten has quit [Remote host closed the connection]
<promach_>
strange, both cover(tx_clk) and cover(!tx_clk) failed
<promach_>
this is not making sense
<ZipCPU>
Could be that your assumptions are prohibiting any solution.
<promach_>
what ? tx_clk is only a one-bit register
<promach_>
reg tx_clk
<ZipCPU>
I'm just saying that's a plausable reason why both cover(tx_clk) and cover(!tx_clk) would fail.
<ZipCPU>
If somewhere within your design you were to assume(0), then cover would fail immediately before it even gets to tx_clk
<promach_>
assume(0); ? I do not have this in the code
<ZipCPU>
Can you share a screen capture of the output of SymbiYosys?