Commits · b3736c48b7efd5de35558f0acf102cfac303c496 · sdram20 / coqdram · GitLab

Snippets Groups Projects

Jul 19, 2021
- Requestor_t is simply defined as a natural number · b3736c48
  Felipe Lisboa authored Jul 19, 2021
  b3736c48
Jul 08, 2021
- different interface for arbiter · fd572126
  Florian Brandner authored Jul 8, 2021
  
  fd572126
May 26, 2021
- Fix: request instantiation on test section · d56a5b1b
  Felipe Lisboa authored May 26, 2021
  
  d56a5b1b
May 21, 2021
- add ACT proof obligation on Trace · 01fe886e
  Felipe Lisboa authored May 21, 2021
  
  01fe886e
- add requestor field as a nat · 457c089c
  Felipe Lisboa authored May 21, 2021
  
  457c089c
May 19, 2021
- Added proof on PRE between two ACTS · ab89d648
  Felipe Lisboa authored May 19, 2021
  
  ab89d648
- implement T_RRD and T_FAW constraints · a40c0b76
  Florian Brandner authored May 19, 2021
  
  a40c0b76
May 18, 2021
- replacing the word -cmd- for CAS where it refers to the CAS command · 7b5f36a4
  Felipe Lisboa authored May 18, 2021
  
  7b5f36a4
- add proof on ACT between PREs · 6692b2fc
  Felipe Lisboa authored May 18, 2021
  
  6692b2fc
- implement most timing constraints · c1890297
  Florian Brandner authored May 18, 2021
  c1890297
May 17, 2021
- add row number to requests · 74a1c032
  Florian Brandner authored May 17, 2021
  74a1c032
May 16, 2021
- entirely rework proofs for FIFO · 23b6f041
  Florian Brandner authored May 16, 2021
  23b6f041
May 07, 2021
- implement T_RAS constraint. · 476778e3
  Florian Brandner authored May 7, 2021
  
  476778e3
- implement T_RCD constraint. · 6d50a8ec
  Florian Brandner authored May 7, 2021
  
  6d50a8ec
- clean up. · a33ae3f1
  Florian Brandner authored May 7, 2021
  
  a33ae3f1
- fix type error (correctly) · c6eb1f47
  Florian Brandner authored May 7, 2021
  
  c6eb1f47
- fix type error · 5361e9fa
  Florian Brandner authored May 7, 2021
  
  5361e9fa
May 06, 2021
- correct Req_handled constraint and its proof. · 648758e4
  Florian Brandner authored May 6, 2021
  
  648758e4
- Cleanup last commit : deleted unused definitions, Cmds_PRE_ok definition updated. · 32701650
  Felipe Lisboa authored May 6, 2021
  
  32701650
- Added constraint on having one ACT between 2 PREs · 9bdf1a21
  Felipe Lisboa authored May 6, 2021
  
  9bdf1a21
May 05, 2021
- Added constraint on having one ACT between PREs · cabf78e4
  Felipe Lisboa authored May 5, 2021
  
  cabf78e4
- implement T_RP constraint · 230f8997
  Florian Brandner authored May 5, 2021
  
  230f8997
May 04, 2021
- clean up proofs. · 6af67763
  Florian Brandner authored May 4, 2021
  
  6af67763
May 03, 2021
- completed proof for FIFO. · e6ee8e1c
  Florian Brandner authored May 3, 2021
  
  e6ee8e1c
- correct T_RC parameter for FIFO, some more proofs. · 22a16c7b
  Florian Brandner authored May 2, 2021
  
  22a16c7b
Apr 29, 2021
- some more proofs · 7b480278
  Florian Brandner authored Apr 29, 2021
  
  7b480278
Apr 28, 2021
- fix FIFO arbiter, start proofs · ff586b1a
  Florian Brandner authored Apr 28, 2021
  
  ff586b1a
Apr 23, 2021
- coq project file for the Coq IDE · 5650854b
  Florian Brandner authored Apr 23, 2021
  
  5650854b
- simple test framework for Coq models · e85fe874
  Florian Brandner authored Apr 23, 2021
  
  e85fe874
Mar 11, 2021
- Added upper-level module for the memory, also a RT module for separating the... · 18087f6e
  Felipe Lisboa Malaquias authored Mar 11, 2021
  18087f6e
Mar 10, 2021
- Added specification for handling count-down timers · a5bde1c7
  Felipe Lisboa Malaquias authored Mar 10, 2021
  
  a5bde1c7
- Added bank specification · 6883946d
  Felipe Lisboa Malaquias authored Mar 10, 2021
  
  6883946d
- Changed README · f309107b
  Felipe Lisboa Malaquias authored Mar 10, 2021
  
  f309107b
- Merge branch 'develop' into 'master' · 25c077a2
  Felipe Lisboa Malaquias authored Mar 10, 2021
  25c077a2
- Restructured TLA+ Modules · c6651f32
  Felipe Lisboa Malaquias authored Mar 10, 2021
  
  c6651f32
- Reorganized repository structure · 0495e59c
  Felipe Lisboa Malaquias authored Mar 10, 2021
  
  0495e59c
Mar 05, 2021
- Added SequencesExt · ff9f74c9
  Felipe Lisboa Malaquias authored Mar 5, 2021
  
  ff9f74c9
- TLA+ updated v6, using countdown timers to advance through time · 2132dd22
  Felipe Lisboa Malaquias authored Mar 5, 2021
  
  2132dd22
Mar 03, 2021
- Model following Lamports RT modelization. Seems to be the good way to do things · 271d0b5b
  Felipe Lisboa Malaquias authored Mar 3, 2021
  
  271d0b5b
Feb 26, 2021
- Amelioration on time continuous model, many concepts are now implemented · 9f3ee2b3
  Felipe Lisboa Malaquias authored Feb 26, 2021
  
  9f3ee2b3