remove rdflags in pipe_data.py (redundant)

move over to using power_regspec_map.py from PowerDecode2 rather than distributed maps in pipe_data.py

move obtaining simulator data into common function for logical pipe tests

mention TODO on SPR regfile

Check completion of the sub-processes

This detects the case where busy_o goes low before the rel / go
cycle finishes.

Fixed missing nia.ok.eq(1) in OP_RFID

Fixed merge conflict by using remote changes

tidyup branch.  comments

convenience variables

FormX not FormXL

add bit more TODO

update submodule for ISA tables

convenience rename for spr pipe_data.py, consistent naming for PowerDecode2

Simplify immediate check

add more TODOs

Preliminary check of the alu protocol

Still need to check that the operand to the alu is held stable.
For now, it's more like a placeholder of what will become the full check.

Pass along the operand, in the cycle in which go is active

Fixed OP_RFID and OP_SC in fu/trap/main_stage

add some more constants and ref to POWER9 pdf

add an if for OP_MTMSR and some comments

Attempted to fix OP_RFID in TRAP pipeline

Implement TRAP instructions OP_RFID and OP_SC

argh - bad hack, detecting when there are no registers to write, in MultiCompUnit

take out unneeded code, add Settle() to see if it helps with bug

add lk field to DecodeOut2

move setting cia input to branch from get_cu_inputs function

hooray, get_cu_inputs now common to both types of tests

oooo very annoying.  there does not appear to be any difference between two set_inputs functions

add get_inputs function to branch test_pipe_caller

remove unneeded variable

Revert "ok ok - for OP_BCREG put CTR in spr2 as well"

This reverts commit 87810631b7ecbd34ad89b2853bbdb763fe003633.

ok ok - for OP_BCREG put CTR in spr2 as well

Select spr1 for bcctr - use fast_spr decoding from decoder

set up CTR and LR only on BCREG when needed

decode fast spr for OP_BCREG CTR, TAR and LR

add TODO comments for read_fast1/2

proof_datamerger: proof that output is zero when idle

argh overlapping commits on submodule (rebase did not work properly)
extra commit just to make sure it updates properly

debugging branch fast registers

Fix broken wiki version

Handle removal of spr2 field from decoder

add comment about fast1 and fast2 in branch test_pipe_caller

add regspecmap function to PowerDecode2

Fix test_bc_reg

Fix issues with test_bc_reg, wrong instruction field for CR selector

move regspec function to separate module

add in fast regs support in decoder and into regspec_decode

add 2nd write-reg for LD/ST Update mode

add write-regs encoding to regspec decoder

add read-write register numbering detection

whoops cut/paste error, creating write_ports not read_ports

whoops syntax error

add function expressing the relationship between regspecs and Decode2Execute1Type

whitespace

rename regspecs to give a consistent naming scheme
the Decode phase needs to be able to associate regspec information with
actual signals, back in Decode2Execute1Type.  the simplest way to do this
is to make the regspec register names consistent and actually refer
*to* Decode2Execute1Type signals

add MSR constants, TODO translated

add TODO comments from microwatt source code

Allow at least one operand to be fetched

We successfully disabled all rel signals. One was immediate, the other was
masked. Let's enable at least one of them, for now.
When the test code is complete, we will be able to issue several
transactions in sequence, with different combinations. We are not there
yet.

Hold rdmaskn active during the busy_o cycle

remove reading port 3 for CR pipeline.  RS moved to port 1

okaaay add a "rdflags" function which obtains the yes/no flags for each register to the CompUnit
this to be used by the Decode phase

add test_bc_reg (fails)

remove unneeded fields from Decode2Execute1Type

Add proof for RegFile

more unneeded fields from SR InputRecord

remove data_len from SR input record

remove zero/invert from ShiftRot Input Record

add shift-rot input record and use it

CompBROpSubset exists

RS moved to port 1 (from port 3), remove need in ALU to read/mux into A operand

Add proof for RegFileArray

remove use of reg3 in logical pipeline: CSV files moved RS to position 1

Have regfile use AnySeq instead of AnyConst

rotator carry is set into both XER CA and CA32 fields

comment out rlwinm. for now

argh - need to zero the src_i input after "Read" is actioned

Enable k-induction for register file proof

That was weird. For some reason it wasn't generating any ports

Full BMC proof of Register

Begin rewrite of proof_regfile.py

put RB in 2nd position (matching immediate) in ShiftRot Input Data

sigh - another instance where write-mask needed to mask out wr.rel

remove xer so/ov, swap rs/rb to correct(?) order in shiftrot test

proof_datamerger wip

add rlwinm. test instruction (sets CR0)

remove duplicate signal

allow ALU / Logical ops to select RS as 1st operand

allow M*-Form shiftrot to swap RS/RB back to consistent positions

add first version of ShiftRot CompUnit test

shiftrot uses LogicalOutputData not ALUOutputData

Add rdmaskn parameter and assert it along issue_i

Like zero_a and imm_ok, rdmaskn disallows the activation of go.

add assertions for branch compunit output

invert SPR1/2 in branch output data

decode SPRs for branch

swap over SPR1/2 to fit with microwatt SPR conventions

add first version compunit branch test

whoops need to read RS in CR inputs test

add first version of CR CompUnit test

minor adjustment, zero test in ALU output stage

remove unneeded code