<ZipCPU>
promach__: So, I'm working on my own UART proof this evening.
<ZipCPU>
It's taken me a bit of work to force the two states, transmitter and receiver, together.
<ZipCPU>
One thing I did was to count clocks within both transmitter and receiver, and then insist that the difference between them was within a minimal limit.
<ZipCPU>
promach: Another thing I did was force the transmission in the transmitter, and the reception in the receiver, to match the state given by the clock count.
<ZipCPU>
Hence, if the receiver is N*BAUDCLOCKS+k clocks following the last idle, and *if* it is transmitting a known value, *then* the state of the receiver must be ... (assert the shift register state)
<awygle>
ZipCPU: so if I understand correctly, you are proving the TX and RX halves of the UART together? Under what conditions?
<ZipCPU>
I then had to repeat this within the transmitter. If the transmitter is N*BAUDCLOCKS+k clocks following a valid start bit, then it must have received either N or N-1 bits that matched the known transmit patttern.
<ZipCPU>
awygle: Not quite.
<ZipCPU>
I'm actually only proving the RX half.
<ZipCPU>
However, to prove it I need to assume a transmitter.
<ZipCPU>
That transmitter is within the RXUART code.
<ZipCPU>
The condition I'm trying to hold to is that the clocks are within a half-a-baud of each other, but otherwise potentially dissimilar.
<ZipCPU>
Or should I say, the clock rates are such that after 10 baud intervals, the result will be within a half a baud of each other.
<awygle>
ZipCPU: hmm... I don't clearly see why a transmitter is required. why wouldn't the SAT solver control the input arbitrarily?
gnufan has quit [Ping timeout: 240 seconds]
<ZipCPU>
2 reasons. 1) you want to make certain the input obeys the rules of a UART, and 2) you want to make certain that at the end of the transmission, you received the "right" value.
<ZipCPU>
Rules of UART include: a start bit, a stop bit, 8-data bits, and things only change on baud intervals.
<awygle>
ZipCPU: okay, I see why you might want a transmitter for your second purpose. at least, I don't see an obvious way to check the "rightness" without one
<awygle>
I'm less sanguine about the first purpose. wouldn't one of the reasons to prove the receiver be to prove that it does the right thing in the presence of bad input?
<ZipCPU>
I'm not sure I follow.
<ZipCPU>
??
<ZipCPU>
Ahh ... okay, so ... does the receiver do "good things" in the presence of something that doesn't behave like a UART, is that your question?
<awygle>
if I have a UART core in my FPGA, and someone hooks a SPI driver up to the receiver, it seems to me that I'd want *something* in particular to happen
<awygle>
yes
<ZipCPU>
What would you consider the "right" answer to be if you gave a UART RX processor something other than a UART input?
<ZipCPU>
I would struggle with that, as it seems the "right" answer for a UART depends upon the "right" data being given to it.
<awygle>
Probably to assert an error bit (either in a register or as an output from the module)
<awygle>
More importantly, I'd say that it should be able to recover if the input becomes "good" again
<sorear>
also, if it's hooked up to a bus of some kind, it should respect the rules of that bus (e.g. ack all transactions that require acks) no matter what it's connected to
<ZipCPU>
sorear: That's the easy part. I've already got that working without problems. ;)
<awygle>
Sure, although I'd call that a property of (e.g.) a MODBUS controller that just happens to contain a UART
gnufan has joined #yosys
<ZipCPU>
Actually, let me back up a bit .... I've only managed to "prove" so far the transmitter and the FIFO. I'm working on the receiver. The bus interaction takes place within the module that integrates all of these parts.
<ZipCPU>
Right now, my abilities with FV are really limited to leaf nodes, so I haven't gotten to the parent module yet.
<awygle>
In any case I don't particularly care what you do in response to bad input, but defining *a* behavior and showing that it occurs seems critical to me
<awygle>
But maybe I'm overly paranoid - #python has spent all day suggesting that might be the case :-P
<ZipCPU>
How so?
<awygle>
I miss the ability to do proper encapsulation. "Private" methods in python are marked by a leading _ but are still entirely accessible
<awygle>
The folks there seem to think that I should trust my users more and not worry about it
<ZipCPU>
I've been instructed on how to do it via abstraction, but I haven't tried it yet.
<ZipCPU>
The basic rule is that if you can prove (A -> C), then it must be true that (AB -> C) as well.
<ZipCPU>
So ... if I can prove that a UART that produces random data "works" in the parent module, then it must also be true that a UART producing the proper data would work as well.
<ZipCPU>
Or ... at least that's how I'm looking at it these days.
<awygle>
I am just starting on this journey as well. I'd appreciate your thoughts on how I am planning to approach it.
gnufan has quit [Ping timeout: 240 seconds]
<ZipCPU>
Well ... that's how I'd approach it. I might even replace the RXUART submodule of the parent with a module that just produces random data outputs, but only if FORMAL is defined.
<awygle>
my intention is to start with what i'd call a "domain model" of a UART. at the lowest level, the UART receives bits. at a higher level, it receives bytes (or whatever the 1-character packets a UART receives are properly called). at a higher level still, those bytes either satisfy or do not satisfy certain properties (parity, primarily). and it does all this under certain conditions (say, configured baud rate must be within 5% of the actual baud
<awygle>
rate)
<awygle>
so first i would prove that, under those conditions, the receiver can properly receive a bit (and properly reject an invalid bit)
<ZipCPU>
How will you know the bit received is the "correct" one, in order to know it was properly received?
<ZipCPU>
Or, for that matter, how will you know you've sampled the channel in the "right" place?
<awygle>
for the first, i would assert that the output bit equals the input bit, and that the input bit has been set for the last 16 samples (assuming 16x oversampling)
<awygle>
or maybe the last 15/16 for glitch rejection, but you get the general approach
<awygle>
actually, that more or less answers your second question as well, doesn't it?
<ZipCPU>
Hmm ... not sampling in the center of the baud?
gnufan has joined #yosys
<awygle>
my understanding of UARTs is that due to their low speed oversampling is more typical than trying to do clock recovery style approaches. although i could be wrong
<ZipCPU>
We must be misunderstanding each other, for I cannot comprehend a reason why you wouldn't sample in the middle of the baud.
<awygle>
because the input is asynchronous
<awygle>
and finding the middle of the baud is nontrivial
<awygle>
and there may be glitching, etc
<ZipCPU>
Not at all! You just want a half-baud interval from the beginning of the start bit. That puts you in the middle of the baud interval.
<ZipCPU>
If you want to the end of the interval, then if the transmitter is just a touch faster than the receiver it will get "bad" data.
<ZipCPU>
*wait
<ZipCPU>
"bad" data in this case means the receiver will appear to "skip" bits that were transmitted.
<awygle>
ah, i see what you're saying now. i was imagining something much more analog, but you're just talking about delaying by a number of clocks that gets you as close as possible to the center of the baud
<ZipCPU>
If you are really worried about glitching, I suppose you could apply a "matched filter", but then it might be harder to align to the start bit.
<awygle>
i was just taking his "sample multiple times" to the extreme
<awygle>
regardless, this is somewhat off the track. if i'm proving the receiver, i don't care if i've sampled at the "right" place. i only care that i got the right data. as long as my input is constrained in such a way that all the "errors" i've claimed to be able to handle (5% baud difference, maybe 100ns of glitching) are allowed to the SAT solver, any bugs caused by bad sampling location will be exposed.
<ZipCPU>
Sounds fair.
<awygle>
basically, at every clock the "bit retriever" portion of the UART makes some claim about the data. if it asserts "valid && output" then it's claiming that the last 16 clocks were a valid 1 bit. as long as we remember the last 16 clocks in our formal verification code, we can check whether that claim is accurate.
<awygle>
at that point i assume we'd also need to use cover() to show that it eventually asserted all combinations of (valid, output) and error
<ZipCPU>
Ok, I think I'm starting to see what you are doing.
<awygle>
once we've got that, we can take the same approach with the character recognizer. the character recognizer claims "i've received a valid 0x7F", we remember the last ~12 input bits, and test the claim with our assertions
<awygle>
does that seem generally sane?
<ZipCPU>
Yes, but more than that ... it sounds like you might be able to "cheat" on the clock cycles as well.
<ZipCPU>
To your benefit, if the second stage only runs once every 16 clocks, and if it is independent of the lower stages clock rate, you might manage to run your formal proof on only every 16th clock.
<awygle>
True, but two caveats - one, I'm not sure proving the pieces independently proves the combination correct, and a full-system simulation would have to be evaluated at the fastest rate. Two, I'm not totally sure how glitching would work but handling it might result in needing the bit recovery proof to run much much faster than the sample rate.
<awygle>
"simulation" was a bad word there. "proof".
promach__ has quit [Ping timeout: 256 seconds]
gnufan has quit [Ping timeout: 260 seconds]
* ZipCPU
tugs at his beard
gnufan has joined #yosys
<awygle>
Thinking about it further, I don't fully understand how the performance aspects of FV work out, but I don't think it'd be related to the baud rate/clock rate really. At least not for induction.
<awygle>
It's all about the number of states, isn't it?
<awygle>
In that case, adding glitching adds to the state space somewhat but it's not as simple as "now I have to run the simulation 4x faster" because there isn't a simulation
<awygle>
Hard to break that habit of thought...
<ZipCPU>
Yeah ... I guess I'm struggling with that myself.
<awygle>
Unrelated, but how are your preparations for the course you're teaching going?
pie_ has quit [Ping timeout: 248 seconds]
<ZipCPU>
awygle: Thanks for asking!
<ZipCPU>
I've been dealing with a contract I'm working for, and so ... I haven't put enough time into it for the past two weeks.
<ZipCPU>
That said, there's really only three chapters missing or incomplete. 1) on $anyconst and $anyseq, 2) On abstraction, and 3) on the System Verilog bindings available with Verific.
<ZipCPU>
You've probably seen me write about my experiences with the CYCLONE-V. That is for the paid contract.
<ZipCPU>
I should mention, I do have some fun projects coming. One is a port of the ZipCPU to the tinyfpga, and another (nearly identical) project ports the ZipCPU to the MAX1000.
gnufan has quit [Ping timeout: 264 seconds]
<awygle>
ZipCPU: are those paid projects? Being aware that it's none of my business
<ZipCPU>
The post about the cyclone-v is a paid project.
<ZipCPU>
I'm hoping to get paid for teaching, but ... the deal isn't really complete.
<awygle>
ah i see
<awygle>
which tinyfpga are you planning to use?
gnufan has joined #yosys
gnufan has quit [Ping timeout: 260 seconds]
gnufan has joined #yosys
gnufan has quit [Ping timeout: 240 seconds]
gnufan has joined #yosys
xrexeon has quit [Ping timeout: 256 seconds]
gnufan has quit [Ping timeout: 260 seconds]
gnufan has joined #yosys
digshadow has quit [Ping timeout: 248 seconds]
digshadow has joined #yosys
hanetzer has quit [Remote host closed the connection]
hanetzer has joined #yosys
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 276 seconds]
TFKyle has joined #yosys
m_t has joined #yosys
danieljabailey_ has quit [Ping timeout: 255 seconds]
proteusguy has joined #yosys
proteus-guy has quit [Ping timeout: 240 seconds]
leviathan has joined #yosys
<ZipCPU>
awygle: I have the Bx on my desk.
xrexeon has joined #yosys
xrexeon has quit [Quit: leaving]
xrexeon_ has joined #yosys
pie_ has joined #yosys
xrexeon_ has quit [Ping timeout: 256 seconds]
dys has joined #yosys
<thoughtpolice>
ZipCPU: Are you using Yosys with Verific?
pie_ has quit [Ping timeout: 240 seconds]
AlexDaniel has joined #yosys
jwhitmore has joined #yosys
jwhitmore has quit [Ping timeout: 248 seconds]
pie_ has joined #yosys
<ZipCPU>
thoughtpolice: Sadly, no. I need to try it with Verific, but haven't really done so yet. One of the lessons in the formal course is to be based upon that.
kraiskil has joined #yosys
<daveshah>
thoughtpolice: I have done a bit with Yosys/Verific, if you're curious
<ZipCPU>
daveshah: Cheers! How's it going?
<daveshah>
It's been going well, although I didn't get round to the VHDL verification I planned today because SymbiFlow stuff was distracting me...
proteus-guy has joined #yosys
<ZipCPU>
:D
m_t has quit [Quit: Leaving]
kraiskil has quit [Ping timeout: 265 seconds]
kraiskil has joined #yosys
cemerick_ has joined #yosys
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 256 seconds]
cemerick has quit [Ping timeout: 256 seconds]
jwhitmore has joined #yosys
kraiskil has quit [Quit: Leaving]
ravenexp has quit [Quit: WeeChat 1.9.1]
m_t has joined #yosys
m_t has quit [Max SendQ exceeded]
m_t has joined #yosys
ravenexp has joined #yosys
ravenexp has quit [Quit: WeeChat 2.0.1]
ravenexp has joined #yosys
eduardo_ has quit [Quit: Ex-Chat]
m_t has quit [Quit: Leaving]
dmin7 has joined #yosys
proteus-guy has quit [Ping timeout: 264 seconds]
proteus-guy has joined #yosys
dmin7 has quit [Ping timeout: 256 seconds]
leviathan has quit [Remote host closed the connection]