|
|
|---|
|
|
|
|---|
Product type bundling an LHS (some list of FSM signal segments), a time step, and a Boolean indicating signedness, signifying the concatenated value of those segments at that time.
This is a product type introduced by defprod.
These are used for mapping FSM signals to SVTV variables. The signedness is relevant because of peculiarities of SVTV theorems. In SVTV runs, only a lower segment of the bits of any given variable are relevant, but theorems about SVTV runs tend to specify the signedness of the variable. E.g., many input variables are assumed unsigned-byte-p of some size, and override-test variables are usually assumed to be -1 or 0. Thus we need to map the relevant portions of the FSM variables sometimes to unsigned and sometimes to signed values.