<tpb>
Title: UART/test_UART.v at development · promach/UART · GitHub (at github.com)
<ZipCPU>
Lol
<ZipCPU>
You are setting cnt on the positive edge of tx_clk
<ZipCPU>
So, ... it changes on the positive edge of the tx_clk
<promach_>
I would say that this is not a problem at all
<ZipCPU>
You are checking cnt on the positive edge of rx_clk. tx_clk and rx_clk are out of phase by 180 degrees, hence the appearance of a negative edge issue.
<ZipCPU>
Well, I suppose it is a problem .... just not yosys' problem
<promach_>
and yosys seems to interpret posedge rx_clk differently
m_w has quit [Ping timeout: 240 seconds]
<ZipCPU>
Differently?
emeb has joined #yosys
<promach_>
yes
<promach_>
see smt_step=148
<promach_>
yosys should have executed the assertion at step 148 instead of 149
<ZipCPU>
You mean the assertion that eventually failed, the one on line 299?
m_w has joined #yosys
<promach_>
YES
<ZipCPU>
How are you running this? Your makefile only runs 10 steps
GuzTech has quit [Remote host closed the connection]
<ZipCPU>
I just tried running your code, and it passed with an induction length of 90.
<ZipCPU>
I must be looking at the wrong branch
AlexDaniel has quit [Remote host closed the connection]
AlexDaniel has joined #yosys
<promach_>
sby -f UART.sby
<promach_>
ZipCPU
<promach_>
use development branch
<promach_>
passed with an induction length of 90 ???
kraiskil has joined #yosys
<ZipCPU>
Ok, so .... the rx_clk rises and an assertion depending upon the rise of rx_clk fails. Not sure the issue here.
<promach_>
ZipCPU: are you getting assertion failure at line 299 ?
<promach_>
I mean the trace
<promach_>
did you have your own trace now ?
<ZipCPU>
Yes. It also failed at 299
<ZipCPU>
You've also got a problem with your had_been_enabled logic. It fails at line 440.
<ZipCPU>
Looks like a reset is messing that up.
<ZipCPU>
promach_: You don't have your resets properly tied together, now, do you?
<promach_>
tied together ? that is not realistic in real life
<promach_>
there must be clock phase difference between tx_clk and rx_clk in real life
<ZipCPU>
I just got a failing trace from your code where the rx reset was held at one for the entire trace ...
<ZipCPU>
When the tx reset was asserted, the entire design failed.
<promach_>
we have different trace
<promach_>
my reset_tx is not asserted at all in my trace
<promach_>
and reset_rx is not held at one for the entire trace
<ZipCPU>
I set the induction depth to 250 to get that trace. It seems to happen with a length of 200 as well.
<promach_>
ok, let me solve that line 440 first
<promach_>
strange, I have passed induction at length 200 before