<promach>
sensille: are you sure that this is not due to my own bug within my own code ?
<sensille>
even if it is, "segmentation fault" is not a nice way to point out an error in your source code
emeb_mac has quit [Quit: Leaving.]
<promach>
ok, let me have a further look at few more hours on my own before I open a ticket on github
<promach>
ok, let me have a further look at my own code for few more hours before I open a ticket on github
<promach>
sensille: thanks
AlexDaniel has quit [Ping timeout: 260 seconds]
rohitksingh_work has quit [Ping timeout: 246 seconds]
kraiskil has joined #yosys
AlexDaniel has joined #yosys
AlexDaniel has quit [Ping timeout: 252 seconds]
nonlinear has quit [Remote host closed the connection]
nonlinear has joined #yosys
promach has quit [Ping timeout: 252 seconds]
AlexDaniel has joined #yosys
eightdot has joined #yosys
promach has joined #yosys
dxld has quit [Quit: Bye]
AlexDaniel has quit [Ping timeout: 260 seconds]
dxld has joined #yosys
eightdot has quit [Quit: Changing server]
eightdot has joined #yosys
eightdot has quit [Client Quit]
dxld has quit [Quit: Bye]
eightdot has joined #yosys
dxld has joined #yosys
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
develonepi3 has joined #yosys
<mattvenn_>
couldn't see your formal test setup - not in the repo? But do you have the formal solvers installed?
<ZipCPU>
mattvenn_: promach's been using the formal stuff for a while
<ZipCPU>
The problem is that his code is so complex, it's not likely the team will be able to stare at it and instantly discover the problem.
<ZipCPU>
Clifford's got a rule that any bug submitted should be an MCVE: Minimal, Complete, Verifiable, Example
<ZipCPU>
Minimal usually means less than 20 lines of code, and this isn't that.
<ZipCPU>
Complete means that all of the code necessary to reconstruct the problem is represented. promach says this is true, so that would include the test setup you were asking for. (Check the bench directory)
<ZipCPU>
Verifiable means that, given his code and setup, you can create the seg fault. I'm going to guess promach has provided that.
<ZipCPU>
As I understand the problem, the only difference is past(X,8) and past(X,7) versus past(X,9) and past(X,8).
<ZipCPU>
There might truly be an actual bug here ... I doubt anyone has used past(X,9) before. Indeed, I've never (yet) found a reason for past(X,8). The most I've ever needed is past(X,5).
<ZipCPU>
The other problem promach has is that he hasn't gated these values. This is unrelated to the crash, though. On the first clock, past(X,8) will reference time-step -8 (a non existant timestep)
<ZipCPU>
On the second clock, past(X,8) will reference timestep -7. However, his f_past_valid gate will now be true, so he will be referencing negative time.
<ZipCPU>
Any/all asserts of negative time will automatically fail, so either way, with or without seg fault, his design is going to fail at this line.
<ZipCPU>
Meh, never mind about that ... he's gated the asserts with the receiver state being in (or past) the stop bit, so that should keep him out of negative time.
cemerick has joined #yosys
<cr1901_modern>
I understand by definition that past is invalid on the first timestep, but why is it valid on timestep -7?
<ZipCPU>
Timestep -7 has the same problem as timestep -1
<ZipCPU>
No difference.
<cr1901_modern>
>However, his f_past_valid gate will now be true
<cr1901_modern>
Ahhh, so f_past_valid needs to be 0 until 8 timesteps have passed
<ZipCPU>
Yes!
<ZipCPU>
In this case, though, he's checking his design state.
<ZipCPU>
You can't get a uart receiver into the stop bit state without going through at least 8-states, so .... he should be good there.
<ZipCPU>
Let me go back to "Verifiable": I'm not getting a segfault with his posted code.
<ZipCPU>
Certainly not the one he indicated.
<ZipCPU>
That'll make it hard to find and fix whatever bug he had.
AlexDaniel has joined #yosys
cemerick has quit [Ping timeout: 252 seconds]
<ZipCPU>
promach: Could not duplicate
AlexDaniel has quit [Remote host closed the connection]
<promach>
ZipCPU: I was away just now
<promach>
did you duplicate using the original development branch from github ?
<ZipCPU>
Yes
<promach>
without any code modification from your side ?
<ZipCPU>
Correct
<promach>
so, you just ran git pull origin development ?
<ZipCPU>
I even rebuilt both yosys and SymbiYosys from scratch to make certain I was using the current ones. Results didn't change.
<promach>
and went to the bench directory and ran make
<promach>
it would be hard if this does not give the same output with your computer
<promach>
ZipCPU: line 305 of test_UART.v
<promach>
ZipCPU: even with this modification at line 305, you are still getting no segmentation fault with your computer ?
<ZipCPU>
No. Now I am getting a segfault in read_verilog -formal
<ZipCPU>
The stack trace goes through the simplify() function in frontends/ast/...
<ZipCPU>
The actual segfault is in a call to C++ basic_string
<promach>
I am not familiar with yosys internal source code
<ZipCPU>
So, yosys is sort of like GCC ... it takes your code through a series of transformations.
<ZipCPU>
The first transformation involves reading your code and converting it to an internal yosys format
<ZipCPU>
That involves using an "Abstract Syntax Tree" or AST
<ZipCPU>
You should be able to google that--there's good reading there.
<promach>
ok, which call to C++ basic_string ?
<promach>
ZipCPU: is it really not bug from my own code as far as you can reason now ?
<ZipCPU>
Still working on that. The default yosys build doesn't include symbols, so GDB isn't much help. I'm rebuilding now with the debug enabled to see if that helps.
<ZipCPU>
The basic_string call is being made from the simplify() function in frontends/ast/simplify.cc
<ZipCPU>
There's a nasty long level of recursion taking place to get to it, but I can't tell if that's a problem or not.
<promach>
ok, I got to go now. I will be back in half an hour
rohitksingh has joined #yosys
emeb has joined #yosys
lutsabound has joined #yosys
promach_ has joined #yosys
<promach_>
ZipCPU: how can I help to debug this segfault ? strace does not give much info
<lutsabound>
Check the directory SymbiYosys creates for the actual yosys script. Then ryn yosys with that script.
kraiskil has quit [Ping timeout: 264 seconds]
seldridge has joined #yosys
<ZipCPU>
promach_: If you just run yosys, using the yosys script in the UART_proof subdirectory, you'll find that yosys is segfaulting on the first line: read_verilog -formal test_UART.v
<ZipCPU>
To get more information, I needed to go into the yosys build directory and adjust the Makefile to include debugging symbols and information.
<ZipCPU>
The problem in your code is that the number of steps is both constant and not. Your number of steps is determined by a parameter, not by a constant. It will be constant in the end, but isn't really constant during the evaluation.
<ZipCPU>
Had you used a macro or an integer, the line would've worked.
<jer>
ZipCPU, hey, did you have a small list at some point that listed a number of kinds of projects ranked in an order if you were to teach a class? or am i misremembering
<ZipCPU>
Does that look anything like what you remember?
<jer>
it does
<jer>
thanks
<jer>
was interested in the formal verification column ordering
<ZipCPU>
The three columns are really independent of order
* jer
nods
<ZipCPU>
They all three need to be learned together.
<ZipCPU>
Hence, when working with switches and LEDs, you should be learning Verilator
<ZipCPU>
When working with buttons, you'll want to be getting to know VCD files
<ZipCPU>
This breaks down with the debugging bus ... that column looks a bit like its out of order.
<ZipCPU>
Debouncing should be done when you learn about buttons.
<ZipCPU>
Or .... not. You need some form of debugging tool to even know that you need debouncing
<ZipCPU>
Perhaps an instructor supplied debugging bus would be best there--yeah, that's what I think I meant when I wrote that.
<jer>
yeah so i'm actually digging into adding a debug interface to one of my cores currently, but i've taken a certain path in my getting to know formal verification, and did so mostly independently (save from a few clarifications from others) just curious =]
<ZipCPU>
I've also learned formal independently. Indeed, I only just ordered my first text on the topic.
<jer>
cool thanks
<promach_>
ZipCPU: The problem in my code is that the number of steps is both constant and not ??
<ZipCPU>
Yeah ... I'm chasing that down ...
<ZipCPU>
So ... it is marked as a constant.
cemerick has joined #yosys
<promach_>
I really need time to understand simplify.cc
<promach_>
you mean tx_state is marked as constant ?