<ZipCPU>
promach: Because processing is expensive. If you can clean up your design by adding more asserts, it might manage to prove faster.
<ZipCPU>
Further, reducing the induction length might tell you more about how you have (or have not) restricted the design.
digshadow has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
digshadow has quit [Read error: Connection reset by peer]
digshadow has joined #yosys
digshadow has quit [Ping timeout: 264 seconds]
digshadow has joined #yosys
TFKyle has joined #yosys
kuldeep has quit [Ping timeout: 264 seconds]
kuldeep has joined #yosys
pie_ has joined #yosys
m_t has joined #yosys
leviathanch has joined #yosys
eduardo__ has joined #yosys
leviathanch has quit [Read error: Connection reset by peer]
leviathanch has joined #yosys
eduardo_ has quit [Ping timeout: 240 seconds]
quigonjinn has quit [Ping timeout: 252 seconds]
quigonjinn has joined #yosys
dys has quit [Ping timeout: 252 seconds]
<promach>
For line 32 of https://paste.ubuntu.com/26237838/ , I am having ERROR: Parser error in line ../rtl/test_UART.v:32: syntax error, unexpected TOK_IF
<promach>
I am trying to emulate cover property ( @(posedge clk) enable |-> data_is_valid );
leviathanch has quit [Remote host closed the connection]
aw- has joined #yosys
<ZipCPU>
promach: If you want a cover property that uses $past, it'll need to be within a clocked always block.
<ZipCPU>
Perhaps what you want is something closer to always @(posedge clk) if ((f_past_valid)&&($past(enable))) cover(data_is_valid);
<ZipCPU>
I'm not sure why you had the $past(enable,10) in there at all, though, so I took it out.
<ZipCPU>
Referencing items prior to the "start of time" can always be tricky, and is generally to be avoided. Hence ... the f_past_valid.
<ZipCPU>
Hmm ... that didn't come out right ... I've done $past(*,2) before, but always with an (f_past_valid)&&($past(f_past_valid))
<ZipCPU>
You can see from my intro to formal methods post what the f_past_valid register is.
leviathanch has joined #yosys
<promach>
reg has_been_enabled;
<promach>
always @(posedge clk)
<promach>
begin
<promach>
if(enable)
<promach>
has_been_enabled <= 1;
<promach>
if(has_been_enabled)
<promach>
cover(data_is_valid);
<promach>
end
<promach>
ZipCPU: the above does not work for me :|
<ZipCPU>
Why not?
leviathanch has quit [Remote host closed the connection]
<ZipCPU>
What value should one expect from has_been_enabled?
<ZipCPU>
'Cause ... that's your first bug.
<promach>
ZipCPU: you mean I should assume(has_been_enabled == 0); initially ?
<ZipCPU>
NO! Assume inputs, assert outputs (and internals). has_been_enabled is an internal variable. It's value should therefore never be assumed, only asserted.
<ZipCPU>
promach: Sorry if that came across as me jumping on you. But ... you do need to understand the fundamental principle of formal verification: assume inputs, assert everything else.
<ZipCPU>
Hence, you might wish to do: initial assert(has_been_enabled == 0);
<promach>
ok
<ZipCPU>
Be *very* careful about what you assume(). Any assumptions might render your proof little more than something that makes you feel good about your design, yet tells you nothing about how well it actually works.
m_t has quit [Quit: Leaving]
quigonjinn has quit [Remote host closed the connection]
aw- has quit [Quit: Leaving.]
<promach>
ZipCPU: I guess I should also remove the assume() in the initial block as well. They are useless, I suppose ?
<promach>
'Cause ... that's your first bug. <== could you elaborate, ZipCPU ?
<ZipCPU>
initial assert(has_been_enabled==0); and your design will fail.
AlexDaniel has quit [Remote host closed the connection]
AlexDaniel has joined #yosys
pie__ has joined #yosys
pie_ has quit [Ping timeout: 252 seconds]
azonenberg_work has joined #yosys
azonenberg_work has left #yosys [#yosys]
m_t has joined #yosys
Kooda has joined #yosys
quigonjinn has joined #yosys
quigonjinn has quit [Ping timeout: 248 seconds]
pie__ has quit [Ping timeout: 240 seconds]
_whitelogger has joined #yosys
quigonjinn has joined #yosys
quigonjinn has quit [Ping timeout: 252 seconds]
gnufan has quit [Quit: Leaving.]
<ZipCPU>
Let me check what I have then ...
<ZipCPU>
Ooops ... sorry, wrong channel. ;)
quigonjinn has joined #yosys
quigonjinn has quit [Ping timeout: 240 seconds]
m_t has quit [Quit: Leaving]
<promach>
ZipCPU: there is almost no way to around the failure due to initial assert(has_been_enabled==0);
<promach>
to go around*
<ZipCPU>
Why not just declare: initial has_been_enabled = 0; ?
<promach>
initial assume(has_been_enabled == 0); is similar ?
<ZipCPU>
No.
<ZipCPU>
initial assume is very different.
<ZipCPU>
initial assume(has_been_enabled==0); will get you to pass formal verification, even if your code is buggy (has_been_enabled may start at 1 in your code).
<ZipCPU>
Most synthesizer will ignore any assume statements in your code.
<ZipCPU>
Your formal proof must test the parts and pieces the synthesizer will use.
<ZipCPU>
As I said, assume inputs, assert (internal state and) outputs.
<promach>
ok
<ZipCPU>
has_been_enabled is not an input, so ... don't asume it.
<promach>
ok
<promach>
ZipCPU: I guess I need another week time to do a total code revision and check for my UART assert() and assume()
<promach>
as well as cover()
<promach>
the tool still failed my cover(data_is_valid) statement
<promach>
:(
<ZipCPU>
Try building your design without the cover statement ... to see why the cover is failing.
<ZipCPU>
Add as many asserts as you can within your code that will describe how your code works.
<ZipCPU>
The more asserts, the faster the proof will go.
<promach>
ok, sure
<ZipCPU>
The other neat thing about asserts is ... if an assert fails, at least you get a trace showing you what went wrong within your code.
<ZipCPU>
If a cover statement fails ... you don't know what went wrong, other than that it could never be met.