<catlosgay[m]>
my guess for the difference between picosat and the rest would be preprocessing. when entered in competitions, picosat used to be paired with the satelite preprocessor (http://minisat.se/downloads/SatELite.pdf, https://cca.informatik.uni-freiburg.de/papers/Biere-JSAT08.pdf). satelite style (and stronger) preprocessing has been built into minisat and all those other solvers for a while now, whereas if picosat is used directly as
<catlosgay[m]>
in boolector it doesnt have the preprocessor i believe. satelite can make a big difference on solving time for circuit stuff (according to the literature, ive never really experimented myself)
<catlosgay[m]>
although actually idk if the preprocessor gets run in minisat in incremental mode, so maybe im barking up the wrong tree
Raito_Bezarius has quit [Read error: Connection reset by peer]
Raito_Bezarius has joined #amaranth-lang
Raito_Bezarius has quit [Max SendQ exceeded]
Raito_Bezarius has joined #amaranth-lang
zignig has quit [Ping timeout: 276 seconds]
zignig has joined #amaranth-lang
zignig has quit [Ping timeout: 264 seconds]
zignig has joined #amaranth-lang
zignig has quit [Ping timeout: 256 seconds]
zignig has joined #amaranth-lang
zignig has quit [Ping timeout: 276 seconds]
zignig has joined #amaranth-lang
lyxicon has joined #amaranth-lang
<lyxicon>
Hello. I am starting to take a look at Amaranth for a possible audio DSP ASIC application. I have a few questions:
<lyxicon>
1. Is it possible to 'instantiate' systemverilog modules from Amaranth? I see the intro page of the docs mention this but I cannot find any documentation on it?
<whitequark[cis]>
there are some unresolved questions about fixed-point support and it's something community stakeholders are going to discuss in the coming weeks; each Monday on 1700 UTC is when we discuss language and standard library additions
<lyxicon>
I see. Thanks for the quick reply! I will try to join in on that. I am only a beginner in python but I do fixed point stuff in SV for a living so I might be able to contribute.
<whitequark[cis]>
it's almost certain that the language will gain built-in fixed-point support at some point, but exactly how long it'll take can vary depending on priorities of everyone involved and other factors
<whitequark[cis]>
sure, meetings are open for participation
<lyxicon>
Do you have a published roadmap document of sort to understand what the priorities are?
<whitequark[cis]>
there isn't a specific roadmap; the project is to a large degree community-driven so it's just what the people involved choose to work on
<whitequark[cis]>
Monday meetings serve to synchronize, but other than that it's just everyone's personal priorities (even if some of us are getting paid to write or design Amaranth, it's a community project and there is no organization that sets the direction)
<whitequark[cis]>
something you can definitely do if you want fixed point support right now is to start using code from PR#1005. Amaranth's data structures are designed to be modular and to avoid privileging the standard library over other code, so you can pretty much just copy fixed.py out of that PR and start using it
<whitequark[cis]>
it won't be interoperable with the upstream implementation once that lands, so you'll have to switch over if you want your library to be usable by others, or you could continue to just use your local copy indefinitely otherwise
<lyxicon>
Got it, yeah will give that a shot. I am also curious... do you know of Amaranth Verilog output having been used in an ASIC flow? Specifically I am wondering if the generated verilog would be taken in by Cadence tools (Xcelium, Genus, ...) without too many lint issues. I imagine that generated code sticks to very basic and explicit verilog, but
<lyxicon>
figured I'd ask if anyone has experience with that.
<whitequark[cis]>
people have used Amaranth to tape out many ASICs
<whitequark[cis]>
because it's an open source project, many (most, possibly?) people who do so never tell us
<whitequark[cis]>
the code that Amaranth outputs is Verilog-2001 with the absolute bare minimum of features used. you can also get it to output similarly conservative SystemVerilog (mostly just using always_comb and always_ff) which can sometimes be more palatable
<whitequark[cis]>
if you get lint violations you can file a bug, I would consider that a usability issue. personally I've never worked with any of the big 3 ASIC flows since I'm an open source girl by heart
<whitequark[cis]>
I can't imagine that Xcelium would be much more unhappy than Vivado though, which consumes the output just fine
<lyxicon>
Got it. Makes me optimistic about the prospects of this. The main challenge in an 'industry' setting is flying this stuff under the radar. I currently do hand-written SV but do all my validation (as a designer) in cocotb. Of course, our DV team is stuck in the past using SV/UVM, and generated code can make their job painful.
<whitequark[cis]>
I can tell you that it is obvious to anyone looking that the code Amaranth generates is, well, generated
<tpw_rules>
yeah it's arduous to sort through, but possible
<tpw_rules>
(what qualifies as a "lint violation"? iirc quartus whines some about case statements)
<whitequark[cis]>
unlike some other frontends it does give you a hierarchical post-elaboration netlist whose names mostly correspond to the source code, but it's very obviously generated
<whitequark[cis]>
tpw_rules: quartus has a like 20 warning long list of things it should shut up about and it needs to become a 21 warning long list
<tpw_rules>
there are also annotations to help go back to the python source code
<tpw_rules>
ok, that could be my fault too for not letting amaranth drive quartus (yet)
<lyxicon>
Oh yeah I don't mean that people won't know it's generated. It's more about keeping it readable enough... There is also the ECO aspect, i.e. being able to make a minimal change in the verilog to fix bug that leads to a minimal change in the masks.
<whitequark[cis]>
the way amaranth generates verilog has a direct correspondence to the input AST as it does minimal processing, but depending on how your ECO flow looks like, you might have to edit the verilog
<lyxicon>
I see
<tpw_rules>
(does it still always go through yosys?)
<whitequark[cis]>
mainly because you could see the naming of intermediates to become askew with an addition or removal of an operation
<whitequark[cis]>
tpw_rules: yeah
<lyxicon>
Speaking of simulators, is there any (planned) integration with cocotb? We have a bit of an internal framework built around it, and it would be really cool to keep using that. Using cocotb with the autogenerated verilog + Xcelium would probably not be ideal (autogenerated internal net names being one problem).
<tpw_rules>
i was gonna say yeah it feels like reindexing could be a challenge
<whitequark[cis]>
amaranth has its own simulator and at the time we do not plan to integrate more closely with cocotb, mainly because of how verilog-focused it is
<tpw_rules>
dealing with automated internal net names is not tooo bad
<tpw_rules>
and usually easy to fix
<lyxicon>
Got it. Unfortunately, I don't think we could fully switch to Amaranth's simulator, because we also use cocotb to sim the synthesized and PnR'ed verilog netlist with the same test bench that we write for the RTL.
<lyxicon>
so I guess we would just have to deal with the internal net names
<whitequark[cis]>
you can get a mapping of every Amaranth-level signal to each generated net name if you want
<lyxicon>
Ah, that would help. How do I do that?
<whitequark[cis]>
amaranth.back.verilog.convert_fragment returns the verilog text and a SignalMap
<whitequark[cis]>
none of the signals are going to get an internal name though, the internal names are reserved for expression intermediates
<whitequark[cis]>
like a + b in x.eq((a + b) == 0)