nelgau has quit [Remote host closed the connection]
nelgau has joined #amaranth-lang
lf has joined #amaranth-lang
nelgau has quit [Ping timeout: 268 seconds]
lf_ has quit [Ping timeout: 268 seconds]
<cr1901>
nickoe: I have ask florent occasionally if he would start using the amaranth compat layer, but he doesn't want to yet.
<cr1901>
for litex* I mean
Degi_ has joined #amaranth-lang
Degi has quit [Ping timeout: 240 seconds]
Degi_ is now known as Degi
nelgau has joined #amaranth-lang
nelgau has quit [Remote host closed the connection]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 256 seconds]
bl0x has quit [Ping timeout: 250 seconds]
bl0x has joined #amaranth-lang
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 256 seconds]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 256 seconds]
<nickoe>
cr1901: yeah, well, I guess it is a bit of a potentially risky thing to "just do"
<nickoe>
Especially when there are so many other things that would be nice to have as well
<lambda>
huh, I missed the renaming, that just took me a while to figure out
<lambda>
that's what you get for only restarting your IRC client once a month, I guess
xiretza[m] has joined #amaranth-lang
<d1b2>
<286Tech> How does Initial() work exactly? I want to FV my core and for induction, I want to force a reset on the first clock cycle.
<d1b2>
<286Tech> I have tried assigning Initial() to ResetSignal(), but that doesn't seem to do anything.
<d1b2>
<286Tech> I have also assigned it to a Signal and use that, but it never gets set.
<d1b2>
<286Tech> And I don't think we can give signals an initial value AFAIK (I'm not talking about the reset value, since you need the reset to actually assert for that, and that's what I can't get to work haha).
<cr1901>
initial doesn't apply during induction
<d1b2>
<286Tech> Hmm
<d1b2>
<286Tech> How can I force the reset to be high the first clock cycle then? In verilog I was using initial, but Amaranth doesn't have that if I'm not mistaken.
<d1b2>
<286Tech> And is there a reason why it doesn't apply during induction?
<cr1901>
It's 5:40AM here, and I really should go to bed, but I'll try a quick version
<d1b2>
<286Tech> Oh no, go get some sleep 😄
<cr1901>
induction tries _all_ possible chains of "n" state transitions, assuming that your assertions hold in the previous "n-1" steps.
<d1b2>
<286Tech> True
<cr1901>
It doesn't make sense to think of an "initial/starting" state when you're looking at _all_ states
<cr1901>
(and if you did, then you wouldn't be trying _all_ possible chains :).)
<cr1901>
Someone can explain it better than I can. It's bedtime for me, at least for a bit.
<d1b2>
<286Tech> Yes, and I just fixed it 😄 I want to check if after a jump, the LSB of the program counter remains zero. That was giving me problems, so I just added a comb assert that always checks it and now it passes!
<d1b2>
<286Tech> Thanks for the help and have a good sleep!
<d1b2>
<dragonmux> also, Amaranth will generate you a PoR block as available on the target device, and the first step of the sim is always a reset step
<d1b2>
<dragonmux> (sim starting conditions are taken to be the reset values of all signals being simulated)
<d1b2>
<286Tech> For those wondering why this helped: during induction, all Assert statements are assumed to be true for N-1 clock cycles, and only during the Nth clock cycle will it check if the assertions hold true. Me asserting that the LSB of the program counter is zero means that induction starts with assuming that it always starts with it set to zero (which is always true), so now it tries every combination of every instruction to try to make the
<d1b2>
LSB a one which it cannot.
<d1b2>
<286Tech> @dragonmux Yes, but that's for simulation 😉 Induction proofs ignore reset values and pick "random" values for all FFs, unless you force it to start with a known good state like I just did.
<d1b2>
<dragonmux> ahhh, gotcha
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 256 seconds]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 268 seconds]
lkcl has joined #amaranth-lang
lkcl has left #amaranth-lang [Leaving]
gdd has joined #amaranth-lang
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 240 seconds]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 252 seconds]
<gruetzkopf>
this language has just been mentioned live on stage at RC3 (on the r3s stage in the axiom talk)
<whitequark>
neat!
<nickoe>
What is axiom? /asking for a friend that is too lazy to google
swym has joined #amaranth-lang
<jn>
open source cinema camera
<nickoe>
thx
swym has left #amaranth-lang [WeeChat 3.3]
swym has joined #amaranth-lang
<swym>
currently watching a talk about the LLVM CIRCT project - are you aware of this? As an outsider I can't quite tell if it would be useful for amaranth or if it's the same thing in a different language.
<swym>
SiFive seems to be using it for generating SystemVerilog from chisel's FIR RTL
<swym>
IIUC the tl;dr is it's an IR above Verilog, implemented in MLIR so there's all kinds of (optimization) passes
<whitequark>
I'm aware of circt, yes
<swym>
do you think it's sth amaranth could benefit from? Or is it solving the same problems just in a different implementation?
<whitequark>
CIRCT is kind of in the same place as Yosys
<swym>
ah gotcha, thanks
lkcl has joined #amaranth-lang
lkcl was banned on #amaranth-lang by ChanServ [*!*@we.will.rock.you.bnc4you.xyz]
lkcl was kicked from #amaranth-lang by ChanServ [User is banned from this channel]
<d1b2>
<widlarizer> Not sure I understood the sentiment - same place with regards to what?
<d1b2>
<widlarizer> I hope to see interoperability at some point. And I kind of want to get involved, though I have a bunch of compiler stuff to learn to get there