Kestrel-3

Timeline
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

50 most recent check-ins

2018-10-18
18:19
[5aa0d07ad9] Leaf: SIA: Forgot to include SBY file. (user: kc5tja tags: formal)
07:01
[eb7b249c0b] SIA: valid and overrun bits must clear when reading from the data register (user: kc5tja tags: formal)
06:23
[50ec70df3f] SIA: Make sure the overrun flag works as expected (user: kc5tja tags: formal)
06:20
[ae7910af5b] SIA: Make sure o_rxd_valid asserts upon receipt of data (user: kc5tja tags: formal)
06:16
[dd7b7eb8d3] SIA: capture shift register contents upon completion of a frame (user: kc5tja tags: formal)
06:07
[0c8baa992f] SIA: Make sure frame detection is a pulse signal, not a level signal. (user: kc5tja tags: formal)
06:04
[5811734861] SIA: Detect when a frame is received (user: kc5tja tags: formal)
05:45
[aa82c9893b] SIA: Ensures the sample counter decrements when it is supposed to. (user: kc5tja tags: formal)
05:35
[12632108f0] SIA: Ensure sampleCtr is properly set in between characters (user: kc5tja tags: formal)
05:29
[9c0b76c048] SIA: Make sure we maintain plesiosynchronous sampling in the absence of edges (user: kc5tja tags: formal)
05:25
[41b6879592] SIA: Make sure samples happen in the middle of the bit cell after an edge is detected (user: kc5tja tags: formal)
05:20
[cb67ef073d] SIA: Sample counter reset behavior (user: kc5tja tags: formal)
05:13
[f7adb458b1] SIA: Tap the correct input for the shift register (user: kc5tja tags: formal)
05:03
[44ec5e4f5e] SIA: Make sure shiftRegister shifts in the correct direction (user: kc5tja tags: formal)
2018-10-16
17:20
[69de6d6c74] SIA: BMC passes for receiver's bit counter. (user: kc5tja tags: formal)
15:22
[e0a423cfd0] Empty properties.vf file (user: kc5tja tags: formal)
05:58
[ffb41dee02] SIA: Import source code from older SIA implementation, and simplify and document it a whole lot better. Preparing to insert properties as well. NOTE: This module has been simplified from the original SIA receiver logic. It cannot handle anything other than 8N1 serial frames. It's easy enough to restore the missing functionality, but it would require more SIA registers. Since current software does not make use of this functionality, and depends upon the SIA defaulting to 8N1 upon reset, I just decided to hardwire as much as I could. Adding registers can be done later, when it's actually justified. (user: kc5tja tags: formal)
2018-10-14
20:08
[6654e09566] Tickler README (user: kc5tja tags: formal)
01:07
[077f056270] Automate formal verification for SIA (user: kc5tja tags: formal)
2018-10-06
06:27
[4707d76538] Expose the baud rate divisor to the interface (user: kc5tja tags: formal)
06:18
[87571690eb] Expose data written to TXOUT for use by shift register logic (user: kc5tja tags: formal)
04:35
[df6214cf7d] Comments! (user: kc5tja tags: formal)
02:13
[e351f5396b] Add required conditions to make it pass induction. (user: kc5tja tags: formal)
01:03
[60d4a58321] Try to use a saturating counter to see if it will make induction pass. (user: kc5tja tags: formal)
2018-10-01
15:00
[c3ee961383] WIP: need to find out why this fails induction (user: kc5tja tags: formal)
2018-09-06
04:47
[23614639e5] SIA:Implement the register backing BAUD and support for specific byte-lanes. Also, reduce default width of rate generator's divisor to match the width of the BAUD register. (user: kc5tja tags: formal)
2018-09-05
03:19
[d2d579a5a2] Add default nettypes (user: kc5tja tags: formal)
03:15
[f4ede39e18] SIA:WIP:Fix inductive proof failure (user: kc5tja tags: formal)
01:14
[52809c12cd] SIA: WIP: unsure why it doesn't pass formal checks in "prove" mode (user: kc5tja tags: formal)
2018-09-04
02:49
[4276cebda5] SIA:TileLink coupling (WIP) (user: kc5tja tags: formal)
2018-09-03
17:36
[2149cd86a8] SIA: Controlling registers (just BAUD for now) (user: kc5tja tags: formal)
2018-09-02
02:04
[d06bf263a4] SIA:TX:Implement the transmitter shift register logic. (user: kc5tja tags: formal)
2018-09-01
17:49
[0b911e8ec0] First module for transmit engine (user: kc5tja tags: formal)
2018-08-31
06:34
[088d1cf570] Rate generator intended for use with the SIA implementation (user: kc5tja tags: formal)
03:32
[2c5d0f5fce] SIA: Rate Generator (user: kc5tja tags: formal)
01:56
[b3f95194cf] Clearer name to describe intent of the "core". (user: kc5tja tags: formal)
2018-08-30
18:11
[d5debe2752] Per ZipCPU's suggestion, I didn't need the initial block if I qualified some of my assertions more thoroughly. (user: kc5tja tags: formal)
04:57
[b014c7b07f] ROMA: Formal verification of TileLink bus seems to be complete. (user: kc5tja tags: formal)
2018-08-29
18:44
[2f8acc4498] WIP ROMA: Qualify A-channel transaction by comparing opcode. Verify that o_d_valid should be negated for as long as we lack a read result. Remove reg qualifier from all signals we "assign" to. Generate o_a_ready based on state of bits_so_far. Passes bmc; fails to prove inductively. Cause is o_d_valid && i_d_ready true while not engaged in an actual transaction. Cannot figure out how to tell prover that this is an impossible condition. (user: kc5tja tags: formal)
06:57
[2da2614d5c] Enforce proper handling of o_a_ready (user: kc5tja tags: formal)
05:38
[f1b71290ae] First set of formal properties for ROMA core (user: kc5tja tags: formal)
04:56
[c5528419c2] Leaf: Create new branch named "formal" (user: kc5tja tags: formal)
00:59
[e19f2d7e5c] Leaf: Attempt to add ROMA verification properties on my own (user: kc5tja tags: trunk)
2018-08-28
21:51
[3ded29d7df] Fixed the clock leak on ROMA core after adding FV to DMAC. Next step: figure out why only one bus transaction is taking place. (user: kc5tja tags: trunk)
21:51
[7756138d89] Fixed the clock leak on ROMA core after adding FV to DMAC. Next step: figure out why only one bus transaction is taking place. (user: kc5tja tags: trunk)
05:55
[0f3c9ade6a] Remove spurious Or operator (user: kc5tja tags: trunk)
05:42
[f2a9d73ac1] Make unit test pass for DMAC (user: kc5tja tags: trunk)
04:40
[eaace617c1] Fix commentary (user: kc5tja tags: trunk)
04:36
[db46c3c0e7] Introduce some formal verification for the DMAC (user: kc5tja tags: trunk)
01:19
[2795fa984f] ROMA + DMAC = working now, due to DDR clock buffer. (user: kc5tja tags: trunk)