| *** tpb has joined #yosys | 00:00 | |
| *** togo has quit IRC | 00:19 | |
| *** futarisIRCcloud has joined #yosys | 00:31 | |
| *** AlexDaniel has joined #yosys | 00:46 | |
| *** lutsabound has quit IRC | 01:14 | |
| *** AlexDaniel has quit IRC | 01:31 | |
| *** emeb has left #yosys | 01:55 | |
| *** emeb_mac has joined #yosys | 01:55 | |
| *** PyroPeter has quit IRC | 03:32 | |
| *** PyroPeter has joined #yosys | 03:44 | |
| *** rohitksingh_work has joined #yosys | 04:31 | |
| *** gsi__ has joined #yosys | 04:54 | |
| *** gsi_ has quit IRC | 04:57 | |
| *** proteusguy has joined #yosys | 05:03 | |
| *** gsi__ is now known as gsi_ | 05:31 | |
| *** leviathanch has joined #yosys | 06:08 | |
| *** bpye has joined #yosys | 06:35 | |
| 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:37 |
|---|---|---|
| tpb | Title: min.v · GitHub (at gist.github.com) | 06:37 |
| bpye | Wait try https://gist.github.com/benpye/008009e97f54d732e689bada85e227fe I've included the sby file | 06:38 |
| tpb | Title: min.sby · GitHub (at gist.github.com) | 06:38 |
| bpye | I realise it's a slightly silly assertion in a way, I just can't work out why it's failing | 06:44 |
| bpye | Ah, it's because next_counter is combinatorial? | 06:54 |
| emeb_mac | why not use $past(next_counter) ? | 06:56 |
| bpye | How can I get that to work with the clock enable? | 06:58 |
| bpye | Maybe I'm missing something :) | 06:58 |
| emeb_mac | also, your assertion is keying of f_past_valid = 0, so it's trying to run on the first clock cycle | 06:58 |
| emeb_mac | and f_past_next_counter isn't assigned then | 06:59 |
| bpye | Huh, shouldn't '~f_past_valid' be NOT f_past_valid, sorry, my verilog is rusty | 07:00 |
| emeb_mac | are you making any assumptions about i_clk_en? | 07:02 |
| emeb_mac | and have you looked at the .vcd trace to see what's failing? | 07:03 |
| bpye | No assumptions about i_clk_en | 07:04 |
| bpye | My traces all show f_past_valid starting 1 which is confusing me | 07:05 |
| emeb_mac | yeah | 07:07 |
| emeb_mac | I don't like the way you're setting counter and f_past_valid in their declarations. | 07:07 |
| emeb_mac | I've never seen that syntax before | 07:07 |
| emeb_mac | I'd suggest using an initial statement to set those. | 07:07 |
| bpye | splitting it to an initial block unfortuantely makes no difference | 07:08 |
| 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:09 |
| bpye | But f_past_valid should equal zero if f_past_next_counter has yet to be set, I believe | 07:09 |
| emeb_mac | what exactly is your assertion trying to prove? | 07:10 |
| emeb_mac | and you're not wrapping the clauses inside the assert with () so are you sure of the order of operations? | 07:11 |
| bpye | This is just a minimal example, I hit this in a more complex testbench | 07:12 |
| bpye | Trying to ensure that the state is moved correctly | 07:12 |
| 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:13 |
| emeb_mac | but I see a lot of stuff here that I'd do differently based on the class I took. | 07:13 |
| 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:14 |
| 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 | 07:17 |
| *** emeb_mac has quit IRC | 07:40 | |
| *** proteusguy has quit IRC | 07:57 | |
| *** kraiskil has joined #yosys | 08:08 | |
| *** proteusguy has joined #yosys | 08:09 | |
| *** m4ssi has joined #yosys | 08:11 | |
| *** SpaceCoaster has quit IRC | 08:46 | |
| *** kraiskil has quit IRC | 08:47 | |
| *** wifasoi has joined #yosys | 09:21 | |
| *** leviathanch has quit IRC | 09:35 | |
| *** MoeIcenowy has quit IRC | 10:13 | |
| *** MoeIcenowy has joined #yosys | 10:13 | |
| *** SpaceCoaster has joined #yosys | 10:37 | |
| *** mirage335 has quit IRC | 10:54 | |
| *** proteusguy has quit IRC | 10:59 | |
| *** mirage335 has joined #yosys | 11:01 | |
| *** rohitksingh_work has quit IRC | 11:27 | |
| *** rohitksingh_work has joined #yosys | 11:28 | |
| *** develonepi3 has quit IRC | 11:38 | |
| 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:38 |
| 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:42 |
| tpb | Title: An Exercise in using Formal Induction (at zipcpu.com) | 11:42 |
| ZipCPU | Ok, I just tried it ... the result was "UNKNOWN" | 12:10 |
| 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:11 |
| 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:12 |
| *** leviathanch has joined #yosys | 12:15 | |
| 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:17 |
| 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:18 |
| 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. | 12:19 |
| *** develonepi3 has joined #yosys | 12:26 | |
| *** lutsabound has joined #yosys | 12:39 | |
| *** futarisIRCcloud has quit IRC | 13:10 | |
| *** rohitksingh_work has quit IRC | 13:27 | |
| *** AlexDaniel has joined #yosys | 13:53 | |
| *** emeb_mac has joined #yosys | 14:30 | |
| *** rohitksingh has joined #yosys | 15:08 | |
| *** maikmerten has joined #yosys | 15:40 | |
| *** emeb_mac has quit IRC | 15:40 | |
| *** rohitksingh has quit IRC | 15:41 | |
| *** lutsabound has quit IRC | 15:48 | |
| *** rohitksingh has joined #yosys | 15:54 | |
| *** rohitksingh has quit IRC | 16:06 | |
| *** rohitksingh has joined #yosys | 16:21 | |
| *** rohitksingh has quit IRC | 16:33 | |
| *** leviathanch has quit IRC | 16:37 | |
| *** MoeIcenowy has quit IRC | 16:45 | |
| *** MoeIcenowy has joined #yosys | 16:46 | |
| *** rohitksingh has joined #yosys | 16:59 | |
| *** rohitksingh has quit IRC | 17:56 | |
| *** m4ssi has quit IRC | 18:07 | |
| *** tlwoerner has quit IRC | 18:52 | |
| *** tlwoerner has joined #yosys | 18:58 | |
| *** leptonix has joined #yosys | 19:34 | |
| *** tmbinc2 has quit IRC | 19:48 | |
| *** leptonix has quit IRC | 20:36 | |
| *** develonepi3 has quit IRC | 20:38 | |
| *** mrsteveman1 has joined #yosys | 21:00 | |
| *** shorne has quit IRC | 21:07 | |
| *** leptonix has joined #yosys | 21:09 | |
| *** leptonix has joined #yosys | 21:23 | |
| *** maikmerten has quit IRC | 21:38 | |
| *** togo has joined #yosys | 21:48 | |
| *** leptonix has quit IRC | 22:42 | |
| *** leptonix has joined #yosys | 22:43 | |
| *** leptonix has quit IRC | 23:08 | |
| *** leptonix has joined #yosys | 23:09 | |
| *** develonepi3 has joined #yosys | 23:25 | |
| *** togo has quit IRC | 23:44 | |
| *** emeb_mac has joined #yosys | 23:45 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!