Tuesday, 2019-03-26

*** tpb has joined #yosys00:00
*** togo has quit IRC00:19
*** futarisIRCcloud has joined #yosys00:31
*** AlexDaniel has joined #yosys00:46
*** lutsabound has quit IRC01:14
*** AlexDaniel has quit IRC01:31
*** emeb has left #yosys01:55
*** emeb_mac has joined #yosys01:55
*** PyroPeter has quit IRC03:32
*** PyroPeter has joined #yosys03:44
*** rohitksingh_work has joined #yosys04:31
*** gsi__ has joined #yosys04:54
*** gsi_ has quit IRC04:57
*** proteusguy has joined #yosys05:03
*** gsi__ is now known as gsi_05:31
*** leviathanch has joined #yosys06:08
*** bpye has joined #yosys06:35
bpyeHey, could anyone look at this tiny example: https://gist.github.com/benpye/2fc36cf4555d24c47ff7eebecfac5f78 - I'm not sure why the inductive formal proof is failing06:37
tpbTitle: min.v · GitHub (at gist.github.com)06:37
bpyeWait try https://gist.github.com/benpye/008009e97f54d732e689bada85e227fe I've included the sby file06:38
tpbTitle: min.sby · GitHub (at gist.github.com)06:38
bpyeI realise it's a slightly silly assertion in a way, I just can't work out why it's failing06:44
bpyeAh, it's because next_counter is combinatorial?06:54
emeb_macwhy not use $past(next_counter) ?06:56
bpyeHow can I get that to work with the clock enable?06:58
bpyeMaybe I'm missing something :)06:58
emeb_macalso, your assertion is keying of f_past_valid = 0, so it's trying to run on the first clock cycle06:58
emeb_macand f_past_next_counter isn't assigned then06:59
bpyeHuh, shouldn't '~f_past_valid' be NOT f_past_valid, sorry, my verilog is rusty07:00
emeb_macare you making any assumptions about i_clk_en?07:02
emeb_macand have you looked at the .vcd trace to see what's failing?07:03
bpyeNo assumptions about i_clk_en07:04
bpyeMy traces all show f_past_valid starting 1 which is confusing me07:05
emeb_macI don't like the way you're setting counter and f_past_valid in their declarations.07:07
emeb_macI've never seen that syntax before07:07
emeb_macI'd suggest using an initial statement to set those.07:07
bpyesplitting it to an initial block unfortuantely makes no difference07:08
emeb_macalso 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
bpyeBut f_past_valid should equal zero if f_past_next_counter has yet to be set, I believe07:09
emeb_macwhat exactly is your assertion trying to prove?07:10
emeb_macand you're not wrapping the clauses inside the assert with () so are you sure of the order of operations?07:11
bpyeThis is just a minimal example, I hit this in a more complex testbench07:12
bpyeTrying to ensure that the state is moved correctly07:12
emeb_macwell, I'm a newb @ formal so I'm not much help here. Perhaps ping ZipCPU about it when he's around.07:13
emeb_macbut I see a lot of stuff here that I'd do differently based on the class I took.07:13
bpyeYeah, 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 license07:14
bpyeHm, it does seem that i simply need to constrain it further, using abc pdr rather than smtbmc does result in a sucessful proof07:17
*** emeb_mac has quit IRC07:40
*** proteusguy has quit IRC07:57
*** kraiskil has joined #yosys08:08
*** proteusguy has joined #yosys08:09
*** m4ssi has joined #yosys08:11
*** SpaceCoaster has quit IRC08:46
*** kraiskil has quit IRC08:47
*** wifasoi has joined #yosys09:21
*** leviathanch has quit IRC09:35
*** MoeIcenowy has quit IRC10:13
*** MoeIcenowy has joined #yosys10:13
*** SpaceCoaster has joined #yosys10:37
*** mirage335 has quit IRC10:54
*** proteusguy has quit IRC10:59
*** mirage335 has joined #yosys11:01
*** rohitksingh_work has quit IRC11:27
*** rohitksingh_work has joined #yosys11:28
*** develonepi3 has quit IRC11:38
ZipCPUbpye: 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
ZipCPUWithout trying your example myself, my guess would be that this is what's going on: http://zipcpu.com/blog/2018/03/10/induction-exercise.html11:42
tpbTitle: An Exercise in using Formal Induction (at zipcpu.com)11:42
ZipCPUOk, I just tried it ... the result was "UNKNOWN"12:10
ZipCPUThe 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 passes12:11
ZipCPUThe 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 false12:12
*** leviathanch has joined #yosys12:15
ZipCPUTherefore 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
ZipCPUThen, 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
ZipCPUA 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 #yosys12:26
*** lutsabound has joined #yosys12:39
*** futarisIRCcloud has quit IRC13:10
*** rohitksingh_work has quit IRC13:27
*** AlexDaniel has joined #yosys13:53
*** emeb_mac has joined #yosys14:30
*** rohitksingh has joined #yosys15:08
*** maikmerten has joined #yosys15:40
*** emeb_mac has quit IRC15:40
*** rohitksingh has quit IRC15:41
*** lutsabound has quit IRC15:48
*** rohitksingh has joined #yosys15:54
*** rohitksingh has quit IRC16:06
*** rohitksingh has joined #yosys16:21
*** rohitksingh has quit IRC16:33
*** leviathanch has quit IRC16:37
*** MoeIcenowy has quit IRC16:45
*** MoeIcenowy has joined #yosys16:46
*** rohitksingh has joined #yosys16:59
*** rohitksingh has quit IRC17:56
*** m4ssi has quit IRC18:07
*** tlwoerner has quit IRC18:52
*** tlwoerner has joined #yosys18:58
*** leptonix has joined #yosys19:34
*** tmbinc2 has quit IRC19:48
*** leptonix has quit IRC20:36
*** develonepi3 has quit IRC20:38
*** mrsteveman1 has joined #yosys21:00
*** shorne has quit IRC21:07
*** leptonix has joined #yosys21:09
*** leptonix has joined #yosys21:23
*** maikmerten has quit IRC21:38
*** togo has joined #yosys21:48
*** leptonix has quit IRC22:42
*** leptonix has joined #yosys22:43
*** leptonix has quit IRC23:08
*** leptonix has joined #yosys23:09
*** develonepi3 has joined #yosys23:25
*** togo has quit IRC23:44
*** emeb_mac has joined #yosys23:45

Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!