Way to start register with "random" value?

[RobertBaruch]

I'm guessing the answer is just going to be, run SymbiYosys in prove mode. But just in case I'm missing something... I would love to do something like this:

x = Signal(16)
init_x = AnyConst(16)

m.d.comb += Assume(init_x > 0x1000)
with m.If(Initial()):
    m.d.comb += Assume(x == init_x)

m.d.sync += x.eq(x+1)

The goal here is to start BMC with x being any value above 0x1000. As it is now, this is UNSAT of course because the reset value of x, a synchronous signal, is zero, and the assumption that it isn't is a contradiction.

[cestrauss]

You could use a XOR trick to make a zero-reset register appear to have an arbitrary reset value.

The XOR at the register output undoes the effect of the XOR at the input. But, at reset, the output becomes the value you XOR with.

m = Module()
x = Signal(16)
x_reg = Signal(16)
x_next = Signal(16)

init_x = AnyConst(16)
m.d.comb += Assume(init_x > 0x1000)

m.d.comb += x_next.eq(x + 1)

m.d.sync += x_reg.eq(x_next ^ init_x)
m.d.comb += x.eq(x_reg ^ init_x)

[RobertBaruch]

Well... yeah... I'm not enthusiastic about it though :)

[whitequark]

@RobertBaruch Would you agree with me that this should be the default when you use reset_less=True signals? For context, see #270.

[RobertBaruch]

Hmm, well... I kind of like the current meaning of reset_less=True, where a FF has a reset value on powerup but doesn't get reset by its domain's reset signal. I see the argument for this meaning a reset value (i.e. FPGA power-on reset values) while not hooking up the reset line of that FF.

Using SymbiYosys in prove mode is adequate to test all sorts of random state, but then in a complex design you have to add asserts on internal states that are intimately tied to internal implementation, and seems fragile (i.e. hard to maintain) to me.

But I can see the point of desiring a third state, which is reset_less=True but randomized=True also. I just don't know how that would look like from a formal verification perspective. Equivalent to a reset value of AnyConst?

[cestrauss]

Maybe:

init_x = AnyConst(16)
m.d.comb += Assume(init_x > 0x1000)
x = Signal(16, reset=init_x)

In case the reset parameter is a signal instead of a constant, nMigen would add the XOR gates behind the scenes.

[whitequark]

I kind of like the current meaning of reset_less=True, where a FF has a reset value on powerup but doesn't get reset by its domain's reset signal.

What would change is the behavior during simulation and verification, since, unless you are only interested in behavior following a power-on reset, you cannot assume that you know the value of a reset_less signal following a domain reset. (This is what #270 was about.)

I do not intend to change the meaning of reset_less=True in FPGA synthesis such that the value at power-on reset is undetermined. That would simply make no sense: no FPGA I know of lets you leave registers uninitialized, and those of them which do not support register initialization in bitstream, initialize to zero. (There's a related issue where some FPGA toolchains cannot fold registers with explicit initialization values into e.g. memory or DSP pipeline stages, but I think that's separate from the behavior of reset_less).

But I can see the point of desiring a third state, which is reset_less=True but randomized=True also.

I strongly dislike any approach that adds "randomization" into the language semantics. You do not actually want random values; what you want is an universally quantified value, and randomization is a workaround for the inability to express that in most tools.

In terms of implementation, you can achieve the result you want by simply deleting the init attribute from the register. Add attrmap -remove init w:x to your Yosys script.

[RobertBaruch]

I think this is probably the most comfortable way I can do this now:

        # This is the "normal" logic of the module
        x = Signal(16)
        m.d.sync += x.eq(x+1)

        # This is like the Initial() signal, except for the 2 initial clocks
        init2 = Signal()
        m.d.comb += init2.eq(Initial() | Past(Initial()))

        # Asserts are now only valid past the first 2 clocks, because we
        # use the first clock to load the initial values.
        with m.If(~init2):
            m.d.comb += Assert(x == (Past(x)+1)[:16])

        # This works because formal will just set init_val to 0x2000.
        m.d.comb += Cover(x == 0x2000)

        # Load the initial values. This works because the last equate (in code) for a signal
        # overrides any previous equates.
        init_x = AnyConst(16)
        m.d.comb += Assume(init_x > 0x1000)
        with m.If(Initial()):
            m.d.sync += x.eq(init_x)

The above code passes cover, BMC, and induction.

[RobertBaruch]

I found that if the x signal in the example above is in a separate module, nMigen gives you a warning, similar to this:

/mnt/f/riscv_pysim/sequencer_card.py:32: DriverConflict: Signal '(sig _pc)' is driven from multiple fragments: top, top.sequencer; hierarchy will be flattened
  self._pc = Signal(32)

I solved this by adding an _initialize signal to all affected modules, which also take in an initial value, and loads it if _initialize is high.

[whitequark]

@RobertBaruch Have you tried my suggestion with the Yosys script?

[RobertBaruch]

I'd rather not, since that solution requires me to know what the RTLIL name of the signal is, and to manually add such a line to the sby file, for every signal I want uninitialized. I much rather like my _initialize solution, which allows modules to be initialized with values if they need to be.

[whitequark]

The reason I'm asking is because your _initialize hack will never be added upstream, but my suggestion might, since it is trivial to do while emitting RTLIL.

If you actually told me the reason you dislike it instead of just ignoring it, though, I would have suggested e.g. adding an uninitialized attribute to such signals and then using the attrmap -remove init a:uninitialized Yosys command, which requires no per-signal work.

[RobertBaruch]

Oh I wasn't ignoring it. I thought you meant that I should use it to get around the fact that it can't be done in any other way. I'd rather add something to the Python code than something to the sby if I can. Or, if I can add something to the sby and not touch it after that, no matter how I modify my Python code, that would work too (i.e. it becomes my standard sby skeleton).

In any case, I tried attrmap -remove init a:uninitialized and it seems to have worked:

        self.register = Signal(32, reset=0x12345678,
                               attrs=[("uninitialized", "")])

...

    with m.If(Initial()):
        m.d.comb += Assume(example.register == 0xFFFF1111)

I'd still like to be able to turn uninitialized on and off, depending on need, though. I suppose something like this:

class Example(Elaboratable):
    def __init__(self, uninit: bool = False):
        attrs = [] if not uninit else [("uninitialized", "false")]
        self.register = Signal(32, reset=0x12345678, attrs=attrs)

[whitequark]

I'd rather add something to the Python code than something to the sby if I can.

Right, I see. Since this is an issue asking for nmigen improvements, I'm approaching it thinking of a way that could be solved for everyone, not just you.

I'd still like to be able to turn uninitialized on and off, depending on need

Once we have a formal runner, I'm thinking that there could be two modes: one that assumes you just reset the entire FPGA (so all the registers have their reset values), and one that does not (so the reset-less registers have unknown/uninitialized values). Would this be enough for your use cases?

[RobertBaruch]

But then how would I specify that I want some signals to be initialized (e.g. internals), and some to not be initialized (e.g. the states I'm really interested in initializing with AnyConst)?

My use cases would be:

• Signals that are reset on init and their domain's reset signal: Signal(reset=x)
• Signals that are reset only on init: Signal(reset=x, reset_less=True)
• Signals that are unknown/uninitialized on startup: Signal(reset=x, reset_less=True, uninit=True)

This way, I can use Initial+Assume+AnyConst to initialize for myself all those signals that are uninit for the purposes of formal verification.

For example, I might want an internal counter to always start at zero. But I want to initialize a CPU register with an AnyConst.

[whitequark]

Okay, I see what you mean: my reset_less proposal would solve some but not all of your use cases. We should probably discuss this in more detail when working on a formal platform.