aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
ModeNameSize
-rw-r--r--AbstractBasicBlocksDef.v14193logstatsplain
-rw-r--r--ForwardSimulationBlock.v13777logstatsplain
-rw-r--r--ImpSimuTest.v39585logstatsplain
-rw-r--r--InstructionScheduler.ml43158logstatsplain
-rw-r--r--InstructionScheduler.mli5109logstatsplain
-rw-r--r--Machblock.v14488logstatsplain
-rw-r--r--Machblockgen.v8040logstatsplain
-rw-r--r--Machblockgenproof.v29105logstatsplain
-rw-r--r--Parallelizability.v24715logstatsplain
-rw-r--r--PseudoAsmblock.v10235logstatsplain
-rw-r--r--PseudoAsmblockproof.v39030logstatsplain
-rw-r--r--README.md1721logstatsplain
-rw-r--r--RTLpath.v42570logstatsplain
-rw-r--r--RTLpathLivegen.v9814logstatsplain
-rw-r--r--RTLpathLivegenaux.ml10152logstatsplain
-rw-r--r--RTLpathLivegenproof.v27342logstatsplain
-rw-r--r--RTLpathSE_impl.v55383logstatsplain
-rw-r--r--RTLpathSE_simu_specs.v39444logstatsplain
-rw-r--r--RTLpathSE_theory.v77100logstatsplain
-rw-r--r--RTLpathScheduler.v12179logstatsplain
-rw-r--r--RTLpathScheduleraux.ml13010logstatsplain
-rw-r--r--RTLpathSchedulerproof.v12960logstatsplain
-rw-r--r--RTLpathproof.v1411logstatsplain
-rw-r--r--SeqSimuTheory.v13190logstatsplain
generated by cgit (git 2.34.1) at 2024-06-02 20:36:47 +0000