Commits · 52dd50048bd0281d76a13b207fcd6926f55bd22e · sdram20 / coqdram

Sep 08, 2022
- DDR4: adapting proofs to DDR4 modification · 52dd5004
  Felipe Lisboa authored 2 years ago
  
  52dd5004
- DDR4: updating trace & proofs · 58b06e84
  Felipe Lisboa authored 2 years ago
  
  58b06e84
Sep 02, 2022
- simulating the cava fifo state machine works · 24fd59b5
  Felipe Lisboa authored 2 years ago
  
  24fd59b5
- Changed README · 2e74acbc
  Felipe Lisboa authored 2 years ago
  
  2e74acbc
- Fix: Default_arbitrate definition does not need a Program command · 09096359
  Felipe Lisboa authored 2 years ago
  
  09096359
- Remove unused Lemma in Util.v · 83c51d8a
  Felipe Lisboa authored 2 years ago
  
  83c51d8a
- removing makefiles from git: these are generated files · 33d6fea5
  Felipe Lisboa authored 2 years ago
  
  33d6fea5
- Non-standard README · 91b264a9
  Felipe Lisboa authored 2 years ago
  
  91b264a9
- Finished TDM proofs · 6f055770
  Felipe Lisboa authored 2 years ago
  
  6f055770
Sep 01, 2022
- Added README · 49913204
  Felipe Lisboa authored 2 years ago
  
  49913204
- Cleanup: deleted early efforts · 9d0ca556
  Felipe Lisboa authored 2 years ago
  
  9d0ca556
- Merge branch 'master' of gitlab.enst.fr:florian.brandner/sdram · 44076c67
  Felipe Lisboa authored 2 years ago
  
  44076c67
- Upload local changes: TDM proofs, Cava Development, Haskell Code Generation · f5e41ddd
  Felipe Lisboa authored 2 years ago
  
  f5e41ddd
Aug 31, 2022
- Add LICENSE · 5b093ff2
  Felipe Lisboa Malaquias authored 2 years ago
  
  5b093ff2
May 27, 2022
- Trimed whitespace · 877bac94
  Felipe Lisboa authored 2 years ago
  
  877bac94
- Functional FIFO: a first design · 0a014df8
  Felipe Lisboa authored 2 years ago
  
  0a014df8
May 08, 2022
- Added submodule: Modified MCsim · 9626d510
  Felipe Lisboa authored 2 years ago
  
  9626d510
May 04, 2022
- TDM: new proofs · a68b7503
  Felipe Lisboa authored 2 years ago
  
  a68b7503
- TDM: separe test section · f196db6e
  Felipe Lisboa authored 2 years ago
  
  f196db6e
May 01, 2022
- Minor changes: some empty space correction & fix TDM build · ee8cbe1a
  Felipe Lisboa authored 2 years ago
  
  ee8cbe1a
Apr 26, 2022
- Added submodule to the project · 57c49f84
  Felipe Lisboa authored 2 years ago
  
  57c49f84
Apr 25, 2022
- Cava model: first version compiles · 29d1d21b
  Felipe Lisboa authored 2 years ago
  
  29d1d21b
Apr 20, 2022
- Restored README · ac1e2a60
  Felipe Lisboa authored 2 years ago
  
  ac1e2a60
- Moved README · 6fa7bcd1
  Felipe Lisboa authored 2 years ago
  
  6fa7bcd1
- fixed build list and readme · 09d7c90a
  Felipe Lisboa authored 2 years ago
  
  09d7c90a
- Changed file structure for TDM · 01e3c840
  Felipe Lisboa authored 2 years ago
  
  01e3c840
- wip: developed a few new components for the fifo circuit · 8ee23821
  Felipe Lisboa authored 2 years ago
  
  8ee23821
Apr 19, 2022
- Trimmed whitespace · 2362f5b0
  Felipe Lisboa authored 2 years ago
  
  2362f5b0
- dev cava model: more components added · 5d980934
  Felipe Lisboa authored 2 years ago
  
  5d980934
- Renamed FIFO & TDM Extraction Files · a10519d5
  Felipe Lisboa authored 2 years ago
  
  a10519d5
- Cava Counter_t · b6682ae8
  Felipe Lisboa authored 2 years ago
  
  b6682ae8
- FIFO: renamed the extraction files and some minor modifications on the... · 4e102a0e
  Felipe Lisboa authored 2 years ago
  
  FIFO: renamed the extraction files and some minor modifications on the implementation, proofs and simulation
  4e102a0e
Mar 28, 2022
- FIFO: finished all proofs · 0c982794
  Felipe Lisboa authored 2 years ago
  
  0c982794
Mar 22, 2022
- Refactoring: DDR3 and DDR4 separation, exclusive proof file for arbiters · 0f5cf826
  Felipe Lisboa authored 2 years ago
  
  0f5cf826
Mar 07, 2022
- Minor modifications Trace_t: rewrote some POs · 186e61f6
  Felipe Lisboa authored 3 years ago
  
  186e61f6
Jan 21, 2022
- TDM refactoring · 59758d99
  Felipe Lisboa authored 3 years ago
  
  59758d99
Jan 20, 2022
- Re-introduced proof about time: needed for TDM · 1f600b8a
  Felipe Lisboa authored 3 years ago
  
  1f600b8a
Jan 17, 2022
- Default_arbitrate / new POs / DDR4 refactoring · 998c518a
  Felipe Lisboa authored 3 years ago
  
  998c518a
- Refresh proofs: incomplete · e6e9e1a7
  Felipe Lisboa authored 3 years ago
  
  e6e9e1a7
Dec 10, 2021
- coq3: Implemented refresh, additional proof obligations, reworked... · 1fa7cb43
  Felipe Lisboa authored 3 years ago
  
  coq3: Implemented refresh, additional proof obligations, reworked default_arbitration and DDR4 support
  1fa7cb43