Kestrel-3

Timeline
Login

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

51 check-ins related to "formal"

2018-10-22
01:57
Formal verification has proven itself as a viable development method. Merging into trunk. check-in: af53196bd7 user: kc5tja tags: trunk
01:37
SIA: IRQ support! Closed-Leaf check-in: bcb48b6e07 user: kc5tja tags: formal
00:54
SIA: Implement INTENA register check-in: bfd80199ba user: kc5tja tags: formal
2018-10-21
23:41
Expose loopback controls for external circuitry (top level perhaps) check-in: 49b4a6be70 user: kc5tja tags: formal
23:24
SIA: Map loopback control bits into BAUD register check-in: 237f455dc6 user: kc5tja tags: formal
21:02
Map receiver status bits and data to their respective registers. check-in: df3f069cc2 user: kc5tja tags: formal
2018-10-20
22:38
SIA: Revise block diagram for end result check-in: 3de7c2bf82 user: kc5tja tags: formal
22:20
Removed edge-sensitivity and support for external clocks, and made receiver sampling unconditionally plesiochronous. This eliminated a number of edge-case bugs from the receiver that hinted at some serious noise sensitivity issues. The SIA is thus now 100% a UART, with no synchronous reception capabilities at all. check-in: eeabb18974 user: kc5tja tags: formal
2018-10-18
18:19
SIA: Forgot to include SBY file. check-in: 5aa0d07ad9 user: kc5tja tags: formal
07:01
SIA: valid and overrun bits must clear when reading from the data register check-in: eb7b249c0b user: kc5tja tags: formal
06:23
SIA: Make sure the overrun flag works as expected check-in: 50ec70df3f user: kc5tja tags: formal
06:20
SIA: Make sure o_rxd_valid asserts upon receipt of data check-in: ae7910af5b user: kc5tja tags: formal
06:16
SIA: capture shift register contents upon completion of a frame check-in: dd7b7eb8d3 user: kc5tja tags: formal
06:07
SIA: Make sure frame detection is a pulse signal, not a level signal. check-in: 0c8baa992f user: kc5tja tags: formal
06:04
SIA: Detect when a frame is received check-in: 5811734861 user: kc5tja tags: formal
05:45
SIA: Ensures the sample counter decrements when it is supposed to. check-in: aa82c9893b user: kc5tja tags: formal
05:35
SIA: Ensure sampleCtr is properly set in between characters check-in: 12632108f0 user: kc5tja tags: formal
05:29
SIA: Make sure we maintain plesiosynchronous sampling in the absence of edges check-in: 9c0b76c048 user: kc5tja tags: formal
05:25
SIA: Make sure samples happen in the middle of the bit cell after an edge is detected check-in: 41b6879592 user: kc5tja tags: formal
05:20
SIA: Sample counter reset behavior check-in: cb67ef073d user: kc5tja tags: formal
05:13
SIA: Tap the correct input for the shift register check-in: f7adb458b1 user: kc5tja tags: formal
05:03
SIA: Make sure shiftRegister shifts in the correct direction check-in: 44ec5e4f5e user: kc5tja tags: formal
2018-10-16
17:20
SIA: BMC passes for receiver's bit counter. check-in: 69de6d6c74 user: kc5tja tags: formal
15:22
Empty properties.vf file check-in: e0a423cfd0 user: kc5tja tags: formal
05:58
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. check-in: ffb41dee02 user: kc5tja tags: formal
2018-10-14
20:08
Tickler README check-in: 6654e09566 user: kc5tja tags: formal
01:07
Automate formal verification for SIA check-in: 077f056270 user: kc5tja tags: formal
2018-10-06
06:27
Expose the baud rate divisor to the interface check-in: 4707d76538 user: kc5tja tags: formal
06:18
Expose data written to TXOUT for use by shift register logic check-in: 87571690eb user: kc5tja tags: formal
04:35
Comments! check-in: df6214cf7d user: kc5tja tags: formal
02:13
Add required conditions to make it pass induction. check-in: e351f5396b user: kc5tja tags: formal
01:03
Try to use a saturating counter to see if it will make induction pass. check-in: 60d4a58321 user: kc5tja tags: formal
2018-10-01
15:00
WIP: need to find out why this fails induction check-in: c3ee961383 user: kc5tja tags: formal
2018-09-06
04:47
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. check-in: 23614639e5 user: kc5tja tags: formal
2018-09-05
03:19
Add default nettypes check-in: d2d579a5a2 user: kc5tja tags: formal
03:15
SIA:WIP:Fix inductive proof failure check-in: f4ede39e18 user: kc5tja tags: formal
01:14
SIA: WIP: unsure why it doesn't pass formal checks in "prove" mode check-in: 52809c12cd user: kc5tja tags: formal
2018-09-04
02:49
SIA:TileLink coupling (WIP) check-in: 4276cebda5 user: kc5tja tags: formal
2018-09-03
17:36
SIA: Controlling registers (just BAUD for now) check-in: 2149cd86a8 user: kc5tja tags: formal
2018-09-02
02:04
SIA:TX:Implement the transmitter shift register logic. check-in: d06bf263a4 user: kc5tja tags: formal
2018-09-01
17:49
First module for transmit engine check-in: 0b911e8ec0 user: kc5tja tags: formal
2018-08-31
06:34
Rate generator intended for use with the SIA implementation check-in: 088d1cf570 user: kc5tja tags: formal
03:32
SIA: Rate Generator check-in: 2c5d0f5fce user: kc5tja tags: formal
01:56
Clearer name to describe intent of the "core". check-in: b3f95194cf user: kc5tja tags: formal
2018-08-30
18:11
Per ZipCPU's suggestion, I didn't need the initial block if I qualified some of my assertions more thoroughly. check-in: d5debe2752 user: kc5tja tags: formal
04:57
ROMA: Formal verification of TileLink bus seems to be complete. check-in: b014c7b07f user: kc5tja tags: formal
2018-08-29
18:44
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. check-in: 2f8acc4498 user: kc5tja tags: formal
06:57
Enforce proper handling of o_a_ready check-in: 2da2614d5c user: kc5tja tags: formal
05:38
First set of formal properties for ROMA core check-in: f1b71290ae user: kc5tja tags: formal
04:56
Create new branch named "formal" Leaf check-in: c5528419c2 user: kc5tja tags: formal
2018-08-28
01:19
ROMA + DMAC = working now, due to DDR clock buffer. check-in: 2795fa984f user: kc5tja tags: trunk