<jhol>
basically it's a simple SDR powered by the IcoBoard
<jhol>
and I have an implementation of the Cummings FIFO - which doesn't work, then I can across your article which is guiding me towards debugging it
<jhol>
it's a good opportunity for me to try doing some formal methods
<ZipCPU>
Nice
<ZipCPU>
Have you seen my own video driver?
<ZipCPU>
It includes a C++ simulator, which will plot your generated video to the screen
<jhol>
I saw a link to it - didn't look into detail yet
<jhol>
but yes, that's pretty cool
<ZipCPU>
If you are building a Video controller, I think you'd want the simulator
<jhol>
while I have you, I'm puzzled by the induction behaviour
<jhol>
it seems odd that it disregards values set by initial statements
<ZipCPU>
Lol
<ZipCPU>
That's a very common response/question
<jhol>
...like I'm struggling to understand why you have to assume those things
<ZipCPU>
It even generated a yosys issue
<jhol>
hmmm... and it was closed with NOTABUG?
<ZipCPU>
It's how induction works tho: assume there exist N steps in time (not the initial state) that meet your assertions, find if the N+1th will also meet your assertions
<ZipCPU>
The problem is ... those N states may not be reachable
<ZipCPU>
Have you read my article on the induction exercise?
<jhol>
ok I might have glossed of the part where you explained WHY
<ZipCPU>
You *need* to make all unreachable states illegal via an assertion (or two, or four, etc.)
<ZipCPU>
Did you see today's tweet?
<jhol>
I did now!
<ZipCPU>
Use that .... it'll tell you where your bug is when working with induction
<ZipCPU>
If you find a problem in section A, you need more assertions
<awygle>
jhol: i find it useful to think of induction as going backwards
<jhol>
my reaction to this is about code-cleanliness - specifically the never-repeat-yourself rule
<jhol>
I had similar feelings about you unrolling Cummings submodules
<awygle>
starting from the success state and working backwards to see if it can reach a failure state, thus it ignores intiial statements because you're operating at some time T in the future
<awygle>
that's not really how it works but it helped me
<ZipCPU>
I had to unroll the Cummings modules
<jhol>
awygle: that's a helpful thought
<ZipCPU>
I didn't have much choice
<jhol>
can you not reference things inside them?
<ZipCPU>
Well, there is the "dot" notation assert(toplevel.main.reg == v)
<jhol>
yes
<ZipCPU>
But only the Verific enabled Yosys supports it
<jhol>
:(
<awygle>
why is that? that seems like a bug
<jhol>
-- or a todo at least
<ZipCPU>
No, it's just a feature/capability that has yet to be implemented.
<ZipCPU>
Yeah, todo
<awygle>
well, it's legal verilog that doesn't work. however you want to parse that
<awygle>
(as opposed to legal SystemVerilog, or legal VHDL)
<jhol>
just takes someone to volunteer to fix it ;)
<jhol>
it's not the end of the world - it just makes my code a bit more ugly
<jhol>
and it seems to me that without a fix for this, formal rules aren't going to scale very well with more complex Verilog modules
<jhol>
ZipCPU: another question...
<ZipCPU>
Go on
<jhol>
in some places you write assume/assert and in others `ASSUME/`ASSERT what's the purpose of the `define ?
<ZipCPU>
The purpose has to deal with aggregation
<ZipCPU>
I've aggregated modules by replacing ASSERT's with assume's when the module has been proved, and is now a submodule
<ZipCPU>
Likewise replacing ASSUME's with assert
<ZipCPU>
See the article on Aggregation
<jhol>
right! that makes sense
<ZipCPU>
That said, someone recently pointed out to me that the technique is quite broken
<ZipCPU>
It is possible that the assumption would interfere with the assertion, rendering the approach invalid.
<jhol>
oh ok... well for now I don't need to aggregate, so I'll await a brilliant article to show us the path forward
<ZipCPU>
That's my problem. I don't have a brilliant path forward. ;(
<ZipCPU>
We'll see what I can come up with
<jhol>
I have faith in you!
<ZipCPU>
I'm now studying someone else's book on the topic ... we'll see what he says. That said, I'm already disagreeing with him on several points --- but that's beside the point here.
seldridge has joined #yosys
cemerick has quit [Ping timeout: 245 seconds]
<awygle>
i try and only prove my modules from higher-level modules, so that the module only contains assert()s. i've met with mixed success but i think i just didn't properly understand what i was doing.
ym has joined #yosys
m_t_ has quit [Read error: Connection reset by peer]
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
<ZipCPU>
awygle: Do you use induction for your proofs?
<awygle>
ZipCPU: yup
<ZipCPU>
.... and you do the proof from higher level modules, with no insight into the state of the module(s) below?
<awygle>
and i definitely had to do some hacking around various limitations
<awygle>
we've had this discussion more than a couple of times :)