Timeline



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.

Oct 22, 2010:

3:56 PM Changeset [206] by mulligan
Fixed serial output.
3:06 PM Changeset [205] by mulligan
Reworked handling of serial port input, and implemented remaining …

Oct 21, 2010:

1:36 PM Changeset [204] by mulligan
Added file that performs both serial input and output on the 8051.
1:32 PM Changeset [203] by mulligan
Serial input test: seems to work correctly (small bug corrected where …

Oct 20, 2010:

5:59 PM Changeset [202] by mulligan
Remaining two timer modes implemented.
4:29 PM Changeset [201] by mulligan
Implemented output onto P1 and P3 lines, implemented a few of the …
1:35 PM Changeset [200] by mulligan
New features: 1) conditional jumps to labels implemented [Note: …

Oct 19, 2010:

3:29 PM Changeset [199] by mulligan
Fixes to debug code to make serial output more clear. CJNE/JNZ is not …
2:20 PM Changeset [198] by mulligan
Added more info to status printout. Found weird bug in emulator: cjne …
1:42 PM Changeset [197] by campbell
Add some first draft text for 3.1.
10:55 AM Changeset [196] by mulligan
Improvements to processor status output. Now includes readout of main …
10:40 AM Changeset [195] by mulligan
Added printout of processor status when we enter the infinite SJMP …

Oct 18, 2010:

3:20 PM Changeset [194] by mulligan
Oops: small change caused compile to fail. Works again, now.
3:19 PM Changeset [193] by mulligan
Fixed type errors relating to serial output. The serial port code …
12:15 PM Changeset [192] by campbell
matita rev in README
11:54 AM Changeset [191] by mulligan
Changed way we handle I/O due to assert false bug on first serial I/O …
11:36 AM Changeset [190] by campbell
Minor changes to work with current matita HEAD (r10998).
11:36 AM Changeset [189] by campbell
Rework monad notation so that it is displayed well in proof mode.
10:40 AM Changeset [188] by mulligan
Added README file for Roberto.

Oct 15, 2010:

4:14 PM Changeset [187] by mulligan
Bug found in IO handling. Something is throwing assert false.
2:37 PM Changeset [186] by mulligan
Added C code to write to SBUF SFR for Roberto.

Oct 14, 2010:

5:02 PM Changeset [185] by mulligan
Found a way to inline SDCC ASM directly into C to test hard to reach …
2:41 PM Changeset [184] by mulligan
Found out how to directly access 8051's registers from C code. Added …
12:11 PM Changeset [183] by mulligan
A few more opcodes covered. Emulator seems to work fine on LFSR program.
11:20 AM Changeset [182] by mulligan
Linear feedback shift register (random number generator) example added.

Oct 13, 2010:

4:27 PM Changeset [181] by campbell
Sort out some axioms.
3:12 PM Changeset [180] by mulligan
Arctan floating point approximation code. 8051 really struggles with …
2:11 PM Changeset [179] by mulligan
Program executes as required.
12:19 PM Changeset [178] by campbell
Bring README file up to date.
12:19 PM Changeset [177] by campbell
Missing cost labels file.
12:19 PM Changeset [176] by campbell
Remove old executable semantics without I/O.
12:19 PM Changeset [175] by campbell
Add cost labels, with the semantics that the label is added to the …
12:19 PM Changeset [174] by campbell
Add a form of non-terminating functional semantics.
12:12 PM Changeset [173] by campbell
Minor changes for newer versions of matita.
12:07 PM Changeset [172] by mulligan
JZ was not buggy after all (miscount of loop cycles). Branchless …
11:11 AM Changeset [171] by mulligan
Parity check program. Bug found with jump zero instruction. A few …
10:55 AM Changeset [170] by mulligan
Emulator successfully emulates rounding program.
10:43 AM Changeset [169] by mulligan
Latest test C file: fast roundup to closest power of two.
Note: See TracTimeline for information about the timeline view.