Tuesday, 2018-06-26

*** tpb has joined #yosys00:00
*** emeb_mac has joined #yosys00:25
*** m_w has quit IRC00:48
*** dxld has quit IRC00:55
*** dxld has joined #yosys00:57
*** knielsen has quit IRC01:07
*** promach_ has joined #yosys01:09
*** seldridge has joined #yosys01:26
*** promach_ has quit IRC01:40
*** digshadow has quit IRC02:16
*** knielsen has joined #yosys02:53
*** seldridge has quit IRC03:30
*** digshadow has joined #yosys03:38
*** AlexDaniel has quit IRC03:43
*** danieljabailey has quit IRC03:59
*** danieljabailey has joined #yosys04:02
*** cr1901_modern has quit IRC04:33
*** cr1901_modern has joined #yosys04:33
*** xerpi has joined #yosys05:51
*** xerpi has joined #yosys05:52
*** cr1901_modern has left #yosys05:58
*** mazzoo_ has joined #yosys06:20
*** mazzoo has quit IRC06:20
*** mazzoo_ has quit IRC06:23
*** cr1901_modern has joined #yosys06:24
*** mazzoo has joined #yosys06:25
*** promach_ has joined #yosys06:27
*** promach has quit IRC06:29
*** emeb_mac has quit IRC06:42
*** leviathan has joined #yosys07:21
*** kraiskil has joined #yosys07:40
*** pie_ has joined #yosys07:46
*** jwhitmore has joined #yosys08:20
*** jwhitmore has quit IRC08:59
*** kraiskil_ has joined #yosys09:06
*** kraiskil has quit IRC09:09
*** kraiskil_ is now known as kraiskil09:18
*** jwhitmore has joined #yosys09:27
*** jwhitmore has quit IRC09:49
*** pie_ has quit IRC10:05
*** pie_ has joined #yosys10:06
*** proteus-guy has joined #yosys11:25
*** develonepi3 has joined #yosys11:30
*** xerpi has quit IRC11:47
*** fsasm has joined #yosys11:58
*** pie_ has quit IRC12:25
*** seldridge has joined #yosys13:02
*** pie_ has joined #yosys13:24
*** pie_ has quit IRC13:34
*** AlexDaniel has joined #yosys13:40
*** seldridge has quit IRC14:17
*** pie_ has joined #yosys14:22
*** seldridge has joined #yosys14:35
*** promach has joined #yosys14:54
*** emeb has joined #yosys15:02
*** develonepi3 has quit IRC15:05
*** pie_ has quit IRC16:01
*** luismarques has joined #yosys16:07
*** fsasm has quit IRC16:11
luismarquesHi. 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 resets16:12
*** m_w has joined #yosys16:12
awyglei could not get async resets working, actually16:12
*** pie_ has joined #yosys16:13
ZipCPUIs the question about async resets or synchronous resets?  Both work.16:13
awygleif you share an example of what you're trying to do, i can take a look16:13
luismarquesWell, consider for instance the example in this PDF: http://www.clifford.at/papers/2016/yosys-smtbmc/slides.pdf16:14
luismarquesIt 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 clock16:15
*** seldridge has quit IRC16:15
ZipCPUAre you using symbiyosys or yosys/yosys-smtbmc with clk2fflogic?16:15
ZipCPU.... and which slide of the pdf are you referencing?16:16
luismarquesI’m using yosys-smtbmc, but I don’t know anything about clk2fflogic16:16
ZipCPUclk2fflogic 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.16:17
awygleit must be the "hello test-bench" slide, 12 or 1316:17
ZipCPU(You may not see it toggle in your trace ...)16:17
luismarquespage 13 of the slide16:17
awyglei hate this example by the way16:17
awyglehate 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.16:18
ZipCPUinitial assume(i_reset); isn't a bad assumption16:18
luismarquesIn 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 reset16:19
ZipCPUDon't look for clock toggles in the VCD file ... you may not see them.16:19
ZipCPUThings will change on the clock, even if the clock doesn't appear to toggle.16:20
*** emeb has quit IRC16:20
luismarquesOk, 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 then16:21
ZipCPUAre you using the example, or your own design?  If your own design, can you share it at all?16:22
luismarquesMy own design. I’ll share a smaller design16:22
*** emeb has joined #yosys16:33
*** seldridge has joined #yosys16:38
luismarquesOk, 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…16:43
*** digshadow has quit IRC16:46
ZipCPUThat shouldn't be the problem.16:48
ZipCPUYou should be able to make assertions on wires, regs, inputs and outputs with no difference between the two16:49
luismarquesPerhaps 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?16:50
ZipCPUNo, that shouldn't have affected anything.  I have a lot of dangling wires in my designs that I use for formal properties only.16:52
awygleI could see that happening if you ran synthesis before formal in your flow.16:54
daveshahassertions should still mean a wire is loaded and therefore kept though16:54
awygleWhich would probably be incorrect but would be easy to do without thinking16:54
awygleMm, good point. Not sure how that works.16:55
daveshahYosys creates an internal cell for assertions - with a single input - during elaboration and should be kept through synthesis16:55
awygleIf not that then I bet it's default_nettype again16:56
luismarqueswell, I was doing read_verilog -formal tb.v; prep -top tb; memory -nordff; write_smt2 -wires tb.smt216:58
daveshahthat looks like a perfectly good flow16:59
luismarquesIn 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?17:15
awyglei usually define an "f_reset_in_past" signal for this purpose17:16
*** ZipCPU|ztop has quit IRC17:26
*** ZipCPU|ztop has joined #yosys17:26
luismarquesWhat’s the first numeric column in the output of yosys-smtbmc?17:37
*** kraiskil has quit IRC17:50
luismarquesWeird: 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)...18:18
*** promach has quit IRC18:20
luismarquesOK, I removed all the other asserts, just to be sure it wasn’t a wrong line output; same result18:27
mjoldfieldAre the zeros different widths ? Does == care ?18:28
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 LSB18:35
ZipCPUluismarques: Was the assert on a positive edge of a clock?18:38
luismarquesZipCPU: you mean the assert condition or the triggered assert?18:40
luismarquesIt wasn’t written to be checked at the clock edge, but it triggered on a positive edge of the clock, yes18:40
ZipCPUIs the assert an always @(posedge i_clk) assert (A == B); or an always @(*) assert(A == B);18:40
ZipCPUOk, @* will show in the final clock of the VCD file, @(posedge clk) one column before that.18:41
luismarquesyeah, the problem was the bit width, as mjoldfield guessed18:41
ZipCPUGot it.18:41
luismarquesThanks guys18:41
*** jwhitmore has joined #yosys18:44
*** mjoldfie_ has joined #yosys18:59
*** mjoldfield has quit IRC19:02
*** jwhitmore has quit IRC19:03
*** jwhitmore has joined #yosys19:07
*** m_w_ has joined #yosys19:12
*** m_w has quit IRC19:14
*** dys has joined #yosys19:23
*** leviathan has quit IRC19:29
*** m_w_ has quit IRC19:42
*** seldridge has quit IRC20:08
*** m_w has joined #yosys20:22
*** seldridge has joined #yosys20:29
*** jwhitmore has quit IRC21:02
*** pie_ has quit IRC21:05
luismarquesWhat’s the first numeric column in the output of yosys-smtbmc?21:27
*** seldridge has quit IRC21:28
*** pie_ has joined #yosys21:42
*** seldridge has joined #yosys21:49
*** seldridge has quit IRC22:08
*** mjoldfield has joined #yosys22:11
*** mjoldfie_ has quit IRC22:15
* ZipCPU needs to remind himself what that column looks like ...22:21
ZipCPUYou mean the time column?22:21
ZipCPUshowing the time since yosys-smtbmc was started?22:22
*** dys has quit IRC22:23
luismarques##   2909   0:48:29  Checking asserts in step 36..22:25
luismarques##   3622   1:00:22  Checking asserts in step 37..22:25
awygle2909 seconds. 2909/60 = 48 remainder 2922:34
*** mjoldfield has quit IRC22:35
*** mjoldfield has joined #yosys22:36
luismarquesAh. I thought it would be something fancy like some number of SAT terms or whatever ;)22:37
*** jwhitmore has joined #yosys23:02
*** ZipCPU|ztop is now known as ZipCPU|Laptop23:03
*** mjoldfield has quit IRC23:09
*** mjoldfield has joined #yosys23:10
*** mjoldfield has joined #yosys23:12
*** mjoldfield has quit IRC23:14
*** m_w has quit IRC23:16
*** mjoldfield has joined #yosys23:16
*** mjoldfield has joined #yosys23:18
*** mjoldfield has joined #yosys23:22
*** mjoldfield has quit IRC23:23
*** mjoldfield has joined #yosys23:24
*** dxld has quit IRC23:34
*** mjoldfield has quit IRC23:45
*** mjoldfield has joined #yosys23:47
*** jwhitmore has quit IRC23:58
*** X-Scale has quit IRC23:59

Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!