Aleksandar-K has quit [Remote host closed the connection]
<ZipCPU>
One of my goals was to get to simulation immediately
<ZipCPU>
Another, was to separate synthesizable Verilog from simulation constructs
<ZipCPU>
I'm not planning on introducing simulation only Verilog constructs for example.
<shapr>
my first step in my class was to setup tools and load a bitstream
<shapr>
I'm still not sure if I like the simulation only parts or not
<ZipCPU>
So, the last recommendation I had on the register section was to start with a blinky that was way too slow, and then to show how it could be increased using simulation
Aleksandar-K has joined #yosys
<ZipCPU>
... up to the point where you could see it actually blink
<qu1j0t3>
shapr: Not only re tutorial, but pedagogically good books are hard to find as well
<ZipCPU>
qui1j0t3: o/
<ZipCPU>
I'm also stuck in a bit of a conundrum: Make the tutorial hardware specific, or hardware agnostic?
<ZipCPU>
... or perhaps make extra/bonus hardware specific sections
leviathan has quit [Read error: Connection reset by peer]
emeb has joined #yosys
<qu1j0t3>
ZipCPU: o/
<ZipCPU>
Let's see ... other feedback ... the "this is a module" slide didn't discuss the portlist ...
<ZipCPU>
shapr: So you like the approach then?
<ZipCPU>
So the basic idea of the course is to teach what folknology calls "Verilog --"
<ZipCPU>
That is, rather than teaching the full spec, focus on only those parts of the spec that are synthesizable with most tools
leviathan has joined #yosys
<ZipCPU>
For example, I'm going to avoid the : A <= #10 B; assignments
<ZipCPU>
I'll probably avoid teaching loops for quite some time as well
<ZipCPU>
I don't plan to teach 1'bx values, and that inouts are only toplevel ports
<ZipCPU>
MPY's and block RAM's *MUST* fit specific formats to be used
<ZipCPU>
Etc.
<ZipCPU>
Oh, I'm also planning on skipping $display, $monitor, and the $final commands too
GuzTech has quit [Quit: Leaving]
<shapr>
ZipCPU: I do like the approach of starting with something that works and needs changes, and then showing how to change that thing
<ZipCPU>
Thank you
<ZipCPU>
I enjoy your encouragement!
<shapr>
I also like the idea of deciding on specific hardware
<ZipCPU>
That's what I think I'll do for blinky
<shapr>
for me, I spent months on #yosys and #openfpga trying to figure out where to start
<ZipCPU>
Really? Specific hardware?
<shapr>
from the total newbie viewpoint, I want a cake recipe
<ZipCPU>
Usually the vendor provides such a design for you
<shapr>
1. buy an icestick 2. git clone the repos 3. install the repos in this order
<shapr>
4. test the loading tools with this binary blinky
<shapr>
5. test the compilers with the source for this binary blinky
<shapr>
6. notice how the blinky needs improvement, here we go!
<ZipCPU>
shapr: Is that what you expect of a tutorial, or the vendor's first design? That looks like what I'd expect of the Vendors first design
<shapr>
what does that mean?
<shapr>
I haven't heard of a "vendors first design"
<ZipCPU>
I would expect the Vendor to provide an initial blinky and source for it
<shapr>
that is a strange thing to me
<ZipCPU>
Probably even more than just blinky, something that proves that everything on the board works in the first place
<ZipCPU>
They need to, otherwise support is a real problem
<ZipCPU>
Customer: My board doesn't work
<shapr>
from my software dev viewpoint, I expect to get tools and demo code in a tutorial
<ZipCPU>
Support desk: Did you try our design on it?
<shapr>
I think that's because hardware has clear expectations and behavior in my world
<ZipCPU>
Customer: No, I didn't. Support: Try our demo design. Customer: It works. Support: It's your fault then.
<shapr>
yeah, I see what you're saying
<shapr>
haha
<shapr>
I don't know how to put that into a tutorial
<shapr>
I also don't know how to write tutorials for an audience that isn't software devs
<ZipCPU>
Right now, I think a tutorial for software dev's would be a good thing
<shapr>
I decided on the BeagleWire because the entire stack is specified
<shapr>
that is, the FPGA is directly attached to a Linux system that can run the tools
<shapr>
so I don't have to think about how to install yosys on mac/linux/win
<ZipCPU>
Did it come with an example demo file?
<ZipCPU>
s/file/design/?
<shapr>
yes, bunches
<ZipCPU>
Did you try any of them?
<shapr>
yes!
<ZipCPU>
Good, then you are in a good position to start learning from a generic tutorial!
<shapr>
I went through them quickly until I hit the one where I need to write some C to modify memory
<ZipCPU>
See where I'm coming from there?
<shapr>
I don't have the tutorial in front of me, I'm on my work laptop
<ZipCPU>
Not what I meant
<shapr>
oh, I see what you mean
<ZipCPU>
My point was just that: if you've been through the demo design, building and implementing it, then you are in a good position to start with a more generic tutorial
<ZipCPU>
You no longer need something that is device specific
<shapr>
yeah, that's a good point
* ZipCPU
writes down a note to add something else to the preface (which isn't written yet)
<ZipCPU>
shapr: You seem quite excited about this, and I only have two chapters drafted
<shapr>
I know a good thing when I see it.
<shapr>
and the existing verilog tutorials are really not that great
* ZipCPU
appreciates the compliment
* ZipCPU
is still a bit embarrassed that shapr is advertising an incomplete tutorial
<shapr>
perhaps you'll put it on github and others could contribute?
m4ssi has quit [Remote host closed the connection]
rohitksingh has joined #yosys
dys has quit [Ping timeout: 276 seconds]
<shapr>
ZipCPU: assign is routing, <= is assignment via ram?
<shapr>
that was today's question
<ZipCPU>
??
<ZipCPU>
via RAM?
<ZipCPU>
Most of the design of an FPGA is held in a static RAM, but that gets into underlying implementation
<ZipCPU>
from the designers point of view, how it's done is fairly irrelevant (I'm not the expert on it either)
<ZipCPU>
The assign statement does more than routing--it can be used for combinatorial logic as well
<ZipCPU>
Some of the designs within lesson one should illustrate that
rohitksingh has quit [Quit: Leaving.]
<shapr>
bah, I should paste the code, but it's on my personal laptop
<shapr>
we had to use <= where I expected I could use assign
<shapr>
but that was not the case
<shapr>
I don't so much care about how it compiles onto the FPGA as much as the constraints of the language
<ZipCPU>
So ... only an always @(posedge i_clk) block should have a <= assignment within it
<shapr>
but can't do assign?
<ZipCPU>
(clifford corrected me on this sometime ago ...)
<ZipCPU>
Assign should have a "=" assignment
<shapr>
oh right, that's what we used
<shapr>
so what's the difference between = and <= ?
<ZipCPU>
"=" acts immediately, and leaves you open for simulation/hardware differences
<ZipCPU>
<= should be used for clock edge signals
<shapr>
<= acts on the next cycle?
<shapr>
Why should <= be used for clock edge signals?
<ZipCPU>
<= acts on the edge of the clock
<ZipCPU>
Let's consider: always @(posedge i_clk) a <= b;
<ZipCPU>
If b = 5 on clock 6, a will = 5 on clock 7
<shapr>
ah, interesting
<ZipCPU>
With an always @(*) statement, or an assign statement, you should use "=". In that case, the assignment takes place immediately.
<ZipCPU>
Let me go back to the sim/hardware differences ...
<ZipCPU>
You should use "=" with assign or always @(*), and should not have sim/hardware differences
<shapr>
I've not yet seen "always @(*)" in any verilog source
<ZipCPU>
Where you get the sim/hardware differences is if the "=" is applied in one always @(posedge i_clk) block, and the value is referenced in another
<ZipCPU>
Really? I use it often
<shapr>
might not have noticed it yet
<shapr>
I've mostly read the beaglewire examples
<ZipCPU>
always @(*) and assign both create (roughly) the same type of hardware on your board, although they have different syntaxes
<shapr>
interesting
<ZipCPU>
Sometimes you'll seen an always @(*) block written as always @* or even always_comb
<sensille>
at some point i want to learn how to properly mix '=' and '<=' in an always block for flow control
<ZipCPU>
???
* ZipCPU
thinks about it
<ZipCPU>
Ok, I have done this
<sensille>
:)
<shapr>
I want to port all my examples to clash-lang
<ZipCPU>
The variables set via "=" should be referenced in that always block *ONLY*
rohitksingh has joined #yosys
<sensille>
yes
<shapr>
I teach two lunch time classes at work, Monday is FPGA and Tuesday is Haskell, I want them to be the same class!
<ZipCPU>
You can then set a value via "<=" based upon the "=" variable
<shapr>
ZipCPU: what?
* shapr
thinks
<sensille>
that's exactly what i have in mind
* ZipCPU
steps away
<sensille>
if/else is quite limited as flow control
* shapr
steps to the side
* sensille
looks around
<shapr>
verilog still feels like assembly
<shapr>
to me
<sensille>
assembly is much better than drawing gates :)
<qu1j0t3>
^
<shapr>
you right about that
<shapr>
one day I'll be sufficiently comfortable with verilog that I can write Haskell and generate verilog
<qu1j0t3>
isn't Conal doing that already
<sensille>
shapr: and when you got there you don't want it anymore
<shapr>
qu1j0t3: Conal is much higher level than that, he defines the problem from the viewpoint of denotational semantics / category theory and then maps it onto the implementation
<shapr>
whether that's Haskell, FPGAs, or whatever
<shapr>
I spent an hour sitting between Conal and John Wiegely
<qu1j0t3>
but am i right in that you're saying you feel more comfortable at a higher level
<shapr>
I don't mind writing low level code for fun or learning, but I'd rather not be required to write low level code
rohitksingh has quit [Quit: Leaving.]
<ZipCPU>
shapr: Look at what a "blif" file looks like
<ZipCPU>
That looks more like assembly to me personally
Aleksandar-K has joined #yosys
<sensille>
yeah, assembly would be to instantiate all primitives directly
dys has joined #yosys
<shapr>
ZipCPU: yeah, fair point... but C++ and Python also feel low level after writing Haskell
* ZipCPU
likes c++
<shapr>
let me teach you Haskell someday :-)
* ZipCPU
looks around for an exit
<ZipCPU>
;D
<shapr>
:-D
<shapr>
Many of my friends have rolled their eyes the past twenty years or so when I suggested they learn Haskell
<shapr>
a few of them have decided to try it, most of those are now much more productive
<qu1j0t3>
heh
<sensille>
shapr: is it good to write server applications in it, like mail servers for example?
<sensille>
or what kind of software do you write in it?
<shapr>
sensille: yeah, I've used mail servers written in Haskell
<shapr>
I write just about anything in Haskell
<shapr>
though it's not good at running on embedded systems
<shapr>
you really want 512mb or 1gb of ram
<sensille>
well, everything has been written in any language, but is it _good_ for it
* shapr
thinks about that question
<sensille>
1GB for a single process? really?
<shapr>
I'd say yes, Haskell is good for writing mail servers
* ZipCPU
dreams of formally verifying a transactional memory
* jer
has grand dreams of formally verifying all manner of things =D
<ZipCPU>
o/
<jer>
\o
<jer>
can be so frustrating though =]
<ZipCPU>
How so?
<jer>
but i will say, it's far easier to formally verify some hardware than software systems =]
<jer>
ZipCPU, oh nothing specific, just lack of knowledge i'm learning as i run into walls
<ZipCPU>
I'm game ... anything you need to learn? ;)
<ZipCPU>
What kind of design have you struggled with? Perhaps I may have done something similar? Perhaps I might just offer you some encouragement?
<jer>
ZipCPU, like i say, nothing pressing, but i still also have a problem of not being able to ask sensical questions re FV atm =] so when i do, i sometimes flounder ... mostly just trying to get better with understanding the mechanics
<ZipCPU>
I can understand that
<ZipCPU>
Did you see the FV article about the ZipTimer on zipcpu.com?
<jer>
ZipCPU, i tried to (on my own) formally verify a uart transmitter, and ended up making a list of things i need to better understand, to put it on the side for now
<jer>
ZipCPU, yeah i'm a patron =] i read your stuff a lot
<ZipCPU>
That walks you all the way from a counter to a timer peripheral
<jer>
yeah a few things have really helped
<ZipCPU>
BTW ... the UART seems to be more of a challenge than one would expect, since it's one of the easiest designs to build.
<jer>
hehe yeah
<ZipCPU>
I'll tell you a little secret ... shhh ... (Yosys refuses to verify my fully featured UART transmitter) ... shhh
<jer>
=D
<ZipCPU>
sshhhh ...
<jer>
i won't say a word =]
<sorear>
i assumed the transmitter would be easy, since it's all logic in one clock domain
<ZipCPU>
sorear: The simple transmitter I verified had no problems
<ZipCPU>
The one with problems is the full featured transmitter: breaks, user controlled baud rate, user controlled byte size, parity (or none), etc.
<ZipCPU>
(I'm also doing this on what will be the commercial version .... )
* ZipCPU
has been spending a couple months formally verifying someone else's RISC-V core .... jer, this things aren't necessarily easy
maikmerten has quit [Remote host closed the connection]
<jer>
ZipCPU, my main project is a transport triggered cpu, should be far easier to FV the control logic (which is effectively just a bus controller), but it's not a FV target for me yet -- feels like too much for my current FV skill level
<jer>
(also for those who'll ask why? ... why not, it's interesting, no particular use case =D)
<ZipCPU>
Here's the crazy thing ... Teaching Verilog starts with blinky, and hence counters. Then later, you find you use counters within everything. Same is true of formal verification.
<ZipCPU>
There are just a couple fundamental formal verification tricks. Learn them well, and you can use them everywhere.
<jer>
yep... i've been starting with simple things, first thing i did any FV of, was a jk flipflop
* ZipCPU
approves
<ZipCPU>
Bus interfaces are another one of the "more simple" things to verify
<jer>
yeah
<ZipCPU>
This weeks FV quiz was about the basic property used within those