danieljabailey has quit [Quit: ZNC 1.6.5+deb2build2 - http://znc.in]
danieljabailey has joined #yosys
philtor has quit [Ping timeout: 240 seconds]
gnufan has quit [Ping timeout: 252 seconds]
gnufan has joined #yosys
digshadow has joined #yosys
m_w has quit [Quit: leaving]
AlexDaniel has quit [Ping timeout: 256 seconds]
leviathanch has joined #yosys
dys has quit [Ping timeout: 276 seconds]
sunxi_fan has joined #yosys
FabM has joined #yosys
eduardo_ has joined #yosys
dys has joined #yosys
eduardo__ has quit [Ping timeout: 264 seconds]
AlexDaniel has joined #yosys
leviathanch has quit [Remote host closed the connection]
qu1j0t3 has quit [Remote host closed the connection]
leviathanch has joined #yosys
<ZipCPU>
promach: I haven't dug into your code, but it sounds like you are having this problem: https://imgur.com/Sz1vAWq (again)
AlexDani` has joined #yosys
AlexDaniel has quit [Ping timeout: 260 seconds]
m_t has joined #yosys
pie___ has joined #yosys
pie__ has quit [Ping timeout: 248 seconds]
<promach>
ZipCPU: give me time until tomorrow. I need some time
<ZipCPU>
promach: I'd like to chat before you dive into it again.
<ZipCPU>
Your current method of going about this is somewhat flawed, and I'd hate to have you spin your wheels a whole lot before coming to a solution.
<promach>
ZipCPU: flaw ?
<promach>
why ?
<ZipCPU>
Yes.
<ZipCPU>
I struggled with this myself.
<ZipCPU>
Part of the problem you are having, at least from a first glance, is that you have a "hidden state" than you cannot insure stays consistent with the assertions in your test module.
<promach>
of course, because sa and sb could have different values during induction
<ZipCPU>
Ok, good, so how would you fix this?
<promach>
you just hitmy weakness
<promach>
ouch
<ZipCPU>
Heheh ... well, exactly, because this is where you are struggling. That's why I wanted to chat about this.
<ZipCPU>
I'd rather you were successful, so ... it's worth discussing.
<promach>
give me a moment, let me think for a while
<promach>
assert(sa == sb)
<ZipCPU>
Absolutely! That's one of my favorite ways to solve this problem.
<ZipCPU>
Now, how does that apply to your UART?
<ZipCPU>
You have state within the modules of your UART, and tests in the top level module.
<promach>
did I face the similar issue in UART ?
<ZipCPU>
What keeps these variables "in synch"?
<ZipCPU>
Yes, but across files.
<promach>
which variables ?
<ZipCPU>
As I understand your UART (and I didn't look too deeply), you've got something like sa in one module, and sb in another. (Not literally, and not necessarily shift registers, but ... I hope you get my idea.)
<promach>
Tx or Rx ?
<ZipCPU>
Then, you have a difficulty in your top level module asserting that (sa==sb), since your top level module doesn't have access to sa or sb.
<ZipCPU>
Which variables? All of them.
<ZipCPU>
Or, more specifically, all of the internal variables.
<ZipCPU>
So, ... one of the ways I get around this is by placing all of my formal logic within the file I'm testing.
<ZipCPU>
Another way I get around this is to pass internal state variables around for formal verification purposes.
<promach>
sa==sb <-- do I need this for UART ?
<ZipCPU>
Please don't confuse the example with the concept.
<promach>
ok
<ZipCPU>
Conceptually, yes, you need this for your UART.
<promach>
I got your idea conceptually
<ZipCPU>
Ok, let me try teaching from another example's standpoint then.
<promach>
it is how I use the same concept to solve the induction bug I am facing
<ZipCPU>
When "proving" a module with a WB interface, I like to include a module containing the FV properties of a WB bus into a module having a WB interface.
<ZipCPU>
The biggest property I'm interested in is that a response cannot come back from the bus without a request.
<ZipCPU>
That means that my formal WB property file *must* count requests and acknowledgements.
<ZipCPU>
However, any module containing its own WB interface is also counting requests and acknowledgements.
<ZipCPU>
The two counters need to be asserted to be the same.
<ZipCPU>
Otherwise, these two counters will be different in induction and ... bad things will happen.
<ZipCPU>
I didn't want to do this, it messed up my concept of how the formal properties should be independent of the module, but eventually I gave in and: exported the counters of requests and acknowledgements from the formal properties module.
<ZipCPU>
As a result, I can assert that the numbers of requests and acknowledgements match the counts in the parent module.
<ZipCPU>
Making sense?
<promach>
yes
<ZipCPU>
I can show you the example of what I'm talking about if you would like.
<promach>
sure :)
<ZipCPU>
Perhaps my best example is that of a priority wishbone arbiter.
<promach>
round robin ?
<ZipCPU>
The logic for the arbiter itself is amazingly simply. Proving it ... well ...
<ZipCPU>
There's also an fwb_master set of properties.
<ZipCPU>
... in the same place that is.
<ZipCPU>
Note how the formal properties have the output parameters f_nreqs, f_nacks, and f_outstanding.
<ZipCPU>
I *need* these parameters within the arbiter to make certain these are consistent with the various slave's and masters of the arbiter.
<ZipCPU>
For example, consider lines 242-247 of the arbiter.
<ZipCPU>
If slave A has "ownership" of the outgoing bus, the B has neither any outstanding requests nor any outstanding acknowledgements--"B" hasn't had access to the bus yet.
<ZipCPU>
(I don't allow transactions to be broken in the middle.)
<promach>
broken in the middle ??
<ZipCPU>
Yes ... once "B" starts a request, the arbiter waits until "B"s transaction finishes before letting "A" have access to the bus.
<promach>
ok
<ZipCPU>
Hence, if "A" wants the bus while "B" has it, then "A" must have *NO* outstanding requests.
<promach>
I see
<ZipCPU>
Notice, though, how this formal property information needs to transition across modules.
<promach>
but I need some time to find out how I assert all the relevant internal variables
<promach>
I mean for my UART
<ZipCPU>
Notice also how my "top-level" formal module is the same as the module under test.
<ZipCPU>
Yeah, for your UART, yeah. That's why I wanted to have this chat.
<promach>
your top-level module ?
<ZipCPU>
In this case, wbpriarbiter.v
<promach>
ok
<ZipCPU>
If I wanted to make wbpriarbiter.v a submodule within any larger design, I'd need to export these same acknowledgement and request counters.
<ZipCPU>
(at a minimum)
<promach>
ok
<promach>
I understand
<promach>
I guess my UART will need a bit of time for passing induction :|
<ZipCPU>
Do you now see what you were missing before? ;)
<promach>
yes
<promach>
ZipCPU: thanks
qu1j0t3 has joined #yosys
<shapr>
howdy qu1j0t3
<qu1j0t3>
hi.
AlexDani` is now known as AlexDaniel
m_t has quit [Quit: Leaving]
FabM has quit [Quit: ChatZilla 0.9.93 [Firefox 52.5.0/20171114221957]]
vinny has joined #yosys
philtor has joined #yosys
m_w has joined #yosys
ZipCPU has quit [Ping timeout: 248 seconds]
digshadow has quit [Ping timeout: 264 seconds]
dys has quit [Ping timeout: 252 seconds]
ZipCPU has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]