[dv,fpv] Automatically add FSM asserts

[marnovandermaas]

For CSRNG and EDN, I added asserts to make sure that error states are stable. These and possibly other asserts could be automatically added to a dedicated FSM macro, especially one that is aware of what is an error state.

The asserts that I am talking about are similar to the ones I added at the bottom of the files in this PR: https://github.com/lowRISC/opentitan/pull/16535/files

This issue is related to the ideas in this issue: https://github.com/lowRISC/opentitan/issues/16572

[andreaskurth]

Thanks @marnovandermaas, I think automatically adding some assertions on sparse FSMs could be valuable, at least for certain IPs. Were you thinking of something like this?

`define PRIM_FLOP_SPARSE_FSM_ASSERT(__name, __d, __q, __type, __resval, __err_state, __err_output, __non_err_states, /*...*/) \
  `PRIM_FLOP_SPARSE_FSM(__name, __d, __q, __type, __resval, /*...*/) \
  `ASSERT(FpvSecCmErrStIsStable_A,  __q == __err_state |=> $stable(__q)) \
  `ASSERT(FpvSecCmErrStImplErrOup_A, __q == __err_state |-> __err_output) \
  `ASSERT(FpvSecCmNonLegalStTranToErrSt_A, !(__q inside __non_err_states) |=> __q == __err_state) \
  `ASSERT(FpvSecCmNonLegalStImplErrOup_A, !(__q inside __non_err_states) |-> __err_output)

which could be used like this

`PRIM_FLOP_SPARSE_FSM_ASSERT(u_state_regs, state_d, state_q, state_e, Idle, Error, err_o, {Idle, Busy, Wait})

Would this mean FPV could prove properties that it currently cannot?

[marnovandermaas]

Yes, I think that that is pretty much what I was imagining. As far as I know the current FPV does not provide this functionality, but it would be good for someone else to chime in on that topic.

[weicaiyang]

Thanks @marnovandermaas, I think automatically adding some assertions on sparse FSMs could be valuable, at least for certain IPs. Were you thinking of something like this?

`define PRIM_FLOP_SPARSE_FSM_ASSERT(__name, __d, __q, __type, __resval, __err_state, __err_output, __non_err_states, /*...*/) \
  `PRIM_FLOP_SPARSE_FSM(__name, __d, __q, __type, __resval, /*...*/) \
  `ASSERT(FpvSecCmErrStIsStable_A,  __q == __err_state |=> $stable(__q)) \
  `ASSERT(FpvSecCmErrStImplErrOup_A, __q == __err_state |-> __err_output) \
  `ASSERT(FpvSecCmNonLegalStTranToErrSt_A, !(__q inside __non_err_states) |=> __q == __err_state) \
  `ASSERT(FpvSecCmNonLegalStImplErrOup_A, !(__q inside __non_err_states) |-> __err_output)

which could be used like this

`PRIM_FLOP_SPARSE_FSM_ASSERT(u_state_regs, state_d, state_q, state_e, Idle, Error, err_o, {Idle, Busy, Wait})

Would this mean FPV could prove properties that it currently cannot?

I like this idea. It can be automatically added to all the blocks and run in both DV and FPV. I have a few suggestions

1. we could utilize the enum type (state_t) to find out if the state is valid or not. @cindychip found below works for FPV, VCS and Xcelium, after tried with tons of experiments. https://github.com/lowRISC/opentitan/blob/214163160f5c8858b2806a2d734a1463347c428a/hw/ip/prim/rtl/prim_sparse_fsm_flop.sv#L43-L50

we could consider moving assertion to prim_sparse_fsm_flop, in order to use this function - is_undefined_state.

2. not all the sparse FSM has an error state, such as this one. The default state is the error state. We could define __err_state as a parameter queue for prim_sparse_fsm_flop. Perhaps call it ErrStateQ or similar. The input of ErrStateQ can have one or more states. If the FSM only has default state as the error state, we could input 0 for ErrStateQ, since we never use all 1s or all 0s as a defined state. (in another word, 0 is always an error state).

For the assertion that checks error state stable, it can be done in this way.

assign unused_err_o = is_undefined_state(state_o) or (state_o inside ErrStateQ);
`ASSERT(FpvSecCmErrStIsStable_A,  unused_err_o |=> $stable(unused_err_o)) 

3. The unused_err_o in prim_sparse_fsm_flop is a "fake" error, which is a helper flag for DV and FPV. When it's set, we will check a fatal alert will be triggered. The actual error signal that we use in RTL is a helper flag for design, which eventually leads to an alert. I'm not sure if all the FSM has this flag. And each FSM may call this differently. It may be not necessary to check it, but if it's easy to check, I'm fine too.

@sriyerg @cindychip can also chime in

[sriyerg]

This proposal sounds good to me, thanks!

[andreaskurth]

Triaged for edn and csrng, where those asserts were handwritten, so no direct action required. I'm adding this to M2.5 with https://github.com/lowRISC/opentitan/labels/Priority%3AP4, because it could increase FPV coverage, but I'm fairly sure that if the current design had any bugs related to this, we'd have caught them by now.

[msfschaffner]

Moving to the backlog, since low-priority.

[andreaskurth]

Suggest M5 or backlog

[vogelpi]

What we currently have in the design is sufficient. The proposal here would simplify things. It's more like a cleanup things. While it would be nice, I don't think we get to this. Moving to Backlog / FutureReleases.