clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
ZipCPU|Laptop has joined #yosys
m_t has quit [Quit: Leaving]
<promach> For https://i.imgur.com/1w6imIw.png using BMC test, is there anything wrong with my initial statement for shift_reg ?
<awygle> promach: did you mean to set it to all 1's?
<promach> yes
<awygle> then technically, no. that should work.
<promach> huh ?
<awygle> your initial statement should set shift_reg to all 1's
<qu1j0t3> Tenacious-Techhu: you mean apart from vendor tools like Quartus?
<Tenacious-Techhu> qu1j0t3, yes.
<promach> awygle: so, the bug is not in the initial statement, I suppose ?
<awygle> promach: i'd bet line 29 is wrong
<promach> awygle: why would you say so ?
<awygle> promach: how many bits is "1"? how many bits is "0"?
<promach> one bit '1' and one bit '0'
<awygle> that's not what you wrote
<promach> you mean I should have
<promach> shift_reg <= {1'b1, i_data, 1'b0};
<promach> ??
<awygle> yes
<awygle> unqualified numeric constants in verilog are 32 bits wide
<promach> I recompile, but still same error at line 62
<promach> :|
<awygle> you can often get away with ignoring this, because verilog will truncate, but you're concatenating before truncating in this case so you probably get the wrong result
<promach> awygle: I will come back in half an hour
<promach> seems to me line 29 is not the real source bug ?
<awygle> promach: i'm not sure how the math rules work out for that assert, but i'd bet it's the same issue - ~0 is 32'hFFFFFFFF
<awygle> i'd recommend being more explicit that you mean 10'h3FF
<promach> awygle: let me try later. I got your message
<awygle> ... also, nothing actually resets shift_reg to ~0 when enable is low, at least in that image you sent me.
<promach> yes
<promach> I have to go now. I will come back later
<awygle> ZipCPU: it's always a cache problem ;-)
dys has quit [Ping timeout: 240 seconds]
ZipCPU|Laptop has quit [Ping timeout: 260 seconds]
ZipCPU|Laptop has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 260 seconds]
<ZipCPU> awygle: Is it really? If so, that was my first experience with one.
Tenacious-Techhu has quit [Ping timeout: 260 seconds]
pie__ has quit [Ping timeout: 260 seconds]
pie_ has joined #yosys
_whitelogger has joined #yosys
pie_ has joined #yosys
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 265 seconds]
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
dys has joined #yosys
dys has quit [Ping timeout: 268 seconds]
<promach_> awygle: it is not about 'enable' is not asserted and shift_reg is not reset to ~0
<promach_> see my initial statement at line 18
<promach_> it is at the second clock tick
<promach_> 'enable' and 'reset' signals have not been asserted yet by the second clock tick
<promach_> so, the only possible bug is at line 18
<promach_> maybe I should check the value of baud_clk at second clock tick
<promach_> but it is having value of zero
<promach_> so lines 24, 29 and 34 have not been executed yet by the second clock tick
<promach_> awygle: do you get what I am trying to convey ?
dys has joined #yosys
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 268 seconds]
m_t has joined #yosys
dys has left #yosys ["Killed buffer"]
<promach_> https://i.imgur.com/1w6imIw.png and baud_clk = 0 for the two clock ticks
<promach_> does this mean line 18 is the only culprit ?
<promach_> awygle: I have got past this problem.
dys has joined #yosys
<ZipCPU> promach: If you change the check on shift_reg to a check of whether or not it is equal to {(INPUT_DATA_WIDTH+PARITY_ENABLED+2){1'b1}} you will get past the problem of last night.
<ZipCPU> Not sure if you did that or not.
<ZipCPU> The next problem I had, looking at your code, was that you never constrained the enable line with any assumptions. Had you been meaning to do that?
<promach_> ZipCPU: no, that if statement and assert() is wrong
<promach_> I should not have done that assert()
<ZipCPU> Remember what I said: assume inputs, assert internal state and outputs.
<promach_> and awygle is right about 1'b1 and 1'b0
<promach_> for lines 29 and 34
<promach_> now I am stuck at another assert() in another module
<promach_> :|
<ZipCPU> Smile. This is just how development goes. ;)
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
<promach> ZipCPU: induction test is really frustrating
<ZipCPU> Smile. This is just how development goes. ;)
<ZipCPU> Yes, it can be.
<ZipCPU> It's also a very fundamental part of formal verification, so ... it is worth understanding well.
<promach> I am so irritated with how one bug comes after another
<ZipCPU> Relax ... there's only one bug left. :)
<ZipCPU> (There's always *only* one bug left ...)
<promach> I do not feel and think so
<ZipCPU> No, it's true. Why? Because it's the fundamental assumption of all debugging: there is never more than one bug in your code. If you didn't make that assumption, then you'd *really* struggle to debug *anything*.
<ZipCPU> Basically: assume(a); assert(a); where (a) is (no_more_than_one_bug). It's always true--because you are always assuming it.
<promach> maybe assuming such way would make me feel better in debugging
<ZipCPU> Sure, go ahead! You are already assuming it any way, might as well acknowledge it.
<promach> using hamster method to compute busy signal give me problems in induction test :|
massi has joined #yosys
pie_ has joined #yosys
<ZipCPU> Or is that because you asserted on the positive edge of a clock?
<ZipCPU> What if you asserted like, always @(*) assert(o_busy == (shif_reg != 0));
<promach> see, the shift reg will be appended and preappended with start bit and stop bit respectively
<promach> only one clock cycle after (enable & !o_busy)
<promach> so what happened in the screenshot is that
<promach> when 'enable' is asserted, 'o_busy' is not asserted
<promach> and also the problem of 'has_been_enabled' is HIGH before it should
<promach> ZipCPU: you may not be able to see it directly from here because you are not using hamster's approach
<promach> hamster approach seems to work only on one UART transaction
<promach> At clock tick 17, I am not sure why shift_reg changes value to 0
<promach> oh, okay. line 34
AlexDaniel has quit [Ping timeout: 252 seconds]
m_w has joined #yosys
massi has quit [Remote host closed the connection]
gnufan has quit [Ping timeout: 248 seconds]
gnufan has joined #yosys
cr1901_modern1 is now known as cr1901_modern
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
dys has quit [Ping timeout: 276 seconds]
dys has joined #yosys
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
philtor has quit [Ping timeout: 248 seconds]
philtor has joined #yosys
dys has quit [Ping timeout: 240 seconds]
pie_ has quit [Ping timeout: 246 seconds]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 250 seconds]
pie_ has joined #yosys
dys has joined #yosys
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
AlexDaniel has joined #yosys
m_w has quit [Quit: Leaving]
MrBusiness has quit [Read error: Connection reset by peer]
MrBusiness has joined #yosys