<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
<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
rlee287 has quit [Quit: Konversation terminated!]
citypw has joined #yosys
<Forty-Bot>
ok turns out that the always block has to go on the inside of the for loops
Degi has quit [Ping timeout: 265 seconds]
Degi has joined #yosys
<ZipCPU>
Forty-Bot: There's more to it
<ZipCPU>
If you want to use a genvar as a for loop, the always block goes within a generate block
<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"
<ZipCPU>
Where's the "endgenerate" statement in your updated code?
<Forty-Bot>
there's no generate/endgenerate
<Forty-Bot>
since it's optional in the standard, and yosys doesn't seem to care
<ZipCPU>
Hmm ... okay, I'll need to go back and check the standard again then
<ZipCPU>
I'd still recommend using `default_nettype none and passing this design through a verilator -Wall pass .... ;)
<Forty-Bot>
the relevant part is section 12.4 in the 5th paragraph
<Forty-Bot>
hm, I'm getting some spurious warning from verilator
<Forty-Bot>
for example, it complains about `+:` in the left hand side of line 16 and 17
<ZipCPU>
What's the complaint?
<Forty-Bot>
it was expecting a `:`
<ZipCPU>
Okay ... looking at your lines there ... is that type of declaration even legal?
<Forty-Bot>
yes; it's synthesizing to what I expect
<ZipCPU>
Good luck, then, I'm headed offline for the night
<Forty-Bot>
gn
BinaryLust has quit [Ping timeout: 272 seconds]
gmc has quit [Remote host closed the connection]
dys has joined #yosys
X-Scale` has joined #yosys
X-Scale has quit [Ping timeout: 260 seconds]
X-Scale` is now known as X-Scale
Asu has joined #yosys
BinaryLust has joined #yosys
vidbina has joined #yosys
BinaryLust has quit [Ping timeout: 256 seconds]
smarter has quit [Quit: No Ping reply in 180 seconds.]
smarter has joined #yosys
vidbina has quit [Ping timeout: 272 seconds]
jakobwenzel has quit [Quit: jakobwenzel]
jakobwenzel has joined #yosys
futarisIRCcloud has joined #yosys
jakobwenzel1 has joined #yosys
DaKnig has quit [Ping timeout: 246 seconds]
DaKnig has joined #yosys
dys has quit [Ping timeout: 240 seconds]
vidbina has joined #yosys
emeb has joined #yosys
jakobwenzel1 has quit [Ping timeout: 265 seconds]
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
vidbina has quit [Ping timeout: 258 seconds]
jfcaron has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
jfcaron has quit [Ping timeout: 265 seconds]
Asuu has joined #yosys
Asu has quit [Ping timeout: 272 seconds]
somlo has quit [Quit: Leaving]
somlo has joined #yosys
ayazar has joined #yosys
somlo has quit [Quit: Leaving]
jfcaron has joined #yosys
somlo has joined #yosys
vidbina has joined #yosys
rlee287 has joined #yosys
vidbina has quit [Ping timeout: 264 seconds]
<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)
<rlee287>
Is this supposed to be duplicated?
<awygle>
are there good resources on like
<awygle>
philosophy of formal verification
<awygle>
when it's not worth it
<awygle>
what it looks like for various types of components
<awygle>
etc
<awygle>
context - i have a UDP de-packetizer component and i'm not sure what amount of formal verification is appropriate/useful
<ZirconiumX>
rlee287: Pay close attention to the calls; the first has find_regs = true, and the second has find_regs = false
<rlee287>
OK that makes more sense then
rlee287 has quit [Quit: Konversation terminated!]
BinaryLust has joined #yosys
<ZipCPU>
awygle: I'd probably use it for a UDP de-packetizer. I'd tread carefully around the checksum though
<ZipCPU>
I'd avoid using formal for anything that depends upon the result of a multiply or anything crypto related
<ZipCPU>
I've certainly been quite successful using formal on network stuffs in the past
<awygle>
What properties would you verify?
<ZipCPU>
First? Counters
<awygle>
I am having a hard time phrasing properties so they don't sound like "works correctly"
<ZipCPU>
Heh ... Yeah, I can understand that
<ZipCPU>
Can you tell me a bit about what this depacketizer is supposed to do?
<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
<ZipCPU>
The trick so far that I've noticed is that the more/better you break down the problem the easier it gets
<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
<awygle>
Technically it also handles the IPv4 layer because they're inseparable (I'm still mad about the "pseudo-header")
<ZipCPU>
Hmm
<ZipCPU>
I'd strip the IPv4 layer off in one process, then the UDP layer in a second
<ZipCPU>
That sort of approach really made processing easy
<ZipCPU>
(one process == one module and therefore one proof)
<awygle>
I tried to do that but you need significant information from the IPv4 header to calculate the udp checksum
<ZipCPU>
Such as ... the length of the packet?
<awygle>
The layers are not well separated
<ZipCPU>
The port numbers?
<awygle>
Length, source ip, dest ip, and protocol (which is presumably udp)
<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
<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
<awygle>
Because of the length
<ZipCPU>
You could send a "cancel" signal to the UDP layer if the validation wasn't complete before the first UDP data sample
<ZipCPU>
That was one of the things I had done
<ZipCPU>
... cept that was between Ethernet layers and IP layer
<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"
<ZipCPU>
sorear: That's one of my early slides in explaining formal ;)
<awygle>
lol, true
<awygle>
hm well I'll consider the division a bit more, maybe I'll decide its a good idea
<tpb>
Title: videozip/rxemin.v at dev · ZipCPU/videozip · GitHub (at github.com)
* ZipCPU
looks to see if it really was a good example ...
<ZipCPU>
It looks okay ...
<ZipCPU>
Here's another way of stating counters: for every request, there should be one response, but that's from a bus context
<ZipCPU>
Counters: Packets of length "N" should have length "N"
<ZipCPU>
Counters --- anything that counts through something. They tend to be easy to verify, but powerful in effect
<awygle>
I see
<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.