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

bit-test on the function-unit value being tested
this because Function Unit is a bitfield

update isatables to cmpb not modifying CR0

add logical compunit test

comment inputs and outputs from ALU unit test

imports - use of globals. baaaad

remove unneeded code and inputs. convert to "naming" in CompUnit inputs

split out common code from test_alu_compunit.py

add comments for MultiCompUnit parallel test

de-hard-code-ify getting results from MultiCompUnit

remove unneeded imports

split out compalu unit tests to separate module (getting quite big)

HA! found a bug in MultiCompUnit handling of write-masks

clarify

OP_CMPEQB also requesting change of output reg (stop that)

OP_CMP is requesting a change of the output register (should not do that)

still investigating

start with zero, try not to compare against 9 bytes in a 64-bit value: cmpeqb test

more debug statements

add in more CR debug statements

copy in cr0.data into cr0 temp, not whole of cr0 (including ok flag)

remove commented-out vars from ALU input record

write cr0 when op.write_cr.ok is set

add write_cr to ALU record subset

comment out xer ov/so for now

get carry from cr write_cr

select CR0 write out only when RC=1

set CR0 output when OP_CMP or OP_CMPEQB need it

add in use of "Settle"

add in write-mask into MultiCompUnit and MCU-ALU unit test: bug detected in
RC handling

Merge branch 'master' of ssh://git.libre-riscv.org:922/soc

unit test for DataMerger

create read-mask for ALU CompUnit: switches off optional operands

create a write-mask, anything with an "ok" in the Record fields

allow MultiCompUnit outputs to be Records, to capture Data.ok

add read-mask to MultiCompUnit

code-shuffle / comments

mess - but a functional mess.  ALU-MultiCompUnit semi-functional using pipeline

grab other results from ALU pipeline in compunit test

order of XER so/ca wrong way round from regspec

still experimenting with ALU-CompUnit interaction

interesting.  use of Settle() works, showing that Regfile is combinatorial on read

module comments for popcount

comments on popcount

trigger ALU ready when operands ready

fixes for DataMerger

trigger read ALU ready/valid from latch as well

use a latch to communicate read/valid output from ALU