projects / soc.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add proof for RegFile
[soc.git] / src /
2020-06-01 Michael NolanAdd proof for RegFile tree | commitdiff
2020-06-01 Luke Kenneth Casso... more unneeded fields from SR InputRecord tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove data_len from SR input record tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove zero/invert from ShiftRot Input Record tree | commitdiff
2020-06-01 Luke Kenneth Casso... add shift-rot input record and use it tree | commitdiff
2020-06-01 Luke Kenneth Casso... CompBROpSubset exists tree | commitdiff
2020-06-01 Luke Kenneth Casso... RS moved to port 1 (from port 3), remove need in ALU... tree | commitdiff
2020-06-01 Michael NolanAdd proof for RegFileArray tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove use of reg3 in logical pipeline: CSV files moved... tree | commitdiff
2020-06-01 Michael NolanHave regfile use AnySeq instead of AnyConst tree | commitdiff
2020-06-01 Luke Kenneth Casso... rotator carry is set into both XER CA and CA32 fields tree | commitdiff
2020-06-01 Luke Kenneth Casso... comment out rlwinm. for now tree | commitdiff
2020-06-01 Luke Kenneth Casso... argh - need to zero the src_i input after "Read" is... tree | commitdiff
2020-06-01 Michael NolanEnable k-induction for register file proof tree | commitdiff
2020-06-01 Michael NolanThat was weird. For some reason it wasn't generating... tree | commitdiff
2020-06-01 Michael NolanFull BMC proof of Register tree | commitdiff
2020-06-01 Michael NolanBegin rewrite of proof_regfile.py tree | commitdiff
2020-06-01 Luke Kenneth Casso... put RB in 2nd position (matching immediate) in ShiftRot... tree | commitdiff
2020-06-01 Luke Kenneth Casso... sigh - another instance where write-mask needed to... tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove xer so/ov, swap rs/rb to correct(?) order in... tree | commitdiff
2020-06-01 Tobias Platenproof_datamerger wip tree | commitdiff
2020-06-01 Luke Kenneth Casso... add rlwinm. test instruction (sets CR0) tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove duplicate signal tree | commitdiff
2020-06-01 Luke Kenneth Casso... allow ALU / Logical ops to select RS as 1st operand tree | commitdiff
2020-06-01 Luke Kenneth Casso... allow M*-Form shiftrot to swap RS/RB back to consistent... tree | commitdiff
2020-06-01 Luke Kenneth Casso... add first version of ShiftRot CompUnit test tree | commitdiff
2020-06-01 Luke Kenneth Casso... shiftrot uses LogicalOutputData not ALUOutputData tree | commitdiff
2020-06-01 Cesar StraussAdd rdmaskn parameter and assert it along issue_i tree | commitdiff
2020-06-01 Luke Kenneth Casso... add assertions for branch compunit output tree | commitdiff
2020-06-01 Luke Kenneth Casso... invert SPR1/2 in branch output data tree | commitdiff
2020-06-01 Luke Kenneth Casso... decode SPRs for branch tree | commitdiff
2020-06-01 Luke Kenneth Casso... swap over SPR1/2 to fit with microwatt SPR conventions tree | commitdiff
2020-06-01 Luke Kenneth Casso... add first version compunit branch test tree | commitdiff
2020-06-01 Luke Kenneth Casso... whoops need to read RS in CR inputs test tree | commitdiff
2020-06-01 Luke Kenneth Casso... add first version of CR CompUnit test tree | commitdiff
2020-06-01 Luke Kenneth Casso... minor adjustment, zero test in ALU output stage tree | commitdiff
2020-06-01 Luke Kenneth Casso... remove unneeded code tree | commitdiff
2020-05-31 Luke Kenneth Casso... bit-test on the function-unit value being tested tree | commitdiff
2020-05-31 Luke Kenneth Casso... add logical compunit test tree | commitdiff
2020-05-31 Luke Kenneth Casso... comment inputs and outputs from ALU unit test tree | commitdiff
2020-05-31 Luke Kenneth Casso... imports - use of globals. baaaad tree | commitdiff
2020-05-31 Luke Kenneth Casso... remove unneeded code and inputs. convert to "naming... tree | commitdiff
2020-05-31 Luke Kenneth Casso... split out common code from test_alu_compunit.py tree | commitdiff
2020-05-31 Luke Kenneth Casso... add comments for MultiCompUnit parallel test tree | commitdiff
2020-05-31 Luke Kenneth Casso... de-hard-code-ify getting results from MultiCompUnit tree | commitdiff
2020-05-31 Luke Kenneth Casso... remove unneeded imports tree | commitdiff
2020-05-31 Luke Kenneth Casso... split out compalu unit tests to separate module (gettin... tree | commitdiff
2020-05-31 Luke Kenneth Casso... HA! found a bug in MultiCompUnit handling of write... tree | commitdiff
2020-05-31 Luke Kenneth Casso... clarify tree | commitdiff
2020-05-31 Luke Kenneth Casso... OP_CMPEQB also requesting change of output reg (stop... tree | commitdiff
2020-05-31 Luke Kenneth Casso... OP_CMP is requesting a change of the output register... tree | commitdiff
2020-05-31 Luke Kenneth Casso... still investigating tree | commitdiff
2020-05-31 Luke Kenneth Casso... start with zero, try not to compare against 9 bytes... tree | commitdiff
2020-05-31 Luke Kenneth Casso... more debug statements tree | commitdiff
2020-05-31 Luke Kenneth Casso... add in more CR debug statements tree | commitdiff
2020-05-31 Luke Kenneth Casso... copy in cr0.data into cr0 temp, not whole of cr0 (inclu... tree | commitdiff
2020-05-31 Luke Kenneth Casso... remove commented-out vars from ALU input record tree | commitdiff
2020-05-31 Luke Kenneth Casso... write cr0 when op.write_cr.ok is set tree | commitdiff
2020-05-31 Luke Kenneth Casso... add write_cr to ALU record subset tree | commitdiff
2020-05-31 Luke Kenneth Casso... comment out xer ov/so for now tree | commitdiff
2020-05-30 Luke Kenneth Casso... get carry from cr write_cr tree | commitdiff
2020-05-30 Luke Kenneth Casso... select CR0 write out only when RC=1 tree | commitdiff
2020-05-30 Luke Kenneth Casso... set CR0 output when OP_CMP or OP_CMPEQB need it tree | commitdiff
2020-05-30 Luke Kenneth Casso... add in use of "Settle" tree | commitdiff
2020-05-30 Luke Kenneth Casso... add in write-mask into MultiCompUnit and MCU-ALU unit... tree | commitdiff
2020-05-30 Tobias PlatenMerge branch 'master' of ssh://git.libre-riscv.org... tree | commitdiff
2020-05-30 Tobias Platenunit test for DataMerger tree | commitdiff
2020-05-30 Luke Kenneth Casso... create read-mask for ALU CompUnit: switches off optiona... tree | commitdiff
2020-05-30 Luke Kenneth Casso... create a write-mask, anything with an "ok" in the Recor... tree | commitdiff
2020-05-30 Luke Kenneth Casso... allow MultiCompUnit outputs to be Records, to capture... tree | commitdiff
2020-05-30 Luke Kenneth Casso... add read-mask to MultiCompUnit tree | commitdiff
2020-05-30 Luke Kenneth Casso... code-shuffle / comments tree | commitdiff
2020-05-30 Luke Kenneth Casso... mess - but a functional mess. ALU-MultiCompUnit semi... tree | commitdiff
2020-05-30 Luke Kenneth Casso... grab other results from ALU pipeline in compunit test tree | commitdiff
2020-05-30 Luke Kenneth Casso... order of XER so/ca wrong way round from regspec tree | commitdiff
2020-05-30 Luke Kenneth Casso... still experimenting with ALU-CompUnit interaction tree | commitdiff
2020-05-29 Luke Kenneth Casso... interesting. use of Settle() works, showing that Regfi... tree | commitdiff
2020-05-29 Luke Kenneth Casso... module comments for popcount tree | commitdiff
2020-05-29 Luke Kenneth Casso... comments on popcount tree | commitdiff
2020-05-29 Luke Kenneth Casso... trigger ALU ready when operands ready tree | commitdiff
2020-05-29 Tobias Platenfixes for DataMerger tree | commitdiff
2020-05-29 Luke Kenneth Casso... trigger read ALU ready/valid from latch as well tree | commitdiff
2020-05-29 Luke Kenneth Casso... use a latch to communicate read/valid output from ALU tree | commitdiff
2020-05-29 Tobias PlatenDataMerger: rename addr_match_i to addr_array_i tree | commitdiff
2020-05-29 Tobias Platenfixed 'return m is missing' tree | commitdiff
2020-05-29 Tobias Platenwhitespace fixes tree | commitdiff
2020-05-29 Luke Kenneth Casso... latch all output on ALU output valid tree | commitdiff
2020-05-29 Luke Kenneth Casso... create read-done pulse tree | commitdiff
2020-05-29 Luke Kenneth Casso... write-release moves out of "ALU valid" due to using... tree | commitdiff
2020-05-29 Luke Kenneth Casso... signal start of request from when ALU triggers result... tree | commitdiff
2020-05-29 Luke Kenneth Casso... create rising pulse from ALU valid tree | commitdiff
2020-05-29 Luke Kenneth Casso... names of attributes needs to be dest_o not dest_i tree | commitdiff
2020-05-29 Luke Kenneth Casso... rename output signals in Test ALU tree | commitdiff
2020-05-29 Cesar StraussAllow immediate assertion of go in the same cycle as rel tree | commitdiff
2020-05-29 Cesar StraussCorrect typo tree | commitdiff
2020-05-29 Cesar StraussSend a one-clock "go" pulse after a configurable number... tree | commitdiff
2020-05-28 Luke Kenneth Casso... messing about with proof_regfile.py tree | commitdiff
2020-05-28 Luke Kenneth Casso... move simple_popcount out of class (does not use any... tree | commitdiff
2020-05-28 colepoirierAdded Initial() synchronous check with draft truth tree | commitdiff
2020-05-28 Luke Kenneth Casso... extra check on rd.req in test_alu_compunit tree | commitdiff
next