<alcorn>
so it can output FIRRTL, but currently it can't read it
<ZipCPU>
Are you sure?
<alcorn>
fairly sure. do you have other information?
<ZipCPU>
Trying to find/check it ... what I remember is rather vague, and could be wrong
<ZipCPU>
Here's the command I was remembering: read_ilang
<ZipCPU>
On the other hand, the help command doesn't clearly state its relationship to FIRRTL
<ZipCPU>
... and the presence of a separate write_firrtl suggests the two are very different
<alcorn>
I believe ilang is separate, it's a serializable version of yosys' internal RTLIL
<ZipCPU>
Ok, that's my confusing, I'm confusing RTLIL with FIRRTL
<alcorn>
they achieve the same purpose and are quite similar so that's an easy mistake
<ZipCPU>
So, you want to build a FIRRTL front end ... that could be a lot of fun. Any special underlying purpose? (I'm not trying to be nosy, but I would love the opportunity to understand and encourage you ...)
<alcorn>
I happen to be using Chisel (high level HDL language) for a project and it emits FIRRTL so that's what I'm working with
<ZipCPU>
I know others have gone from Chisel to Yosys, have they all used the Verilog parser?
<alcorn>
the project is automated hardware design for machine learning inference. one challenge i'm facing is that the circuits i'm working with can get quite large, so the ->Verilog and Verilog-> steps of Chisel and yosys respectively are prohibitively slow
<alcorn>
Verilog is just a bad serialization language (who would have guessed!)
<ZipCPU>
Is FIRRTL really that much better? Every example I've seen of synthesized verilog looks like it could be an internal RTL representation
<alcorn>
yes, afaik everyone else has had Chisel emit Verilog
<ZipCPU>
Are you a regular chisel user then?
<ZipCPU>
If so, do you like it? What's your experience with it been like? (Just curious ...)
<ZipCPU>
I've heard a lot about it, but my own experience seems to be quite limited to Verilog and only a dangerous touch of VHDL
* ZipCPU
turns back to his proof ... and keeps waiting
<alcorn>
I think Chisel is excellent. My perspective may be a little different because I come from a software background
<ZipCPU>
Actually, I come from a software background myself
<ZipCPU>
I only picked up gateware after about 20-25yrs with software
<alcorn>
oh, well then I'd encourage you to check it out
<alcorn>
for most people the steepest part of the learning curve is getting familiar with Scala, but if you have a background in software that should be a little easier
<ZipCPU>
Never used scala either, but I figure it's just another language, right?
<alcorn>
(though Scala is tricky, don't get discouraged if it takes a while to get the hang of it)
Laksen has quit [Remote host closed the connection]
<alcorn>
if you happen to be in the bay area you should come along to the next Chisel user's group
<alcorn>
I and others there can help you get started with Chisel
<ZipCPU>
Thank you for the invitation!
<ZipCPU>
I'm actually on the other side of the US, but I think I would be both encouraged and fascinated to attend such. Let me write a mental note to take you up on it sometime
<alcorn>
absolutely. there is a chisel mailing list/google group where the announcements go out
<ZipCPU>
Has the language started to stabilize much? Most of the "news" I've heard has been about this shiny new object, and I'll admit ... the price of verifying that something works makes me shy away from shiny new objects
* ZipCPU
starts another 10mn proof
<alcorn>
The Chisel version 2 -> 3 transition a year or two ago was, as I understand it, a big change, but it feels pretty stable to me. I started using it mid-2018. FIRRTL, the intermediate representation, has helped with understanding and firming up Chisel semantics. Overall, I think people look at Chisel as a serious contender for next-gen design language although it has warts (e.g. verification and testing are not well supported yet)
<ZipCPU>
So ... not much support for formal properties then?
<alcorn>
One thing Chisel people are excited about is the development of a standard library of parametrizable hardware components
<ZipCPU>
Ever thought of adding formal properties as part of your FIRRTL front end?
<alcorn>
re: formal properties: I'm not sure. There might be someone at UC Berkeley working on it though
<ZipCPU>
Fair enough
<alcorn>
In a bigger sense, verification is a recognized challenge that the community is working on
* ZipCPU
is working on formally verifying AXI-based interfaces currently
<alcorn>
if you have some use cases in mind I'm sure the Chisel developers would love to hear about it
<ZipCPU>
I've heard folks argue that verification is not just a challenge, but *the* challenge of all digital design
<ZipCPU>
I can think of a couple of use cases
<ZipCPU>
1) Interface verification, and the ability to ingest properties describing interfaces. These can often provide the biggest bang for the formal buck
<ZipCPU>
2) riscv-formal verification
<alcorn>
what kind of properties are you interested in?
<ZipCPU>
riscv-formal has been written in Verilog, and it would be nice to be able to integrate the two
<ZipCPU>
The types of properties?
<ZipCPU>
always @(posedge i_clk) assert(expression); // and: always @(*) assert(expression_2); and the same for assume() and cover()
<sorear>
well the east coast has Bluespec /s
<ZipCPU>
sorear: o/ and welcome to the discussion ;)
<alcorn>
oh, so yeah Chisel supports simulation time assertions
<alcorn>
is that what you're looking for?
<ZipCPU>
Have you tried any of the formal tools before?
* ZipCPU
rummages for a picture
<sorear>
in typical Valley fashion chisel seems to largely ignore prior art
<sorear>
they managed to glue rocket onto riscv-formal eventually, but AFAICT it was developed without formal tools of any kind
<ZipCPU>
alcorn: If you've never used formal before, this diagram will help identify some of the differences: https://imgur.com/0bN3zva
<tpb>
Title: Imgur: The magic of the Internet (at imgur.com)
<sorear>
it would definitely have been possible to encode properties in FIRRTL, but it doesn't seem like anyone tried :(
<ZipCPU>
Sadly, after putting the diagram together, I was kindly informed that "functional" and "simulation" aren't synonymous. :/
<ZipCPU>
sorear: That was sort of my thought -- it's got to be possible
<ZipCPU>
But no one will do so if they don't see any value in doing it
<sorear>
you kind of need `assume`, not just assert
<ZipCPU>
I would argue that you need assume(), assert(), and cover(). restrict() is useful too, although more so the way yosys implemented it than how the spec describes it
<sorear>
unclear how much industry experience there was on the chisel team
<ZipCPU>
Yeah, that wouldn't surprise me ... I think the team is getting experience by fire though
<alcorn>
sorear: afaict not a lot of industry experience, but the labs involved did tape out a lot of chips using Chisel fwiw
<sorear>
yes
<sorear>
i've seen raven3 in person :)
<alcorn>
another data point is that the Google TPU team used Chisel with some success but ended up disliking the testing story and going back to verilog I think
<sorear>
chris was trying to demo it, but it's hard to do anything interesting with a chip that locks up every trillion cycles
<ZipCPU>
Doh!
<sorear>
they never did manage to reproduce the L2 cache lockup in any kind of simulation environment, so they wound up just throwing out the L2
<alcorn>
also, SiFive of course uses Chisel
<ZipCPU>
That'd be a shame, cache's aren't all that difficult to formally verify
<ZipCPU>
They're also *really* hard to fully test
<ZipCPU>
(Either that, or I just kept getting burned by my cache not working before discovering formal)
X-Scale has quit [Ping timeout: 255 seconds]
<alcorn>
sorear: what's your background?
<sorear>
mostly "lurking in a million project chats"
<sorear>
i was at the workshop in 2016Q4, haven't made one since
<ZipCPU>
"lurking in a million project chats" ... Lol! And offering valuable insights as well
<ZipCPU>
There's been more than once I've been (properly and graciously) corrected by sorear. o/
<sorear>
I've done software professionally, kinda hoping to get into hardware but haven't found my opening
<ZipCPU>
What kind of opening are you looking for?
shenchen_ has joined #yosys
* ZipCPU
starts his proof again
shenchen has quit [Ping timeout: 244 seconds]
<alcorn>
looking at it, I think it wouldn't be terribly difficult to implement formal verification support in Chisel/FIRRTL. The main trick would be to implement a FIRRTL pass that looks for formal verif annotations and emits the right SV statements. Output would be some SV that you can use in any formal verif tools
<ZipCPU>
Yeah, I didn't think it'd be that difficult either
cr1901_modern has quit [Ping timeout: 258 seconds]
shenchen_ has quit [Quit: Leaving]
X-Scale has joined #yosys
ric96 has quit [Ping timeout: 258 seconds]
ric96 has joined #yosys
gsi__ has joined #yosys
gsi_ has quit [Ping timeout: 268 seconds]
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
PyroPeter has quit [Ping timeout: 276 seconds]
futarisIRCcloud has joined #yosys
cr1901_modern has joined #yosys
PyroPeter has joined #yosys
X-Scale has quit [Ping timeout: 246 seconds]
X-Scale` has joined #yosys
X-Scale` is now known as X-Scale
emeb has quit [Quit: Leaving.]
_whitelogger has joined #yosys
rohitksingh_work has joined #yosys
rohitksingh_work has quit [Ping timeout: 246 seconds]
kraiskil has joined #yosys
rohitksingh_work has joined #yosys
rohitksingh_work has quit [Ping timeout: 246 seconds]
rohitksingh_work has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
kraiskil has joined #yosys
m4ssi has joined #yosys
rohitksingh_work has quit [Ping timeout: 258 seconds]
GuzTech has joined #yosys
proteusguy has joined #yosys
proteusguy has quit [Ping timeout: 268 seconds]
_whitelogger has joined #yosys
proteusguy has joined #yosys
proteusguy has quit [Excess Flood]
proteusguy has joined #yosys
togo has joined #yosys
rohitksingh_work has joined #yosys
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
proteusguy has quit [Ping timeout: 268 seconds]
eightdot has joined #yosys
rohitksingh_work has quit [Read error: Connection reset by peer]
_whitelogger has joined #yosys
gnufan_home has joined #yosys
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
gsi__ is now known as gsi_
futarisIRCcloud has joined #yosys
jevinskie has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
proteusguy has joined #yosys
dys has joined #yosys
GuzTech has quit [Remote host closed the connection]
gnufan_home has quit [Ping timeout: 246 seconds]
emeb has joined #yosys
jakobwenzel has quit [Quit: jakobwenzel]
maikmerten has joined #yosys
m4ssi has quit [Remote host closed the connection]
jevinskie has joined #yosys
kraiskil has quit [Ping timeout: 250 seconds]
dys has quit [Ping timeout: 276 seconds]
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
maikmerten has quit [Remote host closed the connection]
kraiskil has joined #yosys
mithro has quit [Remote host closed the connection]
mithro has joined #yosys
kraiskil has quit [Read error: Connection reset by peer]
togo has quit [Quit: Leaving]
futarisIRCcloud has joined #yosys
nrossi has quit [*.net *.split]
srk has quit [Ping timeout: 250 seconds]
kerel_ has quit [*.net *.split]
pointfree has quit [*.net *.split]
jryans has quit [*.net *.split]
smarter has quit [*.net *.split]
srk has joined #yosys
proteusguy has quit [Ping timeout: 244 seconds]
smarter has joined #yosys
nrossi has joined #yosys
kerel has joined #yosys
jryans has joined #yosys
cr1901_modern has quit [Ping timeout: 245 seconds]