06:30 <bpye> Hey, could anyone look at this tiny example: https://gist.github.com/benpye/2fc36cf4555d24c47ff7eebecfac5f78 - I'm not sure why the inductive formal proof is failing

06:30 <tpb> Title: min.v · GitHub (at gist.github.com)

06:30 <bpye> Wait try https://gist.github.com/benpye/008009e97f54d732e689bada85e227fe I've included the sby file

06:30 <tpb> Title: min.sby · GitHub (at gist.github.com)

06:37 <bpye> I realise it's a slightly silly assertion in a way, I just can't work out why it's failing

06:47 <bpye> Ah, it's because next_counter is combinatorial?

06:49 <emeb_mac> why not use $past(next_counter) ?

06:50 <bpye> How can I get that to work with the clock enable?

06:51 <bpye> Maybe I'm missing something :)

06:51 <emeb_mac> also, your assertion is keying of f_past_valid = 0, so it's trying to run on the first clock cycle

06:51 <emeb_mac> and f_past_next_counter isn't assigned then

06:52 <bpye> Huh, shouldn't '~f_past_valid' be NOT f_past_valid, sorry, my verilog is rusty

06:54 <emeb_mac> are you making any assumptions about i_clk_en?

06:55 <emeb_mac> and have you looked at the .vcd trace to see what's failing?

06:56 <bpye> No assumptions about i_clk_en

06:57 <bpye> My traces all show f_past_valid starting 1 which is confusing me

06:59 <emeb_mac> yeah

06:59 <emeb_mac> I don't like the way you're setting counter and f_past_valid in their declarations.

06:59 <emeb_mac> I've never seen that syntax before

07:00 <emeb_mac> I'd suggest using an initial statement to set those.

07:00 <bpye> splitting it to an initial block unfortuantely makes no difference

07:01 <emeb_mac> also you're not setting an initial value for f_past_next_counter so it could be anything and definitely not equal to counter when the assert runs.

07:01 <bpye> But f_past_valid should equal zero if f_past_next_counter has yet to be set, I believe

07:02 <emeb_mac> what exactly is your assertion trying to prove?

07:03 <emeb_mac> and you're not wrapping the clauses inside the assert with () so are you sure of the order of operations?

07:04 <bpye> This is just a minimal example, I hit this in a more complex testbench

07:04 <bpye> Trying to ensure that the state is moved correctly

07:05 <emeb_mac> well, I'm a newb @ formal so I'm not much help here. Perhaps ping ZipCPU about it when he's around.

07:06 <emeb_mac> but I see a lot of stuff here that I'd do differently based on the class I took.

07:06 <bpye> Yeah, I did take a class on formal verification as an undergrad but we covered SVA so I would have never written code like this anyway, sadly I don't have a Verific license

07:09 <bpye> Hm, it does seem that i simply need to constrain it further, using abc pdr rather than smtbmc does result in a sucessful proof

11:31 <ZipCPU> bpye: Were you having problems with BMC (i.e. was FAIL the result) or with the induction step (i.e. was UNKNOWN the result)?

11:34 <ZipCPU> Without trying your example myself, my guess would be that this is what's going on: http://zipcpu.com/blog/2018/03/10/induction-exercise.html

11:34 <tpb> Title: An Exercise in using Formal Induction (at zipcpu.com)

12:03 <ZipCPU> Ok, I just tried it ... the result was "UNKNOWN"

12:03 <ZipCPU> The problem is the assertion regarding (~f_past_valid || counter == f_past_next_counter); If you move this assertion outside of the i_clk_en if block, then the design passes

12:04 <ZipCPU> The problem is specifically that clk_en, and the fact that you are not saying anything about what counter and f_past_next_counter must be when clk_en is false

12:09 <ZipCPU> Therefore the solver is setting this value false for all but the third to the last cycle. During the first several cycles, f_past_next_counter doesn't match counter--because this is induction and assertions are required to get you into a valid state.

12:11 <ZipCPU> Then, on the third to the last cycle, the solver raises i_clk_en. To make this design fail, this must be the case. On the second to the last cycle the assertion is now checked. It fails, because the design was allowed to get into an illegal state, not because the design would've failed.

12:12 <ZipCPU> A better assertion, such as moving the counter == f_past_next_counter outside the if (i_clk_en) would fix this problem, since it would keep the solver from starting with an illegal state.