aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/ExtValues.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-301-0/+94
|\
| * standardize semantics, 1David Monniaux2019-05-121-1/+7
| * apply .xs onto addx4 etcDavid Monniaux2019-05-111-1/+4
| * add with shift, beginningDavid Monniaux2019-05-111-0/+24
| * generate multiply-sub longDavid Monniaux2019-05-111-1/+32
| * Pmsub compiledDavid Monniaux2019-05-111-0/+16
| * use shift 1-4 in backendDavid Monniaux2019-05-101-0/+14
* | detailDavid Monniaux2019-05-151-1/+1
* | more lemmas on divisionDavid Monniaux2019-05-151-0/+48
* | more lemmas on divisionDavid Monniaux2019-05-151-1/+55
* | some lemmas on division etc.David Monniaux2019-05-141-0/+258
* | 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-131-0/+36
* | we directly call 64-bit unsigned divisionDavid Monniaux2019-05-131-1/+1
* | begin proving that we can use 64-bit division for doing 32David Monniaux2019-05-131-0/+64
|/
* Srsd / SrswDavid Monniaux2019-04-291-0/+18
* detect insf case, beginDavid Monniaux2019-04-281-4/+11
* compute the highest bit in a numberDavid Monniaux2019-04-271-0/+10
* add bitfield insert opcode but not yet used nor translatedDavid Monniaux2019-04-271-4/+10
* more base operators on bitfieldDavid Monniaux2019-04-271-0/+19
* factor expressions into single fileDavid Monniaux2019-04-271-12/+14
* moved operators to specific file instead of common fileDavid Monniaux2019-04-271-0/+57
generated by cgit (git 2.34.1) at 2024-07-04 12:52:32 +0000