<az0re>
So, that's cool, and I'm sure it's a fun project
<az0re>
But: Why not Chisel?
vidbina has quit [Ping timeout: 260 seconds]
<FL4SHK>
You might also ask why not SystemVerilog given that sv2v exists
<az0re>
Anyway you should check out how they do bulk connections
<FL4SHK>
spitting out behavioral Verilog is probably not something Chisel does
<az0re>
Yes, but I understand that even SystemVerilog is rather clunky
<az0re>
No indeed
<FL4SHK>
I'm doing that. That's unique.
<az0re>
That's cool
<az0re>
Why do you want it?
<FL4SHK>
Other than my own stubbornness, I don't know if I can give a good answer.
GenTooMan has joined #yosys
<az0re>
Fair enough :)
<FL4SHK>
My language resembles C++
<az0re>
How does this language relate to/integrate with Yosys formal verification?
<FL4SHK>
Well, it'll pass through the stuff that is supported by yosys.
<FL4SHK>
so your `assert` and `assume` stuff that you do in my language ends up in the generated Verilog.
<az0re>
I actually have my own attempt at a higher-level HDL with support for exists-forall synthesis and extra-functional modeling
<az0re>
So, it's not really a first-class citizen, just something that will expose equivalents for $assert, $assume?
<FL4SHK>
There's no dollar sign
<FL4SHK>
No, it's just part of the language's syntax
<az0re>
In Verilog, no, in RTLIL cell names, yes :)
<FL4SHK>
I don't know what would make the assert and assume stuff first class.
<az0re>
If not, I am very interested to hear your ideas about it
<FL4SHK>
Because those constructs are just going to end up in your .v file
<az0re>
I mean more integrated into the language, a more prominent feature
<FL4SHK>
same as if you had hand-written them, I guess
<FL4SHK>
a module in my language translates to a Verilog module
<FL4SHK>
so if you stick your assert and assume into a module in my language, it'll show up in the Verilog code.
<az0re>
For example, just spitballing something maybe half-sensical, you could have module inheritance with automatic interface-correctness automatically verified
<FL4SHK>
At some point I might consider doing something like that
<az0re>
Or maybe just some sweet syntax so you can make statements like: "This module is an adder. Prove that it is equivalent to a basic ripple-carry adder"
<FL4SHK>
FPGA developers just use the + operator, eh?
<az0re>
Like "Module myadder [Prove: is +] { /* ...*/ }"
<FL4SHK>
My tool doesn't invoke Yosys
<az0re>
Just makes output for it, I understand
<az0re>
But it could automatically translate those kinds of things to asserts/assumes for Yosys to verify
<FL4SHK>
I don't want any fancy syntax until I've finished with the basic language that I personally want to use.
<az0re>
Of course
<FL4SHK>
Looks like Chisel in particular says that classes are the replacement for modules?
<FL4SHK>
I have a separation between modules and classes in my thing.
<az0re>
My curiosity was just piqued because of "
<FL4SHK>
classes are essentially just fancy structs or records
<az0re>
<FL4SHK> I only started developing this because I wanted to use a higher level HDL than Verilog with yosys's formal verification"
<FL4SHK>
Yeah, that was my original motivation
<FL4SHK>
I hadn't explored other possibilities enough at the time
<FL4SHK>
I did figure out how to let classes have virtual functions, for example
<FL4SHK>
But I think the fancier OOP stuff in my language will show up more in the interpreter thing
<az0re>
Well, have fun
<az0re>
But KISS
<az0re>
;)
<az0re>
Just don't make the C++ of HDLs where the language is literally undecidable :P
<DDHQ>
<FL4SHK> That's not what I'm doing
<DDHQ>
<FL4SHK> How dare there be a Discord bridge
m4ssi has quit [Quit: Leaving]
somlo has quit [Ping timeout: 260 seconds]
somlo has joined #yosys
az0re has quit [Ping timeout: 240 seconds]
Cerpin has quit [Quit: leaving]
az0re has joined #yosys
Cerpin has joined #yosys
Asu has quit [Ping timeout: 256 seconds]
Asuu has joined #yosys
craigo_ has joined #yosys
BinaryLust has joined #yosys
DDHQ has quit [Ping timeout: 258 seconds]
BinaryLust has quit [Ping timeout: 265 seconds]
BinaryLust has joined #yosys
Ristovski has quit [Quit: 0]
[Ristovski] has joined #yosys
az0re has quit [Quit: Leaving]
[Ristovski] is now known as Ristovski
az0re has joined #yosys
<az0re>
FL4SHK: thinking about it some more, a behavioral Verilog backend might be interesting for a language designed to be used alongside Verilog in a project with other Verilog designers, where all RTL is expected to be normal-ish, readable Verilog. In other words, if you can produce some output that looks natural for how a designer would write the same design in Verilog, a lot more people might be interested in trying out your language. That way
<az0re>
there's zero cost to abandoning your language altogether at any point: The design RTL is already specified naturally in Verilog.
<az0re>
The ability to include inline Verilog segments and to go back and forth between your language and Verilog (or at least, Verilog -> your language for those constructs it recognizes) would be even cooler
<ZirconiumX>
The fine semantics of Verilog are going to make things a bit tricky, I think...
Asuu has quit [Remote host closed the connection]
<az0re>
No doubt!
<az0re>
But I think if you limit yourself to only attempting to translate Verilog AST patterns that you *know* correspond *exactly* to some of your custom language AST patterns, it could be done
<az0re>
For everything else, just do an inline Verilog block quote
<az0re>
Like, you know how you emit registers in Verilog, and you can recognize parts of the Verilog that correspond to exactly how you emit a register, remove them from the inline Verilog block quote and translate them to your language. If it doesn't match exactly, it stays in Verilog.
<ZirconiumX>
Put it this way, there's a two year old Yosys PR called "write_verilog: inline cells used only once"
<ZirconiumX>
Even in that simple context, producing something that is correct in all situations is painful