| *** tpb has joined #yosys | 00:00 | |
| *** BinaryLust has quit IRC | 00:14 | |
| *** BinaryLust has joined #yosys | 00:15 | |
| *** smkz has quit IRC | 00:48 | |
| *** zkms has joined #yosys | 00:49 | |
| *** rlee287 has joined #yosys | 01:24 | |
| *** emeb has left #yosys | 01:39 | |
| *** futarisIRCcloud has quit IRC | 01:45 | |
| Forty-Bot | I having trouble with generate expressions in this code https://gist.github.com/c470f33a232d582e94ef695cfb19c671 | 01:47 |
|---|---|---|
| tpb | Title: add_pipe.v · GitHub (at gist.github.com) | 01:47 |
| Forty-Bot | I get the error ERROR: Left hand side of 1st expression of generate for-loop is not a register! with the first for loop | 01:48 |
| Forty-Bot | if I change the type of i and j to reg, I get the error ERROR: Left hand side of 1st expression of generate for-loop is not a gen var! with the last for loop | 01:48 |
| *** rlee287 has quit IRC | 02:06 | |
| *** citypw has joined #yosys | 02:06 | |
| Forty-Bot | ok turns out that the always block has to go on the inside of the for loops | 02:34 |
| *** Degi has quit IRC | 03:19 | |
| *** Degi has joined #yosys | 03:22 | |
| ZipCPU | Forty-Bot: There's more to it | 03:32 |
| ZipCPU | If you want to use a genvar as a for loop, the always block goes within a generate block | 03:32 |
| Forty-Bot | here's what I ended up doing https://gist.github.com/292dea5094e82ccc3ca604c97a119da8 | 03:32 |
| tpb | Title: add_pipe.v · GitHub (at gist.github.com) | 03:32 |
| ZipCPU | Otherwise, it is legal to have a for loop inside an always block--it's just not a generate construct. In that case, the loop variable needs to be an "integer" | 03:33 |
| ZipCPU | Where's the "endgenerate" statement in your updated code? | 03:34 |
| Forty-Bot | there's no generate/endgenerate | 03:34 |
| Forty-Bot | since it's optional in the standard, and yosys doesn't seem to care | 03:35 |
| ZipCPU | Hmm ... okay, I'll need to go back and check the standard again then | 03:35 |
| ZipCPU | I'd still recommend using `default_nettype none and passing this design through a verilator -Wall pass .... ;) | 03:36 |
| Forty-Bot | the relevant part is section 12.4 in the 5th paragraph | 03:37 |
| Forty-Bot | hm, I'm getting some spurious warning from verilator | 03:40 |
| Forty-Bot | for example, it complains about `+:` in the left hand side of line 16 and 17 | 03:40 |
| ZipCPU | What's the complaint? | 03:41 |
| Forty-Bot | it was expecting a `:` | 03:41 |
| ZipCPU | Okay ... looking at your lines there ... is that type of declaration even legal? | 03:41 |
| Forty-Bot | yes; it's synthesizing to what I expect | 03:42 |
| ZipCPU | Good luck, then, I'm headed offline for the night | 03:42 |
| Forty-Bot | gn | 03:42 |
| *** BinaryLust has quit IRC | 05:10 | |
| *** gmc has quit IRC | 06:16 | |
| *** dys has joined #yosys | 06:39 | |
| *** X-Scale` has joined #yosys | 08:19 | |
| *** X-Scale has quit IRC | 08:20 | |
| *** X-Scale` is now known as X-Scale | 08:20 | |
| *** Asu has joined #yosys | 08:23 | |
| *** BinaryLust has joined #yosys | 09:04 | |
| *** vidbina has joined #yosys | 09:44 | |
| *** BinaryLust has quit IRC | 09:44 | |
| *** smarter has quit IRC | 11:02 | |
| *** smarter has joined #yosys | 11:03 | |
| *** vidbina has quit IRC | 11:39 | |
| *** jakobwenzel has quit IRC | 11:46 | |
| *** jakobwenzel has joined #yosys | 11:47 | |
| *** futarisIRCcloud has joined #yosys | 12:08 | |
| *** jakobwenzel1 has joined #yosys | 13:10 | |
| *** DaKnig has quit IRC | 13:46 | |
| *** DaKnig has joined #yosys | 13:49 | |
| *** dys has quit IRC | 14:10 | |
| *** vidbina has joined #yosys | 14:11 | |
| *** emeb has joined #yosys | 14:11 | |
| *** jakobwenzel1 has quit IRC | 14:11 | |
| *** citypw has quit IRC | 14:23 | |
| *** citypw has joined #yosys | 14:24 | |
| *** citypw has quit IRC | 14:29 | |
| *** citypw has joined #yosys | 14:29 | |
| *** vidbina has quit IRC | 14:40 | |
| *** jfcaron has joined #yosys | 14:40 | |
| *** citypw has quit IRC | 14:45 | |
| *** jfcaron has quit IRC | 14:53 | |
| *** Asuu has joined #yosys | 14:55 | |
| *** Asu has quit IRC | 14:56 | |
| *** somlo has quit IRC | 15:02 | |
| *** somlo has joined #yosys | 15:06 | |
| *** ayazar has joined #yosys | 15:46 | |
| *** somlo has quit IRC | 16:12 | |
| *** jfcaron has joined #yosys | 16:57 | |
| *** somlo has joined #yosys | 17:13 | |
| *** vidbina has joined #yosys | 17:22 | |
| *** rlee287 has joined #yosys | 17:56 | |
| *** vidbina has quit IRC | 18:05 | |
| rlee287 | In verilog_backend.cc, "dump_process" is invoked twice: once on line 1717 (right after the warning about mappings is printed) and once on line 1774. (Line numbers are relative to the latest master commit 2d573a0f) | 18:21 |
| rlee287 | Is this supposed to be duplicated? | 18:21 |
| awygle | are there good resources on like | 18:22 |
| awygle | philosophy of formal verification | 18:22 |
| awygle | when it's not worth it | 18:22 |
| awygle | what it looks like for various types of components | 18:22 |
| awygle | etc | 18:22 |
| awygle | context - i have a UDP de-packetizer component and i'm not sure what amount of formal verification is appropriate/useful | 18:22 |
| ZirconiumX | rlee287: Pay close attention to the calls; the first has find_regs = true, and the second has find_regs = false | 18:24 |
| rlee287 | OK that makes more sense then | 18:25 |
| *** rlee287 has quit IRC | 18:35 | |
| *** BinaryLust has joined #yosys | 18:53 | |
| ZipCPU | awygle: I'd probably use it for a UDP de-packetizer. I'd tread carefully around the checksum though | 19:22 |
| ZipCPU | I'd avoid using formal for anything that depends upon the result of a multiply or anything crypto related | 19:22 |
| ZipCPU | I've certainly been quite successful using formal on network stuffs in the past | 19:23 |
| awygle | What properties would you verify? | 19:23 |
| ZipCPU | First? Counters | 19:23 |
| awygle | I am having a hard time phrasing properties so they don't sound like "works correctly" | 19:23 |
| ZipCPU | Heh ... Yeah, I can understand that | 19:23 |
| ZipCPU | Can you tell me a bit about what this depacketizer is supposed to do? | 19:23 |
| ZipCPU | I can also point you at my own ethernet cores (and proofs) if you would find them interesting. I just don't handle UDP in RTL normally | 19:24 |
| ZipCPU | The trick so far that I've noticed is that the more/better you break down the problem the easier it gets | 19:24 |
| awygle | Basically all it does is accepts a framed data stream, confirms its a valid UDP packet with the correct dport and destination address, and then outputs the payload as a framed stream | 19:26 |
| awygle | Technically it also handles the IPv4 layer because they're inseparable (I'm still mad about the "pseudo-header") | 19:27 |
| ZipCPU | Hmm | 19:27 |
| ZipCPU | I'd strip the IPv4 layer off in one process, then the UDP layer in a second | 19:28 |
| ZipCPU | That sort of approach really made processing easy | 19:28 |
| ZipCPU | (one process == one module and therefore one proof) | 19:28 |
| awygle | I tried to do that but you need significant information from the IPv4 header to calculate the udp checksum | 19:28 |
| ZipCPU | Such as ... the length of the packet? | 19:28 |
| awygle | The layers are not well separated | 19:29 |
| ZipCPU | The port numbers? | 19:29 |
| awygle | Length, source ip, dest ip, and protocol (which is presumably udp) | 19:29 |
| ZipCPU | So, imagine processing a stream--on the first word of the stream, all that data should be available to you and constant. That would all be outputs of the IPv4 handler | 19:30 |
| awygle | You're also substantially increasing the buffering requirements by doing them separately, if you want to fully validate the ip layer before passing to the udp layer | 19:31 |
| awygle | Because of the length | 19:31 |
| ZipCPU | You could send a "cancel" signal to the UDP layer if the validation wasn't complete before the first UDP data sample | 19:31 |
| ZipCPU | That was one of the things I had done | 19:32 |
| ZipCPU | ... cept that was between Ethernet layers and IP layer | 19:32 |
| sorear | all forms of software quality assurance boil down to "say the same thing in two as-different-as-possible ways, and cross-check them" | 19:33 |
| ZipCPU | sorear: That's one of my early slides in explaining formal ;) | 19:34 |
| awygle | lol, true | 19:37 |
| awygle | hm well I'll consider the division a bit more, maybe I'll decide its a good idea | 19:37 |
| awygle | Can you elaborate more on "counters"? | 19:38 |
| * ZipCPU rummages for an example | 19:38 | |
| ZipCPU | This should be a good example of using a counter with network stuffs, https://github.com/ZipCPU/videozip/blob/dev/rtl/ethernet/rxemin.v | 19:39 |
| tpb | Title: videozip/rxemin.v at dev · ZipCPU/videozip · GitHub (at github.com) | 19:40 |
| * ZipCPU looks to see if it really was a good example ... | 19:40 | |
| ZipCPU | It looks okay ... | 19:40 |
| ZipCPU | Here's another way of stating counters: for every request, there should be one response, but that's from a bus context | 19:41 |
| ZipCPU | Counters: Packets of length "N" should have length "N" | 19:41 |
| ZipCPU | Counters --- anything that counts through something. They tend to be easy to verify, but powerful in effect | 19:41 |
| awygle | I see | 19:45 |
| ZipCPU | Often, I can create a state machine and a master counter to describe how the states are to be moved through. I can then tie the state machine to the counter, and assertions to it as well. It makes it easy--if it fits that form. | 19:46 |
| ZipCPU | (SPI fits that form nicely) | 19:46 |
| *** ayazar has quit IRC | 21:10 | |
| *** jfcaron has quit IRC | 21:24 | |
| *** thardin has left #yosys | 21:57 | |
| *** rlee287 has joined #yosys | 22:12 | |
| *** Asuu has quit IRC | 22:29 | |
| *** cr1901_modern has quit IRC | 22:31 | |
| *** BinaryLust has quit IRC | 22:33 | |
| *** rlee287 has quit IRC | 23:04 | |
| *** emeb has quit IRC | 23:40 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!