AlexDaniel has quit [Remote host closed the connection]
danieljabailey has quit [Ping timeout: 240 seconds]
danieljabailey has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
xerpi has joined #yosys
xerpi has quit [Remote host closed the connection]
xerpi has joined #yosys
cr1901_modern has left #yosys [#yosys]
mazzoo_ has joined #yosys
mazzoo has quit [Read error: Connection reset by peer]
mazzoo_ has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
mazzoo has joined #yosys
promach_ has joined #yosys
promach has quit [Ping timeout: 240 seconds]
emeb_mac has quit [Ping timeout: 245 seconds]
leviathan has joined #yosys
kraiskil has joined #yosys
pie_ has joined #yosys
jwhitmore has joined #yosys
jwhitmore has quit [Remote host closed the connection]
kraiskil_ has joined #yosys
kraiskil has quit [Ping timeout: 256 seconds]
kraiskil_ is now known as kraiskil
jwhitmore has joined #yosys
jwhitmore has quit [Remote host closed the connection]
pie_ has quit [Read error: Connection reset by peer]
pie_ has joined #yosys
proteus-guy has joined #yosys
develonepi3 has joined #yosys
xerpi has quit [Quit: Leaving]
fsasm has joined #yosys
pie_ has quit [Ping timeout: 255 seconds]
seldridge has joined #yosys
pie_ has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
AlexDaniel has joined #yosys
seldridge has quit [Ping timeout: 276 seconds]
pie_ has joined #yosys
seldridge has joined #yosys
promach has joined #yosys
emeb has joined #yosys
develonepi3 has quit [Remote host closed the connection]
pie_ has quit [Ping timeout: 256 seconds]
luismarques has joined #yosys
fsasm has quit [Ping timeout: 276 seconds]
<luismarques>
Hi. For formal verification, how do you do synchronous resets? The example I found with an initial block and a if (!$initstate) block seems geared towards async resets
m_w has joined #yosys
<awygle>
i could not get async resets working, actually
pie_ has joined #yosys
<ZipCPU>
Is the question about async resets or synchronous resets? Both work.
<awygle>
if you share an example of what you're trying to do, i can take a look
<luismarques>
It has an initial block which assumes(rst); But because my reset is synchronous, that’s not enought to actually reset my circuit, you also need to toggle the clock
seldridge has quit [Ping timeout: 256 seconds]
<ZipCPU>
Are you using symbiyosys or yosys/yosys-smtbmc with clk2fflogic?
<ZipCPU>
.... and which slide of the pdf are you referencing?
<luismarques>
I’m using yosys-smtbmc, but I don’t know anything about clk2fflogic
<ZipCPU>
clk2fflogic is a yosys command to make asynchronous logic useful. If you aren't using it, then don't worry about toggling the clock--the formal tool will handle it for you.
<awygle>
it must be the "hello test-bench" slide, 12 or 13
<ZipCPU>
(You may not see it toggle in your trace ...)
<luismarques>
page 13 of the slide
<awygle>
i hate this example by the way
<awygle>
hate is a strong word, i just woke up cranky today. but i don't like this example, i think it confuses more than it helps.
<ZipCPU>
initial assume(i_reset); isn't a bad assumption
<luismarques>
In the VCD I see the reset=1, but because the clock hasn’t yet toggled the port I’m looking at still has garbage. I thought if (!$initstate) would take care of that, but not with a sync reset
<ZipCPU>
Don't look for clock toggles in the VCD file ... you may not see them.
<ZipCPU>
Things will change on the clock, even if the clock doesn't appear to toggle.
emeb has quit [Ping timeout: 265 seconds]
<luismarques>
Ok, but the result doesn’t make sense. I know that if the circuit is reset that port should equal 1, and the VCD shows it equals 0 immediately, so I’m doing something wrong. I’ll try a smaller example then
<ZipCPU>
Are you using the example, or your own design? If your own design, can you share it at all?
<luismarques>
My own design. I’ll share a smaller design
emeb has joined #yosys
seldridge has joined #yosys
<luismarques>
Ok, apparently the issue is that I tried to directly assert on the output port instead of using a wire. With the wire it works as expected…
digshadow has quit [Quit: Leaving.]
<ZipCPU>
That shouldn't be the problem.
<ZipCPU>
You should be able to make assertions on wires, regs, inputs and outputs with no difference between the two
<luismarques>
Perhaps it was because the output port of the circuit wasn’t connected to anything in the testbed (other than the assert) and the optimizations influenced the result?
<ZipCPU>
No, that shouldn't have affected anything. I have a lot of dangling wires in my designs that I use for formal properties only.
<awygle>
I could see that happening if you ran synthesis before formal in your flow.
<daveshah>
assertions should still mean a wire is loaded and therefore kept though
<awygle>
Which would probably be incorrect but would be easy to do without thinking
<awygle>
Mm, good point. Not sure how that works.
<daveshah>
Yosys creates an internal cell for assertions - with a single input - during elaboration and should be kept through synthesis
<awygle>
If not that then I bet it's default_nettype again
<luismarques>
well, I was doing read_verilog -formal tb.v; prep -top tb; memory -nordff; write_smt2 -wires tb.smt2
<daveshah>
that looks like a perfectly good flow
<luismarques>
In any case, I don’t really understand the reset: if I only want to assert some property after a synchronous reset, what’s the correct way to do that?
<awygle>
i usually define an "f_reset_in_past" signal for this purpose
ZipCPU|ztop has quit [Remote host closed the connection]
ZipCPU|ztop has joined #yosys
<luismarques>
What’s the first numeric column in the output of yosys-smtbmc?
kraiskil has quit [Ping timeout: 240 seconds]
<luismarques>
Weird: yosys-smtbmc seemed to be working fine. I compared two modules that should behave equally and it found a bug. But now it failed in a line that says “assert(dqo1 == dqo2);” but in the VCD file both dqo1 and dqo2 are always zero (and thus equal)...
promach has quit [Ping timeout: 265 seconds]
<luismarques>
OK, I removed all the other asserts, just to be sure it wasn’t a wrong line output; same result
<mjoldfield>
Are the zeros different widths ? Does == care ?
<luismarques>
@mjoldfield yup, that was it. I was using two 1-bit wires, instead of two 16-bit ones. Still, I would have expected the wires to be set to the LSB of each port and thus to compare equal, thus missing the bug. But the wire had the full value, although the VCD only showed the LSB
<ZipCPU>
luismarques: Was the assert on a positive edge of a clock?
<luismarques>
ZipCPU: you mean the assert condition or the triggered assert?
<luismarques>
It wasn’t written to be checked at the clock edge, but it triggered on a positive edge of the clock, yes
<ZipCPU>
Is the assert an always @(posedge i_clk) assert (A == B); or an always @(*) assert(A == B);
<luismarques>
@*
<ZipCPU>
Ok, @* will show in the final clock of the VCD file, @(posedge clk) one column before that.
<luismarques>
yeah, the problem was the bit width, as mjoldfield guessed
<ZipCPU>
Got it.
<luismarques>
Thanks guys
<ZipCPU>
;)
jwhitmore has joined #yosys
mjoldfie_ has joined #yosys
mjoldfield has quit [Ping timeout: 260 seconds]
jwhitmore has quit [Remote host closed the connection]