Luke Kenneth Casson Leighton [Wed, 20 May 2020 18:45:12 +0000 (19:45 +0100)]
store CR lut result in temporary
Michael Nolan [Wed, 20 May 2020 18:32:29 +0000 (14:32 -0400)]
Begin adding CR proof
Michael Nolan [Wed, 20 May 2020 18:33:15 +0000 (14:33 -0400)]
Fix small bug in op_crop
Luke Kenneth Casson Leighton [Wed, 20 May 2020 18:10:53 +0000 (19:10 +0100)]
add register specs to pipeline in/out so that they can be used to connect up
Function Units to regfiles
Luke Kenneth Casson Leighton [Wed, 20 May 2020 17:41:05 +0000 (18:41 +0100)]
damn. assigning to temporary signals may turn out to be crucial. it could
just be something that affects Arrays: generating the ilang for CR pipeline
went mental. 100% CPU for several minutes. bad sign
Luke Kenneth Casson Leighton [Wed, 20 May 2020 17:31:51 +0000 (18:31 +0100)]
ehn? moo? CR test_pipe_caller locks up 100% CPU on writing ilang file
Luke Kenneth Casson Leighton [Wed, 20 May 2020 17:24:33 +0000 (18:24 +0100)]
correct XER variable names
Luke Kenneth Casson Leighton [Wed, 20 May 2020 17:24:16 +0000 (18:24 +0100)]
correct import on shift_rot maskgen
Michael Nolan [Wed, 20 May 2020 17:04:43 +0000 (13:04 -0400)]
Use overflow definition from microwatt
Michael Nolan [Wed, 20 May 2020 16:44:46 +0000 (12:44 -0400)]
Add overflow handling and proof
Michael Nolan [Wed, 20 May 2020 17:11:18 +0000 (13:11 -0400)]
Fix bug introduced in rebase
Luke Kenneth Casson Leighton [Wed, 20 May 2020 17:00:56 +0000 (18:00 +0100)]
fixup XER names in shift_rot pipe tests
Luke Kenneth Casson Leighton [Wed, 20 May 2020 16:54:34 +0000 (17:54 +0100)]
formal proof rename on XER flags
Luke Kenneth Casson Leighton [Wed, 20 May 2020 16:50:32 +0000 (17:50 +0100)]
update to new names for XER fields
Luke Kenneth Casson Leighton [Wed, 20 May 2020 16:47:41 +0000 (17:47 +0100)]
normalise XER regs carry/32 and SO
Michael Nolan [Wed, 20 May 2020 15:29:59 +0000 (11:29 -0400)]
Add proof for OP_CNTZ
Luke Kenneth Casson Leighton [Wed, 20 May 2020 15:27:26 +0000 (16:27 +0100)]
add cross-reference to bugtracker and wiki
Michael Nolan [Wed, 20 May 2020 15:15:10 +0000 (11:15 -0400)]
Add test for edge cases that were previously buggy
Michael Nolan [Wed, 20 May 2020 15:12:14 +0000 (11:12 -0400)]
Delete assume left over from testing
Michael Nolan [Wed, 20 May 2020 15:10:18 +0000 (11:10 -0400)]
Add proof for OP_PRTY
Michael Nolan [Wed, 20 May 2020 15:04:57 +0000 (11:04 -0400)]
Formally verify OP_POPCNT
Michael Nolan [Wed, 20 May 2020 14:49:54 +0000 (10:49 -0400)]
Fix bug with popcntd
Popcount on -1 (64 ones) would overflow the signal holding the sum,
giving 0 instead of 64
Luke Kenneth Casson Leighton [Wed, 20 May 2020 14:38:27 +0000 (15:38 +0100)]
convert CompUnit to use CompUnitRecord
Luke Kenneth Casson Leighton [Wed, 20 May 2020 14:23:42 +0000 (15:23 +0100)]
whitespace, rename ilang to alu_main_stage.il
Luke Kenneth Casson Leighton [Wed, 20 May 2020 14:22:22 +0000 (15:22 +0100)]
i seem to like short names that happen to make things fit onto one line
under 80 chars...
Michael Nolan [Wed, 20 May 2020 14:07:16 +0000 (10:07 -0400)]
Add proof for OP_CMP and OP_CMPEQB
Michael Nolan [Wed, 20 May 2020 14:01:29 +0000 (10:01 -0400)]
Add proof for OP_EXTS
Michael Nolan [Wed, 20 May 2020 13:52:05 +0000 (09:52 -0400)]
Add 32 bit carry handling to alu
Luke Kenneth Casson Leighton [Wed, 20 May 2020 13:50:39 +0000 (14:50 +0100)]
output ilang for ALU to unique file
Luke Kenneth Casson Leighton [Wed, 20 May 2020 13:46:45 +0000 (14:46 +0100)]
use nmutil exts helper in ALU OP_EXTS
Luke Kenneth Casson Leighton [Wed, 20 May 2020 13:34:11 +0000 (14:34 +0100)]
use nmutil exts helper
Luke Kenneth Casson Leighton [Wed, 20 May 2020 13:30:23 +0000 (14:30 +0100)]
fix imports in fu matrix tests
Luke Kenneth Casson Leighton [Wed, 20 May 2020 13:30:01 +0000 (14:30 +0100)]
use nmutil exts helper
Michael Nolan [Wed, 20 May 2020 13:28:40 +0000 (09:28 -0400)]
Fix broken test_caller.py
Luke Kenneth Casson Leighton [Wed, 20 May 2020 05:07:16 +0000 (06:07 +0100)]
munge / simplify code
Luke Kenneth Casson Leighton [Wed, 20 May 2020 05:00:47 +0000 (06:00 +0100)]
minor code-munge, use shorter names
Luke Kenneth Casson Leighton [Wed, 20 May 2020 04:46:17 +0000 (05:46 +0100)]
convert shift_rot to use XER Data
Luke Kenneth Casson Leighton [Wed, 20 May 2020 04:44:52 +0000 (05:44 +0100)]
convert Logical to use new XER use of Data()
Luke Kenneth Casson Leighton [Wed, 20 May 2020 04:42:45 +0000 (05:42 +0100)]
convert alu output to use Data for XER and CR0
Luke Kenneth Casson Leighton [Wed, 20 May 2020 01:01:19 +0000 (02:01 +0100)]
whoops changed name of ALUInputData to LogicalInputData
Luke Kenneth Casson Leighton [Wed, 20 May 2020 00:58:38 +0000 (01:58 +0100)]
fix a series of random imports
Luke Kenneth Casson Leighton [Wed, 20 May 2020 00:23:00 +0000 (01:23 +0100)]
add DIV and MUL to POWER Function enum
Luke Kenneth Casson Leighton [Tue, 19 May 2020 21:55:54 +0000 (22:55 +0100)]
output ilang to branch_pipeline.il for branch
Luke Kenneth Casson Leighton [Tue, 19 May 2020 21:54:44 +0000 (22:54 +0100)]
use field AA directly
Luke Kenneth Casson Leighton [Tue, 19 May 2020 21:14:00 +0000 (22:14 +0100)]
add OP_RFID to enums
Luke Kenneth Casson Leighton [Tue, 19 May 2020 21:11:54 +0000 (22:11 +0100)]
update submodule to latest (including OP_TDI/OP_TRAP
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:58:13 +0000 (21:58 +0100)]
remove SPR3 from Branch Data, rename lr and spr to SPR1 and SPR2
colepoirier [Tue, 19 May 2020 20:43:13 +0000 (13:43 -0700)]
Renamed bperm files in fu/logical and fu/logical formal to correct name
of operation 'bpermd', added up-to-date docstring from spec v3.1
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:38:51 +0000 (21:38 +0100)]
rename module, remove extraneous code and imports
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:37:40 +0000 (21:37 +0100)]
hmmm, branch sets nia to Data as well and sets nia.ok if branch should occur
therefore do the same thing?
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:34:02 +0000 (21:34 +0100)]
whitespace
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:33:38 +0000 (21:33 +0100)]
use Data on SPRs in Trap InputData just like in BranchOutputData
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:30:42 +0000 (21:30 +0100)]
code-munge
Luke Kenneth Casson Leighton [Tue, 19 May 2020 20:22:38 +0000 (21:22 +0100)]
update comments
Michael Nolan [Tue, 19 May 2020 19:59:33 +0000 (15:59 -0400)]
Add should_trap signal to trap output data
Michael Nolan [Tue, 19 May 2020 19:52:52 +0000 (15:52 -0400)]
Add trap main stage
Michael Nolan [Tue, 19 May 2020 19:34:49 +0000 (15:34 -0400)]
Update to latest wiki version - fixing OP_TRAP
Michael Nolan [Tue, 19 May 2020 19:34:35 +0000 (15:34 -0400)]
Change OP_TWI/TDI/TW/TD to OP_TRAP
Michael Nolan [Tue, 19 May 2020 19:26:48 +0000 (15:26 -0400)]
Begin adding trap FU
Luke Kenneth Casson Leighton [Tue, 19 May 2020 17:33:48 +0000 (18:33 +0100)]
rename ALUPipeData to LogicalPipeData
Luke Kenneth Casson Leighton [Tue, 19 May 2020 16:25:51 +0000 (17:25 +0100)]
annoying syntax error
Luke Kenneth Casson Leighton [Tue, 19 May 2020 16:25:18 +0000 (17:25 +0100)]
code-shuffle on OP_CNTZ
Michael Nolan [Tue, 19 May 2020 16:06:52 +0000 (12:06 -0400)]
Implement 32 bit cntlz and cnttz
Michael Nolan [Tue, 19 May 2020 15:58:19 +0000 (11:58 -0400)]
Actually implement cntlzd
Michael Nolan [Tue, 19 May 2020 15:35:54 +0000 (11:35 -0400)]
Fix weird edge cases with carry
Michael Nolan [Tue, 19 May 2020 15:20:04 +0000 (11:20 -0400)]
Add ca32 to caller.py
Michael Nolan [Tue, 19 May 2020 15:06:04 +0000 (11:06 -0400)]
Handle carry out in alu
Michael Nolan [Tue, 19 May 2020 15:05:41 +0000 (11:05 -0400)]
Handle carry in caller.py
Luke Kenneth Casson Leighton [Tue, 19 May 2020 15:15:54 +0000 (16:15 +0100)]
add TRAP FunctionUnit type
Luke Kenneth Casson Leighton [Mon, 18 May 2020 10:30:50 +0000 (11:30 +0100)]
32-bit testing of output for CR0 conditions
colepoirier [Tue, 19 May 2020 00:18:59 +0000 (17:18 -0700)]
Added luke's suggested code to cover all 3 assertions in proof_bperm.py
colepoirier [Mon, 18 May 2020 22:25:37 +0000 (15:25 -0700)]
Added 2nd of 3 assertions for proof_bperm.py, currently not correct
Michael Nolan [Mon, 18 May 2020 17:53:48 +0000 (13:53 -0400)]
Fix error with selecting a selectableint using a selectableint
Michael Nolan [Mon, 18 May 2020 17:53:32 +0000 (13:53 -0400)]
Update to latest wiki version
Luke Kenneth Casson Leighton [Mon, 18 May 2020 10:11:32 +0000 (11:11 +0100)]
move countzero to fu/logical
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:59:19 +0000 (04:59 +0100)]
fix countzero import on test
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:58:05 +0000 (04:58 +0100)]
correct import after soc.fu move
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:56:54 +0000 (04:56 +0100)]
dumb syntax error
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:56:29 +0000 (04:56 +0100)]
mass-rename of modules to soc.fu.*
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:52:43 +0000 (04:52 +0100)]
rename pipe to fu
Luke Kenneth Casson Leighton [Mon, 18 May 2020 03:52:30 +0000 (04:52 +0100)]
move pipelines to pipe dir
colepoirier [Sun, 17 May 2020 18:49:16 +0000 (11:49 -0700)]
Removed extraneous variable from 'ports=[..]' of main in bperm.py
colepoirier [Sun, 17 May 2020 18:41:52 +0000 (11:41 -0700)]
Applied PEP8 formatting to bperm.py
Luke Kenneth Casson Leighton [Sun, 17 May 2020 18:18:57 +0000 (19:18 +0100)]
test 32/64 bit mode CTR in branch
Luke Kenneth Casson Leighton [Sun, 17 May 2020 18:12:04 +0000 (19:12 +0100)]
add comments from spec on branch
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:47:21 +0000 (18:47 +0100)]
add instruction to assert statement so if there is an error the failed
insn is displayed
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:45:09 +0000 (18:45 +0100)]
rename nia_out to nia, clarify with variables in main_stage branch
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:43:55 +0000 (18:43 +0100)]
rename nia_out to just nia, we know it is an output
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:41:55 +0000 (18:41 +0100)]
add convenience name to branch main stage and branch output data
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:36:09 +0000 (18:36 +0100)]
bit of code-munging in branch main stage
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:26:09 +0000 (18:26 +0100)]
field cleanup
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:17:24 +0000 (18:17 +0100)]
whitespace cleanup
Luke Kenneth Casson Leighton [Sun, 17 May 2020 17:10:58 +0000 (18:10 +0100)]
simplify field access
Michael Nolan [Sun, 17 May 2020 17:12:32 +0000 (13:12 -0400)]
Add incomplete proof_bperm.py with comments on how to finish the proof
Michael Nolan [Sun, 17 May 2020 16:50:02 +0000 (12:50 -0400)]
Move perm inside Bpermd as it's not an input or output
Luke Kenneth Casson Leighton [Sun, 17 May 2020 16:33:40 +0000 (17:33 +0100)]
code-shuffle
Luke Kenneth Casson Leighton [Sun, 17 May 2020 16:24:44 +0000 (17:24 +0100)]
realised that the instruction fields have a namedtuple thing going on
Luke Kenneth Casson Leighton [Sun, 17 May 2020 16:15:58 +0000 (17:15 +0100)]
use slightly more elegant way to access CR lookup table
Luke Kenneth Casson Leighton [Sun, 17 May 2020 16:08:22 +0000 (17:08 +0100)]
use Cat(*list) on CR mask
Luke Kenneth Casson Leighton [Sun, 17 May 2020 14:21:06 +0000 (15:21 +0100)]
try lbzu