[libre-riscv-dev] Signal names for trap pipeline??

[Luke Kenneth Casson Leighton]

On Saturday, July 18, 2020, Samuel Falvo II <sam.falvo at gmail.com> wrote:

> I'm running into an irreconcilable property violations with the formal
> properties for the trap main stage.
>
> I'm noticing that there's repeated references to SRR0 and SRR1
> registers in https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/
> trap/main_stage.py;h=325fb373546673df3ec19a15554e775bcc6fe9a9;hb=HEAD;
> however, after spending about 30 minutes hacking away at what might be
> the cause, I realized after reviewing the graphs in GTKWave that I
> don't see these signals in either the top or the DUT module signals.


you've likely been caught out by the convenience naming here:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/pipe_data.py;h=d2de8552a62a55bada4a5e83726c273ef943ac83;hb=HEAD#l15

initiating the instance TrapInputData by now you should know that the
IntegerData base class drops Signals into it according to the regspec.

however in some cases we want better names for things, more closely related
to the context of the actual opcode.

we give them *multiple* convenience namesin some cases.  see branch and
associated proof.

particularly OP_BCREG where the fast reg can be one of three: LR, CTR or
TAR.  i made a table somewhere.

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/branch/formal/proof_main_stage.py;hb=HEAD

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/branch/pipe_data.py;hb=HEAD

so yes they don't "exist", they are same Signal different names and when
created Signal.name was set and that's what goes into gtkwave.

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68