Luke Kenneth Casson Leighton [Wed, 27 May 2020 15:49:36 +0000 (16:49 +0100)]
remove XER.ca from logical Input Data - not needed
Luke Kenneth Casson Leighton [Wed, 27 May 2020 15:40:18 +0000 (16:40 +0100)]
cleanup logical main proof
Luke Kenneth Casson Leighton [Wed, 27 May 2020 15:27:51 +0000 (16:27 +0100)]
check cr0, ov and ca ok signals in ALU main_stage proof
Luke Kenneth Casson Leighton [Wed, 27 May 2020 15:19:31 +0000 (16:19 +0100)]
add carry-out, overflow and cr0 ok setting in ALU main_stage
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:48:40 +0000 (15:48 +0100)]
add SRR0 to TrapInputData
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:35:09 +0000 (15:35 +0100)]
add links to bugreports into ALu formal proof as well
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:34:01 +0000 (15:34 +0100)]
add links to bugreports into alu output stage proof
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:28:30 +0000 (15:28 +0100)]
check reg output Data.ok in shift_rot formal proof
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:16:43 +0000 (15:16 +0100)]
rename CROutputData.cr_o to just CROutputData.cr
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:15:14 +0000 (15:15 +0100)]
test Data.ok for cr output and full cr output
Luke Kenneth Casson Leighton [Wed, 27 May 2020 14:10:00 +0000 (15:10 +0100)]
assign and test on Data, TODO add Data.ok checking in CR proof
Michael Nolan [Wed, 27 May 2020 14:00:57 +0000 (10:00 -0400)]
Fix bug in alu main stage proof
Cesar Strauss [Wed, 27 May 2020 10:06:37 +0000 (07:06 -0300)]
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.
Tobias Platen [Wed, 27 May 2020 09:27:19 +0000 (11:27 +0200)]
Merge branch 'master' of ssh://git.libre-riscv.org:922/soc
Tobias Platen [Wed, 27 May 2020 09:27:06 +0000 (11:27 +0200)]
elaborate function for DataMerger
Cesar Strauss [Wed, 27 May 2020 09:23:58 +0000 (06:23 -0300)]
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.
Luke Kenneth Casson Leighton [Wed, 27 May 2020 02:45:40 +0000 (03:45 +0100)]
make power function unit enum bitmasked
Luke Kenneth Casson Leighton [Wed, 27 May 2020 00:40:34 +0000 (01:40 +0100)]
add extra INT regs port for now, add Fast Regfile
Luke Kenneth Casson Leighton [Wed, 27 May 2020 00:34:31 +0000 (01:34 +0100)]
added XER and CR regfiles, using new VirtualRegPort
Luke Kenneth Casson Leighton [Tue, 26 May 2020 23:47:53 +0000 (00:47 +0100)]
check assertions
Luke Kenneth Casson Leighton [Tue, 26 May 2020 23:40:02 +0000 (00:40 +0100)]
make read/write regs properly internal
Luke Kenneth Casson Leighton [Tue, 26 May 2020 23:14:07 +0000 (00:14 +0100)]
add VirtualRegPort test, seems to demonstrate it working
Luke Kenneth Casson Leighton [Tue, 26 May 2020 22:24:16 +0000 (23:24 +0100)]
remove sync (not needed)
Luke Kenneth Casson Leighton [Tue, 26 May 2020 22:17:18 +0000 (23:17 +0100)]
get score6600_multi.py working again
Luke Kenneth Casson Leighton [Tue, 26 May 2020 22:02:47 +0000 (23:02 +0100)]
redo focus of virtual reg port to do only full datawidth not share with mini-regs
Michael Nolan [Tue, 26 May 2020 18:03:30 +0000 (14:03 -0400)]
Add extras from bottom of the file
Michael Nolan [Tue, 26 May 2020 17:33:19 +0000 (13:33 -0400)]
Rewrite proof to be more in line with what appears in the wiki
Luke Kenneth Casson Leighton [Tue, 26 May 2020 15:54:33 +0000 (16:54 +0100)]
sort-of (maybe) implemented a virtual port on top of RegFileArray.
needs checking
Luke Kenneth Casson Leighton [Tue, 26 May 2020 15:03:58 +0000 (16:03 +0100)]
try new variant of VirtualRegFile
Luke Kenneth Casson Leighton [Tue, 26 May 2020 12:45:58 +0000 (13:45 +0100)]
use nmutil treereduce
Luke Kenneth Casson Leighton [Tue, 26 May 2020 11:44:18 +0000 (12:44 +0100)]
continue virtual regfile port
Luke Kenneth Casson Leighton [Tue, 26 May 2020 11:43:57 +0000 (12:43 +0100)]
whitespace, add commentary
colepoirier [Tue, 26 May 2020 01:04:37 +0000 (18:04 -0700)]
First attempt at implementing block access rd and wr regfile port onto
an array-based regfile
Cesar Strauss [Mon, 25 May 2020 22:50:32 +0000 (19:50 -0300)]
Check that busy_o doesn't rise on its own
Cesar Strauss [Mon, 25 May 2020 22:28:43 +0000 (19:28 -0300)]
Implement the issue_i/busy_o protocol check.
It will timeout, until the rel/go signals are implemented.
Cesar Strauss [Mon, 25 May 2020 19:11:03 +0000 (16:11 -0300)]
Move process list to CompUnitParallelTest
The process list (implementation detail) is best left for the class.
Michael Nolan [Mon, 25 May 2020 19:11:32 +0000 (15:11 -0400)]
Correct polarity of shadow signal
Luke Kenneth Casson Leighton [Mon, 25 May 2020 19:00:45 +0000 (20:00 +0100)]
document shadown inversion
Michael Nolan [Mon, 25 May 2020 18:53:49 +0000 (14:53 -0400)]
Add link to compunit wiki page
Michael Nolan [Mon, 25 May 2020 18:47:58 +0000 (14:47 -0400)]
Correct property numbers, add assertions about busy
Luke Kenneth Casson Leighton [Mon, 25 May 2020 18:45:55 +0000 (19:45 +0100)]
update comments on compalu_multi.py
Michael Nolan [Mon, 25 May 2020 18:28:42 +0000 (14:28 -0400)]
Add assertions about go_wr and wr_rel
Michael Nolan [Mon, 25 May 2020 18:12:01 +0000 (14:12 -0400)]
Minor cleanup of comments
Michael Nolan [Mon, 25 May 2020 18:10:54 +0000 (14:10 -0400)]
Minor changes to alu_hier.py to allow it to be used in proof
Michael Nolan [Mon, 25 May 2020 18:08:20 +0000 (14:08 -0400)]
Begin working on proof for compunit/fu
Luke Kenneth Casson Leighton [Mon, 25 May 2020 15:28:30 +0000 (16:28 +0100)]
add some more stub comments
Luke Kenneth Casson Leighton [Mon, 25 May 2020 15:24:50 +0000 (16:24 +0100)]
yield blank so test passes
Luke Kenneth Casson Leighton [Mon, 25 May 2020 15:24:10 +0000 (16:24 +0100)]
add stubs
Luke Kenneth Casson Leighton [Mon, 25 May 2020 15:21:40 +0000 (16:21 +0100)]
add comments
Cesar Strauss [Mon, 25 May 2020 15:07:15 +0000 (12:07 -0300)]
Fix detection of busy_o inside the monitor process
Found the bug literally seconds after pushing...
Cesar Strauss [Mon, 25 May 2020 14:53:42 +0000 (11:53 -0300)]
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.
Tobias Platen [Mon, 25 May 2020 14:31:15 +0000 (16:31 +0200)]
fix own copy/paste error
Tobias Platen [Mon, 25 May 2020 14:29:39 +0000 (16:29 +0200)]
whitespace fix in docstring
Luke Kenneth Casson Leighton [Mon, 25 May 2020 14:24:31 +0000 (15:24 +0100)]
correct links in regfile docstring
Luke Kenneth Casson Leighton [Mon, 25 May 2020 14:13:16 +0000 (15:13 +0100)]
document regfiles
Luke Kenneth Casson Leighton [Mon, 25 May 2020 13:54:06 +0000 (14:54 +0100)]
argh! frickin MACos terminal expanded out to 86x30 not 80x30
Luke Kenneth Casson Leighton [Mon, 25 May 2020 13:52:40 +0000 (14:52 +0100)]
add docstring
Luke Kenneth Casson Leighton [Mon, 25 May 2020 13:43:15 +0000 (14:43 +0100)]
add INT, SPR and CR regfiles
Tobias Platen [Mon, 25 May 2020 13:41:49 +0000 (15:41 +0200)]
refactoring (see #216 Comment 43)
Tobias Platen [Mon, 25 May 2020 13:03:54 +0000 (15:03 +0200)]
whitespace changes
Luke Kenneth Casson Leighton [Mon, 25 May 2020 11:44:38 +0000 (12:44 +0100)]
quick addition of zero+immed test to LDSTCompUnit
Luke Kenneth Casson Leighton [Mon, 25 May 2020 10:43:28 +0000 (11:43 +0100)]
must not do rd-req checking when both imm and zero mode are enabled
Tobias Platen [Mon, 25 May 2020 09:47:00 +0000 (11:47 +0200)]
implement DataMerger interface
Luke Kenneth Casson Leighton [Mon, 25 May 2020 03:43:56 +0000 (04:43 +0100)]
add zero immed on LDST, untested
Luke Kenneth Casson Leighton [Mon, 25 May 2020 02:26:46 +0000 (03:26 +0100)]
comment out invalid test
Luke Kenneth Casson Leighton [Mon, 25 May 2020 02:23:10 +0000 (03:23 +0100)]
lots of greater than 80 chars
Luke Kenneth Casson Leighton [Mon, 25 May 2020 02:19:20 +0000 (03:19 +0100)]
switch out req rel if immediate enabled
Cesar Strauss [Mon, 25 May 2020 00:40:52 +0000 (21:40 -0300)]
Show oper_r and oper_i in the signal list, in simulation
Luke Kenneth Casson Leighton [Mon, 25 May 2020 00:11:49 +0000 (01:11 +0100)]
mention zeroing
Luke Kenneth Casson Leighton [Mon, 25 May 2020 00:09:54 +0000 (01:09 +0100)]
add links to pseudocode
Luke Kenneth Casson Leighton [Sun, 24 May 2020 23:58:19 +0000 (00:58 +0100)]
spelling
Luke Kenneth Casson Leighton [Sun, 24 May 2020 23:55:52 +0000 (00:55 +0100)]
spelling
Luke Kenneth Casson Leighton [Sun, 24 May 2020 22:00:59 +0000 (23:00 +0100)]
add comments for SPR pipe_data
Luke Kenneth Casson Leighton [Sun, 24 May 2020 21:43:27 +0000 (22:43 +0100)]
add SPR pipe_data.py
Luke Kenneth Casson Leighton [Sun, 24 May 2020 20:57:32 +0000 (21:57 +0100)]
over 80 char limit
Luke Kenneth Casson Leighton [Sun, 24 May 2020 20:46:56 +0000 (21:46 +0100)]
add test of reg output, for MFCRF and ISEL
Cesar Strauss [Sun, 24 May 2020 19:48:46 +0000 (16:48 -0300)]
Avoid overwriting the first vcd file with the second one
Cesar Strauss [Sun, 24 May 2020 19:44:12 +0000 (16:44 -0300)]
Rename the internal DFF of latchregisters to avoid conflict
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:47:53 +0000 (20:47 +0100)]
add gitignore for branch fu formal
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:23:54 +0000 (20:23 +0100)]
add OP_CMPB formal proof
Michael Nolan [Sun, 24 May 2020 19:16:28 +0000 (15:16 -0400)]
Assert that ctr is only written when needed
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:17:36 +0000 (20:17 +0100)]
split out Popcount into separate module: visually it interferes with readability of the fu logical main stage graphviz
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:05:55 +0000 (20:05 +0100)]
copy code for MTMSR from microwatt into comments
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:01:56 +0000 (20:01 +0100)]
add links for trap main stage
Luke Kenneth Casson Leighton [Sun, 24 May 2020 19:00:07 +0000 (20:00 +0100)]
add untested OP_MTMSR and OP_MFMSR
Luke Kenneth Casson Leighton [Sun, 24 May 2020 18:53:38 +0000 (19:53 +0100)]
update to new CSV files in submodule
Luke Kenneth Casson Leighton [Sun, 24 May 2020 18:49:30 +0000 (19:49 +0100)]
add MFMSR and MTMSRD enums to Function
Luke Kenneth Casson Leighton [Sun, 24 May 2020 18:30:56 +0000 (19:30 +0100)]
comment and add links to branch formal proof
Luke Kenneth Casson Leighton [Sun, 24 May 2020 18:20:18 +0000 (19:20 +0100)]
add copy of bpermd proof to logical formal proof (not nice but hey)
Luke Kenneth Casson Leighton [Sun, 24 May 2020 17:58:02 +0000 (18:58 +0100)]
track down overwrite of variable b
Michael Nolan [Sun, 24 May 2020 15:17:12 +0000 (11:17 -0400)]
Fix proof of bpermd module
Michael Nolan [Sun, 24 May 2020 15:15:54 +0000 (11:15 -0400)]
Fix bpermd and make tests pass
Michael Nolan [Sun, 24 May 2020 15:15:14 +0000 (11:15 -0400)]
Fix test_pipe_caller to conform to new Data() interface on outputs
Luke Kenneth Casson Leighton [Sun, 24 May 2020 15:05:00 +0000 (16:05 +0100)]
add stub regfiles.py
Luke Kenneth Casson Leighton [Sun, 24 May 2020 14:00:03 +0000 (15:00 +0100)]
hmm...
Luke Kenneth Casson Leighton [Sun, 24 May 2020 13:54:41 +0000 (14:54 +0100)]
add very rapid DummyALU for test purposes in MultiCompUnit
Luke Kenneth Casson Leighton [Sun, 24 May 2020 13:47:20 +0000 (14:47 +0100)]
comments on branch pipeline
Luke Kenneth Casson Leighton [Sun, 24 May 2020 13:36:28 +0000 (14:36 +0100)]
convert CR pipeline to Data.ok
Luke Kenneth Casson Leighton [Sun, 24 May 2020 13:07:02 +0000 (14:07 +0100)]
convert ALU to output Data on int reg
Luke Kenneth Casson Leighton [Sun, 24 May 2020 13:01:28 +0000 (14:01 +0100)]
convert logical to output Data on int reg