aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* builtins pour signed div/modDavid Monniaux2022-02-161-0/+88
* Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_divisionDavid Monniaux2022-02-141-1/+53
|\
| * abs builtinsDavid Monniaux2022-02-141-1/+54
* | modulosDavid Monniaux2022-02-111-0/+44
* | remove singleoflongu (does not exist)David Monniaux2022-02-111-0/+22
* | fpdivuDavid Monniaux2021-12-171-1/+26
* | fix assembly syntaxDavid Monniaux2021-12-121-0/+8
|/
* generate insfDavid Monniaux2021-09-271-32/+32
* more cases detectedDavid Monniaux2021-09-271-1/+33
* recognize insf (missing one case)David Monniaux2021-09-271-0/+23
* Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1David Monniaux2021-09-171-3/+105
* replacing omega with lia in some fileLéo Gourdin2021-03-291-18/+19
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+9
|\
| * centralize if_sameDavid Monniaux2020-10-091-6/+0
| * do not synthesize select if both operands are identicalDavid Monniaux2020-10-091-0/+15
* | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-281-1/+0
|/
* k1c -> kvx changesDavid Monniaux2020-05-261-0/+1735