Timeline



Nov 22, 2010:

7:25 PM Changeset [256] by mulligan
Work on ASM.ma file.
3:57 PM Changeset [255] by campbell
Really restore matita root.
2:40 PM Changeset [254] by campbell
Reset matita root.
2:40 PM Changeset [253] by campbell
Update completeness proof for executable semantics with separate …
2:40 PM Changeset [252] by campbell
Separate out soundness of exec_step from definition.
2:40 PM Changeset [251] by campbell
Separate out soundness of exec_expr from definition.
2:40 PM Changeset [250] by campbell
Begin separating soundness from executable semantics.
1:55 PM Changeset [249] by mulligan
More work on defining fundamental datatypes.
11:43 AM Changeset [248] by mulligan
More changes. Added datatype for addressing modes.
11:12 AM Changeset [247] by mulligan
Changes to get directory to compile.
10:05 AM Changeset [246] by mulligan
Added physical file (Arithmetic) for arithmetic on bit vectors, and …

Nov 16, 2010:

1:42 PM Changeset [245] by campbell
Some progress on whole-execution soundness.

Nov 15, 2010:

10:42 AM Changeset [244] by mulligan
Vector.ma now compiles.
10:41 AM Changeset [243] by mulligan
Updated Util.ma too.
10:28 AM Changeset [242] by mulligan
Got List to compile.
10:26 AM Changeset [241] by mulligan
Also needed an updated List.ma.
10:22 AM Changeset [240] by mulligan
Updated Vector / BitVector? files taken from my Matita library.

Nov 12, 2010:

7:16 PM Changeset [239] by campbell
More work on soundness and completeness of executable Clight semantics.
5:09 PM Changeset [238] by mulligan
More work on bitvectors.
4:51 PM Changeset [237] by mulligan
More functions on bitvectors written.
4:01 PM Changeset [236] by mulligan
Strange problem with matita and the Maybe file? Cannot find Maybe.ng.
2:43 PM Changeset [235] by mulligan
More work on bitvectors.
2:27 PM Changeset [234] by mulligan
Division and modulus implemented. All necessary orders on naturals …
11:51 AM Changeset [233] by mulligan
Changes from this morning: Bool / Prop division = nightmare.

Nov 11, 2010:

4:56 PM Changeset [232] by mulligan
Lots of work from today. Writing bitvector library is harder than it …
12:27 PM Changeset [231] by mulligan
BitVector? stuff from this morning: need further development of Nat …

Nov 10, 2010:

5:26 PM Changeset [230] by mulligan
Lots of work from today.

Nov 9, 2010:

5:00 PM Changeset [229] by mulligan
More changes.
3:27 PM Changeset [228] by mulligan
Conjunction, disjunction and 'xorjunction' implemented on bitvectors. …
12:52 PM Changeset [227] by campbell
Update notation in an example.
12:52 PM Changeset [226] by campbell
Some incomplete work on completeness of CexecIO wrt Csem. Features …
12:52 PM Changeset [225] by campbell
Missing case in cast.

Nov 8, 2010:

5:04 PM Changeset [224] by mulligan
Changes to bit vectors and vectors.
2:24 PM Changeset [223] by mulligan
File for bitvector specific stuff added.
1:53 PM Changeset [222] by mulligan
Datatype for fixed length lists (vectors) as well as some recursive …
11:17 AM Changeset [221] by mulligan
Starting formalisation in Matita

Nov 5, 2010:

3:07 PM Changeset [220] by mulligan
Started on timer 2 capture mode.
2:48 PM Changeset [219] by mulligan
Additional features of timer 2 auto reload implemented.
2:19 PM Changeset [218] by mulligan
Timer 2 16 bit auto reload implemented.

Nov 4, 2010:

5:05 PM Changeset [217] by mulligan
Back to the drawing board with interrupts ... giving up and …
12:27 PM Changeset [216] by mulligan
Interrupts are harder than they look.
11:37 AM Changeset [215] by mulligan
More on implementation of interrupts. Need to add a queue for …

Nov 3, 2010:

5:34 PM Changeset [214] by mulligan
Started implementation of interrupts.
3:23 PM Changeset [213] by mulligan
implementing interrupts
1:16 PM Changeset [212] by mulligan
Refactored main emulator loop to improve clarity. Debugging serial …
12:41 PM Changeset [211] by campbell
Make io_inject definition more straightforward.

Nov 2, 2010:

10:09 AM Changeset [210] by mulligan
Three new opcodes ticked off. Going through remaining untested …
9:44 AM Changeset [209] by mulligan
Compiled again.

Nov 1, 2010:

11:10 AM Changeset [208] by campbell
Fix up IO monad syntax.

Oct 27, 2010:

4:27 PM Changeset [207] by campbell
Add memory extensions and rework parts of D3.1.
Note: See TracTimeline for information about the timeline view.