projects
/
soc.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
MUL pipeline formal proofs complete, I *think*.
2020-08-29
Samuel A. Falvo II
MUL pipeline formal proofs complete, I *think*.
commit
|
commitdiff
|
tree
2020-08-29
Samuel A. Falvo II
WIP: prep for 64-bit insns
commit
|
commitdiff
|
tree
2020-08-21
Samuel A. Falvo II
MUL pipeline WIP: mullw and mullwu covered.
commit
|
commitdiff
|
tree
2020-08-21
Samuel A. Falvo II
MUL pipeline: account for overflow flags. WIP
commit
|
commitdiff
|
tree
2020-08-21
Samuel A. Falvo II
MUL pipeline proofs: mulli / mullw WIP.
commit
|
commitdiff
|
tree
2020-08-20
Samuel A. Falvo II
MUL pipeline proof: muldw(u)
commit
|
commitdiff
|
tree
2020-08-20
Samuel A. Falvo II
MUL pipeline proof: signed mulhw
commit
|
commitdiff
|
tree
2020-08-19
Samuel A. Falvo II
WIP: OP_MUL proofs started.
commit
|
commitdiff
|
tree
2020-08-10
Samuel A. Falvo II
WIP!! Make MUL pipeline proof run again.
commit
|
commitdiff
|
tree
2020-08-04
Samuel A. Falvo II
Remove XXX; this seems done otherwise.
commit
|
commitdiff
|
tree
2020-08-03
Samuel A. Falvo II
WIP: check MB > ME and select mask appropriately
commit
|
commitdiff
|
tree
2020-07-31
Samuel A. Falvo II
WIP: more debugging signals for inspection
commit
|
commitdiff
|
tree
2020-07-30
Samuel A. Falvo II
WIP: rlwinm/rlwnm/rlwimi-type proofs
commit
|
commitdiff
|
tree
2020-07-26
Samuel A. Falvo II
MTMSR(D) properties.
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
Properties for MFMSR
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
Reorganize code layout
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
WIP: SC properties more closely match doc'd behavior
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
WIP: addressing code review, restoring proofs, etc.
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
Refactorin of common code
commit
|
commitdiff
|
tree
2020-07-24
Samuel A. Falvo II
Address code review comments
commit
|
commitdiff
|
tree
2020-07-22
Samuel A. Falvo II
Complete FV properties for OP_TRAP instructions.
commit
|
commitdiff
|
tree
2020-07-22
Samuel A. Falvo II
PEP8 compliance
commit
|
commitdiff
|
tree
2020-07-21
Samuel A. Falvo II
Completed SC FV properties
commit
|
commitdiff
|
tree
2020-07-21
Samuel A. Falvo II
Refine properties to comply with spec
commit
|
commitdiff
|
tree
2020-07-21
Samuel A. Falvo II
Fix where msr_i gets its value from
commit
|
commitdiff
|
tree
2020-07-21
Samuel A. Falvo II
Merge in recent updates to TRAP FV properties.
commit
|
commitdiff
|
tree
2020-07-20
Samuel A. Falvo II
Rework SC properties to conform to style
commit
|
commitdiff
|
tree
2020-07-20
Samuel A. Falvo II
Formal properties for RFID.
commit
|
commitdiff
|
tree
2020-07-18
Samuel A. Falvo II
WIP: FV failing for unknown reasons.
commit
|
commitdiff
|
tree
2020-07-18
Samuel A. Falvo II
Failing test: fast1/fast2 vs srr0/srr1? on trap pipe
commit
|
commitdiff
|
tree
2020-07-18
Samuel A. Falvo II
forgot to clean up workspace in source
commit
|
commitdiff
|
tree
2020-07-18
Samuel A. Falvo II
FV props for SC instruction
commit
|
commitdiff
|
tree
2020-07-17
Samuel A. Falvo II
First FV property for trap unit
commit
|
commitdiff
|
tree
2020-07-17
Samuel A. Falvo II
Flesh out SPR-related FV properties.
commit
|
commitdiff
|
tree
2020-07-14
Samuel A. Falvo II
SPR: FV that should fail currently passes
commit
|
commitdiff
|
tree