00:28 <cr1901> Nothing concrete, just a minddump: I was running symbiyosys against Verilog generated by Amaranth. It failed, so sby made a vcd, verilog testbench, and a so-called "witness file". While looking at the output vcd, I found _another_ bug. Wouldn't it be cool to "somehow" go from the witness file to an amaranth module that automatically reproduces the exact input states to trigger the bugs?

00:42 <whitequark[cis]> that is very much possible

00:47 <cr1901> Very cool... I'll keep it on the backburner. If I didn't just learn what a "witness file" was today (and I wasn't trying to "just fix the bugs" right now), I may very well be taking a stab at generating an Amaranth TB module.

02:35 <whitequark[cis]> zyp: so my concern re: ready_i is: suppose I am making a memory controller. in the ideal scenario I am probably feeding bytes from the read stream of the IO buffer directly into the AXI rdata channel

02:36 <whitequark[cis]> if the RDATA stream becomes not ready, you do have to buffer these words somewhere

07:52 <zyp[m]> oh, absolutely, I'd say it's very application specific whether ready_i is useful or not, I'm just saying I want both options, and to be explicit about it

07:54 <zyp[m]> and to clarify, in my mind out and in are still two independent streams that both has a valid and optionally have a ready

07:56 <zyp[m]> there's also single stream endpoints where you can't have backpressure, e.g. the data you receive from an ethernet PHY, an audio ADC or any other source without flow control

07:57 <whitequark[cis]> yeah, okay, I see your point

07:58 <whitequark[cis]> I do think we need a way to indicate that there can be no backpressure, but without removing ready; rather ready for such streams should be a Const(1)

07:58 <whitequark[cis]> (connect already handles this case specially)

10:46 <cr1901> http://gopher.wdj-consulting.com:70/paste/72bfa4f7-ab9b-4040-86d9-09a2ba9a344f.txt This is a self-contained attempt at a tb generator via a witness. I got as far as mapping the witness back to Signals on the interface and extracting the values to set to each signal on each clock cycle

10:48 <cr1901> unfortunately, the tb doesn't actually ever generate VCDs for the signals I extract, despite the process running fine for 25 iters. I'm sure I'm doing something not right w/ the return values from find_signature, but this is about the amount of time I'm willing to spend

10:48 <cr1901> I'll manually copy and paste the parsed values for now

10:53 <whitequark[cis]> this is the wrong approach

10:53 <whitequark[cis]> take a look at the methods in back.rtlil which return a name_map

11:09 <cr1901> Ack, I'll try again when I'm ready to play w/ this some more. In the short term, I got what I wanted (an automated way to extract the values I need to paste into a testbench file)

15:27 <mcc111[m]> I have a low-skill question. I want a register/signal that has this pattern over time:... (full message at <https://catircservices.org/_matrix/media/v3/download/catircservices.org/IgKNVsSveqWppwPJmOkyGShT>)

15:29 <whitequark[cis]> or something like `out = Cat(cnt[:n] == (2<<(n+1))-1 for n in range(4))`

15:30 <mwk> ws2qxsXZ

15:30 <whitequark[cis]> or even

15:30 <mcc111[m]> whitequark[cis]: mm, that's interesting too

15:30 <whitequark[cis]> out = Cat(cnt[:n] == ~0 for n in range(4))

15:30 <whitequark[cis]> no, wait, that won't work; ~0 is negative

15:30 <whitequark[cis]> out = Cat(~cnt[:n] == 0 for n in range(4))

15:31 <whitequark[cis]> anyway, that lets you avoid having a "previous value" register which can cause issues when the counter overflows

15:32 <mcc111[m]> Wouldn't the counter overflowing be good? Because it just wraps?

15:32 <mcc111[m]> What I REALLY want is, I want to have a trigger whose frequency I can speed up or speed down in increments of 2x

15:32 <mcc111[m]> So I was going to have the "counter change" register, and then I was going to have a "check me" mask that I &'d with it, and check if the result is equal to 0

15:32 <mcc111[m]> Maybe this is too complicated to begin with

15:33 <whitequark[cis]> oh

15:33 <mcc111[m]> whitequark[cis]: ok it took me a minute to understand what this is doing but it is neat

15:34 <whitequark[cis]> mcc111[m]: > <@mcc111:matrix.org> What I REALLY want is, I want to have a trigger whose frequency I can speed up or speed down in increments of 2x

15:34 <whitequark[cis]> > So I was going to have the "counter change" register, and then I was going to have a "check me" mask that I &'d with it, and check if the result is equal to 0

15:34 <whitequark[cis]> have a counter whose high bits are masked off on each increment; whenever it overflows you have your trigger

15:35 <whitequark[cis]> so like...

15:35 <whitequark[cis]> m.d.sync += count.eq((count + 1) & ((2 << n) - 1))

15:35 <whitequark[cis]> m.d.comb += trigger.eq(count == 0)

15:35 <mcc111[m]> ok, i think i see what you mean. i'll think about that

21:57 <mcc111[m]> wow uhhh it really does not take a lot of simulating to get a gtkwave file above 1 GB

22:52 <cr1901> >an automated way to extract the values I need to paste into a testbench file <-- Realized tonight; there's value to both "generate source code to a python function implementing the TB" and "generate a generator ready for use w/ Amaranth sim"; the former is useful if your design's interface/timing changes and the witness file can no longer be used directly (but is still useful for automating _most_ of the work)

22:53 <galibert[m]> witness file = generated trace including inputs that formal has found breaking the asserts?

22:54 <cr1901> it's a serialization format for the formal inputs that break the asserts, so external tools can ingest it and "create testbenches/whatever"

22:55 <galibert[m]> ok, I got it essentially right, thanks

22:55 <jwise0[m]> recommend having your simulator write out LXT2 instead of VCD

22:57 <galibert[m]> I'm fascinated that gtkwave has 4 custom formats

22:57 <cr1901> in Yosys' case it's JSON. From reading "yosys-witness" help AIGER and Boolector's BTOR formats also can be used for witness traces