aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
* new OpWeightsDavid Monniaux2020-10-222-0/+25
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-182-7/+16
|\
| * centralize if_sameDavid Monniaux2020-10-091-6/+0
| * do not synthesize select if both operands are identicalDavid Monniaux2020-10-092-7/+22
* | update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
* | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-872/+0
* | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1655-11464/+859
|\ \
| * | so that all architectures compileDavid Monniaux2020-10-021-0/+1
| * | non pipelined units = none on KVXDavid Monniaux2020-09-301-1/+3
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-09-2923-769/+765
| |\|
| | * simpl -> cbnDavid Monniaux2020-09-2923-793/+789
| * | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-221-14/+0
| |\ \
| | * | reflect changesDavid Monniaux2020-09-221-14/+0
| * | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-212-272/+1
| |\| |
| | * | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-271/+0
| | |/
| | * use scheduler_by_nameDavid Monniaux2020-09-103-9/+11
| * | just missing OpWeights for AARCH64David Monniaux2020-09-1614-9446/+0
| * | starting to move common filesDavid Monniaux2020-09-1616-1651/+0
| * | Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-...David Monniaux2020-09-1012-222/+230
| |\ \
| | * | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash...David Monniaux2020-09-056-75/+117
| | |\|
| | | * fix issue 198 (incorrect reservation table for multiply-add)David Monniaux2020-09-021-5/+5
| | | * "nop" is not even printed out and thus uses no resourcesDavid Monniaux2020-09-011-13/+21
| | | * clean solution to close channelsDavid Monniaux2020-08-311-21/+24
| | | * fix problem with some file descriptors possibly never getting closedDavid Monniaux2020-08-311-4/+10
| | | * links to the impure library on githubSylvain Boulmé2020-07-311-1/+2
| | | * Improving Coqdoc on abstractbbSylvain Boulmé2020-07-314-46/+71
| * | | use with_destructorDavid Monniaux2020-09-102-20/+29
* | | | removing useless opt_simuSylvain Boulmé2020-10-133-36/+25
* | | | refactoring of RTLpathSE_impl.v (split with _simu_specs)Sylvain Boulmé2020-10-135-3911/+2086
* | | | remove the last tiny issue!Sylvain Boulmé2020-10-121-10/+3
* | | | simpl hsstate_simu_core_correctSylvain Boulmé2020-10-121-3/+1
* | | | fix one issue by generalizing RTLpathSE_theory.sstate_simuSylvain Boulmé2020-10-122-9/+18
* | | | move issue from hsexec_correct to hsstate_simu_core_correctSylvain Boulmé2020-10-121-14/+19
* | | | most of the proof is done ! two (small ?) issues remain...Sylvain Boulmé2020-10-121-30/+83
* | | | oops: forget to save before compile/commit/pushSylvain Boulmé2020-10-121-2/+5
* | | | end of merge with Cyril's proofSylvain Boulmé2020-10-122-59/+227
* | | | starting to merge with Cyril's proofSylvain Boulmé2020-10-111-48/+773
* | | | hconsing: full proof of hsiexec_path_correctSylvain Boulmé2020-10-102-42/+71
* | | | progress on hslocal_set_sreg_correctSylvain Boulmé2020-10-101-37/+53
* | | | progress on hsexec_inst_correct_dynSylvain Boulmé2020-10-101-39/+140
* | | | hconsing: red_PTree_set_correctSylvain Boulmé2020-10-091-0/+11
* | | | hconsing: root_happly_correct + simplify_correct DONESylvain Boulmé2020-10-094-15/+145
* | | | prove the kvx-test-prepass fix (commit 0e4186b8f)Sylvain Boulmé2020-10-081-14/+58
* | | | Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverifSylvain Boulmé2020-10-081-30/+29
|\ \ \ \
| * | | | prove the trick of simplify (as implemented in RTLpathSE_impl_junk)Sylvain Boulmé2020-08-271-18/+6
| * | | | prove that Mem.valid is preserved by symbolic execution of RTLpathSylvain Boulmé2020-08-271-12/+22
* | | | | Restart the proof with cherry-pick from Cyril and commit 0e4186b8fSylvain Boulmé2020-10-082-1795/+433
* | | | | update from kvx-test-prepass (commit 0e4186b8f)Sylvain Boulmé2020-10-081-4/+10
* | | | | Some theorem was wrongCyril SIX2020-09-301-4/+18
* | | | | Proof of hsok_local_set_sregCyril SIX2020-09-301-4/+25
generated by cgit (git 2.34.1) at 2024-06-02 21:57:05 +0000