messing about with proof_regfile.py

move simple_popcount out of class (does not use any class state)

Added Initial() synchronous check with draft truth
table for rp.ren and wp.wen of Register() in proof_regfile

extra check on rd.req in test_alu_compunit

indention

Add proof for OP_SETB

Update to latest wiki version

Add OP_SETB

Fix test_isel to properly examine registers

unittest for DataMerger

more fixes for DataMerger

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

fixes for l0_cache.py

debug-print rd/wr rel in test_alu_compunit

add quick test of 3-operand DummyALU in MultiCompALU

add 3rd parameter to DummyALU

debugging test_alu_compunit.py

start on a compunit ALU test

update comment

remove trick of not setting SO

Check that rd rises after issue_i, unless it's immediate

hmm....

Add sync Assert for _wrports 'wen' signal in proof_regfile.py, proof
still not working

Store and present parameters together with issue_i

do not use range(0, x) - just range(x)

remove write-block on register zero

code-morph, add TODO on OP_RFID, OP_SC, OP_ADDPCIS

Derive proof_regfile Driver from regfile.Register() so test actually
runs

Fix indentation of regfile/formal/proof_regfile.py

First commit of proof of regfile, not working yet

add LD/ST pipe_data

LogicalOutputData does not need XER.so

comments

remove XER.ca from logical Input Data - not needed

cleanup logical main proof

check cr0, ov and ca ok signals in ALU main_stage proof

add carry-out, overflow and cr0 ok setting in ALU main_stage

add SRR0 to TrapInputData

add links to bugreports into ALu formal proof as well

add links to bugreports into alu output stage proof

check reg output Data.ok in shift_rot formal proof

rename CROutputData.cr_o to just CROutputData.cr

test Data.ok for cr output and full cr output

assign and test on Data, TODO add Data.ok checking in CR proof

Fix bug in alu main stage proof

Move test case parameters to an "operation" member function

This allows running several operation cases in succession, without needing
to restart the processes, losing state and trace history.

I expect the need to synchronize the processes for each new operation.

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

elaborate function for DataMerger

Remove the monitor process

It may be useful for debugging, but GTKWave is better.
It has served well its purpose, when first setting up the simulation.
Can be added back if needed.

make power function unit enum bitmasked

add extra INT regs port for now, add Fast Regfile

added XER and CR regfiles, using new VirtualRegPort

check assertions

make read/write regs properly internal

add VirtualRegPort test, seems to demonstrate it working

remove sync (not needed)

get score6600_multi.py working again

redo focus of virtual reg port to do only full datawidth not share with mini-regs

Add extras from bottom of the file

Rewrite proof to be more in line with what appears in the wiki

sort-of (maybe) implemented a virtual port on top of RegFileArray.
needs checking

try new variant of VirtualRegFile

use nmutil treereduce

continue virtual regfile port

whitespace, add commentary

First attempt at implementing block access rd and wr regfile port onto
an array-based regfile

Check that busy_o doesn't rise on its own

Implement the issue_i/busy_o protocol check.

It will timeout, until the rel/go signals are implemented.

Move process list to CompUnitParallelTest

The process list (implementation detail) is best left for the class.

Correct polarity of shadow signal

document shadown inversion

Add link to compunit wiki page

Correct property numbers, add assertions about busy

update comments on compalu_multi.py

Add assertions about go_wr and wr_rel

Minor cleanup of comments

Minor changes to alu_hier.py to allow it to be used in proof

Begin working on proof for compunit/fu

add some more stub comments

yield blank so test passes

add stubs

add comments

Fix detection of busy_o inside the monitor process

Found the bug literally seconds after pushing...

Proof of concept of a parallel test

It doesn't work as expected.
For some reason, only the driver sees the rise of busy_o.

fix own copy/paste error

whitespace fix in docstring

correct links in regfile docstring

document regfiles

argh!  frickin MACos terminal expanded out to 86x30 not 80x30

add docstring

add INT, SPR and CR regfiles

refactoring (see #216 Comment 43)

whitespace changes

quick addition of zero+immed test to LDSTCompUnit

must not do rd-req checking when both imm and zero mode are enabled

implement DataMerger interface

add zero immed on LDST, untested

comment out invalid test

lots of greater than 80 chars

switch out req rel if immediate enabled