Re: [PATCH v3 09/13] verification/rvgen: Delete __parse_constraint()

[Nam Cao <namcao@linutronix.de>]

Gabriele Monaco <gmonaco@redhat.com> writes:
> This function used to validate things we are no longer validating, now it's
> alright to create a model where a clock is never reset, which doesn't fully
> make sense. Should we add that check somewhere else?

Theory does not require clock reset, right? This is not some sort of
hidden issue that trips up unsuspecting people. It is obvious from the
model that the clock is never reset. So I think it's fine to allow
people to do that, maybe there will be an actual useful model without
clock reset, you never know.

The self.env_types check is enforced by the grammar. We do lose the
self.env_types check, but that is likely redundant anyway because we
have this:

        for transition in self.transitions:
            [...]
            if transition.reset:
                envs.append(transition.reset.env)
                self.env_stored.add(transition.reset.env)

so it is clear that all envs that are reset do have a storage.

That said, I am fine with keeping these sanity checks, if you are
paranoid.

Nam