<jmamish>
Hi everyone! I'm trying to start learning about Formal Verification on my own, and I'm using symbiyosys (Claire and co., y'all are absolute superstars. If I could do 1/10th the work y'all have done, I'd be very proud of myself).
<jmamish>
I've been reading "Formal Verification: an Essential Toolkit" by Seligman, Schubert, and Kumar and also reading ZipCPU's excellent blog posts. I'm having trouble using SVA things like `default clocking ... endclocking`, presumably because the verific frontend is needed.
<jmamish>
I'm wonder if SVA's `default clocking ... endclocking` can be replaced by an `always @($global_clock) assume(clk == !clk_prev)` like what ZipCPU suggests in his "my first experience with Formal Methods" blogpost
<jmamish>
s/wonder/wondering/
<jmamish>
Or even better, if I'm somehow misusing symbiyosys and it can support `default clocking ... endclocking` even without verific.
<ZipCPU>
jamish: Do you need to?
<ZipCPU>
How many clocks are in your design?
<jmamish>
Just one clock, but I think I don't fully understand the utility of `default clocking` or the utility of the always @($global_clock) statement in your blog.
<jmamish>
Sorry to bring these basic questions to this channel, but there's not a lot of good stuff on FV for free on the web. Well, aside from @ZipCPU's blog posts.
<ZipCPU>
So, if you only have one clock, then don't worry about the default clocking statement
<ZipCPU>
... and don't use $global_clock (it's deprecated anyway)
<ZipCPU>
With just one clock.... things are easy
<jmamish>
hahaha thanks. I'm guessing that yosys and the provers know which one is the clock cause it's the only thing in the sensitivity lists?
<ZipCPU>
You also don't need to do anything like assume(clk == !clk_prev)
<ZipCPU>
You only need to do that if you are using multiple clocks
<ZipCPU>
If you aren't using multiple clocks, it'd just double the workload of the formal solver
<ZipCPU>
Yes, if there's only one clock in the sensitivity list, Yosys will know what's going on
<jmamish>
Thanks a ton; this cleared up some major misunderstandings for me.
<ZipCPU>
Glad to help
<jmamish>
I was confused before about how you can communicate to the solver that it doesn't matter if inputs change in-between clock cycles..... but the solver already knows that.
<ZipCPU>
Well, there's two modes
<ZipCPU>
In one mode, everything is synchronous
<ZipCPU>
In the second mode, you have to assume the clock
<jmamish>
What are the terms for the 2 modes?
<ZipCPU>
The second mode allows you to handle asynchronous time steps and such
<ZipCPU>
Have you found my formal lesson slides?
<jmamish>
I have. I'm about 30% of the way through them.
<ZipCPU>
So, towards the end there's a lesson on multiple clocks
<ZipCPU>
That lesson discusses how to go about assuming the existence of more than one clock
<ZipCPU>
That's also the time where I introduce the SymbiYosys option, "multiclock on"
<jmamish>
awesome, I'll keep looking through them.
<ZipCPU>
But there is a caution: Don't use the clock in any logic context before then
<ZipCPU>
The tool ... won't do what you want if you do
<ZipCPU>
So, for example, you'd want to avoid things like: assign OUT = (CLK) ? A : B;
<jmamish>
well, that seems like a pretty bad idea in the first place.
<ZipCPU>
(You should be avoiding those in general anyway, but that's another issue)
<ZipCPU>
Yep!
az0re has joined #yosys
<jmamish>
hahaha I wish someone would have told me that during my bachelor's degree :P
<ZipCPU>
How so?
<ZipCPU>
Oh, don't tell me, you tried that?
<ZipCPU>
Ouch!
<jmamish>
I tried something similar....
<jmamish>
I thought I was being creative.
<ZipCPU>
... and ... it didn't do what you wanted, did it?
<jmamish>
It did... sometimes...
<ZipCPU>
Heh, yeah, "sometimes"
<ZipCPU>
Leaving you in "FPGA Hell" every other time
<jmamish>
hahaha oohhhh yeah.
<ZipCPU>
"My design doesn't work. Why not, teacher?"
<ZipCPU>
Sigh.
<jmamish>
Thankfully It's been 5 or 6 years since then and Ive gotten a bit smarter about things
<ZipCPU>
Ok, I was just about to ask
<ZipCPU>
So, what sort of projects bring you this way?
<jmamish>
I worked as a robotics engineer for 2 years out of undergrad, but went back to get a PhD doing low power embedded systems.
<ZipCPU>
Low power is ... it's own challenge.
<ZipCPU>
Is that what you are working with now? Low power?
<jmamish>
yeah, but for the project I've got here, 'low power' is a little loose.
<jmamish>
I'm working on a jpeg compression core that will hopefully take 10 - 20 mW on an iCE40.
<ZipCPU>
Wow, JPEG compression on an iCE40?
<ZipCPU>
Does it ... fit?
<jmamish>
I don't know yet...
<ZipCPU>
How many multiplies?
<jmamish>
5
<jmamish>
well, it's configurable
<ZipCPU>
How many bits each?
<ZipCPU>
18x18?
<ZipCPU>
16x16?
<jmamish>
no, 16x15
<jmamish>
16x16
<ZipCPU>
Ok ...
<ZipCPU>
Will you be needing DSP's?
<jmamish>
to fit inside the sysdsp blocks
<ZipCPU>
So, you are using the UP5k's then??
<jmamish>
yep.
<ZipCPU>
The room just got smaller
<jmamish>
???
<ZipCPU>
(Fewer LUTs)
<ZipCPU>
Have you found Yosys' capability of estimating logic usage?
<jmamish>
ohhh yeah. but most of what I'm doing is going to be in EBR RAM and DSP blocks.
<jmamish>
I should do that ASAP.
<ZipCPU>
It's easy to use
<ZipCPU>
For most things, you can just run "synth_* ..." and it'll synthesize the design and report usage to you
<ZipCPU>
You can also use that "stat" command to get logic usage
<jmamish>
that's awesome. I'm really glad that it supports the iCE40
<ZipCPU>
Many of my designs have nearby yosys scripts for logic usage measurements
<ZipCPU>
Oh, yeah ;)
<ZipCPU>
I also tend to keep my logic usage notes in the Yosys script
<jmamish>
probably a good idea resynth like that the same way that running unit tests in software land is a good idea.
<ZipCPU>
After everytime I run it, I'll scribble the usage down at the end of the script. Start lines with "#" commentsto create
<ZipCPU>
You've been doing logic design for 5-6 years you said? Or has it been 5-6 years since you've done any, since way back in college?
<jmamish>
I did it in undergrad for about 3 semesters and have done a few side projects since then.
<ZipCPU>
Ok. Next question ...
<ZipCPU>
Have you given any thought to how you'll get your JPEG images on and off the FPGA?
<jmamish>
We have an hm01b0 camera that we're pulling images from.
<jmamish>
and the FPGA is attached to an STM32Fsomething
<ZipCPU>
Ok, so that's well defined ... will you be taking images off via the STM then?
<jmamish>
yep.
<ZipCPU>
Next question, Jpeg 2K?
<jmamish>
haha no,
<jmamish>
I'm not that good at DSP math
<jmamish>
do you think I should grit my teeth for 2 or 3 weeks and figure it out?
<ZipCPU>
That's a shame. I would've loved to connect you w/ someone whose wanted some JPEG2k help, but isn't an FPGA type
<jmamish>
hmmmmm
<ZipCPU>
DSP math? Not sure
<ZipCPU>
Do you have two solid weeks to devote to it?
<ZipCPU>
... and would two weeks be enough?
<jmamish>
I mean, you know how time estimates are always too small when you're relatively green.
<jmamish>
and I might have 2 weeks, but my PhD advisor would probably disagree.
<ZipCPU>
Lol ... yes, I do
<ZipCPU>
Do you have a "working" design to start from, say from the last PhD student, or are you starting from scratch?
<jmamish>
I'm starting from scratch on my jpeg compressor, but I wrote one from scratch in C
<tpb>
Title: A Cheaper Fast FIR Filter (at zipcpu.com)
<Cerpin>
I suppose I do have -a- higher clock in play I could run this off
<Cerpin>
The application is pulse shaping
<ZipCPU>
So ... filtering, right?
<Cerpin>
Yes
<ZipCPU>
Multiclock filtering?
<ZipCPU>
Pulse shaping is often done in connection with an upsampler, no?
<Cerpin>
Well, I don't think it has to be
<Cerpin>
Yes
<Cerpin>
So here's how I was planning to achieve said upsampling
* ZipCPU
sits down to listen
<Cerpin>
Basically, I have the time-domain pulse shaping filter coefficients stored in a memory, truncated +/- some MT_s where T_s is the -symbol- period
<ZipCPU>
That's a good start. Keep going
<Cerpin>
And every L clocks, if L is the upsampling factor, I read a new symbol. I want to have a mod-L counter that loops over the constants
<Cerpin>
And basically each cycle you multiply by the sample at the value of that counter offset by each multiple of T_s within the window you truncated the filter response to
<Cerpin>
So you if you had say, M=3, you'd multiply 7 of these numbers, then sum them all
<ZipCPU>
7 number on one clock cycle?
<ZipCPU>
7 numbers on one clock cycle?
<Cerpin>
In parallel, surely that's not an issue other than the DSP block usage, no?
<ZipCPU>
Not really
<Cerpin>
If even -then- it's one somehow, I can explore another idea
<ZipCPU>
But the algorithm in the article above would work nicely for the task
<ZipCPU>
Rather than an adder tree, you use an adder chain
<ZipCPU>
You schedule the multiplies carefully, though, to make certain everything aligns properly when done
<ZipCPU>
Well ... you would need to modify the algorithm a bit. The one in the article is a straight up FIR, running at the system clock rate, but your adder "chain" would also run at the system clock rate
<Cerpin>
That assumes the sample rate at in/out is the same, no? I guess I could just make the module itself pad zeroes on each symbol
<ZipCPU>
No, no, no ... don't pad zeros. It's too expensive to do
<ZipCPU>
I mean, yes, pad zeros, but then don't build the logic to handle the multiplied by zero stuff--since you already know the result would be zero
<Cerpin>
Yes, I didn't think that was a good idea
<ZipCPU>
I just mean that the idea of the adder chain would work nicely
<ZipCPU>
Sort of like Fig 2
<ZipCPU>
You'd update the incoming value every couple cycles, and rotate the coefficients in the meantime
<ZipCPU>
jmamish: Before you wander off, let me invite you to join the ##dsp channel
<jmamish>
ZipCPU: I wasnt gonna wander anywhere :)
<jmamish>
Thanks!
<ZipCPU>
Heh ... yeah, it's just too often that someone shows up, asks a question, and then vanishes before you can get back to them
<ZipCPU>
It's one of my frustrations with IRC
<Cerpin>
Apologies if I derailed things a bit, I'll have a more detailed look at using the chain modification there later tonight
<jmamish>
I *love* the stuff you write about, so I wouldn't wander off on you
<jmamish>
Cerpin: no worries, IRC is always a little mercurial
<ZipCPU>
Cerpin, yeah, no worries
<ZipCPU>
Cerpin: Do you need to?
<ZipCPU>
Oh, dear, responding to backlog
<ZipCPU>
Let me scroll back to the here and now, sorry 'bout that
* ZipCPU
looks around for his sanity, just to check if it's still around somewhere
<Cerpin>
If that was at the clock thing, yes there is a PWM later that absolutely -requires- higher clock relative to this
<ZipCPU>
Really? Okay, so ... how much faster will the PWM run then?
<Cerpin>
I'm not sure what the minimum I can get away with is yet; I suppose I should check that with the hardware before going much further
<Cerpin>
But it needs to reproduce the passband signal in PWM form (this is fairly low-freq, for a rather niche application)
<jmamish>
Cerpin: Can you tell us what the niche app is?
<Cerpin>
If anything from what I saw with this system before with another person working with the frontend, the limiting factor is going to be how fine my phase control needs to be
<Cerpin>
Underwater acoustic comms
<jmamish>
ahhh that's fun!
<Cerpin>
Carrier frequency should be in the hundreds of kHz
<Cerpin>
I want to put a lot of channels of this on one FPGA
<jmamish>
How many bits / symbol? What sort of coding scheme?
<Cerpin>
Convolutional right now, QPSK right now but I'm designing it to generalize to higher order PSK and support precoding
<Cerpin>
The receiver side uses a turbo equalization scheme, so there's also an interleaver, etc.
<Cerpin>
There's another person doing that bit though
<jmamish>
Super cool. Is this just for fun, or...?
<ZipCPU>
That underwater PWM thing is ... a crazy beast, at least for the hardware I've applied it to
<Cerpin>
jmamish: nope, am grad student
<jmamish>
Cerpin: Cheers! me too.
<ZipCPU>
Let's see ... lots of channels in one FPGA, are we doing beamforming? So, are all the channels coming from one source?
<Cerpin>
Yes, precoding = generalization of beamforming
<Cerpin>
What do you mean one source?
<Cerpin>
datawise?
<Cerpin>
There will be multiple transducers for sure
<ZipCPU>
Datawise, definitely, signal generation wise too ... as in one signal that is then formed into a shaped beam via a series of delays
rrika_ is now known as rrika
<ZipCPU>
When I did that recently, I generated the PWM waveform and then handled all the delays
<ZipCPU>
I think I was building for ... 20 delay elements or so IIRC
<ZipCPU>
Getting all of those delays to fit in the FPGA was quite the challenge
<Cerpin>
I guess this is another good point; if I don't intend to transmit more than one kind of data, this would take care of the need to have a coordinator phase-locking all the PWMs etc.
<ZipCPU>
There are physical rules on those transducers too
<Cerpin>
Indeed
<ZipCPU>
Are you using bipolar ones? Or just unipolar? Does the PWM have outputs of 0,1, or -1,0,1 ?
<Cerpin>
So the frontend really is pretty well tested via microcontroller already
<Cerpin>
50% duty is 0
<Cerpin>
I don't want to get into the hardware details really, but that should give you an idea how to control it
<ZipCPU>
Fair enough
<ZipCPU>
Just one caution: beware of the amount of logic that the beamformer will use
<ZipCPU>
Oh, one other question for you, Cerpin: Will you be publishing a paper on your work and results, and if so ... in what time frame?
<Cerpin>
The plan is to use a linear precoding technique like WF
<Cerpin>
End of summer, hopefully?
<ZipCPU>
Awesome!
<ZipCPU>
I'd like to read it when you publish it
<ZipCPU>
Can you give me a heads up on it when you get there?
<jmamish>
Me too.
<Cerpin>
Alright
<ZipCPU>
And, in the meantime, come back if you have problems or need any help. I'll be around
<Cerpin>
Thank you! Will do my best
<ZipCPU>
Enjoy!
<jmamish>
ZipCPU: I could be enticed to write a jpeg 2k compressor if an open source one doesn't already exist, and if you think that could be a useful thing.
<ZipCPU>
:D
<jmamish>
also, my 8x8 DCT engine takes about 860 logic cells. IDK if it's using the SysDSP or not.
<ZipCPU>
Oh, and ... and how many of those DCT's do you need to run in parallel?
<jmamish>
I was hoping for 4 or 5, but that's not looking so likely anymore.
<jmamish>
It'll work fine with just 1, but it will be less efficient.
<ZipCPU>
See ... I remember going through this work some time back ...
<ZipCPU>
It'd be a shame to have you reinvent the wheel, but I'd need to make an introduction ... Hmm ...
<ZipCPU>
At least, when I did it last, I was doing a wavelet transform and the limit turned out to be memory bandwidth
<jmamish>
I dimly remember avoiding jpeg2k because of something memory related.
<jmamish>
but I could be inventing memories.
<ZipCPU>
Well, that was only the first half of the algorithm. There was another half that needed to be done as well that I hadn't dug into. He had
<ZipCPU>
In that case, it turned out the ZipCPU was just as fast as the raw hardware. Kind of a surprise that way
<ZipCPU>
I would've expected a raw hardware, doing nothing but the wavelet transform, tuned to the purpose, to have been faster. It was, but not by that much
<jmamish>
Working on my own little jpeg thing, I was surprised to find that mine takes much fewer cycles than an ARM doing something similar.
<jmamish>
I've ended up with a microcoded core to do the DSPs that just does fetch, multiply, and accumulate
<jmamish>
but I think I've been able to pipeline mine more smoothly than an ARM cortex m4 would've
<ZipCPU>
The ARM... is that the attached STM that youare referencing?
<jmamish>
originally this project had 2 ARMs on it
<jmamish>
one for compression and one for system control
<jmamish>
we were using the Ambiqmicro near-threshold Apollo3 blue
<jmamish>
But the arm took WAY more cycles than I expected, probably because of wait states and stalls on the SRAM bus... also probably because that MCU lets you operate the core 2x as fast as the SRAM bus.
<ZipCPU>
Was the design bus limited? That's a key question
<jmamish>
No idea. I found the documentation for the Apollo3 blue hard to read.
<jmamish>
so I had a hard time reasoning about what the bus would be doing, and I didn't know how to measure how well its prefetch engine was doing.
<jmamish>
So as far as I can tell, the benefits for me doing it in Verilog are that I can run multiple DCT engines in parallel, and the DCT engines can all have perfect data fetching
<ZipCPU>
Yeah, that's a "key" question. For any design. You'll need/want to know where your bottlenecks are
<jmamish>
Well, as far as I can tell, using an FPGA instead of a microcontroller will totally eliminate that bottleneck.
<ZipCPU>
Not if data memory is the bottleneck
<ZipCPU>
Perhaps if memory is shared between data and instructions--but that would only be true if there were no cache
<jmamish>
The microcontroller was buffering an entire image and then operating on it, and all reads and writes were shared on one bus.
<jmamish>
On the FPGA, I'm doing it line-by-line, and the input buffer and intermediate buffers are all in seperate EBRs, so there's no bus contention
<jmamish>
(when I say line-by-line, I mean lines 8 pixels tall)
<ZipCPU>
So, you are able to operate on an image in sections of 8x8 pixels?
<jmamish>
with ancient jpeg, yes.
<ZipCPU>
The challenge I had been struggling with was trying to operate on images in sections of 256x256 pixels--nothing that would fit in any block RAM
<jmamish>
ohhhhhhh lol
<jmamish>
with ancient jpeg, the fundamental unit is 8x8 'samples', never bigger, never smaller. One sample can be an average of up to 16 pixels
<ZipCPU>
The algorithm wanted to first operate on the image section in horizontal rows. That was easy for the memory. Then it wanted to operate in vertical columns. That ... hurt
<jmamish>
this was jpeg2000?
<ZipCPU>
Yes
<jmamish>
I thought the wavelet transform was on 8x8 pixel blocks....
<jmamish>
I think even with the newest jpeg, 'jpeg XL', the max block size is 32x32
<ZipCPU>
Could be this was just how this user wanted it done
<jmamish>
I should go back and digest the jpeg2k spec a little more carefully, but something about that doesn't sound right to me.
<jmamish>
my problem with reading thick specifications is that after about 10 pages my eyes start to glaze over
<jmamish>
or else I'd do it more often :P
<ZipCPU>
Yeah ... I never got that far
<ZipCPU>
I think I'd want to pick up a USB spec first
<ZipCPU>
Or perhaps a good fiction book, you know, something like the Mueller report or some such :D
<jmamish>
hahahaha I had a much harder time with the USB spec than the jpeg spec.
<ZipCPU>
:D
<jmamish>
When I was a sophomore in undergrad, the place I was working at asked me to implement USB 2.0 device firmware on bare metal
<jmamish>
For a few weeks I thought I was gonna switch back to my music degree
<ZipCPU>
Lol
<jmamish>
But then I found Jan Axelson's books
<ZipCPU>
tinyfpga did implement USB 2.0 on an iCE40
<jmamish>
??????
<jmamish>
no way.
<jmamish>
an iCE40 can go that fast??
<ZipCPU>
Yeah, I was a bit surprised myself
<ZipCPU>
As I recall, it only went up to a bit rate of 12Mbps
<jmamish>
ohhhhhhh
<ZipCPU>
So, perhaps not the entire protocol ...
<ZipCPU>
But that 12Mbps rate required some fancy physical footwork, and a 48MHz clock
<jmamish>
I was thinking the 480Mbps one, with the 12 --> 480 handshaking and the current-based signalling.
<ZipCPU>
Yeah, not sure it'd go that fast
<ZipCPU>
That said, I've been surprised at a lot of things so far
<jmamish>
I'd be awfully pleased with myself if I got full-speed usb on an FPGA
<jmamish>
I haven't seen much, so I'm still surprised by a lot of things
<jmamish>
but yosys absolutely blew me away once I figured how much work it took
<ZipCPU>
How much work it took to ... build and run Yosys?
<jmamish>
to write yosys
<jmamish>
lol
<ZipCPU>
Ahh, yes, and the task remains far from finished
<jmamish>
I've looked through some of the github issues, and I don't see many good places to dip my toe in
<jmamish>
Is there another list of issues?
<ZipCPU>
That's really a question for others on the team. I'm more of a formal methods guy myself.
<jmamish>
Well, I feel like I'd be fooling myself if I thought I had the time or discipline right now to contribute to such a big project.
<jmamish>
ZipCPU: Thanks a ton for the brief chat about formal methods and for the more extensive chat about other stuff.
<ZipCPU>
Glad I could help
<jmamish>
You cleared up some fundamental misunderstandings I had about this stuff.
<ZipCPU>
PM me some time if you want to know more about my contact w/ JPEG stuffs
<jmamish>
Sounds good!
<jmamish>
And now that I know how friendly people on this IRC are I'll stop by more often.
<ZipCPU>
You might want to find a way to stay logged in
<ZipCPU>
IRC stays open 24/7, and not everybody operates on the same time zones
<jmamish>
I appreciate the suggestion.
<jmamish>
It's been a long time since I've used IRC, so I don't really know the ins and outs of how to use it effectively
<Cerpin>
There are bouncers you can use for that purpose if maintaining the connection yourself is burdensome
<Cerpin>
My desktop is always on though, so I just stick irssi in a tmux session and leave it
<jmamish>
I've only got a laptop, so that doesn't work well for me
<ZipCPU>
Yes, mine is always on as well
<ZipCPU>
There's also channel logs that can be useful--see the title bar
<jmamish>
well, I don't want to pollute this IRC talking about IRC bouncers. I can just google it
<jmamish>
It seems like the channel logs don't capture everything?
<jmamish>
I see lots of conversations on the channel logs that look half-finished.
<ZipCPU>
Sometimes folks leave before they get answers
<ZipCPU>
Not everyone is online 24/7
<ZipCPU>
I will also often stay silent if not directly addressed, or if I don't know anything about the issue being discussed
<jmamish>
Ah, so you responded because I mentioned your nick when talking about your blog posts?
<ZipCPU>
Exactly
<ZipCPU>
I like to use HexChat. If anyone mentions my nick, it notifies me, so I then take a look if I'm not otherwise watching the channel
<jmamish>
ZipCPU: until I figure out how to get a bouncer set up although I don't have a desktop, I can just look at the logs for this channel.
<ZipCPU>
;)
<jmamish>
It's evening where I am, so have a good evening everyone.
jmamish has quit [Quit: leaving]
Degi has quit [Ping timeout: 246 seconds]
Degi has joined #yosys
SpaceCoaster has joined #yosys
adjtm has quit [Remote host closed the connection]
<awygle>
Anybody check the new text yet? I cannot conveniently log into my lattice account atm
<whitequark>
i checked the text, (3) is just gone
<az0re>
Before anyone flies in on a fighter jet to celebrate in front of a "mission accomplished" banner, how can anyone have confidence this won't happen again? The process here is totally opaque, and it's not clear just how committed to open source they really are.
<az0re>
How did that clause get there in the first place?
Cerpin has joined #yosys
proteusguy has quit [Read error: Connection reset by peer]
<whitequark>
so, lattice has historically been friendly to OSS efforts, in the sense that they have never (before yesterday's incident) actively opposed it, have been in the loop, and donated small amounts of hardware towards that end
<whitequark>
based on that and the indication that it hasn't changed, my understanding is that we see an example of corporate dysfunction rather than an u-turn
<whitequark>
which means that it could as well happen again and we should probably be ready for it
Cerpin has quit [Ping timeout: 260 seconds]
<thardin>
cool, good on themfor fixing it
Cerpin has joined #yosys
_whitelogger has joined #yosys
<thardin>
az0re: there's never a way to be sure when you're dealing with a company beholden to shareholders
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 246 seconds]
Cerpin has quit [Quit: leaving]
Cerpin has joined #yosys
Cerpin has quit [Client Quit]
Cerpin has joined #yosys
proteusguy has joined #yosys
emeb_mac has quit [Quit: Leaving.]
hitomi2500 has joined #yosys
<Lofty>
Isn't this the first public support for FOSSi from Lattice, though?
<Lofty>
My understanding is before we've had just private "we don't mind" type statements from people.
cyrozap has quit [Ping timeout: 246 seconds]
<daveshah>
Yes, as far as I know it is
<daveshah>
Their European sales office invited us to give a talk at a workshop in Italy (and paid for hotel iirc) but I don't know if Lattice HQ endorsed that
<Lofty>
So, even though it sucks that clause was there, we have a small silver lining, I suppose?
<daveshah>
Oh, I don't mean as a response, that was two years ago
<daveshah>
In terms of 'previous support for open source'
<Lofty>
Mm
<daveshah>
But yeah, given how quickly they turned around maybe it was just a legal team error rather than anything more problematic
<Lofty>
And I suppose this means we the community have a surprisingly loud voice
<Lofty>
Collective action: it works
<daveshah>
I mean Lattice's poor twitter team must have been a bit inundated if they read their mentions
<Lofty>
I thought asking a company to read their Twitter feed was a bit too much to ask
<Lofty>
Apparently not
kraiskil has joined #yosys
cyrozap has joined #yosys
<thardin>
the squeaky wheel gets the grease
kraiskil has quit [Ping timeout: 256 seconds]
kraiskil has joined #yosys
Asu has joined #yosys
dys has joined #yosys
kraiskil has quit [Ping timeout: 260 seconds]
kraiskil has joined #yosys
hitomi2500 has quit [Quit: Nettalk6 - www.ntalk.de]
kraiskil has quit [Ping timeout: 246 seconds]
craigo has quit [Ping timeout: 260 seconds]
carlomaragno has joined #yosys
kgugala_ has joined #yosys
kgugala has quit [Ping timeout: 246 seconds]
<Lofty>
daveshah: does anything actually consume BLIF from synth_ecp5?
<daveshah>
Nope
<daveshah>
If someone hypothetically did a vpr flow then it would be needed
<Lofty>
Hmm.
<Lofty>
BLIF on iCE40 was for arachne-pnr, right?
<daveshah>
Yes
<whitequark>
does arachne even still work?
<whitequark>
weren't there some primitive changes, like LUT order or something?
kgugala_ has quit [Read error: Connection reset by peer]
<Lofty>
Likewise, what actually uses EDIF on iCE40/ECP5? Lattice's toolchain?
kgugala has joined #yosys
<daveshah>
No idea about arachne, but the lack of constraints make me think it still works
<daveshah>
I don't think the LUT order change affects the final netlist
<daveshah>
The ice40 tools could take EDIF in theory but it crashed on Yosys' output, idk about ECP5
* whitequark
shudders at EDIF
<whitequark>
the ATF15xx tools are extremely picky about EDIF in a bad way
<daveshah>
Almost everything is tbh
<mwk>
as far as I'm aware, yosys write_edif is really "write EDIF that ISE/Vivado can read" and isn't actively used with anything else
<whitequark>
then let's drop it on non-xilinx?
<mwk>
you mean the `-edif` option?
<whitequark>
yeah
<mwk>
yeah, I mean, if it really doesn't work and/or has better alternatives
<mwk>
I have no idea what's the state of a lot of targets in yosys tbh
<whitequark>
should we have like... a doc section about them?
<mwk>
for all targets but xilinx and sf2 (whatever that is), the `-edif` option is no different from `yosys -o <file>.edif`
<mwk>
while xilinx and sf2 pass some extra options
<whitequark>
oh yeah what's the point in synth_ice40 -json anyway
<mwk>
that's a bit annoying btw, and perhaps worth rethinking
<mwk>
like
<mwk>
-json option is definitely redundant for every target, since we don't ever want to have target-specific options here
<mwk>
at the same time, this is not true for -edif, with all its variants
<mwk>
maybe it would be good to kill all -edif options in favor of having the target implicitely set the proper EDIF options via some side channel, so that `-o file.edif` works right?
<Lofty>
Scratchpad? Scratchpad.
<FL4SHK>
whitequark: is it crazy if my custom HDL's compiler has a handwritten parser?
<Lofty>
Like, synth_intel_alm behaves differently between default mode and -vqm.
<mwk>
I mean, it's magicky
<Lofty>
FL4SHK: why would it?
<Lofty>
*why would it be
<mwk>
and I don't particularly like it
<whitequark>
FL4SHK: not really? i write a lot of parsers by hand, fsvo "by hand"
<mwk>
but then, I'm also annoyed by having both `-o x.json` and `synth_whatever -json x.json`
<Lofty>
Honestly, I *could* make -quartus the default, but I like synthesis printing the more detailed stats about what it's doing
<Lofty>
Which is information that kinda gets lost if you use the vendor primitives directly.
SpaceCoaster has quit [Ping timeout: 246 seconds]
emeb_mac has joined #yosys
<FL4SHK>
I see
<FL4SHK>
I've been writing this parser with a framework I've developed myself
<FL4SHK>
also working, as a side project, on SNES Binutils
kgugala has quit [Read error: Connection reset by peer]
kgugala has joined #yosys
<whitequark>
nice
<whitequark>
nit: I don't like the use of "bloat" very much as people have a strong negative connotation to it
<whitequark>
but if you're using -nocarry you probably know what you are doing
<whitequark>
also, the increase in size from -nocarry is a lot smaller than from -nobram
<FL4SHK>
I heard that yosys struggles with inferring block RAM
<FL4SHK>
I also heard that Lattice is out
develonepi3 has joined #yosys
<Lofty>
The latter is out of date
<whitequark>
yeah, they fully backtracked
<Lofty>
They retracted the clause that forbids bitstream RE
<FL4SHK>
Oh neat
<FL4SHK>
so yosys does indeed struggle with inferring block RAM?
<whitequark>
regarding yosys and BRAM, I wouldn't say it struggles exactly
<FL4SHK>
I see
<Lofty>
As for the former; kinda - Yosys struggles with inferring true dual port RAMs, and with multiple write ports
<whitequark>
IME all toolchains have some difficulty with inferring RAM in Verilog
<whitequark>
(because the entire idea is flawed)
<FL4SHK>
The idea is flawed?
<whitequark>
yeah
<FL4SHK>
I've done it in SV a number of times.
<whitequark>
you write a behavioral definition of a RAM instead of a structural, and expect the tools to follow an undocumented heurstic algorithm to guess what you mean
<Lofty>
You have to describe how a RAM is made, and the tool has to guess what you're actually looking for
<whitequark>
this is stupid. you should just request a specific kind of RAM
<FL4SHK>
makes your code non-portable
<whitequark>
(well, sometimes undocumented, sometimes it is)
<whitequark>
it only does because Verilog doesn't offer a standard way to do it
<FL4SHK>
That is fair
<Lofty>
Or VHDL
<FL4SHK>
VHDL seems to, kind of
<FL4SHK>
shared stuff
<whitequark>
there's no reason it couldn't other than Verilog being unsuitable for synthesis of synchronous logic
<whitequark>
or "not well suited" would be a less inflammatory way to put it
<FL4SHK>
I haven't really had it fail on me?
<FL4SHK>
I do like that VHDL doesn't have undefined semantics
<whitequark>
Xilinx has a few serious footguns
<FL4SHK>
I honestly might switch to defining my HDL in terms of VHDL
<FL4SHK>
Or at least I'd do so if I could do formal verification in VHDL...
<whitequark>
the worst one is when you describe a RAM with an async output but it infers a transparent synchronous output
<develonepi3>
jmamish: Are you on this board, now? ZipCPU said you were interest in jpeg.
<whitequark>
because it finds a register somewhere else in the design
<whitequark>
and the pattern it looks for happens to match, even though it is not your intent
<whitequark>
what do you mean by VHDL not having undefined semantics?
<FL4SHK>
well, maybe I remembered wrongly
<whitequark>
are you perhaps referring to simulation determinism?
<FL4SHK>
yes
<whitequark>
VHDL's simulator is awesome and IMO the single best thing that came out of Verilog and VHDL together
<whitequark>
but... it doesn't help synthesis much
<whitequark>
consider that most toolchains don't differentiate VHDL and Verilog past the frontend
<FL4SHK>
That is true
<FL4SHK>
I honestly really want to have my own HDL done
<FL4SHK>
I want to use that language.
<FL4SHK>
It's difficult
<FL4SHK>
I shrunk the language, even
<Lofty>
FIRRTL :P
<FL4SHK>
I still have to do all the lowering
<Lofty>
You can tell something is a good idea when none of the proprietary tools support it
<whitequark>
like what?
<Lofty>
Portable memory instantiation for example :P
<Lofty>
Also, I fixed your nit, wq
<Lofty>
And also posted about it on Twitter
<Lofty>
*about my cookbook on Twitter
<whitequark>
oh, yeah
GenTooMan has quit [Quit: Leaving]
dys has quit [Ping timeout: 246 seconds]
GenTooMan has joined #yosys
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 260 seconds]
strongsaxophone has joined #yosys
kraiskil has joined #yosys
mirage335 has quit [Ping timeout: 246 seconds]
mirage335 has joined #yosys
dys has joined #yosys
strongsaxophone has quit [Quit: Lost terminal]
FFY00 has quit [Remote host closed the connection]