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

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

[Samuel Falvo II]

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.

Looking in https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/pipe_data.py;h=d2de8552a62a55bada4a5e83726c273ef943ac83;hb=HEAD
seems to confirm my suspicion that neither srr0 nor srr1 actually
exist; they are (confusingly) called fast1 and fast2.  Double-checking
GTKWave's signal lists confirms that fast1 and fast2 exist.

Can anyone please advise on how to proceed?  I see several ways of
resolving this going forward, but I need input from others:

1.  Rename fast1 and fast2 to srr0 and srr1, or,
2.  Keep fast1/fast2 and rebind them to srr0/srr1 in the main_stage.py
and prove_main_stage.py files, or,
3.  ...?

Thanks.


-- 
Samuel A. Falvo II

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

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

[Samuel Falvo II]

On Fri, Jul 17, 2020 at 5:58 PM Samuel Falvo II <sam.falvo@gmail.com> wrote:
> I'm running into an irreconcilable property violations with the formal
> properties for the trap main stage.

Please disregard; I just spotted the convenience assignments in the
TrapInputData class.  Egg, meet face.

-- 
Samuel A. Falvo II

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

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

[Luke Kenneth Casson Leighton]

On Saturday, July 18, 2020, Samuel Falvo II <sam.falvo@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
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev