<d1b2>
<marble> is there a way to access a signals value from previous clock cycles during formal verification without instantiating a register for that?
<d1b2>
<marble> Ah, Past...
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 256 seconds]
<cr1901>
I'll have more to announce at a more reasonable time, but... I used Amaranth in the past few days to revive a dead ISA card I had.
<cr1901>
It was fast enough to prototype a design for icebreaker- kinda like a scripting language- to dump a PAL and work as a TTL chip tester, to find the bad chip :D
<d1b2>
<Darius> nice
<d1b2>
<widlarizer> I want to test my CPU with various programs loaded into Memory. However, to write into Memory, I have to initialize it, which seems to only be possible in elaborate, so I have to build the design multiple times. This seems to not work, probably because my m instance of Module isn't in top scope: https://www.toptal.com/developers/hastebin/yojiqekibe.py
<Sarayan>
slightly light on very dark? Is the aim being totally unreadable?
<Sarayan>
Oh I see, I didn't understand your problem was with the internal simulation
<Sarayan>
makes sense
<Sarayan>
whitequark probably has a better answer, but for testing the cpu I wouldn't put a Memory in, I'd do it in the sim itself (e.g. simulate the bus cycles and answer from a python array)
<whitequark>
widlarizer: once you create a Simulator with an elaboratable, the contents of the memory is fixed
<whitequark>
you can rewrite it using `yield top.mem[idx].eq(...)`, though
<d1b2>
<widlarizer> awesome - I thought the __getitem__ implementation wouldn't let me write into the fields
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 268 seconds]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 250 seconds]
nelgau has joined #amaranth-lang
nelgau has quit [Ping timeout: 250 seconds]
<cr1901>
widlarizer: You already got your answer, but: in the code you pasted, between "this doesn't work" and "but this does", all you did was move two statements into the "simulate" function?
<cr1901>
Why are those two statements "load-bearing"?
<d1b2>
<widlarizer> I don't think either were actually working
<cr1901>
ahhh
peeps has joined #amaranth-lang
peeps[zen] has quit [Ping timeout: 256 seconds]
<d1b2>
<widlarizer> how do I extract from the simulator a value of a signal manually, to check if my CPU test passed?
<d1b2>
<286Tech> Is there a way to simulate Verilog's (* anyconst *) in Amaranth?
<whitequark>
there's `AnyConst`
<d1b2>
<286Tech> Ah cool. I should have known that you had already implemented it!
<d1b2>
<286Tech> And with that, I have just used FV with induction to prove that my RISC-V core can read from and write to data memory \o/
<whitequark>
very nice!
<d1b2>
<286Tech> I know many people say this, but I really appreciate all the hard work you all have and continue to put in Amaranth. It's my default HDL for a reason 🙂 Thank you!