-
- Downloads
Make cores explicit in ProcessorState
- Added unfolding lemmas to basic_facts/ideal - Fixed proofs depending on the previous definition using unfolding lemmas The changes follow the discussion in Paris.
Showing
- restructuring/analysis/abstract/core/abstract_seq_rta.v 171 additions, 171 deletionsrestructuring/analysis/abstract/core/abstract_seq_rta.v
- restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v 43 additions, 56 deletions...re/sufficient_condition_for_run_to_completion_threshold.v
- restructuring/analysis/basic_facts/ideal_schedule.v 35 additions, 7 deletionsrestructuring/analysis/basic_facts/ideal_schedule.v
- restructuring/analysis/basic_facts/service_of_jobs.v 50 additions, 51 deletionsrestructuring/analysis/basic_facts/service_of_jobs.v
- restructuring/analysis/transform/facts/edf_opt.v 31 additions, 28 deletionsrestructuring/analysis/transform/facts/edf_opt.v
- restructuring/behavior/schedule.v 24 additions, 7 deletionsrestructuring/behavior/schedule.v
- restructuring/model/processor/ideal.v 9 additions, 3 deletionsrestructuring/model/processor/ideal.v
- restructuring/model/processor/multiprocessor.v 1 addition, 1 deletionrestructuring/model/processor/multiprocessor.v
- restructuring/model/processor/spin.v 7 additions, 3 deletionsrestructuring/model/processor/spin.v
- restructuring/model/processor/varspeed.v 7 additions, 4 deletionsrestructuring/model/processor/varspeed.v
Loading
Please register or sign in to comment