Commits · b6682ae85262a18332841e523d67fbc1aa0ee82e · sdram20 / coqdram

Apr 19, 2022
- 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
Nov 21, 2021
- Added TDM extraction · 2c58a150
  Felipe Lisboa authored 3 years ago
  
  2c58a150
Nov 20, 2021
- Minor fixes: functional with MCsim · 44f00d53
  Felipe Lisboa authored 3 years ago
  
  44f00d53
Nov 19, 2021
- Implemented the command interfacing part · b380a80b
  Felipe Lisboa authored 3 years ago
  
  b380a80b
Nov 18, 2021
- Renamed to just haskell_gencode · 4081c636
  Felipe Lisboa authored 3 years ago
  
  4081c636
- Changed Arbiter_trace_t to Implementation_t · 654b7bd9
  Felipe Lisboa authored 3 years ago
  
  654b7bd9
- Deleted printable version: can print directly with generated code · 0dff9182
  Felipe Lisboa authored 3 years ago
  
  0dff9182
Nov 15, 2021
- Fix: wrong enqueing order on next_state function · 03ae17db
  Felipe Lisboa authored 3 years ago
  
  03ae17db
Nov 14, 2021
- More modifications on the README files · d1d9f602
  Felipe Lisboa authored 3 years ago
  
  d1d9f602
- Fixed type on README file extension · 51247bfb
  Felipe Lisboa authored 3 years ago
  
  51247bfb
- Haskell extraction, printable version · 5e91ea7e
  Felipe Lisboa authored 3 years ago
  
  5e91ea7e
- Haskell extraction: c++ functional application · accb8140
  Felipe Lisboa authored 3 years ago
  
  accb8140
- Updated timing proofs: apart is now less equal and added some new proofs · 36e997e8
  Felipe Lisboa authored 3 years ago
  
  36e997e8
Oct 26, 2021
- Timing proof RRD completed · 93a4e769
  Felipe Lisboa authored 3 years ago
  
  93a4e769
Oct 12, 2021
- Merge branch 'master' of gitlab.enst.fr:florian.brandner/sdram · f9a8f672
  Felipe Lisboa authored 3 years ago
  
  f9a8f672
- WIP · 5d73e6cc
  Felipe Lisboa authored 3 years ago
  
  5d73e6cc
Oct 11, 2021
- TDM: restructure request proofs in order to get all command types · 8d33a8f1
  Florian Brandner authored 3 years ago
  
  8d33a8f1
- TDM: minor clean up in hypotheses · 60a00477
  Florian Brandner authored 3 years ago
  
  60a00477
- FIFO: speed-up make · e8a8e52f
  Florian Brandner authored 3 years ago
  
  e8a8e52f
- TDM/Util: basis proofs for request handling and timing constraints · 6966ff9b
  Florian Brandner authored 3 years ago
  
  * the timing proofs are incomplete, but should be easy to do (copy-paste) * add some helper proofs (mostly related to filtering/removing in lists)
  6966ff9b
- arbiter: fix indentation · 637f1bd9
  Florian Brandner authored 3 years ago
  
  637f1bd9
Oct 08, 2021
- Updated interface and implementations · 7b1c4897
  Felipe Lisboa authored 3 years ago
  
  7b1c4897
Jul 27, 2021
- Updated TDM policy · 149e7337
  Felipe Lisboa authored 3 years ago
  
  149e7337
Jul 19, 2021
- Added simple TDM arbiter · a128b8f0
  Felipe Lisboa authored 3 years ago
  
  a128b8f0
- Requestor_t is simply defined as a natural number · b3736c48
  Felipe Lisboa authored 3 years ago
  
  Requestor_t as an eqType and later instantiated as unit_eqType generated problems to operate it as a natural number. Hence, the change.
  b3736c48
Jul 08, 2021
- different interface for arbiter · fd572126
  Florian Brandner authored 3 years ago
  
  fd572126
May 26, 2021
- Fix: request instantiation on test section · d56a5b1b
  Felipe Lisboa authored 3 years ago
  
  d56a5b1b
May 21, 2021
- add ACT proof obligation on Trace · 01fe886e
  Felipe Lisboa authored 3 years ago
  
  01fe886e
- add requestor field as a nat · 457c089c
  Felipe Lisboa authored 3 years ago
  
  457c089c
May 19, 2021
- Added proof on PRE between two ACTS · ab89d648
  Felipe Lisboa authored 3 years ago
  
  ab89d648
- implement T_RRD and T_FAW constraints · a40c0b76
  Florian Brandner authored 3 years ago
  
  a40c0b76