ZipCPU|Laptop has quit [Ping timeout: 248 seconds]
promach_ has joined #yosys
digshadow has quit [Ping timeout: 248 seconds]
promach_ has quit [Quit: Leaving]
awygle has quit [Ping timeout: 246 seconds]
awygle has joined #yosys
ZipCPU|Laptop has joined #yosys
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Ping timeout: 240 seconds]
digshadow has joined #yosys
cr1901_modern1 is now known as cr1901_modern
xshock has joined #yosys
<xshock>
ZipCPU: you wrote that someone is working on supporting ice40up5k. are there any more details you can share? a forked repository and/or any reverse engineering notes/docs? thank you
mbuf has joined #yosys
xshock has quit [Quit: Page closed]
pie_ has quit [Ping timeout: 248 seconds]
m_t has joined #yosys
dys has quit [Ping timeout: 240 seconds]
proteusguy has quit [Remote host closed the connection]
proteusguy has joined #yosys
nrossi has joined #yosys
hobbes- has quit [Ping timeout: 248 seconds]
azonenberg has quit [Ping timeout: 246 seconds]
captain_morgan has quit [Ping timeout: 248 seconds]
azonenberg has joined #yosys
hobbes- has joined #yosys
captain_morgan has joined #yosys
jophish has joined #yosys
hobbes- has quit [Ping timeout: 248 seconds]
hobbes- has joined #yosys
befedo has joined #yosys
befedo has quit [Quit: befedo]
proteusguy has quit [Remote host closed the connection]
<promach>
interface and block level check is not enough
<ZipCPU>
Ok ... I see the document, but don't get what you are trying to say by it. Care to explain?
<promach>
I plan to do overall testing
<ZipCPU>
Um, okay, explain more please.
<promach>
UART (both Tx aand Rx) as a whole
<ZipCPU>
So you mean you intend to connect the Tx output to the Rx input?
<promach>
is it not possible ?
<ZipCPU>
Well, sure, it's possible, but it's also unreasonable.
<ZipCPU>
It's unreasonable because ... the RX has to deal with dissimilar timing.
<ZipCPU>
It will never have the perfect signal that the TX will create.
proteusguy has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]
<promach>
ZipCPU: that depends on how Rx is built.
<ZipCPU>
You may be missing my point.
<promach>
would you care to elaborate ?
<ZipCPU>
My point is that on real hardware, the Rx has one clock, the Tx has another, and the # of clocks defining a baud interval will be different from the one to the other.
<ZipCPU>
For example, imagine your transmitter.
<ZipCPU>
You define it to have 5000 clocks per baud interval.
<ZipCPU>
That creates a baud rate given by your input clock divided by 5000.
<ZipCPU>
However, if your input clock rate was off ...
<ZipCPU>
Likewise in the receiver, you have 5000 clocks per baud interval. That creates a baud rate given by the receiver's clock divided by 5000.
<ZipCPU>
Now, what happens if the input clock in the receiver isn't the same as the clock in the transmitter?
<promach>
I understand your concern. I am not trying to achieve cycle accurate.
<ZipCPU>
But formal proofs *are* cycle accurate.
<promach>
sigh, you are right.
<promach>
but this is the correct way for testing Tx, I suppose
<promach>
?
<ZipCPU>
Well ... didn't I just find several bugs with how your Tx was set up in the first place?
<promach>
that is my Tx block architecture
<ZipCPU>
Things like there's no serial output bit?
<promach>
it has
<promach>
that is just the FSM
<promach>
that is just one module
<ZipCPU>
Then you're abusing my time since you are asking me why one line is failing, but you haven't presented enough information for me to even evaluate it.
<promach>
sorry, I am not abusing your time
<promach>
I am really stucked
<promach>
even with -g leads me nowhere
<ZipCPU>
What does -g show you? Is the serial port line high or low?
<promach>
## 0 0:00:00 Solving for step 0..
<promach>
## 0 0:00:00 Solving for step 1..
<promach>
## 0 0:00:00 Solving for step 2..
<promach>
## 0 0:00:00 No solution found!
<promach>
sigh, I just feel like....
<ZipCPU>
Try BMC again.
<ZipCPU>
This time add the "--presat" argument.
<promach>
wow, where do you get this argument from ?
<ZipCPU>
Type "yosys-smtbmc" on a command line by itself. It should return usage information--a man page if you will.
<promach>
you got it from somewhere else
<promach>
it is not recognized
<promach>
what is yosys version ?
<promach>
what is your yosys version ?
<ZipCPU>
git log shows the last commit on my distro as: 455c1c9d97330b9d20cafe62cd72c3c3f71d3573
<promach>
what do you mean by last commit ?
<ZipCPU>
Did you clone the git repo, or download a tgz?
<promach>
mine is version 0.7
<ZipCPU>
0.7+364 (git sha1 455c1c9...)
<promach>
strange
<promach>
let me figure what is wrong
<ZipCPU>
promach: Check your "initial" statements. That's where I think you'll find your problem.
<promach>
thanks for the -g tips. now I know all those "passes" I had are not really correct
<promach>
ZipCPU
<ZipCPU>
You're welcome, promach.
jophish has quit [Quit: leaving]
befedo has joined #yosys
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<promach>
ZipCPU: you are against formally verify Tx and Rx together ?
<ZipCPU>
Formal verification is neither religion nor politics. I'm not sure how I'd be "against" it.
<promach>
right
<ZipCPU>
;.D
<promach>
I am not sure how would I know my transmitter works without a receiver
kmehall has quit [K-Lined]
<ZipCPU>
Ah, yes, ok, got it. Yes, I built a receiver just to prove my transmitter.
<ZipCPU>
It doesn't work the other way, though.
<promach>
so, you also have a receiver within formal verification of transmitter ?
<ZipCPU>
That's how I did it, yes.
kmehall has joined #yosys
<promach>
but receiver is not cycle-accurate
<promach>
at least for UART
<ZipCPU>
You mean .... because of my comments above?
<promach>
yeah, that somehow confuses me
<ZipCPU>
So ... the "receiver" that tests the transmitter is different from a generic receiver.
<ZipCPU>
The generic receiver only looks in the center of the transmit baud interval.
<ZipCPU>
The receiver that proves that the transmitter works must look at every sample coming out of the transmitter--not just the ones in the middle of the baud interval.
<promach>
so, how do you 'synchronize' the start bit ?
<ZipCPU>
You tell me.
<ZipCPU>
In my implementation, the UART output had to be '1' anytime !busy
<ZipCPU>
Likewise it had to be zero on the clock following (!busy)&&(i_request)
sklv has quit [Ping timeout: 248 seconds]
sklv1 has joined #yosys
eduardo__ has joined #yosys
azonenberg_work has quit [Ping timeout: 246 seconds]
eduardo_ has quit [Ping timeout: 260 seconds]
<promach>
ok, so you are not considering the situation where the Rx clock is a bit off compared to Tx clock ?
<ZipCPU>
When testing the transmitter, formal verification knows nothing of the rx clock, only the tx clock.
<promach>
ZipCPU: you assume single-clock domain in this case ?
<promach>
I think your Rx code, even in formal verification is using the same clock as Tx ?
<ZipCPU>
Multiple clock domains is an up and coming feature in yosys-smtbmc, not a current feature.
pie_ has joined #yosys
<ZipCPU>
As for "my Rx code", I haven't tried formally verifying it so ... I'm not sure what you are referencing.
<promach>
"your Rx" that is used to test your Tx
<ZipCPU>
Ahh ... okay, sorry.
<ZipCPU>
In the Rx code I wrote to formally test the Tx, both used the same clock.
<ZipCPU>
yes
<promach>
-not just the ones in the middle of the baud interval. ???
<ZipCPU>
Yes.
<promach>
huh ?
<ZipCPU>
In your case, the baud interval is about 5000 clocks long, right?
<promach>
yeah
<ZipCPU>
A formal verification will *prove* that for 5000 clocks, the transmitter isn't changing.
<promach>
I see
befedo has quit [Ping timeout: 260 seconds]
digshadow has joined #yosys
jophish has joined #yosys
sklv1 has quit [Remote host closed the connection]
sklv1 has joined #yosys
<thoughtpolice>
ZipCPU: I was under the impression yosys-smtbmc actually *does* support multiple clock domains?
<thoughtpolice>
I believe there are some notes in clifford's slides somewhere to this effect (and he tweeted it @ me a while back)
<ZipCPU>
Hmm ... you're probably right there, I just haven't gotten to the point where I've been able to simulate both clocks.
<ZipCPU>
I think what I last heard was that yosys didn't actually handle the verification of CDC crossings (yet)
sklv1 has quit [Read error: Connection reset by peer]
sklv1 has joined #yosys
befedo has joined #yosys
sklv1 has quit [Remote host closed the connection]
sklv has joined #yosys
azonenberg_work has joined #yosys
mbuf has joined #yosys
mbuf has quit [Remote host closed the connection]
<thoughtpolice>
ZipCPU: Ah, yeah, no clue about CDC.
mbuf has joined #yosys
mbuf has quit [Remote host closed the connection]
mbuf has joined #yosys
ravenexp has quit [Quit: WeeChat 1.9.1]
xshock has joined #yosys
ravenexp has joined #yosys
xshock has quit [Client Quit]
adj__ has quit [Ping timeout: 255 seconds]
mbuf has quit [Remote host closed the connection]
mbuf has joined #yosys
mbuf has quit [Quit: Leaving]
adj__ has joined #yosys
adj__ has quit [Ping timeout: 240 seconds]
adj__ has joined #yosys
adj__ has quit [Ping timeout: 240 seconds]
befedo has quit [Ping timeout: 248 seconds]
AlexDaniel has quit [Remote host closed the connection]
adj__ has joined #yosys
adj__ has quit [Ping timeout: 248 seconds]
befedo has joined #yosys
adj__ has joined #yosys
adj__2 has joined #yosys
adj__ has quit [Read error: Connection reset by peer]
adj__2 has quit [Ping timeout: 248 seconds]
AlexDaniel has joined #yosys
AlexDaniel has quit [Ping timeout: 240 seconds]
adj__ has joined #yosys
pie___ has joined #yosys
pie_ has quit [Read error: Connection reset by peer]
dys has joined #yosys
pie___ has quit [Remote host closed the connection]
pie___ has joined #yosys
pie___ is now known as pie_
gnufan has joined #yosys
befedo has quit [Quit: befedo]
pie_ has quit [Ping timeout: 260 seconds]
pie_ has joined #yosys
m_t has quit [Quit: Leaving]
azonenberg_work has quit [Ping timeout: 240 seconds]