| *** tpb has joined #yosys | 00:00 | |
| *** emeb_mac has joined #yosys | 00:25 | |
| *** m_w has quit IRC | 00:48 | |
| *** dxld has quit IRC | 00:55 | |
| *** dxld has joined #yosys | 00:57 | |
| *** knielsen has quit IRC | 01:07 | |
| *** promach_ has joined #yosys | 01:09 | |
| *** seldridge has joined #yosys | 01:26 | |
| *** promach_ has quit IRC | 01:40 | |
| *** digshadow has quit IRC | 02:16 | |
| *** knielsen has joined #yosys | 02:53 | |
| *** seldridge has quit IRC | 03:30 | |
| *** digshadow has joined #yosys | 03:38 | |
| *** AlexDaniel has quit IRC | 03:43 | |
| *** danieljabailey has quit IRC | 03:59 | |
| *** danieljabailey has joined #yosys | 04:02 | |
| *** cr1901_modern has quit IRC | 04:33 | |
| *** cr1901_modern has joined #yosys | 04:33 | |
| *** xerpi has joined #yosys | 05:51 | |
| *** xerpi has joined #yosys | 05:52 | |
| *** cr1901_modern has left #yosys | 05:58 | |
| *** mazzoo_ has joined #yosys | 06:20 | |
| *** mazzoo has quit IRC | 06:20 | |
| *** mazzoo_ has quit IRC | 06:23 | |
| *** cr1901_modern has joined #yosys | 06:24 | |
| *** mazzoo has joined #yosys | 06:25 | |
| *** promach_ has joined #yosys | 06:27 | |
| *** promach has quit IRC | 06:29 | |
| *** emeb_mac has quit IRC | 06:42 | |
| *** leviathan has joined #yosys | 07:21 | |
| *** kraiskil has joined #yosys | 07:40 | |
| *** pie_ has joined #yosys | 07:46 | |
| *** jwhitmore has joined #yosys | 08:20 | |
| *** jwhitmore has quit IRC | 08:59 | |
| *** kraiskil_ has joined #yosys | 09:06 | |
| *** kraiskil has quit IRC | 09:09 | |
| *** kraiskil_ is now known as kraiskil | 09:18 | |
| *** jwhitmore has joined #yosys | 09:27 | |
| *** jwhitmore has quit IRC | 09:49 | |
| *** pie_ has quit IRC | 10:05 | |
| *** pie_ has joined #yosys | 10:06 | |
| *** proteus-guy has joined #yosys | 11:25 | |
| *** develonepi3 has joined #yosys | 11:30 | |
| *** xerpi has quit IRC | 11:47 | |
| *** fsasm has joined #yosys | 11:58 | |
| *** pie_ has quit IRC | 12:25 | |
| *** seldridge has joined #yosys | 13:02 | |
| *** pie_ has joined #yosys | 13:24 | |
| *** pie_ has quit IRC | 13:34 | |
| *** AlexDaniel has joined #yosys | 13:40 | |
| *** seldridge has quit IRC | 14:17 | |
| *** pie_ has joined #yosys | 14:22 | |
| *** seldridge has joined #yosys | 14:35 | |
| *** promach has joined #yosys | 14:54 | |
| *** emeb has joined #yosys | 15:02 | |
| *** develonepi3 has quit IRC | 15:05 | |
| *** pie_ has quit IRC | 16:01 | |
| *** luismarques has joined #yosys | 16:07 | |
| *** fsasm has quit IRC | 16:11 | |
| 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 | 16:12 |
|---|---|---|
| *** m_w has joined #yosys | 16:12 | |
| awygle | i could not get async resets working, actually | 16:12 |
| *** pie_ has joined #yosys | 16:13 | |
| ZipCPU | Is the question about async resets or synchronous resets? Both work. | 16:13 |
| awygle | if you share an example of what you're trying to do, i can take a look | 16:13 |
| luismarques | Well, consider for instance the example in this PDF: http://www.clifford.at/papers/2016/yosys-smtbmc/slides.pdf | 16:14 |
| 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 | 16:15 |
| *** seldridge has quit IRC | 16:15 | |
| ZipCPU | Are you using symbiyosys or yosys/yosys-smtbmc with clk2fflogic? | 16:15 |
| ZipCPU | .... and which slide of the pdf are you referencing? | 16:16 |
| luismarques | I’m using yosys-smtbmc, but I don’t know anything about clk2fflogic | 16:16 |
| 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. | 16:17 |
| awygle | it must be the "hello test-bench" slide, 12 or 13 | 16:17 |
| ZipCPU | (You may not see it toggle in your trace ...) | 16:17 |
| luismarques | page 13 of the slide | 16:17 |
| awygle | i hate this example by the way | 16:17 |
| 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. | 16:18 |
| ZipCPU | initial assume(i_reset); isn't a bad assumption | 16:18 |
| 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 | 16:19 |
| ZipCPU | Don't look for clock toggles in the VCD file ... you may not see them. | 16:19 |
| ZipCPU | Things will change on the clock, even if the clock doesn't appear to toggle. | 16:20 |
| *** emeb has quit IRC | 16:20 | |
| 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 | 16:21 |
| ZipCPU | Are you using the example, or your own design? If your own design, can you share it at all? | 16:22 |
| luismarques | My own design. I’ll share a smaller design | 16:22 |
| *** emeb has joined #yosys | 16:33 | |
| *** seldridge has joined #yosys | 16:38 | |
| 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… | 16:43 |
| *** digshadow has quit IRC | 16:46 | |
| ZipCPU | That shouldn't be the problem. | 16:48 |
| ZipCPU | You should be able to make assertions on wires, regs, inputs and outputs with no difference between the two | 16:49 |
| 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? | 16:50 |
| 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. | 16:52 |
| awygle | I could see that happening if you ran synthesis before formal in your flow. | 16:54 |
| daveshah | assertions should still mean a wire is loaded and therefore kept though | 16:54 |
| awygle | Which would probably be incorrect but would be easy to do without thinking | 16:54 |
| awygle | Mm, good point. Not sure how that works. | 16:55 |
| daveshah | Yosys creates an internal cell for assertions - with a single input - during elaboration and should be kept through synthesis | 16:55 |
| awygle | If not that then I bet it's default_nettype again | 16:56 |
| luismarques | well, I was doing read_verilog -formal tb.v; prep -top tb; memory -nordff; write_smt2 -wires tb.smt2 | 16:58 |
| daveshah | that looks like a perfectly good flow | 16:59 |
| 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? | 17:15 |
| awygle | i usually define an "f_reset_in_past" signal for this purpose | 17:16 |
| *** ZipCPU|ztop has quit IRC | 17:26 | |
| *** ZipCPU|ztop has joined #yosys | 17:26 | |
| luismarques | What’s the first numeric column in the output of yosys-smtbmc? | 17:37 |
| *** kraiskil has quit IRC | 17:50 | |
| 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)... | 18:18 |
| *** promach has quit IRC | 18:20 | |
| luismarques | OK, I removed all the other asserts, just to be sure it wasn’t a wrong line output; same result | 18:27 |
| mjoldfield | Are 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 LSB | 18:35 |
| ZipCPU | luismarques: Was the assert on a positive edge of a clock? | 18:38 |
| luismarques | ZipCPU: you mean the assert condition or the triggered assert? | 18:40 |
| luismarques | It wasn’t written to be checked at the clock edge, but it triggered on a positive edge of the clock, yes | 18:40 |
| ZipCPU | Is the assert an always @(posedge i_clk) assert (A == B); or an always @(*) assert(A == B); | 18:40 |
| luismarques | @* | 18:40 |
| ZipCPU | Ok, @* will show in the final clock of the VCD file, @(posedge clk) one column before that. | 18:41 |
| luismarques | yeah, the problem was the bit width, as mjoldfield guessed | 18:41 |
| ZipCPU | Got it. | 18:41 |
| luismarques | Thanks guys | 18:41 |
| ZipCPU | ;) | 18:41 |
| *** jwhitmore has joined #yosys | 18:44 | |
| *** mjoldfie_ has joined #yosys | 18:59 | |
| *** mjoldfield has quit IRC | 19:02 | |
| *** jwhitmore has quit IRC | 19:03 | |
| *** jwhitmore has joined #yosys | 19:07 | |
| *** m_w_ has joined #yosys | 19:12 | |
| *** m_w has quit IRC | 19:14 | |
| *** dys has joined #yosys | 19:23 | |
| *** leviathan has quit IRC | 19:29 | |
| *** m_w_ has quit IRC | 19:42 | |
| *** seldridge has quit IRC | 20:08 | |
| *** m_w has joined #yosys | 20:22 | |
| *** seldridge has joined #yosys | 20:29 | |
| *** jwhitmore has quit IRC | 21:02 | |
| *** pie_ has quit IRC | 21:05 | |
| luismarques | What’s the first numeric column in the output of yosys-smtbmc? | 21:27 |
| *** seldridge has quit IRC | 21:28 | |
| *** pie_ has joined #yosys | 21:42 | |
| *** seldridge has joined #yosys | 21:49 | |
| *** seldridge has quit IRC | 22:08 | |
| *** mjoldfield has joined #yosys | 22:11 | |
| *** mjoldfie_ has quit IRC | 22:15 | |
| * ZipCPU needs to remind himself what that column looks like ... | 22:21 | |
| ZipCPU | You mean the time column? | 22:21 |
| ZipCPU | showing the time since yosys-smtbmc was started? | 22:22 |
| *** dys has quit IRC | 22: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 |
| awygle | 2909 seconds. 2909/60 = 48 remainder 29 | 22:34 |
| *** mjoldfield has quit IRC | 22:35 | |
| *** mjoldfield has joined #yosys | 22:36 | |
| luismarques | Ah. I thought it would be something fancy like some number of SAT terms or whatever ;) | 22:37 |
| *** jwhitmore has joined #yosys | 23:02 | |
| *** ZipCPU|ztop is now known as ZipCPU|Laptop | 23:03 | |
| *** mjoldfield has quit IRC | 23:09 | |
| *** mjoldfield has joined #yosys | 23:10 | |
| *** mjoldfield has joined #yosys | 23:12 | |
| *** mjoldfield has quit IRC | 23:14 | |
| *** m_w has quit IRC | 23:16 | |
| *** mjoldfield has joined #yosys | 23:16 | |
| *** mjoldfield has joined #yosys | 23:18 | |
| *** mjoldfield has joined #yosys | 23:22 | |
| *** mjoldfield has quit IRC | 23:23 | |
| *** mjoldfield has joined #yosys | 23:24 | |
| *** dxld has quit IRC | 23:34 | |
| *** mjoldfield has quit IRC | 23:45 | |
| *** mjoldfield has joined #yosys | 23:47 | |
| *** jwhitmore has quit IRC | 23:58 | |
| *** X-Scale has quit IRC | 23:59 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!