davidlattimore has quit [Read error: Connection reset by peer]
davidlattimore has joined #yosys
sorear has quit [Read error: Connection reset by peer]
sorear has joined #yosys
davidlattimore has quit [*.net *.split]
bluesceada has quit [*.net *.split]
bluesceada has joined #yosys
davidlattimore has joined #yosys
fevv8[m] has quit [Ping timeout: 240 seconds]
wiizzard has quit [Ping timeout: 260 seconds]
notafile has quit [Ping timeout: 240 seconds]
jryans has quit [Ping timeout: 240 seconds]
promach3 has quit [Ping timeout: 268 seconds]
wiizzard has joined #yosys
fevv8[m] has joined #yosys
FFY00 has quit [Ping timeout: 260 seconds]
notafile has joined #yosys
jryans has joined #yosys
promach3 has joined #yosys
bwidawsk has quit [Quit: Always remember, and never forget; I'll be back.]
bwidawsk has joined #yosys
emeb_mac has quit [Quit: Leaving.]
danvet has joined #yosys
mndza has joined #yosys
vidbina has joined #yosys
jakobwenzel1 has joined #yosys
jakobwenzel has quit [Ping timeout: 260 seconds]
jakobwenzel1 is now known as jakobwenzel
jakobwenzel has quit [Ping timeout: 240 seconds]
miek has quit [Ping timeout: 265 seconds]
jakobwenzel has joined #yosys
jakobwenzel has quit [Ping timeout: 240 seconds]
jakobwenzel has joined #yosys
jakobwenzel has quit [Ping timeout: 246 seconds]
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
jakobwenzel has joined #yosys
vidbina has quit [Ping timeout: 246 seconds]
vidbina has joined #yosys
FFY00 has joined #yosys
dxld has joined #yosys
jakobwenzel has quit [Ping timeout: 246 seconds]
jakobwenzel has joined #yosys
miek has joined #yosys
vidbina has quit [Ping timeout: 264 seconds]
emeb has joined #yosys
vidbina has joined #yosys
vidbina has quit [Ping timeout: 272 seconds]
kraiskil has joined #yosys
Degi has joined #yosys
citypw has quit [Ping timeout: 268 seconds]
gmc has quit [Remote host closed the connection]
GenTooMan has quit [Quit: Leaving]
GenTooMan has joined #yosys
_whitelogger has joined #yosys
DrWhax has joined #yosys
emeb has quit [Quit: Leaving.]
kraiskil has quit [Ping timeout: 256 seconds]
kraiskil has joined #yosys
nengel has joined #yosys
jakobwenzel has quit [Ping timeout: 240 seconds]
emeb_mac has joined #yosys
kraiskil has quit [Ping timeout: 256 seconds]
vidbina has joined #yosys
kraiskil has joined #yosys
wifasoi has quit [Quit: Connection closed]
nengel has quit [Quit: gone afk]
nengel has joined #yosys
danvet has quit [Ping timeout: 272 seconds]
nengel has quit [Quit: gone afk]
nengel has joined #yosys
jakobwenzel has joined #yosys
jakobwenzel has quit [Client Quit]
vidbina has quit [Ping timeout: 256 seconds]
vidbina has joined #yosys
<roamingryan>
Is this channel an appropriate venue for asking some basic questions about formal verification with SymbiYosys?
nengel has quit [Quit: gone afk]
<roamingryan>
My question is this: I have a module with input and output valid/ready interfaces. The module does some processing on the data. For each word loaded into the module, a output word should be eventually produced. I am trying to implement an assertion that ensures that <# of input words> is equal to <# of output words>. I have implemented some counters that increment in response to (input_valid &&
<roamingryan>
input_ready) and (out_valid && out_ready). The problem is, under induction those can start at any value. Similarly, the internal state of the module isn't necessarily empty under induction. How should I be constraining them to stay matched?
kraiskil has quit [Ping timeout: 240 seconds]
vidbina has quit [Ping timeout: 240 seconds]
<awygle>
roamingryan: this is a tricky problem, with a few approaches, but let me suggest the biggest hammer first - have you tried switching from `smtbmc` to `abc pdr` as your proof engine? sometimes that Just Works, as it uses a different algorithm that doesn't have the same issues with induction
<roamingryan>
awygle: so far, I've only been using smtbmc but I do love "Just Works" solutions. Thanks for the tip.
<awygle>
roamingryan: the "gotchas" are mostly that abc pdr doesn't handle memories intelligently, so if you have a large BRAM or something it will expand it to that many bits, which in practice means it will never finish
<awygle>
to solve your induction problem you need to set up your asserts in such a way that the induction can't start from invalid states. increasing the depth of the induction may help with this, depending
<roamingryan>
Cool, `abc pdr` seems to have worked on one of my modules. No changes necessary to the asserts.
<awygle>
awesome :). it's still good to learn how to prove things with k-induction, but i find it kinda frustrating that k-induction is often the only strategy discussed in much of the documentation and examples
<roamingryan>
I will have to read up more on that proof engine as I'm curious how it works. I can wrap my head around the k-induction method, but as you said that's much better documented.
<ZipCPU>
There's an easier way than switching from an smtbmc based approach.
<ZipCPU>
roamingryan: Add assertions to your design. You should have an input counter, and an output counter, and then an assertion relating the two counters together, together with whatever's in your pipeline.
<tpb>
Title: Run length encoding an AXI stream (at zipcpu.com)
<ZipCPU>
Indeed, I have a whole section dedicated to counting the two streams--the one going in and the other going out.
<roamingryan>
Cool, I'll check that out. Indeed, I have another module where `abc pdr` isn't completing in a reasonable amount of time (presumably because it has more internal memory elements).
<ZipCPU>
Also, by "easier" I suppose I should say more reliable--for the exact same reason you just noticed.
<ZipCPU>
"abc pdr" doesn't always finish for me. At least when smtbmc doesn't pass induction it tells me where to look.
<roamingryan>
So my assert will basically need to compare the counters *and* add a correction/delta to account for the internal state of the module?
<ZipCPU>
I often handle the corrections in a combinatorial signal, separate from the assert, but then make an assertion about the counter.
<roamingryan>
Yeah, I can see how that would be more readable to future me.
<ZipCPU>
The thing you have to be aware of is that the induction engine might pick a counter value that will over flow just to spite you, so making sure you can deal with overflow is important.
<ZipCPU>
In most cases involving this type of counter, "dealing with overflow" simply means truncating to the right number of bits. Provided that number is sufficient .. ;)