SNAPKITTYWEST commited on
Commit
0ba037b
·
verified ·
1 Parent(s): 6713c02

October 2026 main drop: mirror from GitHub

Browse files
This view is limited to 50 files because it contains too many changes.   See raw diff
Files changed (50) hide show
  1. .github/workflows/ci.yml +164 -0
  2. .gitignore +5 -0
  3. LICENSE +277 -0
  4. Makefile +91 -0
  5. README.md +113 -0
  6. asic/Makefile +64 -0
  7. asic/README.md +32 -0
  8. asic/abc.script +11 -0
  9. asic/sta.tcl +16 -0
  10. bit_accelerator/.gitignore +2 -0
  11. bit_accelerator/IMPLEMENTATION_REPORT.md +47 -0
  12. bit_accelerator/Makefile +55 -0
  13. bit_accelerator/README.md +200 -0
  14. bit_accelerator/build.sh +9 -0
  15. bit_accelerator/docs/DATAPATH.md +437 -0
  16. bit_accelerator/formal/bit_addressing.mlw +155 -0
  17. bit_accelerator/formal/bit_addressing_proofs.mlw +45 -0
  18. bit_accelerator/isa/BIT_ISA.md +416 -0
  19. bit_accelerator/rtl/behavioral_memory.sv +102 -0
  20. bit_accelerator/rtl/bit_accelerator.sv +210 -0
  21. bit_accelerator/rtl/bit_accelerator_pkg.sv +140 -0
  22. bit_accelerator/rtl/bit_accelerator_v2.sv +209 -0
  23. bit_accelerator/rtl/bit_address_generator.sv +31 -0
  24. bit_accelerator/rtl/bit_extractor.sv +36 -0
  25. bit_accelerator/rtl/bit_modifier.sv +29 -0
  26. bit_accelerator/run_v2_sim.sh +10 -0
  27. bit_accelerator/scripts/prove.sh +39 -0
  28. bit_accelerator/testbenches/tb_bit_accelerator.sv +322 -0
  29. bit_accelerator/testbenches/tb_bit_accelerator_v2.sv +311 -0
  30. docs/verification.md +58 -0
  31. dual license +171 -0
  32. formal/bit_address.mlw +111 -0
  33. formal/bit_extract.mlw +50 -0
  34. formal/lane_map.mlw +176 -0
  35. fpga/Makefile +115 -0
  36. fpga/README.md +99 -0
  37. fpga/boards/icebreaker.pcf +7 -0
  38. fpga/boards/icebreaker_top.sv +22 -0
  39. fpga/boards/ulx3s.lpf +35 -0
  40. fpga/boards/ulx3s_top.sv +23 -0
  41. fpga/host/Cargo.lock +7 -0
  42. fpga/host/Cargo.toml +10 -0
  43. fpga/host/src/main.rs +283 -0
  44. fpga/host/src/protocol.rs +204 -0
  45. fpga/rtl/fpga_top.sv +162 -0
  46. fpga/rtl/power_on_reset.sv +19 -0
  47. fpga/rtl/uart_rx.sv +49 -0
  48. fpga/rtl/uart_tx.sv +48 -0
  49. fpga/rtl/word_memory.sv +16 -0
  50. fpga/sim/cosim.sh +29 -0
.github/workflows/ci.yml ADDED
@@ -0,0 +1,164 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ name: CI
2
+
3
+ on:
4
+ push:
5
+ branches: [main]
6
+ pull_request:
7
+ workflow_dispatch:
8
+
9
+ permissions:
10
+ contents: read
11
+
12
+ concurrency:
13
+ group: ci-${{ github.ref }}
14
+ cancel-in-progress: true
15
+
16
+ jobs:
17
+ hdl:
18
+ name: RTL lint and simulation
19
+ runs-on: ubuntu-24.04
20
+ steps:
21
+ - uses: actions/checkout@v4
22
+ - name: Install simulators
23
+ run: sudo apt-get update && sudo apt-get install -y --no-install-recommends iverilog verilator
24
+ - name: Compact accelerator
25
+ run: make lint sim
26
+ - name: Compact accelerator, extra random seeds
27
+ run: for s in 2 3 4; do make sim-icarus SEED=$s OPS=3000; done
28
+ - name: bit_accelerator v2
29
+ run: make -C bit_accelerator lint sim
30
+
31
+ formal:
32
+ name: Why3 proofs
33
+ runs-on: ubuntu-24.04
34
+ steps:
35
+ - uses: actions/checkout@v4
36
+ - name: Install Why3 and Z3
37
+ run: |
38
+ sudo apt-get update && sudo apt-get install -y --no-install-recommends why3 z3
39
+ why3 config detect
40
+ - name: Compact accelerator proofs
41
+ run: make formal
42
+ - name: bit_accelerator v2 proofs
43
+ run: make -C bit_accelerator formal
44
+
45
+ spice:
46
+ name: SPICE timing model
47
+ runs-on: ubuntu-24.04
48
+ steps:
49
+ - uses: actions/checkout@v4
50
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends ngspice
51
+ - run: make spice
52
+
53
+ gpu:
54
+ name: Rust OpenCL crate (gpu/)
55
+ runs-on: ubuntu-24.04
56
+ defaults:
57
+ run:
58
+ working-directory: gpu
59
+ steps:
60
+ - uses: actions/checkout@v4
61
+ - name: Install OpenCL (PoCL CPU device)
62
+ run: |
63
+ sudo apt-get update
64
+ sudo apt-get install -y --no-install-recommends pocl-opencl-icd ocl-icd-opencl-dev clinfo
65
+ clinfo -l
66
+ - uses: dtolnay/rust-toolchain@stable
67
+ with:
68
+ components: rustfmt, clippy
69
+ - uses: Swatinem/rust-cache@v2
70
+ with:
71
+ workspaces: gpu
72
+ - run: cargo fmt --check
73
+ - run: cargo clippy --all-targets -- -D warnings
74
+ # Serial: PoCL 5.0 can abort (pocl_release_dlhandle_cache assertion) when
75
+ # several OpenCL contexts are released from different threads at once.
76
+ - run: cargo test
77
+ env:
78
+ RUST_TEST_THREADS: "1"
79
+ - run: cargo run --quiet
80
+
81
+ fpga:
82
+ name: FPGA build (lint, UART testbench, host co-simulation, bitstreams)
83
+ runs-on: ubuntu-24.04
84
+ steps:
85
+ - uses: actions/checkout@v4
86
+ - name: Install FPGA toolchain
87
+ run: |
88
+ sudo apt-get update
89
+ sudo apt-get install -y --no-install-recommends iverilog verilator yosys \
90
+ nextpnr-ice40 nextpnr-ecp5 fpga-icestorm fpga-trellis
91
+ - uses: dtolnay/rust-toolchain@stable
92
+ with:
93
+ components: rustfmt, clippy
94
+ - uses: Swatinem/rust-cache@v2
95
+ with:
96
+ workspaces: fpga/host
97
+ - run: make -C fpga lint sim host cosim icebreaker ulx3s
98
+ - uses: actions/upload-artifact@v4
99
+ with:
100
+ name: bitstreams
101
+ path: |
102
+ fpga/build/icebreaker.bin
103
+ fpga/build/ulx3s.bit
104
+ fpga/build/*_pnr.log
105
+
106
+ fpga-gate-level:
107
+ name: FPGA gate-level simulation (${{ matrix.arch }})
108
+ runs-on: ubuntu-24.04
109
+ strategy:
110
+ matrix:
111
+ arch: [ice40, ecp5]
112
+ steps:
113
+ - uses: actions/checkout@v4
114
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends iverilog yosys
115
+ - run: make -C fpga gl-sim-${{ matrix.arch }}
116
+
117
+ asic:
118
+ name: sky130 synthesis and equivalence
119
+ runs-on: ubuntu-24.04
120
+ steps:
121
+ - uses: actions/checkout@v4
122
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends yosys
123
+ - run: make -C asic all
124
+ - uses: actions/upload-artifact@v4
125
+ with:
126
+ name: sky130-netlist
127
+ path: |
128
+ asic/build/bit_accelerator_sky130.v
129
+ asic/build/area.rpt
130
+
131
+ pcie:
132
+ name: PCIe engine (lint, equivalence vs reference core)
133
+ runs-on: ubuntu-24.04
134
+ steps:
135
+ - uses: actions/checkout@v4
136
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends iverilog verilator
137
+ # The simulation runs are independent make targets; the largest geometry takes ~6 minutes.
138
+ - run: make -C pcie -j$(nproc) lint sim sim-verilator
139
+
140
+ pcie-cosim:
141
+ name: PCIe SoC generation + host co-simulation + throughput
142
+ runs-on: ubuntu-24.04
143
+ steps:
144
+ - uses: actions/checkout@v4
145
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends verilator
146
+ - uses: actions/setup-python@v5
147
+ with:
148
+ python-version: '3.11'
149
+ - name: Install LiteX
150
+ run: |
151
+ for r in m-labs/migen enjoy-digital/litex litex-hub/litex-boards enjoy-digital/litepcie \
152
+ enjoy-digital/litedram enjoy-digital/liteeth enjoy-digital/litescope; do
153
+ git clone --depth 1 https://github.com/$r /tmp/$(basename $r)
154
+ pip install -e /tmp/$(basename $r)
155
+ done
156
+ - run: make -C pcie soc cosim perf
157
+
158
+ tapeout:
159
+ name: Tiny Tapeout project (sync, RTL test)
160
+ runs-on: ubuntu-24.04
161
+ steps:
162
+ - uses: actions/checkout@v4
163
+ - run: sudo apt-get update && sudo apt-get install -y --no-install-recommends iverilog
164
+ - run: make -C tapeout check-sync test
.gitignore ADDED
@@ -0,0 +1,5 @@
 
 
 
 
 
 
1
+ target/
2
+ build/
3
+ obj_dir/
4
+ simv
5
+ *.vcd
LICENSE ADDED
@@ -0,0 +1,277 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ Eclipse Public License - v 2.0
2
+
3
+ THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS ECLIPSE
4
+ PUBLIC LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR DISTRIBUTION
5
+ OF THE PROGRAM CONSTITUTES RECIPIENT'S ACCEPTANCE OF THIS AGREEMENT.
6
+
7
+ 1. DEFINITIONS
8
+
9
+ "Contribution" means:
10
+
11
+ a) in the case of the initial Contributor, the initial content
12
+ Distributed under this Agreement, and
13
+
14
+ b) in the case of each subsequent Contributor:
15
+ i) changes to the Program, and
16
+ ii) additions to the Program;
17
+ where such changes and/or additions to the Program originate from
18
+ and are Distributed by that particular Contributor. A Contribution
19
+ "originates" from a Contributor if it was added to the Program by
20
+ such Contributor itself or anyone acting on such Contributor's behalf.
21
+ Contributions do not include changes or additions to the Program that
22
+ are not Modified Works.
23
+
24
+ "Contributor" means any person or entity that Distributes the Program.
25
+
26
+ "Licensed Patents" mean patent claims licensable by a Contributor which
27
+ are necessarily infringed by the use or sale of its Contribution alone
28
+ or when combined with the Program.
29
+
30
+ "Program" means the Contributions Distributed in accordance with this
31
+ Agreement.
32
+
33
+ "Recipient" means anyone who receives the Program under this Agreement
34
+ or any Secondary License (as applicable), including Contributors.
35
+
36
+ "Derivative Works" shall mean any work, whether in Source Code or other
37
+ form, that is based on (or derived from) the Program and for which the
38
+ editorial revisions, annotations, elaborations, or other modifications
39
+ represent, as a whole, an original work of authorship.
40
+
41
+ "Modified Works" shall mean any work in Source Code or other form that
42
+ results from an addition to, deletion from, or modification of the
43
+ contents of the Program, including, for purposes of clarity any new file
44
+ in Source Code form that contains any contents of the Program. Modified
45
+ Works shall not include works that contain only declarations,
46
+ interfaces, types, classes, structures, or files of the Program solely
47
+ in each case in order to link to, bind by name, or subclass the Program
48
+ or Modified Works thereof.
49
+
50
+ "Distribute" means the acts of a) distributing or b) making available
51
+ in any manner that enables the transfer of a copy.
52
+
53
+ "Source Code" means the form of a Program preferred for making
54
+ modifications, including but not limited to software source code,
55
+ documentation source, and configuration files.
56
+
57
+ "Secondary License" means either the GNU General Public License,
58
+ Version 2.0, or any later versions of that license, including any
59
+ exceptions or additional permissions as identified by the initial
60
+ Contributor.
61
+
62
+ 2. GRANT OF RIGHTS
63
+
64
+ a) Subject to the terms of this Agreement, each Contributor hereby
65
+ grants Recipient a non-exclusive, worldwide, royalty-free copyright
66
+ license to reproduce, prepare Derivative Works of, publicly display,
67
+ publicly perform, Distribute and sublicense the Contribution of such
68
+ Contributor, if any, and such Derivative Works.
69
+
70
+ b) Subject to the terms of this Agreement, each Contributor hereby
71
+ grants Recipient a non-exclusive, worldwide, royalty-free patent
72
+ license under Licensed Patents to make, use, sell, offer to sell,
73
+ import and otherwise transfer the Contribution of such Contributor,
74
+ if any, in Source Code or other form. This patent license shall
75
+ apply to the combination of the Contribution and the Program if, at
76
+ the time the Contribution is added by the Contributor, such addition
77
+ of the Contribution causes such combination to be covered by the
78
+ Licensed Patents. The patent license shall not apply to any other
79
+ combinations which include the Contribution. No hardware per se is
80
+ licensed hereunder.
81
+
82
+ c) Recipient understands that although each Contributor grants the
83
+ licenses to its Contributions set forth herein, no assurances are
84
+ provided by any Contributor that the Program does not infringe the
85
+ patent or other intellectual property rights of any other entity.
86
+ Each Contributor disclaims any liability to Recipient for claims
87
+ brought by any other entity based on infringement of intellectual
88
+ property rights or otherwise. As a condition to exercising the
89
+ rights and licenses granted hereunder, each Recipient hereby
90
+ assumes sole responsibility to secure any other intellectual
91
+ property rights needed, if any. For example, if a third party
92
+ patent license is required to allow Recipient to Distribute the
93
+ Program, it is Recipient's responsibility to acquire that license
94
+ before distributing the Program.
95
+
96
+ d) Each Contributor represents that to its knowledge it has
97
+ sufficient copyright rights in its Contribution, if any, to grant
98
+ the copyright license set forth in this Agreement.
99
+
100
+ e) Notwithstanding the terms of any Secondary License, no
101
+ Contributor makes additional grants to any Recipient (other than
102
+ those set forth in this Agreement) as a result of such Recipient's
103
+ receipt of the Program under the terms of a Secondary License
104
+ (if permitted under the terms of Section 3).
105
+
106
+ 3. REQUIREMENTS
107
+
108
+ 3.1 If a Contributor Distributes the Program in any form, then:
109
+
110
+ a) the Program must also be made available as Source Code, in
111
+ accordance with section 3.2, and the Contributor must accompany
112
+ the Program with a statement that the Source Code for the Program
113
+ is available under this Agreement, and informs Recipients how to
114
+ obtain it in a reasonable manner on or through a medium customarily
115
+ used for software exchange; and
116
+
117
+ b) the Contributor may Distribute the Program under a license
118
+ different than this Agreement, provided that such license:
119
+ i) effectively disclaims on behalf of all other Contributors all
120
+ warranties and conditions, express and implied, including
121
+ warranties or conditions of title and non-infringement, and
122
+ implied warranties or conditions of merchantability and fitness
123
+ for a particular purpose;
124
+
125
+ ii) effectively excludes on behalf of all other Contributors all
126
+ liability for damages, including direct, indirect, special,
127
+ incidental and consequential damages, such as lost profits;
128
+
129
+ iii) does not attempt to limit or alter the recipients' rights
130
+ in the Source Code under section 3.2; and
131
+
132
+ iv) requires any subsequent distribution of the Program by any
133
+ party to be under a license that satisfies the requirements
134
+ of this section 3.
135
+
136
+ 3.2 When the Program is Distributed as Source Code:
137
+
138
+ a) it must be made available under this Agreement, or if the
139
+ Program (i) is combined with other material in a separate file or
140
+ files made available under a Secondary License, and (ii) the initial
141
+ Contributor attached to the Source Code the notice described in
142
+ Exhibit A of this Agreement, then the Program may be made available
143
+ under the terms of such Secondary Licenses, and
144
+
145
+ b) a copy of this Agreement must be included with each copy of
146
+ the Program.
147
+
148
+ 3.3 Contributors may not remove or alter any copyright, patent,
149
+ trademark, attribution notices, disclaimers of warranty, or limitations
150
+ of liability ("notices") contained within the Program from any copy of
151
+ the Program which they Distribute, provided that Contributors may add
152
+ their own appropriate notices.
153
+
154
+ 4. COMMERCIAL DISTRIBUTION
155
+
156
+ Commercial distributors of software may accept certain responsibilities
157
+ with respect to end users, business partners and the like. While this
158
+ license is intended to facilitate the commercial use of the Program,
159
+ the Contributor who includes the Program in a commercial product
160
+ offering should do so in a manner which does not create potential
161
+ liability for other Contributors. Therefore, if a Contributor includes
162
+ the Program in a commercial product offering, such Contributor
163
+ ("Commercial Contributor") hereby agrees to defend and indemnify every
164
+ other Contributor ("Indemnified Contributor") against any losses,
165
+ damages and costs (collectively "Losses") arising from claims, lawsuits
166
+ and other legal actions brought by a third party against the Indemnified
167
+ Contributor to the extent caused by the acts or omissions of such
168
+ Commercial Contributor in connection with its distribution of the Program
169
+ in a commercial product offering. The obligations in this section do not
170
+ apply to any claims or Losses relating to any actual or alleged
171
+ intellectual property infringement. In order to qualify, an Indemnified
172
+ Contributor must: a) promptly notify the Commercial Contributor in
173
+ writing of such claim, and b) allow the Commercial Contributor to control,
174
+ and cooperate with the Commercial Contributor in, the defense and any
175
+ related settlement negotiations. The Indemnified Contributor may
176
+ participate in any such claim at its own expense.
177
+
178
+ For example, a Contributor might include the Program in a commercial
179
+ product offering, Product X. That Contributor is then a Commercial
180
+ Contributor. If that Commercial Contributor then makes performance
181
+ claims, or offers warranties related to Product X, those performance
182
+ claims and warranties are such Commercial Contributor's responsibility
183
+ alone. Under this section, the Commercial Contributor would have to
184
+ defend claims against the other Contributors related to those performance
185
+ claims and warranties, and if a court requires any other Contributor to
186
+ pay any damages as a result, the Commercial Contributor must pay
187
+ those damages.
188
+
189
+ 5. NO WARRANTY
190
+
191
+ EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, AND TO THE EXTENT
192
+ PERMITTED BY APPLICABLE LAW, THE PROGRAM IS PROVIDED ON AN "AS IS"
193
+ BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, EITHER EXPRESS OR
194
+ IMPLIED INCLUDING, WITHOUT LIMITATION, ANY WARRANTIES OR CONDITIONS OF
195
+ TITLE, NON-INFRINGEMENT, MERCHANTABILITY OR FITNESS FOR A PARTICULAR
196
+ PURPOSE. Each Recipient is solely responsible for determining the
197
+ appropriateness of using and distributing the Program and assumes all
198
+ risks associated with its exercise of rights under this Agreement,
199
+ including but not limited to the risks and costs of program errors,
200
+ compliance with applicable laws, damage to or loss of data, programs
201
+ or equipment, and unavailability or interruption of operations.
202
+
203
+ 6. DISCLAIMER OF LIABILITY
204
+
205
+ EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, AND TO THE EXTENT
206
+ PERMITTED BY APPLICABLE LAW, NEITHER RECIPIENT NOR ANY CONTRIBUTORS
207
+ SHALL HAVE ANY LIABILITY FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
208
+ EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING WITHOUT LIMITATION LOST
209
+ PROFITS), HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
210
+ CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
211
+ ARISING IN ANY WAY OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE
212
+ EXERCISE OF ANY RIGHTS GRANTED HEREUNDER, EVEN IF ADVISED OF THE
213
+ POSSIBILITY OF SUCH DAMAGES.
214
+
215
+ 7. GENERAL
216
+
217
+ If any provision of this Agreement is invalid or unenforceable under
218
+ applicable law, it shall not affect the validity or enforceability of
219
+ the remainder of the terms of this Agreement, and without further
220
+ action by the parties hereto, such provision shall be reformed to the
221
+ minimum extent necessary to make such provision valid and enforceable.
222
+
223
+ If Recipient institutes patent litigation against any entity
224
+ (including a cross-claim or counterclaim in a lawsuit) alleging that the
225
+ Program itself (excluding combinations of the Program with other software
226
+ or hardware) infringes such Recipient's patent(s), then such Recipient's
227
+ rights granted under Section 2(b) shall terminate as of the date such
228
+ litigation is filed.
229
+
230
+ All Recipient's rights under this Agreement shall terminate if it
231
+ fails to comply with any of the material terms or conditions of this
232
+ Agreement and does not cure such failure in a reasonable period of
233
+ time after becoming aware of such noncompliance. If all Recipient's
234
+ rights under this Agreement terminate, Recipient agrees to cease use
235
+ and distribution of the Program as soon as reasonably practicable.
236
+ However, Recipient's obligations under this Agreement and any licenses
237
+ granted by Recipient relating to the Program shall continue and survive.
238
+
239
+ Everyone is permitted to copy and distribute copies of this Agreement,
240
+ but in order to avoid inconsistency the Agreement is copyrighted and
241
+ may only be modified in the following manner. The Agreement Steward
242
+ reserves the right to publish new versions (including revisions) of
243
+ this Agreement from time to time. No one other than the Agreement
244
+ Steward has the right to modify this Agreement. The Eclipse Foundation
245
+ is the initial Agreement Steward. The Eclipse Foundation may assign the
246
+ responsibility to serve as the Agreement Steward to a suitable separate
247
+ entity. Each new version of the Agreement will be given a distinguishing
248
+ version number. The Program (including Contributions) may always be
249
+ Distributed subject to the version of the Agreement under which it was
250
+ received. In addition, after a new version of the Agreement is published,
251
+ Contributor may elect to Distribute the Program (including its
252
+ Contributions) under the new version.
253
+
254
+ Except as expressly stated in Sections 2(a) and 2(b) above, Recipient
255
+ receives no rights or licenses to the intellectual property of any
256
+ Contributor under this Agreement, whether expressly, by implication,
257
+ estoppel or otherwise. All rights in the Program not expressly granted
258
+ under this Agreement are reserved. Nothing in this Agreement is intended
259
+ to be enforceable by any entity that is not a Contributor or Recipient.
260
+ No third-party beneficiary rights are created under this Agreement.
261
+
262
+ Exhibit A - Form of Secondary Licenses Notice
263
+
264
+ "This Source Code may also be made available under the following
265
+ Secondary Licenses when the conditions for such availability set forth
266
+ in the Eclipse Public License, v. 2.0 are satisfied: {name license(s),
267
+ version(s), and exceptions or additional permissions here}."
268
+
269
+ Simply including a copy of this Agreement, including this Exhibit A
270
+ is not sufficient to license the Source Code under Secondary Licenses.
271
+
272
+ If it is not possible or desirable to put the notice in a particular
273
+ file, then You may include the notice in a location (such as a LICENSE
274
+ file in a relevant directory) where a recipient would be likely to
275
+ look for such a notice.
276
+
277
+ You may add additional accurate notices of copyright ownership.
Makefile ADDED
@@ -0,0 +1,91 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # bit-string-accelerator: build and verification entry points.
2
+ #
3
+ # make test everything below (what CI runs)
4
+ # make lint verilator -Wall on rtl/bit_accelerator.sv
5
+ # make sim self-checking testbench under Icarus and Verilator
6
+ # make formal Why3 proofs in formal/ (every goal must be proved by Z3)
7
+ # make spice ngspice timing model, fails if the delay is not measured
8
+ # make accel the bit_accelerator/ v2 design (lint, sim, formal)
9
+ # make gpu the Rust OpenCL crate in gpu/ (fmt, clippy, tests)
10
+ # make fpga FPGA wrapper: lint, UART testbench, host co-simulation, bitstreams
11
+ # make fpga-gl FPGA wrapper on post-synthesis netlists (slow, ~10 min)
12
+ # make asic sky130 synthesis + proof that the netlist equals the RTL
13
+ # make pcie parallel engine + PCIe core: lint, equivalence vs the reference core
14
+ # make tapeout Tiny Tapeout project: sources in sync, RTL test at both divisors
15
+
16
+ IVERILOG ?= iverilog
17
+ VVP ?= vvp
18
+ VERILATOR ?= verilator
19
+ NGSPICE ?= ngspice
20
+ WHY3_PROVER ?= z3
21
+ WHY3_TIME ?= 30
22
+ BUILD ?= build
23
+ SEED ?= 1
24
+ OPS ?= 2000
25
+
26
+ RTL := rtl/bit_accelerator.sv
27
+ TB := verification/tb_bit_accelerator.sv
28
+ FORMAL := formal/bit_address.mlw formal/bit_extract.mlw formal/lane_map.mlw
29
+ PROVE := bit_accelerator/scripts/prove.sh
30
+
31
+ .PHONY: all test lint sim sim-icarus sim-verilator formal spice accel gpu fpga fpga-gl asic pcie tapeout clean
32
+ .DEFAULT_GOAL := test
33
+
34
+ all test: lint sim formal spice accel gpu fpga asic pcie tapeout
35
+
36
+ lint:
37
+ $(VERILATOR) --lint-only -Wall $(RTL)
38
+
39
+ sim: sim-icarus sim-verilator
40
+
41
+ sim-icarus:
42
+ mkdir -p $(BUILD)
43
+ $(IVERILOG) -g2012 -o $(BUILD)/tb.vvp $(RTL) $(TB)
44
+ $(VVP) -n $(BUILD)/tb.vvp +seed=$(SEED) +ops=$(OPS)
45
+
46
+ sim-verilator:
47
+ mkdir -p $(BUILD)/verilator
48
+ $(VERILATOR) --binary --timing --timescale 1ns/1ps -Wno-fatal -Wno-lint --top-module tb_bit_accelerator \
49
+ -Mdir $(BUILD)/verilator $(RTL) $(TB) >/dev/null
50
+ $(BUILD)/verilator/Vtb_bit_accelerator +seed=$(SEED) +ops=$(OPS)
51
+
52
+ formal:
53
+ $(PROVE) -P $(WHY3_PROVER) -t $(WHY3_TIME) $(FORMAL)
54
+
55
+ spice:
56
+ mkdir -p $(BUILD)
57
+ $(NGSPICE) -b spice/bit_extract.sp > $(BUILD)/spice.log 2>&1
58
+ @grep -E '^tpd *= *[0-9.e+-]+' $(BUILD)/spice.log || { cat $(BUILD)/spice.log; echo "tpd not measured"; exit 1; }
59
+
60
+ accel:
61
+ $(MAKE) -C bit_accelerator test
62
+
63
+ gpu:
64
+ cd gpu && cargo fmt --check
65
+ cd gpu && cargo clippy --all-targets -- -D warnings
66
+ # Serial: PoCL 5.0 can abort when several contexts are released concurrently.
67
+ cd gpu && RUST_TEST_THREADS=1 cargo test
68
+
69
+ fpga:
70
+ $(MAKE) -C fpga lint sim cosim icebreaker ulx3s
71
+
72
+ fpga-gl:
73
+ $(MAKE) -C fpga gl-sim
74
+
75
+ asic:
76
+ $(MAKE) -C asic all
77
+
78
+ pcie:
79
+ $(MAKE) -C pcie lint sim sim-verilator
80
+
81
+ tapeout:
82
+ $(MAKE) -C tapeout check-sync test
83
+
84
+ clean:
85
+ rm -rf $(BUILD) simv
86
+ $(MAKE) -C bit_accelerator clean
87
+ $(MAKE) -C fpga clean
88
+ $(MAKE) -C asic clean
89
+ $(MAKE) -C pcie clean
90
+ $(MAKE) -C tapeout clean
91
+ cd gpu && cargo clean
README.md ADDED
@@ -0,0 +1,113 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ ---
2
+ license: epl-2.0
3
+ tags:
4
+ - snapkitty
5
+ - october-2026-drop
6
+ - systemverilog
7
+ - rtl
8
+ - fpga
9
+ - asic
10
+ - formal-verification
11
+ ---
12
+
13
+ > Mirrored from [https://github.com/SNAPKITTYAGENT9NOVA/bit-string-accelerator](https://github.com/SNAPKITTYAGENT9NOVA/bit-string-accelerator) at commit `d2b5cfe`. Part of the **SnapKitty October 2026 main drop**.
14
+
15
+ # bit-string-accelerator
16
+
17
+ [![CI](https://github.com/SNAPKITTYAGENT9NOVA/bit-string-accelerator/actions/workflows/ci.yml/badge.svg)](https://github.com/SNAPKITTYAGENT9NOVA/bit-string-accelerator/actions/workflows/ci.yml)
18
+
19
+ Synthesizable SystemVerilog bit-string accelerator for deterministic 64-bit-word bit addressing.
20
+
21
+ effective_bit_address = (base_address * 8) + bit_offset (mod 2^64)
22
+ word_address = (effective_bit_address / 64) * 8
23
+ bit_index = effective_bit_address mod 64
24
+
25
+ Operations: GET, TEST, SET, CLEAR, TOGGLE. Interface contract and verification
26
+ evidence: [`docs/verification.md`](docs/verification.md).
27
+
28
+ ## Layout
29
+
30
+ | Path | Contents |
31
+ |------|----------|
32
+ | `rtl/`, `verification/`, `formal/`, `isa/`, `spice/`, `docs/` | Compact accelerator, its self-checking testbench, Why3 proofs, ISA and timing model |
33
+ | `bit_accelerator/` | Multi-stage v2 accelerator with its own testbench and proofs (also in `rust-opencl-gpu`) |
34
+ | `fpga/` | Hardware build: UART + block-RAM wrapper, iCEBreaker and ULX3S bitstreams, host tool `bitacc` ([`fpga/README.md`](fpga/README.md)) |
35
+ | `asic/` | sky130 standard-cell synthesis, equivalence proof, timing ([`asic/README.md`](asic/README.md)) |
36
+ | `pcie/` | Parallel engine with range operations (count, find, fill, bulk logic, pattern match) + PCIe core for the LiteFury, LiteX SoC, host program, open-source timing flow ([`pcie/README.md`](pcie/README.md)) |
37
+ | `tapeout/` | Tiny Tapeout (ttsky26d, sky130A) project, hardened and prechecked ([`tapeout/README.md`](tapeout/README.md), [`tapeout/SIGNOFF.md`](tapeout/SIGNOFF.md)) |
38
+ | `gpu/` | Rust/OpenCL (`ocl`) crate from `rust-opencl-gpu` |
39
+ | `.github/workflows/ci.yml` | CI: lint, simulation, proofs, SPICE, Rust |
40
+
41
+ ## Requirements
42
+
43
+ Ubuntu 24.04:
44
+
45
+ ```sh
46
+ sudo apt-get install iverilog verilator why3 z3 ngspice pocl-opencl-icd ocl-icd-opencl-dev \
47
+ yosys nextpnr-ice40 nextpnr-ecp5 fpga-icestorm fpga-trellis
48
+ why3 config detect
49
+ ```
50
+
51
+ plus a Rust toolchain (1.85 or newer) for `gpu/`. `pocl-opencl-icd` provides a
52
+ CPU OpenCL device; any other OpenCL driver works too.
53
+
54
+ ## Build and test
55
+
56
+ ```sh
57
+ make test # everything CI runs
58
+ make lint # verilator -Wall
59
+ make sim # testbench under Icarus and Verilator (SEED=n OPS=n to vary)
60
+ make formal # Why3 proofs, every goal must be proved by Z3
61
+ make spice # ngspice timing model
62
+ make accel # bit_accelerator/ v2: lint, sim, proofs
63
+ make gpu # gpu/: cargo fmt, clippy, tests
64
+ make fpga # FPGA wrapper: lint, testbench, host co-simulation, both bitstreams
65
+ make fpga-gl # FPGA wrapper on post-synthesis netlists (slow)
66
+ make asic # sky130 synthesis + RTL/netlist equivalence proof
67
+ make pcie # parallel engine + PCIe core vs the reference core (make -j helps)
68
+ make tapeout # Tiny Tapeout project: RTL test at both divisor settings
69
+ ```
70
+
71
+ ## Roadmap
72
+
73
+ Single-op core (reference, proofs) → parallel engine (`pcie/`, identical
74
+ results) → DMA work queue → range operations (one descriptor, up to the whole
75
+ bit store) → LiteFury PCIe prototype → custom PCIe board, with the Tiny
76
+ Tapeout chip (`tapeout/`) as a separate silicon proof of the core.
77
+ The PCIe design does not depend on the transport, so the same card works in
78
+ the NUC's M.2 slot or in a USB4/Thunderbolt enclosure.
79
+
80
+ ## Running on hardware
81
+
82
+ `make -C fpga icebreaker prog-icebreaker` (or `ulx3s prog-ulx3s`) builds and
83
+ loads a bitstream. Then `bitacc --port /dev/ttyUSB1 selftest` runs the on-board
84
+ acceptance test. See [`fpga/README.md`](fpga/README.md).
85
+
86
+ | Target | Size | Speed |
87
+ |---|---|---|
88
+ | iCE40UP5K (iCEBreaker), core + UART + RAM | 1138 LC (21%), 4 BRAM | 39.06 MHz (12 MHz board clock) |
89
+ | ECP5 25F (ULX3S), core + UART + RAM | 1171 LUT4 (4%), 2 BRAM | 73.22 MHz (25 MHz board clock) |
90
+ | sky130 HD standard cells, core only | 1538 cells, 10,063 µm² | 500 MHz pre-layout, typical corner |
91
+
92
+ GPU tests run serially (`RUST_TEST_THREADS=1`): PoCL 5.0 can abort with a
93
+ `pocl_release_dlhandle_cache` assertion when several OpenCL contexts are released
94
+ from different threads at the same time. With one test thread it passed 40 of
95
+ 40 runs, against 26 of 40 with parallel threads.
96
+
97
+ ## Known limits
98
+
99
+ - BIT_TEST behaves like BIT_GET; there is no separate condition flag output.
100
+ - `base_address << 3` drops the top 3 bits of `base_address` (64-bit wrap).
101
+ - The bitstreams have not been run on a physical board yet (no board was available); pin
102
+ assignments come from the boards' reference constraint files.
103
+ - `asic/` numbers are pre-layout for the bare core. `tapeout/` has a full layout (GDS) of the
104
+ Tiny Tapeout top that passes DRC, LVS, antenna, timing and the Tiny Tapeout precheck; it has
105
+ not been submitted or fabricated. The SPICE deck is an RC model, not extracted silicon.
106
+ - The PCIe design has not run on a LiteFury: the bitstream needs Vivado. An open-source place
107
+ and route (nextpnr-xilinx) reaches 88 MHz (84 MHz with a 2-unit MATCH), not 125 MHz;
108
+ Vivado's result is unknown. The card is slower than one CPU core for COUNT/BULK; MATCH
109
+ (pattern search) with 2 units is expected to be about 2x a 4-thread CPU at 125 MHz and about
110
+ 1.2-1.5x at 84 MHz; see `pcie/README.md`.
111
+
112
+ The Windows OpenCL SDK and `OpenCL.lib` from `rust-opencl-gpu` are not included
113
+ here; the `ocl` crate locates the system OpenCL library.
asic/Makefile ADDED
@@ -0,0 +1,64 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # ASIC synthesis of rtl/bit_accelerator.sv to the SkyWater sky130 high-density
2
+ # standard cells (sky130_fd_sc_hd, typical corner 25 C / 1.80 V).
3
+ #
4
+ # make synth Yosys + ABC (buffering and gate sizing) -> build/bit_accelerator_sky130.v
5
+ # make equiv prove the gate netlist equivalent to the RTL (Yosys equiv_*)
6
+ # make sta OpenSTA at PERIOD ns (needs `sta` on PATH or STA=/path/to/sta)
7
+ # make all synth + equiv
8
+ #
9
+ # Pre-layout only: no floorplan, placement, clock tree or wire parasitics.
10
+
11
+ YOSYS ?= yosys
12
+ STA ?= sta
13
+ PERIOD ?= 2.0
14
+ BUILD ?= build
15
+
16
+ ORFS_COMMIT := 2aeb23bcc3b5aa925abb991c4347ce73827b8b82
17
+ LIB_URL := https://raw.githubusercontent.com/The-OpenROAD-Project/OpenROAD-flow-scripts/$(ORFS_COMMIT)/flow/platforms/sky130hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib
18
+ LIB_SHA256 := ec0e1067a35c8bf20b11e58d1e8ac53326067e4dac84a125cc1b917a3518d0d9
19
+ LIB := $(BUILD)/sky130_fd_sc_hd__tt_025C_1v80.lib
20
+ RTL := ../rtl/bit_accelerator.sv
21
+ NETLIST := $(BUILD)/bit_accelerator_sky130.v
22
+
23
+ .PHONY: all synth equiv sta clean
24
+ .DEFAULT_GOAL := all
25
+
26
+ all: synth equiv
27
+
28
+ $(LIB):
29
+ mkdir -p $(BUILD)
30
+ curl -sSfL -o $@.tmp $(LIB_URL)
31
+ echo "$(LIB_SHA256) $@.tmp" | sha256sum -c --quiet
32
+ mv $@.tmp $@
33
+
34
+ synth: $(NETLIST)
35
+
36
+ # -nofsm keeps the RTL state encoding so the equivalence check can match registers.
37
+ $(NETLIST): $(RTL) $(LIB) abc.script
38
+ $(YOSYS) -q -l $(BUILD)/synth.log -p "read_verilog -sv $(RTL); \
39
+ synth -nofsm -flatten -top bit_accelerator; \
40
+ dfflibmap -liberty $(LIB); \
41
+ abc -liberty $(LIB) -D 2000 -script abc.script; \
42
+ opt_clean; tee -o $(BUILD)/area.rpt stat -liberty $(LIB); \
43
+ write_verilog -noattr -noexpr $@" 2>&1 | grep -v "unsupported expression" || true
44
+ @test -s $@
45
+ @grep -E "Number of cells:|Chip area" $(BUILD)/area.rpt
46
+
47
+ equiv: $(NETLIST)
48
+ $(YOSYS) -q -l $(BUILD)/equiv.log -p " \
49
+ read_verilog -sv $(RTL); prep -flatten -top bit_accelerator; \
50
+ rename bit_accelerator gold; design -stash gold; \
51
+ read_liberty -ignore_miss_func $(LIB); read_verilog $(NETLIST); \
52
+ hierarchy -top bit_accelerator; flatten; rename bit_accelerator gate; design -stash gate; \
53
+ design -copy-from gold -as gold gold; design -copy-from gate -as gate gate; \
54
+ equiv_make gold gate equiv; hierarchy -top equiv; async2sync; \
55
+ equiv_simple -seq 5; equiv_induct -seq 5; equiv_status -assert" 2>&1 | grep -v "unsupported expression" || true
56
+ @grep -q "Equivalence successfully proven" $(BUILD)/equiv.log
57
+ @grep -E "proven and" $(BUILD)/equiv.log | tail -1
58
+
59
+ sta: $(NETLIST)
60
+ LIB=$(LIB) NETLIST=$(NETLIST) PERIOD=$(PERIOD) $(STA) -no_init -exit sta.tcl | tee $(BUILD)/sta_$(PERIOD)ns.rpt
61
+ @! grep -q VIOLATED $(BUILD)/sta_$(PERIOD)ns.rpt
62
+
63
+ clean:
64
+ rm -rf $(BUILD)
asic/README.md ADDED
@@ -0,0 +1,32 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # ASIC synthesis (sky130)
2
+
3
+ Synthesizes `rtl/bit_accelerator.sv` to the SkyWater 130 nm high-density standard
4
+ cells (`sky130_fd_sc_hd`, typical corner, 25 °C, 1.80 V). The liberty file is
5
+ downloaded from OpenROAD-flow-scripts at a pinned commit and checked by SHA-256.
6
+
7
+ ```sh
8
+ make # synth + equiv
9
+ make sta STA=/path/to/sta PERIOD=2.0
10
+ ```
11
+
12
+ Needs Yosys. `make sta` needs [OpenSTA](https://github.com/The-OpenROAD-Project/OpenSTA)
13
+ (build it from source with CUDD; it is not packaged for Ubuntu).
14
+
15
+ ## Results
16
+
17
+ | | |
18
+ |---|---|
19
+ | Cells | 1538 (139 flip-flops, plus buffers inserted for fanout) |
20
+ | Cell area | 10,063 µm² (about 0.010 mm²) |
21
+ | Equivalence to RTL | proved: 223/223 `$equiv` points (Yosys `equiv_simple` + `equiv_induct`) |
22
+ | Timing, 2.0 ns (500 MHz) | met: WNS 0.00 ns, no slew/capacitance/fanout violations |
23
+ | Timing, 1.9 ns | fails: WNS -0.03 ns |
24
+
25
+ These are **pre-layout** numbers: no floorplan, placement, clock tree or wire
26
+ parasitics. Inputs are assumed registered on the same clock. Post-layout Fmax
27
+ will be lower. Getting to a GDS for fabrication (OpenLane or
28
+ OpenROAD-flow-scripts, then a shuttle) is not done here.
29
+
30
+ Synthesis uses `-nofsm` so the gate netlist keeps the RTL state encoding, which
31
+ lets the equivalence check match registers. With FSM re-encoding, Yosys could
32
+ not prove 135 of 220 points without a sequential proof across encodings.
asic/abc.script ADDED
@@ -0,0 +1,11 @@
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # ABC mapping script: map to sky130 cells, then buffer high-fanout nets and
2
+ # resize gates against the liberty timing (as OpenLane does before placement).
3
+ strash
4
+ dch
5
+ map -B 0.9
6
+ topo
7
+ stime -c
8
+ buffer -c -N 8
9
+ upsize -c
10
+ dnsize -c
11
+ stime -p
asic/sta.tcl ADDED
@@ -0,0 +1,16 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # Pre-layout static timing for the sky130 netlist (OpenSTA).
2
+ # Environment: LIB (liberty), NETLIST (gate-level Verilog), PERIOD (ns).
3
+ read_liberty $::env(LIB)
4
+ read_verilog $::env(NETLIST)
5
+ link_design bit_accelerator
6
+ create_clock -name clk -period $::env(PERIOD) [get_ports clk]
7
+ # Inputs come from, and outputs go to, registers on the same clock.
8
+ set_input_delay 0 -clock clk [delete_from_list [all_inputs] [get_ports clk]]
9
+ set_output_delay 0 -clock clk [all_outputs]
10
+ set_input_transition 0.1 [all_inputs]
11
+ set_load 0.005 [all_outputs]
12
+ report_checks -path_delay max -digits 3
13
+ report_check_types -max_slew -max_capacitance -max_fanout -violators
14
+ report_wns
15
+ report_tns
16
+ exit
bit_accelerator/.gitignore ADDED
@@ -0,0 +1,2 @@
 
 
 
1
+ build/
2
+ obj_dir/
bit_accelerator/IMPLEMENTATION_REPORT.md ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # bit_accelerator_v2 - Verified Status
2
+
3
+ Everything below was measured by running `make test` (Verilator 5.020, Icarus Verilog 12.0,
4
+ Why3 1.6.0 with Z3 4.8.12).
5
+
6
+ ## Result
7
+ - Simulation: `checks=182 fails=0` under both Verilator and Icarus.
8
+ - Lint: `verilator --lint-only -Wall` clean.
9
+ - Formal: 33/33 Why3 goals valid with Z3.
10
+
11
+ ## Observed cycle timing (1-cycle-latency memory, no stalls)
12
+ a = cycle in which `op_valid && op_ready` is sampled.
13
+
14
+ | Op | Timeline |
15
+ |----|----------|
16
+ | BIT_GET | READ_REQUEST a+1, READ_RESPONSE a+2, RESULT_VALID a+3 (one cycle) |
17
+ | SET/CLEAR/TOGGLE | READ_REQUEST a+1, READ_RESPONSE a+2, MODIFY a+3, WRITE accepted a+4, RESULT_VALID a+6 |
18
+ | Write stalled (`mem_ready=0` a+4..a+6) | request and wdata held, accepted a+7, RESULT_VALID a+9 |
19
+ | Read stalled (`mem_ready=0` a+1..a+2) | accepted a+3, response a+4, RESULT_VALID a+5 |
20
+
21
+ ## Covered by the testbench
22
+ - Result value for GET (set/clear bits, cross-word offsets, non-zero base).
23
+ - Memory contents after SET/CLEAR/TOGGLE, including word 1 targets.
24
+ - Exactly one `result_valid` pulse per op; `op_ready` low while busy.
25
+ - Write and read backpressure: signals held stable, no early result, write committed once.
26
+ - Reset asserted in each of READ_REQUEST, READ_WAIT, MODIFY, WRITE_REQUEST, WRITE_WAIT:
27
+ no `result_valid`, no write after reset, DUT idle, and a fresh op completes normally.
28
+
29
+ ## Defects found by simulation and fixed
30
+ 1. `result_valid` was registered, so it appeared one cycle later than specified (a+4 instead of a+3).
31
+ It is now combinational from `ST_RESULT`.
32
+ 2. A reset in the same cycle as a write handshake let the memory commit the write.
33
+ `mem_valid/mem_write/mem_wstrb/mem_wdata` are now forced low while `reset` is asserted.
34
+ 3. `error` was set on any `mem_fault`; it is now cleared on accept and set only in `ST_READ_WAIT`.
35
+ 4. Read-fault tests were added (GET/SET/TOGGLE): `error` is high in the result cycle, no write
36
+ is issued, and the next operation clears it. The testbench now exits non-zero on failure.
37
+ 5. Lint fixes: explicit zero-extension of `mem_addr`, bit extraction reads `read_word[bit_index]` directly.
38
+ 6. The previous testbench did not compile, sampled after the clock edge (racy), and modeled
39
+ 2-cycle read latency. It was rewritten to log pre-edge values per cycle.
40
+
41
+ ## Not verified / known limits
42
+ - Only read faults exist; there is no write-fault input path.
43
+ - `BIT_TEST` (3'b001) behaves like GET; no flag output exists.
44
+ - `base_address << 3` truncates the top 3 bits of `base_address`, and `mem_addr` is 61 significant bits.
45
+ - The Why3 proofs cover the specification; RTL-to-specification agreement is checked by simulation only.
46
+ - Undefined opcodes (101-111) execute as a read with no write and no error.
47
+ - No synthesis was run; area/power/frequency numbers elsewhere in this repo are estimates.
bit_accelerator/Makefile ADDED
@@ -0,0 +1,55 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # bit_accelerator build and verification.
2
+ #
3
+ # The verified design is bit_accelerator_v2 (rtl/bit_accelerator_v2.sv).
4
+ # The v1 sources (bit_accelerator.sv and its submodules) are kept for reference
5
+ # only and are not built: v1 multiply-drives result_valid/result_bit and its
6
+ # testbench does not compile. See README.md, "Design versions".
7
+
8
+ VERILATOR ?= verilator
9
+ IVERILOG ?= iverilog
10
+ VVP ?= vvp
11
+ WHY3_PROVER ?= z3
12
+ WHY3_TIME ?= 30
13
+ BUILD ?= build
14
+
15
+ V2_RTL := rtl/bit_accelerator_v2.sv
16
+ V2_TB := testbenches/tb_bit_accelerator_v2.sv
17
+ FORMAL := formal/bit_addressing.mlw formal/bit_addressing_proofs.mlw
18
+
19
+ .PHONY: help all test lint sim sim-verilator sim-icarus formal formal-cvc4 clean
20
+ .DEFAULT_GOAL := help
21
+
22
+ all test: lint sim formal
23
+
24
+ lint:
25
+ $(VERILATOR) --lint-only -Wall $(V2_RTL)
26
+
27
+ sim: sim-verilator sim-icarus
28
+
29
+ sim-verilator:
30
+ OUT=$(abspath $(BUILD))/verilator ./run_v2_sim.sh
31
+
32
+ sim-icarus:
33
+ mkdir -p $(BUILD)
34
+ $(IVERILOG) -g2012 -o $(BUILD)/tb_v2.vvp $(V2_RTL) $(V2_TB)
35
+ $(VVP) -n $(BUILD)/tb_v2.vvp
36
+
37
+ formal:
38
+ ./scripts/prove.sh -P $(WHY3_PROVER) -t $(WHY3_TIME) -L formal $(FORMAL)
39
+
40
+ # Cross-check with CVC4. Informational: CVC4 does not discharge every goal
41
+ # within the time limit, Z3 does.
42
+ formal-cvc4:
43
+ -./scripts/prove.sh -P cvc4 -t $(WHY3_TIME) -L formal $(FORMAL)
44
+
45
+ clean:
46
+ rm -rf $(BUILD) obj_dir
47
+
48
+ help:
49
+ @echo "make test lint + both simulators + Why3 proofs"
50
+ @echo "make lint verilator -Wall on the v2 RTL"
51
+ @echo "make sim v2 testbench under Verilator and Icarus"
52
+ @echo "make formal prove formal/*.mlw with $(WHY3_PROVER) (every goal must be Valid)"
53
+ @echo "make formal-cvc4 informational CVC4 cross-check"
54
+ @echo "make clean remove $(BUILD)/"
55
+ @echo "Needs: verilator >= 5, iverilog >= 12, why3 >= 1.6 with z3 (why3 config detect)"
bit_accelerator/README.md ADDED
@@ -0,0 +1,200 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # Bit-String Hardware Accelerator
2
+
3
+ A dedicated hardware accelerator for bit-string operations with formal verification.
4
+
5
+ ## Architecture Overview
6
+
7
+ ```
8
+ request (base_address + bit_offset)
9
+ ↓
10
+ STAGE 1: Address Generator (base + offset)
11
+ ↓
12
+ STAGE 2: Word & Bit Index Calculator (÷64, mod 64)
13
+ ↓
14
+ STAGE 3: Memory Access (TLB → L1 Cache)
15
+ ↓
16
+ STAGE 4: Bit Extraction (barrel shifter + AND)
17
+ ↓
18
+ STAGE 5: Writeback (register result)
19
+ ↓
20
+ result (0 or 1)
21
+ ```
22
+
23
+ ## Supported Operations
24
+
25
+ - **BIT_GET** (0b000): Read single bit value
26
+ - **BIT_TEST** (0b001): Test bit and set condition flag
27
+ - **BIT_SET** (0b010): Set single bit to 1 (read-modify-write)
28
+ - **BIT_CLEAR** (0b011): Clear single bit to 0 (read-modify-write)
29
+ - **BIT_TOGGLE** (0b100): Toggle single bit (read-modify-write)
30
+
31
+ ## Design versions
32
+
33
+ | Version | Files | Status |
34
+ |---------|-------|--------|
35
+ | **v2** | `rtl/bit_accelerator_v2.sv` | Verified design. Lint-clean (`verilator -Wall`), 182 testbench checks pass under Verilator and Icarus. |
36
+ | v1 | `rtl/bit_accelerator.sv` + submodules | Reference only, not built. `result_valid`/`result_bit` are driven from two processes, and its testbench does not compile. |
37
+
38
+ ## Interface (v2)
39
+
40
+ ```systemverilog
41
+ // Operation interface
42
+ input logic op_valid; output logic op_ready;
43
+ input logic [63:0] base_address; // byte address
44
+ input logic [63:0] bit_offset; // bit offset from base
45
+ input logic [2:0] operation; // 000 GET, 001 TEST, 010 SET, 011 CLEAR, 100 TOGGLE
46
+ output logic result_valid; // one-cycle pulse
47
+ output logic result_bit; // valid with result_valid
48
+ output logic error; // set by a read fault, valid with result_valid,
49
+ // held until the next operation is accepted
50
+ // Memory interface (valid/ready)
51
+ output logic mem_valid, mem_write;
52
+ output logic [63:0] mem_addr; // 8-byte-aligned byte address
53
+ output logic [63:0] mem_wdata; output logic [7:0] mem_wstrb;
54
+ input logic mem_ready, mem_rvalid, mem_fault;
55
+ input logic [63:0] mem_rdata;
56
+ ```
57
+
58
+ Opcodes 101-111 are undefined; v2 executes them as a read with no write.
59
+ Write faults are not modelled.
60
+
61
+ ### Address calculation
62
+
63
+ ```
64
+ absolute_bit = (base_address * 8) + bit_offset (mod 2^64)
65
+ word_address = absolute_bit / 64
66
+ bit_index = absolute_bit mod 64
67
+ result = (memory[word_address] >> bit_index) & 1
68
+ ```
69
+
70
+ ## Directory structure
71
+
72
+ ```
73
+ bit_accelerator/
74
+ ├── rtl/bit_accelerator_v2.sv # verified design
75
+ ├── rtl/*.sv # v1 (reference only)
76
+ ├── testbenches/tb_bit_accelerator_v2.sv
77
+ ├── formal/bit_addressing.mlw # specification + lemmas (Why3)
78
+ ├── formal/bit_addressing_proofs.mlw # derived lemmas
79
+ ├── scripts/prove.sh # proves every goal; fails unless all are Valid
80
+ ├── isa/BIT_ISA.md, docs/DATAPATH.md
81
+ ├── Makefile, build.sh, run_v2_sim.sh
82
+ └── IMPLEMENTATION_REPORT.md # measured results
83
+ ```
84
+
85
+ ## Build and verification
86
+
87
+ Prerequisites (Ubuntu 24.04): `apt-get install verilator iverilog why3 z3`, then `why3 config detect`.
88
+
89
+ ```bash
90
+ make test # lint + Verilator + Icarus simulation + Why3 proofs
91
+ make lint # verilator --lint-only -Wall on v2
92
+ make sim # v2 testbench under both simulators
93
+ make formal # every Why3 goal must be proved by Z3
94
+ make formal-cvc4 # informational cross-check with CVC4
95
+ ./build.sh # same as make test, fails if a tool is missing
96
+ ```
97
+
98
+ ## Formal verification
99
+
100
+ `formal/` is checked by Why3 1.6 with Z3 4.8.12: **33/33 goals valid**, no
101
+ axioms beyond the Why3 standard library. The lemmas cover:
102
+
103
+ 1. Address decomposition: `addr = word * 64 + bit`, `0 <= bit < 64`, and (word, bit) determines the address.
104
+ 2. Boundaries: offset 64 reaches the next word; offsets 0-63 stay in one word **when the base is word-aligned** (`base mod 8 = 0`).
105
+ 3. Bit operations: GET returns 0 or 1 and is deterministic; GET after SET/CLEAR returns 1/0.
106
+ 4. Non-interference: SET or CLEAR on one word does not change a GET from another word.
107
+
108
+ An earlier draft of these files was not valid Why3 and stated three theorems
109
+ that are false (`bit_63_same_word`, `bit_index_wraps_at_64` without the
110
+ alignment condition, and `within_word_uniqueness`). Z3 proves their negations;
111
+ they were corrected.
112
+
113
+ The proofs are about the specification. Agreement between the specification
114
+ and the RTL is checked by simulation, not proved.
115
+
116
+ ## Testing
117
+
118
+ `tb_bit_accelerator_v2.sv` is cycle-accurate and self-checking (exits non-zero
119
+ on any failure). It checks:
120
+
121
+ - GET results (set and clear bits, offset 64, non-zero base) and exact cycle timing
122
+ - SET/CLEAR/TOGGLE memory contents, including cross-word offsets
123
+ - one `result_valid` pulse per operation; `op_ready` low while busy
124
+ - read and write backpressure: request and data held stable, write committed once
125
+ - reset in each of READ_REQUEST, READ_WAIT, MODIFY, WRITE_REQUEST, WRITE_WAIT
126
+ - read faults on GET/SET/TOGGLE: `error` in the result cycle, no write, cleared by the next op
127
+ - undefined opcodes: no write
128
+
129
+ ## Hardware estimates
130
+
131
+ The figures below are design targets, **not measured**: no synthesis,
132
+ place-and-route or power analysis has been run.
133
+
134
+ | Scenario | Latency |
135
+ |----------|---------|
136
+ | L1 cache hit | 4 cycles |
137
+ | L2 cache miss | 10-15 cycles |
138
+ | Memory miss | 50+ cycles |
139
+
140
+ - Gate count ~50k (7nm), area ~0.6 mm², power ~2.5 mW active, 1+ GHz
141
+
142
+ ## Performance Comparison
143
+
144
+ ### Traditional LOAD-SHIFT-AND Sequence
145
+
146
+ ```
147
+ LOAD r1, [base] (3-50 cycles: cache/memory)
148
+ SHIFT r1, r1, offset (1 cycle)
149
+ AND r1, r1, 1 (1 cycle)
150
+ TOTAL: 5-52 cycles
151
+ ```
152
+
153
+ ### Dedicated BIT_GET Instruction
154
+
155
+ ```
156
+ BIT_GET r1, base, offset (4-15 cycles: includes memory)
157
+ TOTAL: 4-15 cycles
158
+ IMPROVEMENT: 20-80% latency reduction
159
+ ```
160
+
161
+ ## Limitations & Future Work
162
+
163
+ ### Current Scope
164
+ - 64-bit word size (fixed)
165
+ - Single-bit operations only (no multi-bit extract yet)
166
+ - No atomic multiword operations
167
+ - No GPU integration
168
+
169
+ ### Future Extensions
170
+ - Variable-width field extraction
171
+ - Atomic compare-and-swap for multiword fields
172
+ - SIMD bit-parallel operations
173
+ - Hardware-assisted population count pipeline
174
+
175
+ ## Design Philosophy
176
+
177
+ This accelerator prioritizes:
178
+
179
+ 1. **Correctness**: Formal verification, not testing alone
180
+ 2. **Determinism**: No undefined behavior, no race conditions
181
+ 3. **Simplicity**: Minimal instruction set, orthogonal operations
182
+ 4. **Performance**: Single-digit cycle latency on hits
183
+ 5. **Verification**: Machine-checkable proofs, not documentation
184
+
185
+ ## References
186
+
187
+ ### Intel 64 & IA-32 Architecture
188
+ - Bit Manipulation Instructions (BMI, BMI2)
189
+ - BITFIELD, BIT_SET, BIT_CLEAR semantics
190
+
191
+ ### Hardware Design
192
+ - Kogge-Stone parallel-prefix adder (address gen)
193
+ - Logarithmic barrel shifter (bit extraction)
194
+ - Standard pipelined memory interface
195
+
196
+ ### Formal Methods
197
+ - Why3 platform for machine verification
198
+ - Euclidean division properties
199
+ - Non-interference proofs for memory operations
200
+
bit_accelerator/build.sh ADDED
@@ -0,0 +1,9 @@
 
 
 
 
 
 
 
 
 
 
1
+ #!/usr/bin/env bash
2
+ # Runs every check (lint, Verilator + Icarus simulation, Why3 proofs) and exits
3
+ # non-zero if any fails. Missing tools are reported as failures, not passes.
4
+ set -euo pipefail
5
+ cd "$(dirname "${BASH_SOURCE[0]}")"
6
+ for tool in verilator iverilog vvp why3; do
7
+ command -v "$tool" >/dev/null || { echo "missing tool: $tool" >&2; exit 1; }
8
+ done
9
+ make test
bit_accelerator/docs/DATAPATH.md ADDED
@@ -0,0 +1,437 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # Bit-Accelerator Datapath Architecture
2
+
3
+ ## 1. High-Level Datapath Diagram
4
+
5
+ ```
6
+ ┌─────────────────────────────────────────────────────────────────────┐
7
+ │ BIT ACCELERATOR DATAPATH │
8
+ └─────────────────────────────────────────────────────────────────────┘
9
+
10
+ Stage 0: DECODE & OPERAND FETCH
11
+ ┌──────────────┐
12
+ │ Opcode │──────────► Opcode Decoder (6-to-12 decoder)
13
+ │ Operands │──────────► Register File (3R1W)
14
+ │ │
15
+ └──────────────┘
16
+ │
17
+ ▼
18
+ Stage 1: ADDRESS GENERATION
19
+ ┌──────────────────────────────────────────┐
20
+ │ Adder (Rs1 + Rs2) ◄─── 64-bit Carry │
21
+ │ eff_bit_address = base + offset │
22
+ │ │
23
+ │ Output: 64-bit effective bit address │
24
+ └──────────────────────────────────────────┘
25
+ │
26
+ ▼
27
+ Stage 2: WORD & BIT INDEX CALCULATION
28
+ ┌──────────────────────────────────────┐
29
+ │ Divider / Shifter (÷64 & mod 64) │
30
+ │ word_index = eff_addr >> 6 │ Combinational or pipelined
31
+ │ bit_index = eff_addr & 0x3F │
32
+ │ │
33
+ │ Output: (word_index[57:0], bit_idx) │
34
+ └──────────────────────────────────────┘
35
+ │
36
+ ▼
37
+ Stage 3: MEMORY ACCESS & TLB LOOKUP
38
+ ┌──────────────────────────────────────────┐
39
+ │ TLB Lookup (word_index → phys_address) │
40
+ │ L1 Cache Tag/Index Match │
41
+ │ Memory Request to Load/Store Queue │
42
+ │ │
43
+ │ Output: 64-bit word from L1/L2/Memory │
44
+ └──────────────────────────────────────────┘
45
+ │
46
+ ▼
47
+ Stage 4: BIT EXTRACTION
48
+ ┌──────────────────────────────────────┐
49
+ │ Barrel Shifter │
50
+ │ (word >> bit_index) │
51
+ │ │
52
+ │ AND Gate (extract LSB) │
53
+ │ result = shifted_word & 1 │
54
+ │ │
55
+ │ Output: 1-bit result │
56
+ └──────────────────────────────────────┘
57
+ │
58
+ ▼
59
+ Stage 5: WRITEBACK
60
+ ┌──────────────────────────────────────┐
61
+ │ Register File Write │
62
+ │ result ──► Rd │
63
+ └──────────────────────────────────────┘
64
+ ```
65
+
66
+ ---
67
+
68
+ ## 2. Component Specifications
69
+
70
+ ### 2.1 Address Generator (Stage 1)
71
+
72
+ **Component**: 64-bit Ripple-Carry Adder or Kogge-Stone Parallel-Prefix Adder
73
+
74
+ **Inputs**:
75
+ - `base_address[63:0]` from Rs1 register
76
+ - `bit_offset[63:0]` from Rs2 register
77
+ - `carry_in` = 0
78
+
79
+ **Outputs**:
80
+ - `effective_bit_address[63:0]`
81
+
82
+ **Latency**: 1 cycle (Kogge-Stone) or 2 cycles (simpler adder)
83
+
84
+ **Control Signals**:
85
+ - `enable_add`: 1 if instruction requires address computation
86
+ - `select_operand`: 0 = Rs1+Rs2, 1 = Rs3+Rs4 (for multi-register ops)
87
+
88
+ ---
89
+
90
+ ### 2.2 Word and Bit Index Calculator (Stage 2)
91
+
92
+ **Component**: Fixed-Point Divider (÷ 64) and Modulo-64 Unit
93
+
94
+ **Inputs**:
95
+ - `effective_bit_address[63:0]` from Address Generator
96
+
97
+ **Outputs**:
98
+ - `word_index[57:0]` = `effective_bit_address >> 6`
99
+ - `bit_index[5:0]` = `effective_bit_address[5:0]`
100
+
101
+ **Hardware Implementation**:
102
+ ```
103
+ word_index[i] = effective_bit_address[i+6], for i = 0 to 57
104
+ bit_index[i] = effective_bit_address[i], for i = 0 to 5
105
+ ```
106
+ (This is purely combinational wiring - no logic!)
107
+
108
+ **Latency**: 0 cycles (combinational)
109
+
110
+ ---
111
+
112
+ ### 2.3 TLB & Cache Lookup (Stage 3)
113
+
114
+ **Component**: TLB (Translation Lookaside Buffer) + L1 Cache Controller
115
+
116
+ **Inputs**:
117
+ - `word_index[57:0]` (virtual word address, 6-bit aligned = 6 bits from effective address)
118
+ - Control: `is_load`, `is_store`
119
+
120
+ **Outputs**:
121
+ - `cache_hit` (1-bit flag)
122
+ - `data_word[63:0]` (from L1 cache on hit)
123
+ - `phys_address[40:0]` (for miss → L2/Memory)
124
+
125
+ **Behavior**:
126
+
127
+ **On Hit** (L1 cache, TLB translate):
128
+ - Return data directly from cache (fastest path)
129
+ - Latency: 1 cycle
130
+
131
+ **On Miss** (TLB or L1 cache miss):
132
+ - Initiate memory request to L2
133
+ - Stall pipeline until data returns
134
+ - Latency: variable (10+ cycles to L2, 50+ to main memory)
135
+
136
+ **Special Case: Page Boundary**:
137
+ - If `bit_address` and `(bit_address + 63)` span different pages:
138
+ - Hardware may need two memory accesses
139
+ - OR: Load both words and merge results (dual-load architecture)
140
+
141
+ ---
142
+
143
+ ### 2.4 Barrel Shifter (Stage 4)
144
+
145
+ **Component**: 64-bit Logarithmic Shifter
146
+
147
+ **Inputs**:
148
+ - `word[63:0]` from memory/cache
149
+ - `bit_index[5:0]` from Index Calculator
150
+ - `shift_direction` (0=right, 1=left, from decoder)
151
+ - `rotate_mode` (0=shift, 1=rotate)
152
+
153
+ **Implementation** (Rotating 64-bit barrel shifter):
154
+ ```
155
+ Level 0: Shift by 32: word[i] ← (shift_by_32 ? word[(i+32)%64] : word[i])
156
+ Level 1: Shift by 16: word[i] ← (shift_by_16 ? word[(i+16)%64] : word[i])
157
+ Level 2: Shift by 8: word[i] ← (shift_by_8 ? word[(i+8)%64] : word[i])
158
+ Level 3: Shift by 4: word[i] ← (shift_by_4 ? word[(i+4)%64] : word[i])
159
+ Level 4: Shift by 2: word[i] ← (shift_by_2 ? word[(i+2)%64] : word[i])
160
+ Level 5: Shift by 1: word[i] ← (shift_by_1 ? word[(i+1)%64] : word[i])
161
+
162
+ bit_index[5:0] is decoded into 6 control signals: {shift_by_32, ..., shift_by_1}
163
+ ```
164
+
165
+ **Outputs**:
166
+ - `shifted_word[63:0]`
167
+
168
+ **Latency**: 1 cycle (combinational through 6 levels of muxes)
169
+
170
+ ---
171
+
172
+ ### 2.5 Bit Extractor (Stage 4, after shifter)
173
+
174
+ **Component**: AND gate + optional sign-extension logic
175
+
176
+ **Inputs**:
177
+ - `shifted_word[63:0]` from Barrel Shifter
178
+ - `mask[63:0]` (computed from field width)
179
+ - Single bit: `mask = 64'h0000_0000_0000_0001`
180
+ - Multi-bit (width w): `mask = (1 << w) - 1`
181
+
182
+ **Outputs**:
183
+ - `extracted_field[63:0]` = `shifted_word & mask`
184
+
185
+ **For BITLOAD** (single-bit extract):
186
+ - Output: `result[63:0]` with `result[0] = extracted_field[0]`, `result[63:1] = 0`
187
+
188
+ **For BITFIELD** (multi-bit extract):
189
+ - Output: `result[63:0]` = extracted field, zero-extended
190
+
191
+ **Latency**: 1 cycle (combinational AND + logic)
192
+
193
+ ---
194
+
195
+ ### 2.6 Control Unit (Combinational + Sequential)
196
+
197
+ **Combinational Decoder**:
198
+ ```
199
+ Opcode[5:0] → 12 control signals:
200
+ - enable_addr_gen
201
+ - enable_mem_load
202
+ - enable_mem_store
203
+ - enable_shift
204
+ - enable_extract
205
+ - enable_writeback
206
+ - shift_direction (L/R)
207
+ - rotate_mode
208
+ - field_width[5:0]
209
+ - is_signed_extend
210
+ ```
211
+
212
+ **Sequential State Machine** (for cache misses, exceptions):
213
+ ```
214
+ State 0: IDLE → await instruction
215
+ State 1: EXECUTE → run datapath
216
+ State 2: MEMORY_WAIT → stall on L1 miss
217
+ State 3: EXCEPTION → handle fault
218
+ State 4: WRITEBACK → commit result
219
+ ```
220
+
221
+ ---
222
+
223
+ ### 2.7 Register File (3-Read, 1-Write Port)
224
+
225
+ **Capacity**: 32 × 64-bit registers
226
+
227
+ **Read Ports**:
228
+ - Port A: Rs1 (base address)
229
+ - Port B: Rs2 (offset/secondary operand)
230
+ - Port C: Rs3 (value to write for BITSTORE)
231
+
232
+ **Write Port**:
233
+ - Port W: Rd (destination register)
234
+
235
+ **Access Time**: 1 cycle (combinational read, synchronous write)
236
+
237
+ ---
238
+
239
+ ## 3. Data Flow for BITLOAD Instruction
240
+
241
+ **Instruction**: `BITLOAD R5, R10, R15`
242
+
243
+ ```
244
+ Clock | Stage | Operation
245
+ ------|-------|-------------------------------------------
246
+ 0 | 0 | Decode BITLOAD, fetch R10=0x1000, R15=0x42
247
+ | |
248
+ 1 | 1 | Address generator: eff_addr = 0x1000 + 0x42 = 0x1042
249
+ | |
250
+ 2 | 2 | Index calc (combinational):
251
+ | | word_idx = 0x1042 >> 6 = 0x41
252
+ | | bit_idx = 0x1042 & 0x3F = 0x02
253
+ | |
254
+ 3 | 3 | TLB lookup: word_index → phys_addr = 0x41000
255
+ | | L1 cache hit: word = 0xABCD_EF01_2345_6789
256
+ | |
257
+ 4 | 4 | Shifter: shifted = word >> 2 = 0x2AF37_BC04_8D15_9E
258
+ | | Extractor: result = shifted & 1 = 0
259
+ | |
260
+ 5 | 5 | Writeback: R5 ← 0
261
+ ```
262
+
263
+ ---
264
+
265
+ ## 4. Pipeline Depth Analysis
266
+
267
+ **Best Case** (L1 hit):
268
+ - Stage 0: Decode (1 cycle)
269
+ - Stage 1: Address gen (1 cycle)
270
+ - Stage 2: Index calc (0 cycles, combinational)
271
+ - Stage 3: Memory access (1 cycle hit)
272
+ - Stage 4: Extract (1 cycle)
273
+ - Stage 5: Writeback (committed)
274
+ - **Total: 4 cycles latency**
275
+
276
+ **Worst Case** (L2 miss, then main memory):
277
+ - Stages 0-3: same as above
278
+ - Stage 3: Memory miss, initiate L2 request (10+ cycles)
279
+ - Stage 4: Extract (1 cycle)
280
+ - **Total: 15+ cycles latency**
281
+
282
+ ---
283
+
284
+ ## 5. Throughput Analysis
285
+
286
+ **Instruction Issue Rate**: 1 instruction per cycle (assuming no structural hazards)
287
+
288
+ **Bottlenecks**:
289
+ - Memory bandwidth: If high % of instructions are BITLOAD/BITSTORE
290
+ - Cache behavior: Working set fit in L1 cache is critical
291
+ - Register contention: Low (3 reads, 1 write per cycle is feasible)
292
+
293
+ **Optimization**: Dual-issue for independent bit operations:
294
+ - Issue BITLOAD + BITCOUNT in same cycle (different functional units)
295
+
296
+ ---
297
+
298
+ ## 6. Critical Path (for clock frequency)
299
+
300
+ The critical path is the longest combinational delay in the pipeline:
301
+
302
+ ```
303
+ TDC = T_mux(operand select) + T_adder(64-bit) + T_setup(register)
304
+ ≈ 0.3ns + 1.2ns + 0.2ns = 1.7ns
305
+ ≈ 588 MHz (f_clock ≤ 1/1.7ns)
306
+ ```
307
+
308
+ For 1+ GHz target, require pipelined adder (Kogge-Stone):
309
+ ```
310
+ T_KS_adder ≈ 0.8ns → allows ~1.2 GHz
311
+ ```
312
+
313
+ ---
314
+
315
+ ## 7. Physical Implementation Details
316
+
317
+ ### 7.1 Gate Counts (Estimates)
318
+
319
+ | Component | Gates |
320
+ |-----------|-------|
321
+ | 64-bit Adder (Kogge-Stone) | 1,500 |
322
+ | Barrel Shifter (6 levels) | 4,000 |
323
+ | TLB (16-32 entries) | 5,000 |
324
+ | L1 Cache Interface | 10,000 |
325
+ | Register File (32×64) | 20,000 |
326
+ | Control Decoder + FSM | 3,000 |
327
+ | Data Muxes, AND gates, misc | 5,000 |
328
+ | **Total estimate** | **~50k gates** |
329
+
330
+ ### 7.2 Area Estimate
331
+
332
+ - Technology: 7nm FinFET
333
+ - Gate density: ~80M gates/mm²
334
+ - **Area ≈ 50k / 80M ≈ 0.6 mm²** (sub-mm² functional unit)
335
+
336
+ ### 7.3 Power Estimate
337
+
338
+ - Dynamic power: ~2mW (1 GHz, 1.2V, 50k gates, 80% switching activity)
339
+ - Static power: ~0.5mW (leakage)
340
+ - **Total: ~2.5mW** (idle or active, instruction-dependent)
341
+
342
+ ---
343
+
344
+ ## 8. Memory System Integration
345
+
346
+ ### 8.1 Memory Hierarchy
347
+
348
+ ```
349
+ CPU Pipeline
350
+ ↓
351
+ L1 I-Cache (32 KB) ←── 1 cycle (instructions)
352
+ L1 D-Cache (32 KB) ←── 1 cycle (data for BITLOAD)
353
+ ↓ (miss)
354
+ L2 Cache (256 KB) ←── 10 cycles
355
+ ↓ (miss)
356
+ L3 Cache (8 MB) ←── 30 cycles
357
+ ↓ (miss)
358
+ Main Memory (DDR4) ←── 50+ cycles
359
+ ```
360
+
361
+ ### 8.2 TLB Integration
362
+
363
+ ```
364
+ Virtual Bit Address (64-bit)
365
+ ↓
366
+ Extract word_index[57:0] = bit_address[63:6]
367
+ ↓
368
+ TLB lookup (16-entry, 4-way associative)
369
+ ├─► Hit: phys_word_addr = phys_base[40:0] | word_index[13:0]
370
+ ├─► Miss: page walk (25+ cycles)
371
+ ↓
372
+ L1 Cache tag lookup
373
+ ```
374
+
375
+ ### 8.3 Boundary Conditions
376
+
377
+ **Case 1**: Bit 0-63 fit in single 64-bit word
378
+ - Single memory access (normal path)
379
+
380
+ **Case 2**: Extract bits spanning two words (e.g., bits 60-65)
381
+ - Hardware loads both words
382
+ - Shifts, masks, combines
383
+ - Transparent to ISA
384
+
385
+ **Case 3**: Bits span two pages (e.g., word 0x1FFFF to 0x20000)
386
+ - May require two separate TLB lookups + memory accesses
387
+ - Hardware handles by stalling until both words available
388
+ - Or: Software constraint to avoid (less common)
389
+
390
+ ---
391
+
392
+ ## 9. Write-Path (BITSTORE)
393
+
394
+ ```
395
+ BITSTORE Rs1, Rs2, Rs3
396
+
397
+ Stage 1: Address gen → eff_addr = Rs1 + Rs2
398
+ Stage 2: Index calc → word_idx, bit_idx
399
+ Stage 3: TLB lookup + load current word
400
+ Stage 4: Bit mask & merge:
401
+ mask = 1 << bit_idx
402
+ new_word = (old_word & ~mask) | ((Rs3 & 1) << bit_idx)
403
+ Stage 5: Store new_word back to memory (writeback cache)
404
+ ```
405
+
406
+ **Read-Modify-Write**:
407
+ - Load old word: 3 cycles
408
+ - Compute new value: 1 cycle
409
+ - Store: pipelined (doesn't wait for commit)
410
+ - **Total latency: 4-5 cycles**
411
+
412
+ ---
413
+
414
+ ## 10. Register Transfer Language (RTL) Skeleton
415
+
416
+ ```verilog
417
+ // Stage 1: Address Generation
418
+ reg [63:0] eff_addr;
419
+ always @(posedge clk)
420
+ eff_addr <= rs1_data + rs2_data;
421
+
422
+ // Stage 2: Index Calculation (combinational)
423
+ wire [57:0] word_index = eff_addr[63:6];
424
+ wire [5:0] bit_index = eff_addr[5:0];
425
+
426
+ // Stage 3: Memory Access
427
+ wire [63:0] memory_word = l1_cache_read(word_index);
428
+
429
+ // Stage 4: Bit Extraction
430
+ wire [63:0] shifted = memory_word >> bit_index;
431
+ wire [63:0] extracted = shifted & 64'h1;
432
+
433
+ // Stage 5: Writeback
434
+ always @(posedge clk)
435
+ rd_data <= extracted;
436
+ ```
437
+
bit_accelerator/formal/bit_addressing.mlw ADDED
@@ -0,0 +1,155 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ (* Bit addressing and single-bit operation specification for bit_accelerator_v2.
2
+
3
+ Memory is a map from word index to an integer word value. Addresses:
4
+ absolute bit address = base_byte_address * 8 + bit_offset
5
+ word index = bit address / 64
6
+ bit index = bit address mod 64 (Euclidean division)
7
+
8
+ Corrections relative to the earlier draft (each disproved by Z3):
9
+ - bit_63_same_word and bit_index_wraps_at_64 only hold for a word-aligned
10
+ base (base mod 8 = 0); base = 7 and base = 1 are counterexamples.
11
+ - within_word_uniqueness claimed two different offsets never share a bit
12
+ index; offsets 0 and 64 do. It now states that (word, bit) determines the
13
+ bit address.
14
+ - disjoint_words_independent used a function where a bit result was meant. *)
15
+
16
+ module BitAddressing
17
+
18
+ use int.Int
19
+ use int.EuclideanDivision
20
+ use int.Power
21
+
22
+ constant word_bits : int = 64
23
+ constant max_address : int = 281474976710656 (* 2^48 words *)
24
+
25
+ predicate is_valid_bit_address (addr : int) =
26
+ 0 <= addr < max_address * word_bits
27
+
28
+ predicate word_aligned (addr : int) = mod addr word_bits = 0
29
+
30
+ function absolute_bit_address (base_byte_addr bit_offset : int) : int =
31
+ base_byte_addr * 8 + bit_offset
32
+
33
+ function word_index (bit_addr : int) : int = div bit_addr word_bits
34
+
35
+ function bit_index_in_word (bit_addr : int) : int = mod bit_addr word_bits
36
+
37
+ (* ---------------------------------------------------- address calculation *)
38
+
39
+ lemma absolute_bit_address_valid :
40
+ forall base offset : int.
41
+ 0 <= base -> 0 <= offset -> absolute_bit_address base offset >= 0
42
+
43
+ lemma word_index_positive :
44
+ forall bit_addr : int. is_valid_bit_address bit_addr ->
45
+ 0 <= word_index bit_addr < max_address
46
+
47
+ lemma bit_index_in_range :
48
+ forall bit_addr : int.
49
+ 0 <= bit_index_in_word bit_addr < word_bits
50
+
51
+ lemma euclidean_division :
52
+ forall bit_addr : int.
53
+ bit_addr = word_index bit_addr * word_bits + bit_index_in_word bit_addr
54
+
55
+ lemma word_and_bit_determine_address :
56
+ forall a1 a2 : int.
57
+ word_index a1 = word_index a2 ->
58
+ bit_index_in_word a1 = bit_index_in_word a2 ->
59
+ a1 = a2
60
+
61
+ (* --------------------------------------------------------------- boundaries *)
62
+
63
+ lemma bit_0_maps_to_word_0 :
64
+ forall base : int. word_index (absolute_bit_address base 0) = div base 8
65
+
66
+ lemma bit_63_same_word :
67
+ forall base : int. mod base 8 = 0 ->
68
+ word_index (absolute_bit_address base 0) =
69
+ word_index (absolute_bit_address base 63)
70
+
71
+ lemma bit_64_next_word :
72
+ forall base : int.
73
+ word_index (absolute_bit_address base 64) =
74
+ word_index (absolute_bit_address base 0) + 1
75
+
76
+ lemma bit_index_wraps_at_64 :
77
+ forall base : int. mod base 8 = 0 ->
78
+ bit_index_in_word (absolute_bit_address base 63) = 63 /\
79
+ bit_index_in_word (absolute_bit_address base 64) = 0
80
+
81
+ lemma within_word_uniqueness :
82
+ forall base offset1 offset2 : int.
83
+ word_index (absolute_bit_address base offset1) =
84
+ word_index (absolute_bit_address base offset2) ->
85
+ bit_index_in_word (absolute_bit_address base offset1) =
86
+ bit_index_in_word (absolute_bit_address base offset2) ->
87
+ offset1 = offset2
88
+
89
+ (* -------------------------------------------------------- bit operations *)
90
+
91
+ function bit_of (w b : int) : int = mod (div w (power 2 b)) 2
92
+
93
+ lemma bit_of_binary :
94
+ forall w b : int. 0 <= b -> bit_of w b = 0 \/ bit_of w b = 1
95
+
96
+ predicate bit_get_correct (memory : int -> int) (base offset result : int) =
97
+ let a = absolute_bit_address base offset in
98
+ is_valid_bit_address a /\
99
+ result = bit_of (memory (word_index a)) (bit_index_in_word a)
100
+
101
+ predicate frame (old_mem new_mem : int -> int) (w : int) =
102
+ forall i : int. i <> w -> new_mem i = old_mem i
103
+
104
+ predicate bit_set_correct (old_mem new_mem : int -> int) (base offset : int) =
105
+ let a = absolute_bit_address base offset in
106
+ is_valid_bit_address a /\
107
+ bit_of (new_mem (word_index a)) (bit_index_in_word a) = 1 /\
108
+ frame old_mem new_mem (word_index a)
109
+
110
+ predicate bit_clear_correct (old_mem new_mem : int -> int) (base offset : int) =
111
+ let a = absolute_bit_address base offset in
112
+ is_valid_bit_address a /\
113
+ bit_of (new_mem (word_index a)) (bit_index_in_word a) = 0 /\
114
+ frame old_mem new_mem (word_index a)
115
+
116
+ predicate bit_toggle_correct (old_mem new_mem : int -> int) (base offset : int) =
117
+ let a = absolute_bit_address base offset in
118
+ is_valid_bit_address a /\
119
+ bit_of (new_mem (word_index a)) (bit_index_in_word a) =
120
+ 1 - bit_of (old_mem (word_index a)) (bit_index_in_word a) /\
121
+ frame old_mem new_mem (word_index a)
122
+
123
+ lemma bit_get_binary :
124
+ forall memory : int -> int, base offset result : int.
125
+ bit_get_correct memory base offset result -> result = 0 \/ result = 1
126
+
127
+ let lemma bit_get_deterministic (memory : int -> int) (base offset r1 r2 : int)
128
+ requires { bit_get_correct memory base offset r1 }
129
+ requires { bit_get_correct memory base offset r2 }
130
+ ensures { r1 = r2 }
131
+ = let a = absolute_bit_address base offset in
132
+ assert { r1 = bit_of (memory (word_index a)) (bit_index_in_word a) = r2 }
133
+
134
+ (* A SET to one word does not change a GET from a different word. *)
135
+ let lemma disjoint_words_independent (old_mem new_mem : int -> int)
136
+ (base1 offset1 base2 offset2 r : int)
137
+ requires { word_index (absolute_bit_address base1 offset1) <>
138
+ word_index (absolute_bit_address base2 offset2) }
139
+ requires { bit_set_correct old_mem new_mem base1 offset1 }
140
+ requires { bit_get_correct new_mem base2 offset2 r }
141
+ ensures { bit_get_correct old_mem base2 offset2 r }
142
+ = let a2 = absolute_bit_address base2 offset2 in
143
+ assert { new_mem (word_index a2) = old_mem (word_index a2) }
144
+
145
+ (* After SET / CLEAR, GET of the same bit returns 1 / 0. *)
146
+ lemma get_after_set :
147
+ forall old_mem new_mem : int -> int, base offset : int.
148
+ bit_set_correct old_mem new_mem base offset ->
149
+ bit_get_correct new_mem base offset 1
150
+
151
+ lemma get_after_clear :
152
+ forall old_mem new_mem : int -> int, base offset : int.
153
+ bit_clear_correct old_mem new_mem base offset ->
154
+ bit_get_correct new_mem base offset 0
155
+ end
bit_accelerator/formal/bit_addressing_proofs.mlw ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ (* Derived properties of BitAddressing, proved from the definitions in
2
+ bit_addressing.mlw (run with `why3 prove -L formal ...`). *)
3
+
4
+ module BitAddressingProofs
5
+
6
+ use int.Int
7
+ use int.EuclideanDivision
8
+ use bit_addressing.BitAddressing
9
+
10
+ (* Every valid bit address has a valid word and an in-range bit index. *)
11
+ lemma valid_address_decomposes :
12
+ forall a : int. is_valid_bit_address a ->
13
+ 0 <= word_index a < max_address /\ 0 <= bit_index_in_word a < 64 /\
14
+ a = word_index a * 64 + bit_index_in_word a
15
+
16
+ (* The 64 offsets from a word-aligned base cover exactly one word, in order. *)
17
+ lemma aligned_base_covers_one_word :
18
+ forall base k : int. mod base 8 = 0 -> 0 <= k < 64 ->
19
+ word_index (absolute_bit_address base k) = div base 8 /\
20
+ bit_index_in_word (absolute_bit_address base k) = k
21
+
22
+ (* Offset k + 64 reaches the same bit of the next word. *)
23
+ lemma offset_plus_64 :
24
+ forall base k : int.
25
+ word_index (absolute_bit_address base (k + 64)) =
26
+ word_index (absolute_bit_address base k) + 1 /\
27
+ bit_index_in_word (absolute_bit_address base (k + 64)) =
28
+ bit_index_in_word (absolute_bit_address base k)
29
+
30
+ (* Offsets are interchangeable with base bytes: 8 bits per byte. *)
31
+ lemma byte_offset_equivalence :
32
+ forall base offset : int.
33
+ absolute_bit_address (base + 1) offset = absolute_bit_address base (offset + 8)
34
+
35
+ (* A CLEAR to one word does not change a GET from a different word. *)
36
+ let lemma clear_disjoint_words_independent (old_mem new_mem : int -> int)
37
+ (base1 offset1 base2 offset2 r : int)
38
+ requires { word_index (absolute_bit_address base1 offset1) <>
39
+ word_index (absolute_bit_address base2 offset2) }
40
+ requires { bit_clear_correct old_mem new_mem base1 offset1 }
41
+ requires { bit_get_correct new_mem base2 offset2 r }
42
+ ensures { bit_get_correct old_mem base2 offset2 r }
43
+ = let a2 = absolute_bit_address base2 offset2 in
44
+ assert { new_mem (word_index a2) = old_mem (word_index a2) }
45
+ end
bit_accelerator/isa/BIT_ISA.md ADDED
@@ -0,0 +1,416 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # Bit-String Hardware Accelerator ISA Specification
2
+
3
+ ## 1. ISA Overview
4
+
5
+ **Architecture**: RISC-style bit-manipulation ISA
6
+ **Operand Width**: 64-bit integer registers
7
+ **Word Size**: 64 bits
8
+ **Addressing**: Bit-addressed linear address space
9
+
10
+ ---
11
+
12
+ ## 2. Register File
13
+
14
+ ```
15
+ Registers: R0-R31 (32 × 64-bit GPRs)
16
+ Special Registers:
17
+ - R0: Hard-wired zero
18
+ - R31: Return value / implicit accumulator
19
+ ```
20
+
21
+ ---
22
+
23
+ ## 3. Instruction Format
24
+
25
+ ### 3.1 R-Type (Register-Register)
26
+ ```
27
+ ┌─────────┬─────┬─────┬─────┬────────────┐
28
+ │ Opcode │ Rd │ Rs1 │ Rs2 │ Reserved │
29
+ │ 6 bits │ 5 │ 5 │ 5 │ 13 bits │
30
+ └─────────┴─────┴─────┴─────┴────────────┘
31
+ ```
32
+
33
+ ### 3.2 I-Type (Register-Immediate)
34
+ ```
35
+ ┌─────────┬─────┬─────┬──────────────┐
36
+ │ Opcode │ Rd │ Rs1 │ Immediate │
37
+ │ 6 bits │ 5 │ 5 │ 18 bits │
38
+ └─────────┴─────┴─────┴──────────────┘
39
+ ```
40
+
41
+ ### 3.3 L-Type (Load Immediate)
42
+ ```
43
+ ┌─────────┬─────┬──────────────────────┐
44
+ │ Opcode │ Rd │ Immediate │
45
+ │ 6 bits │ 5 │ 53 bits (sign-ext) │
46
+ └─────────┴─────┴──────────────────────┘
47
+ ```
48
+
49
+ ---
50
+
51
+ ## 4. Opcode Assignments
52
+
53
+ | Mnemonic | Opcode | Type | Semantics |
54
+ |----------------|--------|------|-----------|
55
+ | BITLOAD | 0x01 | R | rd ← mem[rs1 + rs2 bit offset] & 1 |
56
+ | BITSTORE | 0x02 | R | mem[rs1 + rs2 bit offset] ← rs3 & 1 |
57
+ | BITFIELD | 0x03 | R | rd ← (mem[rs1 + rs2] >> rs3) & ((1 << rs4) - 1) |
58
+ | BITTEST | 0x04 | R | flag ← (mem[rs1 + rs2] >> bit_offset) & 1 |
59
+ | BITCOUNT | 0x05 | R | rd ← popcount(mem[rs1]) |
60
+ | BITSCANFWD | 0x06 | R | rd ← first_set_bit(rs1) |
61
+ | BITSCANREV | 0x07 | R | rd ← last_set_bit(rs1) |
62
+ | LOADIMM64 | 0x08 | L | rd ← immediate (53-bit sign-extended) |
63
+ | BITEXTRACT | 0x09 | R | rd ← extract_field(rs1, rs2, rs3) |
64
+ | BITINSERT | 0x0A | R | rd ← insert_field(rs1, rs2, rs3, rs4) |
65
+ | BITROTL | 0x0B | R | rd ← rotate_left(rs1, rs2) |
66
+ | BITROTR | 0x0C | R | rd ← rotate_right(rs1, rs2) |
67
+
68
+ ---
69
+
70
+ ## 5. Instruction Semantics
71
+
72
+ ### 5.1 BITLOAD (Single-Bit Load)
73
+
74
+ **Encoding**: `BITLOAD Rd, Rs1, Rs2`
75
+
76
+ **Operation**:
77
+ ```
78
+ effective_bit_address = Rs1 + Rs2
79
+ word_index = effective_bit_address / 64
80
+ bit_index = effective_bit_address mod 64
81
+ Rd ← (memory[word_index] >> bit_index) & 1
82
+ ```
83
+
84
+ **Constraints**:
85
+ - `Rs1`: Bit base address (64-bit)
86
+ - `Rs2`: Bit offset (64-bit)
87
+ - `Rd`: Destination register (bit 0 set, bits [63:1] = 0)
88
+ - No privilege required
89
+ - May fault: page fault if effective address invalid
90
+
91
+ **Latency**: 3 cycles (address generation + memory access + extract)
92
+
93
+ ---
94
+
95
+ ### 5.2 BITSTORE (Single-Bit Write)
96
+
97
+ **Encoding**: `BITSTORE Rs1, Rs2, Rs3`
98
+
99
+ **Operation**:
100
+ ```
101
+ effective_bit_address = Rs1 + Rs2
102
+ word_index = effective_bit_address / 64
103
+ bit_index = effective_bit_address mod 64
104
+ bit_value = Rs3 & 1
105
+ old_word = memory[word_index]
106
+ mask = 1 << bit_index
107
+ new_word = (old_word & ~mask) | (bit_value << bit_index)
108
+ memory[word_index] ← new_word
109
+ ```
110
+
111
+ **Constraints**:
112
+ - `Rs1`: Bit base address
113
+ - `Rs2`: Bit offset
114
+ - `Rs3`: Bit value (only bit 0 is meaningful)
115
+ - No destination register
116
+ - Requires write permission on target memory
117
+ - May fault: segmentation fault, write-protect fault
118
+
119
+ **Latency**: 3 cycles (address generation + RMW cycle)
120
+
121
+ ---
122
+
123
+ ### 5.3 BITFIELD (Multi-Bit Extract)
124
+
125
+ **Encoding**: `BITFIELD Rd, Rs1, Rs2, Rs3, Rs4`
126
+
127
+ **Operation**:
128
+ ```
129
+ effective_bit_address = Rs1 + Rs2
130
+ word_index = effective_bit_address / 64
131
+ bit_index = effective_bit_address mod 64
132
+ field_width = Rs3
133
+ bit_offset_in_word = Rs4
134
+
135
+ word = memory[word_index]
136
+ extracted = (word >> bit_offset_in_word) & ((1 << field_width) - 1)
137
+ Rd ← extracted
138
+ ```
139
+
140
+ **Constraints**:
141
+ - `field_width` must be in range [1, 64]
142
+ - If `bit_offset + field_width > 64`, behavior is undefined (may trap)
143
+ - No cross-boundary extraction in this instruction (use software loop)
144
+
145
+ **Latency**: 3 cycles
146
+
147
+ ---
148
+
149
+ ### 5.4 BITTEST (Test and Branch)
150
+
151
+ **Encoding**: `BITTEST Rs1, Rs2`
152
+
153
+ **Operation**:
154
+ ```
155
+ effective_bit_address = Rs1 + Rs2
156
+ word_index = effective_bit_address / 64
157
+ bit_index = effective_bit_address mod 64
158
+ condition_flag ← (memory[word_index] >> bit_index) & 1
159
+ ```
160
+
161
+ **Latency**: 3 cycles
162
+
163
+ **Conditional Execution**: Sets zero flag (ZF) in status register:
164
+ - `ZF = 0` if bit is set
165
+ - `ZF = 1` if bit is clear
166
+
167
+ ---
168
+
169
+ ### 5.5 BITCOUNT (Population Count)
170
+
171
+ **Encoding**: `BITCOUNT Rd, Rs1`
172
+
173
+ **Operation**:
174
+ ```
175
+ Rd ← popcount(Rs1)
176
+ ```
177
+
178
+ **Latency**: 2 cycles (specialized hardware)
179
+
180
+ ---
181
+
182
+ ### 5.6 BITSCANFWD (Find First Set Bit)
183
+
184
+ **Encoding**: `BITSCANFWD Rd, Rs1`
185
+
186
+ **Operation**:
187
+ ```
188
+ If Rs1 = 0:
189
+ Rd ← 64 (or undefined, behavior determined by hardware)
190
+ Else:
191
+ Rd ← position of rightmost set bit (0-indexed)
192
+ Range: Rd ∈ [0, 63]
193
+ ```
194
+
195
+ **Latency**: 2-3 cycles
196
+
197
+ ---
198
+
199
+ ### 5.7 BITSCANREV (Find Last Set Bit)
200
+
201
+ **Encoding**: `BITSCANREV Rd, Rs1`
202
+
203
+ **Operation**:
204
+ ```
205
+ If Rs1 = 0:
206
+ Rd ← 64 (or undefined)
207
+ Else:
208
+ Rd ← position of leftmost set bit (0-indexed)
209
+ Range: Rd ∈ [0, 63]
210
+ ```
211
+
212
+ **Latency**: 2-3 cycles
213
+
214
+ ---
215
+
216
+ ### 5.8 LOADIMM64 (Load 53-Bit Immediate)
217
+
218
+ **Encoding**: `LOADIMM64 Rd, immediate`
219
+
220
+ **Operation**:
221
+ ```
222
+ Rd ← sign_extend(immediate[52:0], 64)
223
+ ```
224
+
225
+ **Latency**: 1 cycle
226
+
227
+ ---
228
+
229
+ ### 5.9 BITEXTRACT (Field Extraction with Width)
230
+
231
+ **Encoding**: `BITEXTRACT Rd, Rs1, Rs2, Rs3`
232
+
233
+ **Operation**:
234
+ ```
235
+ value = Rs1
236
+ start_bit = Rs2
237
+ field_width = Rs3
238
+
239
+ extracted = (value >> start_bit) & ((1 << field_width) - 1)
240
+ Rd ← extracted
241
+ ```
242
+
243
+ **Latency**: 1 cycle (register-only, no memory)
244
+
245
+ ---
246
+
247
+ ### 5.10 BITINSERT (Field Insertion)
248
+
249
+ **Encoding**: `BITINSERT Rd, Rs1, Rs2, Rs3, Rs4`
250
+
251
+ **Operation**:
252
+ ```
253
+ dest_value = Rs1
254
+ source_value = Rs2
255
+ start_bit = Rs3
256
+ field_width = Rs4
257
+
258
+ mask = ((1 << field_width) - 1) << start_bit
259
+ shifted_source = (source_value & ((1 << field_width) - 1)) << start_bit
260
+ Rd ← (dest_value & ~mask) | shifted_source
261
+ ```
262
+
263
+ **Latency**: 2 cycles
264
+
265
+ ---
266
+
267
+ ### 5.11 BITROTL (Rotate Left)
268
+
269
+ **Encoding**: `BITROTL Rd, Rs1, Rs2`
270
+
271
+ **Operation**:
272
+ ```
273
+ value = Rs1
274
+ rotate_amount = Rs2 mod 64
275
+ Rd ← (value << rotate_amount) | (value >> (64 - rotate_amount))
276
+ ```
277
+
278
+ **Latency**: 2 cycles
279
+
280
+ ---
281
+
282
+ ### 5.12 BITROTR (Rotate Right)
283
+
284
+ **Encoding**: `BITROTR Rd, Rs1, Rs2`
285
+
286
+ **Operation**:
287
+ ```
288
+ value = Rs1
289
+ rotate_amount = Rs2 mod 64
290
+ Rd ← (value >> rotate_amount) | (value << (64 - rotate_amount))
291
+ ```
292
+
293
+ **Latency**: 2 cycles
294
+
295
+ ---
296
+
297
+ ## 6. Memory Semantics
298
+
299
+ ### 6.1 Byte Ordering (Little-Endian)
300
+
301
+ All operations assume little-endian byte ordering:
302
+ ```
303
+ Memory layout (64-bit word at address 0x00):
304
+ Bit 0 at byte 0, bit 0
305
+ Bit 7 at byte 0, bit 7
306
+ Bit 8 at byte 1, bit 0
307
+ Bit 63 at byte 7, bit 7
308
+ ```
309
+
310
+ ### 6.2 Alignment Requirements
311
+
312
+ - No alignment requirement for bit addresses
313
+ - Memory accesses are naturally granular to 64-bit words
314
+ - Unaligned word access: hardware loads containing word, extracts bits
315
+
316
+ ### 6.3 Virtual Memory Integration
317
+
318
+ - Bit addresses translate to physical addresses via TLB
319
+ - `word_address = bit_address >> 6` (divide by 64)
320
+ - `word_address` is then translated through MMU
321
+ - Page boundaries: if `bit_address` and `bit_address+63` span different pages, may require two memory accesses
322
+ - Hardware handles transparently for single-bit operations
323
+ - Multi-word operations may trap if boundary conditions not met
324
+
325
+ ### 6.4 Cache Coherency
326
+
327
+ - Follows processor's existing cache coherency protocol
328
+ - BITSTORE is treated as a regular write for coherency purposes
329
+ - No special coherency instruction needed
330
+
331
+ ---
332
+
333
+ ## 7. Exception Behavior
334
+
335
+ | Exception | Opcode | Trigger | Action |
336
+ |-----------|--------|---------|--------|
337
+ | PAGE_FAULT | Any memory op | Address not in TLB | Interrupt handler, retry |
338
+ | PROTECTION_FAULT | BITSTORE | Page not writable | Interrupt handler |
339
+ | INVALID_ADDRESS | Any memory op | Address > max physical | Trap |
340
+ | UNDEFINED_FIELD_WIDTH | BITFIELD | width = 0 or width > 64 | Trap |
341
+
342
+ ---
343
+
344
+ ## 8. Status Register (Implicit)
345
+
346
+ ```
347
+ Bit Name Meaning
348
+ 0 ZF Zero Flag (set by BITTEST)
349
+ 1 CF Carry Flag (unused in this ISA)
350
+ 2-63 Reserved
351
+ ```
352
+
353
+ ---
354
+
355
+ ## 9. Privilege Levels
356
+
357
+ All bit-string instructions are **user-mode executable**. No privilege escalation.
358
+
359
+ Exception: Bit addresses pointing to kernel memory may trigger protection faults.
360
+
361
+ ---
362
+
363
+ ## 10. Formal Semantics (First-Order Logic)
364
+
365
+ ### Correctness Property: Single-Bit Load
366
+
367
+ ```
368
+ ∀ base, offset ∈ ℕ :
369
+ let eff_addr = base + offset
370
+ let word_idx = eff_addr >> 6
371
+ let bit_idx = eff_addr mod 64
372
+ BITLOAD base offset = (mem[word_idx] >> bit_idx) & 1
373
+ ```
374
+
375
+ ### Correctness Property: Single-Bit Store
376
+
377
+ ```
378
+ ∀ base, offset, value ∈ ℕ :
379
+ let eff_addr = base + offset
380
+ let word_idx = eff_addr >> 6
381
+ let bit_idx = eff_addr mod 64
382
+ let mask = 1 << bit_idx
383
+
384
+ after BITSTORE base offset value:
385
+ mem[word_idx] = (mem[word_idx] & ~mask) | ((value & 1) << bit_idx)
386
+ ∀ j ≠ word_idx : mem[j] unchanged
387
+ ```
388
+
389
+ ### Correctness Property: Field Extraction
390
+
391
+ ```
392
+ ∀ value, start, width ∈ ℕ, width ≤ 64 :
393
+ BITEXTRACT value start width = (value >> start) & ((1 << width) - 1)
394
+ ```
395
+
396
+ ---
397
+
398
+ ## 11. Implementation Constraints
399
+
400
+ - **Max memory size**: 2^64 bits (addressable)
401
+ - **Max single extraction**: 64 bits per instruction
402
+ - **Max rotation**: Full 64-bit rotation with any offset
403
+ - **Frequency**: Target 1+ GHz (1-3 cycle latency operations)
404
+ - **Power**: < 2mW per operation (estimated)
405
+ - **Area**: ~100-200k gates (estimates as sub-module)
406
+
407
+ ---
408
+
409
+ ## 12. Future Extensions (Out of Scope)
410
+
411
+ - SIMD bit-parallel operations
412
+ - GPU integration
413
+ - Vector bit strings
414
+ - Conditional bit operations
415
+ - Atomic bit operations (hardware locks)
416
+
bit_accelerator/rtl/behavioral_memory.sv ADDED
@@ -0,0 +1,102 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Behavioral Memory Model for Simulation
2
+ // Provides a simple synchronous memory with configurable read latency
3
+
4
+ module behavioral_memory #(
5
+ parameter int ADDR_WIDTH = 64,
6
+ parameter int WORD_WIDTH = 64,
7
+ parameter int WORD_BYTES = WORD_WIDTH / 8,
8
+ parameter int READ_LATENCY = 2,
9
+ parameter string INIT_FILE = ""
10
+ ) (
11
+ input logic clk,
12
+ input logic reset,
13
+
14
+ // Memory Request Interface
15
+ input logic req_valid,
16
+ output logic req_ready,
17
+ input logic [ADDR_WIDTH-1:0] addr,
18
+ input logic is_read,
19
+ input logic is_write,
20
+ input logic [WORD_BYTES-1:0] wstrb,
21
+ input logic [WORD_WIDTH-1:0] wdata,
22
+
23
+ // Memory Response Interface
24
+ output logic rvalid,
25
+ output logic [WORD_WIDTH-1:0] rdata,
26
+ output logic fault
27
+ );
28
+
29
+ // Memory array: 64K words (512KB total)
30
+ logic [WORD_WIDTH-1:0] memory [0:65535];
31
+
32
+ // Read pipeline for latency emulation
33
+ logic [READ_LATENCY-1:0] read_valid_pipe;
34
+ logic [WORD_WIDTH-1:0] read_data_pipe [0:READ_LATENCY-1];
35
+ logic [ADDR_WIDTH-1:0] read_addr_pipe [0:READ_LATENCY-1];
36
+
37
+ initial begin
38
+ if (INIT_FILE != "") begin
39
+ $readmemh(INIT_FILE, memory);
40
+ end else begin
41
+ for (int i = 0; i < 65536; i++) begin
42
+ memory[i] = 64'h0;
43
+ end
44
+ end
45
+ end
46
+
47
+ // Request handling
48
+ always_ff @(posedge clk or negedge reset) begin
49
+ if (!reset) begin
50
+ req_ready <= 1'b1;
51
+ rvalid <= 1'b0;
52
+ rdata <= 64'h0;
53
+ fault <= 1'b0;
54
+ for (int i = 0; i < READ_LATENCY; i++) begin
55
+ read_valid_pipe[i] <= 1'b0;
56
+ read_data_pipe[i] <= 64'h0;
57
+ end
58
+ end else begin
59
+ // Always ready to accept requests
60
+ req_ready <= 1'b1;
61
+
62
+ // Handle write operations immediately
63
+ if (req_valid && is_write) begin
64
+ // Word-aligned write at address / 8
65
+ logic [ADDR_WIDTH-1:0] word_addr = addr >> 3;
66
+ if (word_addr < 65536) begin
67
+ // Apply write strobes (byte enables)
68
+ for (int i = 0; i < WORD_BYTES; i++) begin
69
+ if (wstrb[i]) begin
70
+ memory[word_addr][i*8 +: 8] <= wdata[i*8 +: 8];
71
+ end
72
+ end
73
+ end
74
+ end
75
+
76
+ // Handle read operations (pipeline)
77
+ read_valid_pipe[0] <= req_valid && is_read;
78
+ if (req_valid && is_read) begin
79
+ logic [ADDR_WIDTH-1:0] word_addr = addr >> 3;
80
+ read_addr_pipe[0] <= word_addr;
81
+ if (word_addr < 65536) begin
82
+ read_data_pipe[0] <= memory[word_addr];
83
+ end else begin
84
+ read_data_pipe[0] <= 64'hDEADBEEFDEADBEEF; // Fault marker
85
+ end
86
+ end
87
+
88
+ // Pipeline shift for READ_LATENCY cycles
89
+ for (int i = 1; i < READ_LATENCY; i++) begin
90
+ read_valid_pipe[i] <= read_valid_pipe[i-1];
91
+ read_data_pipe[i] <= read_data_pipe[i-1];
92
+ read_addr_pipe[i] <= read_addr_pipe[i-1];
93
+ end
94
+
95
+ // Output from pipeline
96
+ rvalid <= read_valid_pipe[READ_LATENCY-1];
97
+ rdata <= read_data_pipe[READ_LATENCY-1];
98
+ fault <= 1'b0; // No faults in this simple model
99
+ end
100
+ end
101
+
102
+ endmodule : behavioral_memory
bit_accelerator/rtl/bit_accelerator.sv ADDED
@@ -0,0 +1,210 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Top-Level Bit-String Hardware Accelerator
2
+ // Implements: BIT_BASE + BIT_OFFSET addressing with atomic read-modify-write
3
+
4
+ module bit_accelerator #(
5
+ parameter int ADDR_WIDTH = 64,
6
+ parameter int WORD_WIDTH = 64,
7
+ parameter int WORD_BYTES = WORD_WIDTH / 8
8
+ ) (
9
+ input logic clk,
10
+ input logic reset,
11
+
12
+ // Operation Interface
13
+ input logic op_valid,
14
+ output logic op_ready,
15
+ input logic [63:0] base_address,
16
+ input logic [63:0] bit_offset,
17
+ input logic [2:0] operation, // 3'b000=GET, 3'b001=TEST, 3'b010=SET, 3'b011=CLEAR, 3'b100=TOGGLE
18
+
19
+ // Response Interface
20
+ output logic result_valid,
21
+ output logic result_bit,
22
+ output logic error,
23
+
24
+ // Memory Interface (AXI-like, word-addressed)
25
+ output logic mem_req_valid,
26
+ input logic mem_req_ready,
27
+ output logic [ADDR_WIDTH-1:0] mem_addr,
28
+ output logic mem_read,
29
+ output logic mem_write,
30
+ output logic [WORD_BYTES-1:0] mem_wstrb,
31
+ output logic [WORD_WIDTH-1:0] mem_wdata,
32
+
33
+ input logic mem_rvalid,
34
+ input logic [WORD_WIDTH-1:0] mem_rdata,
35
+ input logic mem_fault
36
+ );
37
+
38
+ // ===== State Machine =====
39
+ typedef enum logic [2:0] {
40
+ ST_IDLE,
41
+ ST_READ_REQUEST,
42
+ ST_READ_WAIT,
43
+ ST_MODIFY,
44
+ ST_WRITE_REQUEST,
45
+ ST_WRITE_WAIT,
46
+ ST_DONE
47
+ } state_t;
48
+
49
+ state_t current_state, next_state;
50
+
51
+ // ===== Internal Registers =====
52
+ logic [63:0] base_addr_reg, bit_offset_reg;
53
+ logic [2:0] operation_reg;
54
+ logic [63:0] absolute_bit_address;
55
+ logic [57:0] word_address; // byte address / 8
56
+ logic [5:0] bit_index_in_word; // bit position within 64-bit word
57
+ logic [63:0] read_word;
58
+ logic [63:0] modified_word;
59
+ logic is_modify_op; // SET, CLEAR, TOGGLE
60
+
61
+ // ===== Combinational: Address Calculation =====
62
+
63
+ // absolute_bit_address = (base_address × 8) + bit_offset
64
+ logic [127:0] temp_addr;
65
+ assign temp_addr = {1'b0, base_addr_reg} * 8 + {1'b0, bit_offset_reg};
66
+
67
+ // Truncate to 64-bit (overflow handling)
68
+ assign absolute_bit_address = temp_addr[63:0];
69
+
70
+ // word_address = absolute_bit_address / 64 (right-shift by 6)
71
+ assign word_address = absolute_bit_address[63:6];
72
+
73
+ // bit_index_in_word = absolute_bit_address % 64
74
+ assign bit_index_in_word = absolute_bit_address[5:0];
75
+
76
+ // Convert word address to byte address for memory interface
77
+ // word_address is already in 64-bit word units, multiply by 8 for byte address
78
+ assign mem_addr = {word_address, 3'b000}; // Shift left by 3 (multiply by 8)
79
+
80
+ // Check if operation is a modify operation
81
+ assign is_modify_op = (operation_reg == 3'b010) || // SET
82
+ (operation_reg == 3'b011) || // CLEAR
83
+ (operation_reg == 3'b100); // TOGGLE
84
+
85
+ // ===== Submodules =====
86
+
87
+ bit_extractor bit_extractor_inst (
88
+ .word_data (read_word),
89
+ .bit_index (bit_index_in_word),
90
+ .field_width (6'h1),
91
+ .is_multibit (1'b0),
92
+ .result () // Not used directly, result_bit comes from shift+AND
93
+ );
94
+
95
+ bit_modifier bit_modifier_inst (
96
+ .word_data (read_word),
97
+ .bit_index (bit_index_in_word),
98
+ .operation (operation_reg),
99
+ .result (modified_word)
100
+ );
101
+
102
+ // ===== Result Extraction (Combinational) =====
103
+ logic [63:0] shifted_for_result;
104
+ assign shifted_for_result = read_word >> bit_index_in_word;
105
+
106
+ // ===== State Machine: Sequential =====
107
+
108
+ always_ff @(posedge clk or negedge reset) begin
109
+ if (!reset) begin
110
+ current_state <= ST_IDLE;
111
+ base_addr_reg <= 64'h0;
112
+ bit_offset_reg <= 64'h0;
113
+ operation_reg <= 3'h0;
114
+ read_word <= 64'h0;
115
+ result_valid <= 1'b0;
116
+ result_bit <= 1'b0;
117
+ error <= 1'b0;
118
+ end else begin
119
+ current_state <= next_state;
120
+ result_valid <= 1'b0;
121
+ error <= 1'b0;
122
+
123
+ if (op_valid && op_ready) begin
124
+ base_addr_reg <= base_address;
125
+ bit_offset_reg <= bit_offset;
126
+ operation_reg <= operation;
127
+ end
128
+
129
+ if (mem_rvalid && current_state == ST_READ_WAIT) begin
130
+ read_word <= mem_rdata;
131
+ end
132
+
133
+ if (mem_fault) begin
134
+ error <= 1'b1;
135
+ result_valid <= 1'b1;
136
+ end
137
+ end
138
+ end
139
+
140
+ // ===== State Machine: Combinational Next-State Logic =====
141
+
142
+ always_comb begin
143
+ next_state = current_state;
144
+ op_ready = 1'b0;
145
+ mem_req_valid = 1'b0;
146
+ mem_read = 1'b0;
147
+ mem_write = 1'b0;
148
+ mem_wstrb = 8'h00;
149
+ mem_wdata = 64'h0;
150
+
151
+ case (current_state)
152
+ ST_IDLE: begin
153
+ op_ready = 1'b1;
154
+ if (op_valid) begin
155
+ next_state = ST_READ_REQUEST;
156
+ end
157
+ end
158
+
159
+ ST_READ_REQUEST: begin
160
+ mem_req_valid = 1'b1;
161
+ mem_read = 1'b1;
162
+ if (mem_req_ready) begin
163
+ next_state = ST_READ_WAIT;
164
+ end
165
+ end
166
+
167
+ ST_READ_WAIT: begin
168
+ if (mem_rvalid) begin
169
+ if (is_modify_op) begin
170
+ next_state = ST_MODIFY;
171
+ end else begin
172
+ next_state = ST_DONE;
173
+ end
174
+ end
175
+ if (mem_fault) begin
176
+ next_state = ST_DONE;
177
+ end
178
+ end
179
+
180
+ ST_MODIFY: begin
181
+ next_state = ST_WRITE_REQUEST;
182
+ end
183
+
184
+ ST_WRITE_REQUEST: begin
185
+ mem_req_valid = 1'b1;
186
+ mem_write = 1'b1;
187
+ mem_wstrb = 8'hFF; // All 8 bytes of the 64-bit word
188
+ mem_wdata = modified_word;
189
+ if (mem_req_ready) begin
190
+ next_state = ST_WRITE_WAIT;
191
+ end
192
+ end
193
+
194
+ ST_WRITE_WAIT: begin
195
+ // For write operations, we don't wait for a write response in this simple model
196
+ // Assume write completes immediately after acceptance
197
+ next_state = ST_DONE;
198
+ end
199
+
200
+ ST_DONE: begin
201
+ result_valid = 1'b1;
202
+ result_bit = shifted_for_result[0];
203
+ next_state = ST_IDLE;
204
+ end
205
+
206
+ default: next_state = ST_IDLE;
207
+ endcase
208
+ end
209
+
210
+ endmodule : bit_accelerator
bit_accelerator/rtl/bit_accelerator_pkg.sv ADDED
@@ -0,0 +1,140 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Bit Accelerator Package - Type Definitions and Constants
2
+
3
+ package bit_accelerator_pkg;
4
+
5
+ // Opcode Definitions
6
+ typedef enum logic [5:0] {
7
+ BITLOAD = 6'h01,
8
+ BITSTORE = 6'h02,
9
+ BITFIELD = 6'h03,
10
+ BITTEST = 6'h04,
11
+ BITCOUNT = 6'h05,
12
+ BITSCANFWD = 6'h06,
13
+ BITSCANREV = 6'h07,
14
+ LOADIMM64 = 6'h08,
15
+ BITEXTRACT = 6'h09,
16
+ BITINSERT = 6'h0A,
17
+ BITROTL = 6'h0B,
18
+ BITROTR = 6'h0C
19
+ } opcode_t;
20
+
21
+ // Register Specifier (5 bits)
22
+ typedef logic [4:0] reg_addr_t;
23
+
24
+ // Immediate Values
25
+ typedef logic [17:0] imm18_t;
26
+ typedef logic [52:0] imm53_t;
27
+
28
+ // 64-bit Word/Address
29
+ typedef logic [63:0] word64_t;
30
+
31
+ // Bit Index (0-63)
32
+ typedef logic [5:0] bit_idx_t;
33
+
34
+ // Word Index (for 64-bit memory word, within addressable space)
35
+ typedef logic [57:0] word_idx_t;
36
+
37
+ // Effective Bit Address
38
+ typedef logic [63:0] eff_addr_t;
39
+
40
+ // Instruction Format
41
+ typedef struct packed {
42
+ opcode_t opcode; // [5:0]
43
+ reg_addr_t rd; // [10:6]
44
+ reg_addr_t rs1; // [15:11]
45
+ reg_addr_t rs2; // [20:16]
46
+ logic [43:0] unused; // [63:21]
47
+ } instr_r_t;
48
+
49
+ typedef struct packed {
50
+ opcode_t opcode; // [5:0]
51
+ reg_addr_t rd; // [10:6]
52
+ reg_addr_t rs1; // [15:11]
53
+ imm18_t imm; // [33:16]
54
+ logic [29:0] unused; // [63:34]
55
+ } instr_i_t;
56
+
57
+ typedef struct packed {
58
+ opcode_t opcode; // [5:0]
59
+ reg_addr_t rd; // [10:6]
60
+ imm53_t imm; // [58:11]
61
+ logic [4:0] unused; // [63:59]
62
+ } instr_l_t;
63
+
64
+ // Control Signals
65
+ typedef struct packed {
66
+ logic enable_addr_gen;
67
+ logic enable_mem_load;
68
+ logic enable_mem_store;
69
+ logic enable_shift;
70
+ logic enable_extract;
71
+ logic enable_writeback;
72
+ logic shift_direction; // 0=right, 1=left
73
+ logic rotate_mode; // 0=shift, 1=rotate
74
+ logic is_signed;
75
+ bit_idx_t field_width;
76
+ } ctrl_signals_t;
77
+
78
+ // Exception Codes
79
+ typedef enum logic [3:0] {
80
+ EXC_NONE = 4'h0,
81
+ EXC_PAGE_FAULT = 4'h1,
82
+ EXC_PROTECTION = 4'h2,
83
+ EXC_INVALID_ADDR = 4'h3,
84
+ EXC_INVALID_WIDTH = 4'h4
85
+ } exception_t;
86
+
87
+ // Pipeline Stage Signals
88
+ typedef struct packed {
89
+ opcode_t opcode;
90
+ reg_addr_t rd;
91
+ word64_t rs1_data;
92
+ word64_t rs2_data;
93
+ word64_t rs3_data;
94
+ ctrl_signals_t ctrl;
95
+ exception_t exc;
96
+ } stage_s1_t;
97
+
98
+ typedef struct packed {
99
+ opcode_t opcode;
100
+ reg_addr_t rd;
101
+ word64_t rs3_data;
102
+ eff_addr_t eff_addr;
103
+ ctrl_signals_t ctrl;
104
+ exception_t exc;
105
+ } stage_s2_t;
106
+
107
+ typedef struct packed {
108
+ opcode_t opcode;
109
+ reg_addr_t rd;
110
+ word64_t rs3_data;
111
+ word_idx_t word_idx;
112
+ bit_idx_t bit_idx;
113
+ ctrl_signals_t ctrl;
114
+ exception_t exc;
115
+ } stage_s3_t;
116
+
117
+ typedef struct packed {
118
+ opcode_t opcode;
119
+ reg_addr_t rd;
120
+ word64_t memory_word;
121
+ bit_idx_t bit_idx;
122
+ ctrl_signals_t ctrl;
123
+ exception_t exc;
124
+ } stage_s4_t;
125
+
126
+ typedef struct packed {
127
+ opcode_t opcode;
128
+ reg_addr_t rd;
129
+ word64_t extracted_value;
130
+ exception_t exc;
131
+ } stage_s5_t;
132
+
133
+ // Control Status Register
134
+ typedef struct packed {
135
+ logic zf; // Zero flag (from BITTEST)
136
+ logic cf; // Carry flag (unused)
137
+ logic [61:0] reserved;
138
+ } csr_t;
139
+
140
+ endpackage : bit_accelerator_pkg
bit_accelerator/rtl/bit_accelerator_v2.sv ADDED
@@ -0,0 +1,209 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Bit-String Hardware Accelerator v2
2
+ // Corrected implementation with explicit write completion semantics
3
+ // Reset and in-flight operation cancellation
4
+
5
+ module bit_accelerator_v2 #(
6
+ parameter int ADDR_WIDTH = 64,
7
+ parameter int WORD_WIDTH = 64,
8
+ parameter int WORD_BYTES = WORD_WIDTH / 8
9
+ ) (
10
+ input logic clk,
11
+ input logic reset,
12
+
13
+ // Operation Interface
14
+ input logic op_valid,
15
+ output logic op_ready,
16
+ input logic [63:0] base_address,
17
+ input logic [63:0] bit_offset,
18
+ input logic [2:0] operation, // 3'b000=GET, 3'b001=TEST, 3'b010=SET, 3'b011=CLEAR, 3'b100=TOGGLE
19
+
20
+ // Result Interface (one-cycle pulse)
21
+ output logic result_valid,
22
+ output logic result_bit,
23
+ output logic error,
24
+
25
+ // Memory Interface (AXI-like handshaking)
26
+ output logic mem_valid, // Read or write valid
27
+ output logic mem_write, // 0=read, 1=write
28
+ output logic [ADDR_WIDTH-1:0] mem_addr, // Byte address (8-byte aligned)
29
+ output logic [WORD_WIDTH-1:0] mem_wdata, // Write data
30
+ output logic [WORD_BYTES-1:0] mem_wstrb, // Write strobes
31
+ input logic mem_ready, // Ready to accept
32
+
33
+ input logic mem_rvalid, // Read valid
34
+ input logic [WORD_WIDTH-1:0] mem_rdata, // Read data
35
+ input logic mem_fault // Read fault
36
+ );
37
+
38
+ // ===== State Machine =====
39
+ typedef enum logic [3:0] {
40
+ ST_IDLE,
41
+ ST_READ_REQUEST,
42
+ ST_READ_WAIT,
43
+ ST_MODIFY,
44
+ ST_WRITE_REQUEST,
45
+ ST_WRITE_WAIT,
46
+ ST_RESULT
47
+ } state_t;
48
+
49
+ state_t current_state, next_state;
50
+
51
+ // ===== Stored Operation State =====
52
+ logic [63:0] base_addr_reg, bit_offset_reg;
53
+ logic [2:0] operation_reg;
54
+ logic is_modify_op;
55
+
56
+ // ===== Calculated Address Components =====
57
+ logic [63:0] absolute_bit_address;
58
+ logic [57:0] word_address;
59
+ logic [5:0] bit_index_in_word;
60
+
61
+ // ===== Data Path =====
62
+ logic [63:0] read_word;
63
+ logic [63:0] modified_word;
64
+ logic result_data;
65
+
66
+ // ===== Address Calculation (Combinational) =====
67
+ assign absolute_bit_address = (base_addr_reg << 3) + bit_offset_reg;
68
+ assign word_address = absolute_bit_address[63:6];
69
+ assign bit_index_in_word = absolute_bit_address[5:0];
70
+ assign mem_addr = ADDR_WIDTH'({word_address, 3'b000}); // word address -> byte address (zero-extended)
71
+
72
+ // Check if operation is a modify operation
73
+ assign is_modify_op = (operation_reg == 3'b010) || // SET
74
+ (operation_reg == 3'b011) || // CLEAR
75
+ (operation_reg == 3'b100); // TOGGLE
76
+
77
+
78
+ // ===== Bit Modification =====
79
+ always_comb begin
80
+ case (operation_reg)
81
+ 3'b010: modified_word = read_word | (64'h1 << bit_index_in_word); // SET
82
+ 3'b011: modified_word = read_word & ~(64'h1 << bit_index_in_word); // CLEAR
83
+ 3'b100: modified_word = read_word ^ (64'h1 << bit_index_in_word); // TOGGLE
84
+ default: modified_word = read_word;
85
+ endcase
86
+ end
87
+
88
+ // ===== Result Extraction =====
89
+ assign result_data = read_word[bit_index_in_word]; // bit extraction
90
+
91
+ // Result is a one-cycle pulse, combinational from ST_RESULT
92
+ assign result_valid = (current_state == ST_RESULT);
93
+ assign result_bit = (current_state == ST_RESULT) ? result_data : 1'b0;
94
+
95
+ // ===== State Machine: Sequential =====
96
+ always_ff @(posedge clk) begin
97
+ if (reset) begin
98
+ current_state <= ST_IDLE;
99
+ base_addr_reg <= 64'h0;
100
+ bit_offset_reg <= 64'h0;
101
+ operation_reg <= 3'h0;
102
+ read_word <= 64'h0;
103
+ error <= 1'b0;
104
+ end else begin
105
+ current_state <= next_state;
106
+
107
+ // Capture operation on acceptance
108
+ if (op_valid && op_ready) begin
109
+ base_addr_reg <= base_address;
110
+ bit_offset_reg <= bit_offset;
111
+ operation_reg <= operation;
112
+ end
113
+
114
+ // Capture read data
115
+ if (mem_rvalid && current_state == ST_READ_WAIT) begin
116
+ read_word <= mem_rdata;
117
+ end
118
+
119
+ // Error status: cleared on accept, set on read fault while waiting
120
+ if (op_valid && op_ready) begin
121
+ error <= 1'b0;
122
+ end else if (mem_fault && current_state == ST_READ_WAIT) begin
123
+ error <= 1'b1;
124
+ end
125
+ end
126
+ end
127
+
128
+ // ===== State Machine: Combinational Next-State Logic =====
129
+ always_comb begin
130
+ next_state = current_state;
131
+ op_ready = 1'b0;
132
+ mem_valid = 1'b0;
133
+ mem_write = 1'b0;
134
+ mem_wdata = 64'h0;
135
+ mem_wstrb = 8'h00;
136
+
137
+ case (current_state)
138
+ ST_IDLE: begin
139
+ op_ready = 1'b1;
140
+ if (op_valid) begin
141
+ next_state = ST_READ_REQUEST;
142
+ end
143
+ end
144
+
145
+ ST_READ_REQUEST: begin
146
+ mem_valid = 1'b1;
147
+ mem_write = 1'b0;
148
+ if (mem_ready) begin
149
+ next_state = ST_READ_WAIT;
150
+ end
151
+ // else stay in READ_REQUEST (stall)
152
+ end
153
+
154
+ ST_READ_WAIT: begin
155
+ if (mem_rvalid) begin
156
+ if (is_modify_op) begin
157
+ next_state = ST_MODIFY;
158
+ end else begin
159
+ // BIT_GET or BIT_TEST: go directly to result
160
+ next_state = ST_RESULT;
161
+ end
162
+ end
163
+ if (mem_fault) begin
164
+ next_state = ST_RESULT;
165
+ end
166
+ end
167
+
168
+ ST_MODIFY: begin
169
+ // One cycle to calculate modified value
170
+ next_state = ST_WRITE_REQUEST;
171
+ end
172
+
173
+ ST_WRITE_REQUEST: begin
174
+ mem_valid = 1'b1;
175
+ mem_write = 1'b1;
176
+ mem_wdata = modified_word;
177
+ mem_wstrb = 8'hFF; // All bytes
178
+ if (mem_ready) begin
179
+ next_state = ST_WRITE_WAIT;
180
+ end
181
+ // else stay in WRITE_REQUEST (stall)
182
+ end
183
+
184
+ ST_WRITE_WAIT: begin
185
+ // Write accepted, no separate write-response in this model
186
+ // Go to result state
187
+ next_state = ST_RESULT;
188
+ end
189
+
190
+ ST_RESULT: begin
191
+ // result_valid asserted this cycle
192
+ // Next cycle return to IDLE
193
+ next_state = ST_IDLE;
194
+ end
195
+
196
+ default: next_state = ST_IDLE;
197
+ endcase
198
+
199
+ // A request presented in a cycle where reset is asserted is never issued,
200
+ // so reset cannot race with a write handshake at the same clock edge.
201
+ if (reset) begin
202
+ mem_valid = 1'b0;
203
+ mem_write = 1'b0;
204
+ mem_wdata = 64'h0;
205
+ mem_wstrb = 8'h00;
206
+ end
207
+ end
208
+
209
+ endmodule : bit_accelerator_v2
bit_accelerator/rtl/bit_address_generator.sv ADDED
@@ -0,0 +1,31 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Bit Address Generator
2
+ // Computes: effective_bit_address = base_bit_address + bit_offset
3
+ // Implementation: 64-bit Kogge-Stone parallel-prefix adder
4
+
5
+ module bit_address_generator (
6
+ input logic clk,
7
+ input logic rst_n,
8
+
9
+ // Operands
10
+ input logic [63:0] base_addr,
11
+ input logic [63:0] bit_offset,
12
+
13
+ // Control
14
+ input logic enable,
15
+
16
+ // Output
17
+ output logic [63:0] eff_bit_addr,
18
+ output logic carry_out
19
+ );
20
+
21
+ import bit_accelerator_pkg::*;
22
+
23
+ // Stage 1: Ripple-carry adder (simplified for synthesis)
24
+ // For timing closure, use built-in + operator which synthesizes to optimized adder
25
+ logic [64:0] sum;
26
+
27
+ assign sum = {1'b0, base_addr} + {1'b0, bit_offset};
28
+ assign eff_bit_addr = sum[63:0];
29
+ assign carry_out = sum[64];
30
+
31
+ endmodule : bit_address_generator
bit_accelerator/rtl/bit_extractor.sv ADDED
@@ -0,0 +1,36 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Bit Extractor - Single-bit and multi-bit extraction from a 64-bit word
2
+
3
+ module bit_extractor (
4
+ input logic [63:0] word_data,
5
+ input logic [5:0] bit_index,
6
+ input logic [5:0] field_width, // For multi-bit extraction (1-64)
7
+ input logic is_multibit,
8
+
9
+ output logic [63:0] result
10
+ );
11
+
12
+ logic [63:0] shifted_word;
13
+ logic [63:0] mask;
14
+
15
+ // Barrel shifter: rotate right by bit_index positions
16
+ // This is combinational and synthesizes to mux tree
17
+ assign shifted_word = word_data >> bit_index;
18
+
19
+ // Generate mask for field width
20
+ // For width=1: mask = 64'h0000_0000_0000_0001
21
+ // For width=2: mask = 64'h0000_0000_0000_0003
22
+ // For width=64: mask = 64'hFFFF_FFFF_FFFF_FFFF
23
+
24
+ always_comb begin
25
+ if (field_width == 6'h0)
26
+ mask = 64'h0;
27
+ else if (field_width == 6'd64)
28
+ mask = 64'hFFFFFFFFFFFFFFFF;
29
+ else
30
+ mask = (64'h1 << field_width) - 1'b1;
31
+ end
32
+
33
+ // Extract field
34
+ assign result = is_multibit ? (shifted_word & mask) : {63'h0, shifted_word[0]};
35
+
36
+ endmodule : bit_extractor
bit_accelerator/rtl/bit_modifier.sv ADDED
@@ -0,0 +1,29 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Bit Modifier - Set, clear, and toggle operations on a 64-bit word
2
+
3
+ module bit_modifier (
4
+ input logic [63:0] word_data,
5
+ input logic [5:0] bit_index,
6
+ input logic [2:0] operation, // SET=3'b010, CLEAR=3'b011, TOGGLE=3'b100
7
+
8
+ output logic [63:0] result
9
+ );
10
+
11
+ logic [63:0] bit_mask;
12
+
13
+ // Generate mask with single bit set at bit_index
14
+ // For bit_index=0: mask = 64'h0000_0000_0000_0001
15
+ // For bit_index=63: mask = 64'h8000_0000_0000_0000
16
+
17
+ assign bit_mask = 64'h1 << bit_index;
18
+
19
+ // Apply operation
20
+ always_comb begin
21
+ case (operation)
22
+ 3'b010: result = word_data | bit_mask; // BIT_SET
23
+ 3'b011: result = word_data & ~bit_mask; // BIT_CLEAR
24
+ 3'b100: result = word_data ^ bit_mask; // BIT_TOGGLE
25
+ default: result = word_data; // No-op
26
+ endcase
27
+ end
28
+
29
+ endmodule : bit_modifier
bit_accelerator/run_v2_sim.sh ADDED
@@ -0,0 +1,10 @@
 
 
 
 
 
 
 
 
 
 
 
1
+ #!/usr/bin/env bash
2
+ # Build and run the cycle-accurate v2 testbench with Verilator (>= 5.0).
3
+ # Exits non-zero if any check fails ($fatal in the testbench).
4
+ set -euo pipefail
5
+ cd "$(dirname "$0")"
6
+ OUT=${OUT:-build/verilator}
7
+ rm -rf "$OUT" && mkdir -p "$OUT"
8
+ verilator --binary --timing -Wall -Wno-fatal --top-module tb_bit_accelerator_v2 \
9
+ -Mdir "$OUT" rtl/bit_accelerator_v2.sv testbenches/tb_bit_accelerator_v2.sv >/dev/null
10
+ "$OUT"/Vtb_bit_accelerator_v2
bit_accelerator/scripts/prove.sh ADDED
@@ -0,0 +1,39 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ #!/usr/bin/env bash
2
+ # Prove every goal of the given Why3 files with one prover.
3
+ # Usage: scripts/prove.sh [-P prover] [-t seconds] [-L dir] file.mlw...
4
+ # Goals are split with the split_vc transformation before proving.
5
+ # Prints one line per goal and exits non-zero unless every goal is Valid.
6
+ set -euo pipefail
7
+ prover=z3; timelimit=30; loadpath=()
8
+ while getopts "P:t:L:" opt; do
9
+ case "$opt" in
10
+ P) prover=$OPTARG ;;
11
+ t) timelimit=$OPTARG ;;
12
+ L) loadpath+=(-L "$OPTARG") ;;
13
+ *) exit 2 ;;
14
+ esac
15
+ done
16
+ shift $((OPTIND - 1))
17
+ [ $# -gt 0 ] || { echo "usage: $0 [-P prover] [-t s] [-L dir] file.mlw..." >&2; exit 2; }
18
+ command -v why3 >/dev/null || { echo "why3 not found" >&2; exit 2; }
19
+
20
+ total=0; bad=0
21
+ for f in "$@"; do
22
+ out=$(why3 prove "${loadpath[@]}" -a split_vc -P "$prover" -t "$timelimit" "$f" 2>&1) || true
23
+ results=$(printf '%s\n' "$out" | awk '
24
+ /^Goal / { goal = $2; sub(/\.$/, "", goal) }
25
+ /^Sub-goal / { kind = $2; goal = $0; sub(/.* of goal /, "", goal); sub(/\.$/, "", goal); goal = goal ":" kind }
26
+ /Prover result is:/ { r = $0; sub(/.*Prover result is: /, "", r); print goal "\t" r }')
27
+ if [ -z "$results" ]; then
28
+ echo "ERROR $f: no goals reported"; printf '%s\n' "$out" | head -20; bad=$((bad + 1)); continue
29
+ fi
30
+ while IFS=$'\t' read -r goal res; do
31
+ total=$((total + 1))
32
+ case "$res" in
33
+ Valid*) printf ' ok %-40s %s\n' "$(basename "$f"):$goal" "$res" ;;
34
+ *) printf ' FAIL %-40s %s\n' "$(basename "$f"):$goal" "$res"; bad=$((bad + 1)) ;;
35
+ esac
36
+ done <<< "$results"
37
+ done
38
+ echo "why3/$prover: $((total - bad))/$total goals valid"
39
+ [ "$bad" -eq 0 ]
bit_accelerator/testbenches/tb_bit_accelerator.sv ADDED
@@ -0,0 +1,322 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Testbench for Bit-String Hardware Accelerator
2
+ // Comprehensive functional verification of all operations and edge cases
3
+
4
+ module tb_bit_accelerator ();
5
+
6
+ // Parameters
7
+ localparam int ADDR_WIDTH = 64;
8
+ localparam int WORD_WIDTH = 64;
9
+ localparam int WORD_BYTES = WORD_WIDTH / 8;
10
+ localparam int READ_LATENCY = 2;
11
+
12
+ // Clock and Reset
13
+ logic clk;
14
+ logic reset;
15
+
16
+ // DUT: Operation Interface
17
+ logic op_valid;
18
+ logic op_ready;
19
+ logic [63:0] base_address;
20
+ logic [63:0] bit_offset;
21
+ logic [2:0] operation;
22
+
23
+ // DUT: Response Interface
24
+ logic result_valid;
25
+ logic result_bit;
26
+ logic error;
27
+
28
+ // DUT: Memory Interface
29
+ logic mem_req_valid;
30
+ logic mem_req_ready;
31
+ logic [ADDR_WIDTH-1:0] mem_addr;
32
+ logic mem_read;
33
+ logic mem_write;
34
+ logic [WORD_BYTES-1:0] mem_wstrb;
35
+ logic [WORD_WIDTH-1:0] mem_wdata;
36
+ logic mem_rvalid;
37
+ logic [WORD_WIDTH-1:0] mem_rdata;
38
+ logic mem_fault;
39
+
40
+ // DUT Instantiation
41
+ bit_accelerator dut (
42
+ .clk (clk),
43
+ .reset (reset),
44
+ .op_valid (op_valid),
45
+ .op_ready (op_ready),
46
+ .base_address(base_address),
47
+ .bit_offset (bit_offset),
48
+ .operation (operation),
49
+ .result_valid(result_valid),
50
+ .result_bit (result_bit),
51
+ .error (error),
52
+ .mem_req_valid(mem_req_valid),
53
+ .mem_req_ready(mem_req_ready),
54
+ .mem_addr (mem_addr),
55
+ .mem_read (mem_read),
56
+ .mem_write (mem_write),
57
+ .mem_wstrb (mem_wstrb),
58
+ .mem_wdata (mem_wdata),
59
+ .mem_rvalid (mem_rvalid),
60
+ .mem_rdata (mem_rdata),
61
+ .mem_fault (mem_fault)
62
+ );
63
+
64
+ // Memory Model
65
+ behavioral_memory #(
66
+ .ADDR_WIDTH (ADDR_WIDTH),
67
+ .WORD_WIDTH (WORD_WIDTH),
68
+ .READ_LATENCY(READ_LATENCY)
69
+ ) memory_model (
70
+ .clk (clk),
71
+ .reset (reset),
72
+ .req_valid(mem_req_valid),
73
+ .req_ready(mem_req_ready),
74
+ .addr (mem_addr),
75
+ .is_read (mem_read),
76
+ .is_write(mem_write),
77
+ .wstrb (mem_wstrb),
78
+ .wdata (mem_wdata),
79
+ .rvalid (mem_rvalid),
80
+ .rdata (mem_rdata),
81
+ .fault (mem_fault)
82
+ );
83
+
84
+ // Clock generation (10ns period = 100 MHz)
85
+ initial begin
86
+ clk = 1'b0;
87
+ forever #5 clk = ~clk;
88
+ end
89
+
90
+ // Test vector structure
91
+ typedef struct packed {
92
+ logic [63:0] base_addr;
93
+ logic [63:0] bit_offset;
94
+ logic [2:0] op;
95
+ logic [63:0] expected_word;
96
+ logic expected_bit;
97
+ string test_name;
98
+ } test_vec_t;
99
+
100
+ // Test counters
101
+ int test_count = 0;
102
+ int pass_count = 0;
103
+ int fail_count = 0;
104
+
105
+ // Helper tasks
106
+
107
+ task automatic write_memory(logic [63:0] byte_addr, logic [63:0] data);
108
+ logic [63:0] word_addr = byte_addr >> 3;
109
+ // Direct write to memory model's memory array
110
+ // (In real simulation, use the memory interface)
111
+ endtask
112
+
113
+ task automatic init_memory();
114
+ // Initialize memory with test pattern
115
+ // Word at byte address 0x00: 64'h0123456789ABCDEF
116
+ // Word at byte address 0x08: 64'hFEDCBA9876543210
117
+ // Word at byte address 0x10: 64'hAAAAAAAAAAAAAAAA
118
+ // Word at byte address 0x18: 64'h5555555555555555
119
+
120
+ automatic logic [63:0] init_data[4];
121
+ init_data[0] = 64'h0123456789ABCDEF;
122
+ init_data[1] = 64'hFEDCBA9876543210;
123
+ init_data[2] = 64'hAAAAAAAAAAAAAAAA;
124
+ init_data[3] = 64'h5555555555555555;
125
+
126
+ // Write to memory via operation (requires memory to be functional)
127
+ // For now, directly access memory_model.memory
128
+ for (int i = 0; i < 4; i++) begin
129
+ memory_model.memory[i] = init_data[i];
130
+ end
131
+ endtask
132
+
133
+ task automatic run_operation(
134
+ input logic [63:0] base_addr,
135
+ input logic [63:0] bit_off,
136
+ input logic [2:0] op,
137
+ output logic result_bit_out,
138
+ output logic error_out
139
+ );
140
+ logic done = 1'b0;
141
+ int cycles = 0;
142
+
143
+ // Assert operation request
144
+ op_valid <= 1'b1;
145
+ base_address <= base_addr;
146
+ bit_offset <= bit_off;
147
+ operation <= op;
148
+
149
+ // Wait for acceptance
150
+ @(posedge clk);
151
+ while (!op_ready && cycles < 100) begin
152
+ @(posedge clk);
153
+ cycles++;
154
+ end
155
+
156
+ op_valid <= 1'b0;
157
+
158
+ // Wait for result
159
+ cycles = 0;
160
+ while (!result_valid && cycles < 200) begin
161
+ @(posedge clk);
162
+ cycles++;
163
+ end
164
+
165
+ if (result_valid) begin
166
+ result_bit_out = result_bit;
167
+ error_out = error;
168
+ end else begin
169
+ result_bit_out = 1'bX;
170
+ error_out = 1'b1;
171
+ end
172
+ endtask
173
+
174
+ task automatic test_bit_get(logic [63:0] base_addr, logic [63:0] bit_off, logic expected_bit, string test_name);
175
+ logic result_bit_out;
176
+ logic error_out;
177
+
178
+ $display("[%0d] Testing BIT_GET: %s", test_count, test_name);
179
+ run_operation(base_addr, bit_off, 3'b000, result_bit_out, error_out);
180
+
181
+ if (error_out) begin
182
+ $display(" FAIL: Operation returned error");
183
+ fail_count++;
184
+ end else if (result_bit_out === expected_bit) begin
185
+ $display(" PASS: Got expected bit value %b", expected_bit);
186
+ pass_count++;
187
+ end else begin
188
+ $display(" FAIL: Expected %b, got %b", expected_bit, result_bit_out);
189
+ fail_count++;
190
+ end
191
+
192
+ test_count++;
193
+ @(posedge clk);
194
+ endtask
195
+
196
+ task automatic test_bit_set(logic [63:0] base_addr, logic [63:0] bit_off, string test_name);
197
+ logic result_bit_out;
198
+ logic error_out;
199
+
200
+ $display("[%0d] Testing BIT_SET: %s", test_count, test_name);
201
+ run_operation(base_addr, bit_off, 3'b010, result_bit_out, error_out);
202
+
203
+ if (error_out) begin
204
+ $display(" FAIL: Operation returned error");
205
+ fail_count++;
206
+ end else begin
207
+ $display(" PASS: BIT_SET completed, result=%b", result_bit_out);
208
+ pass_count++;
209
+ end
210
+
211
+ test_count++;
212
+ @(posedge clk);
213
+ endtask
214
+
215
+ task automatic test_bit_clear(logic [63:0] base_addr, logic [63:0] bit_off, string test_name);
216
+ logic result_bit_out;
217
+ logic error_out;
218
+
219
+ $display("[%0d] Testing BIT_CLEAR: %s", test_count, test_name);
220
+ run_operation(base_addr, bit_off, 3'b011, result_bit_out, error_out);
221
+
222
+ if (error_out) begin
223
+ $display(" FAIL: Operation returned error");
224
+ fail_count++;
225
+ end else begin
226
+ $display(" PASS: BIT_CLEAR completed, result=%b", result_bit_out);
227
+ pass_count++;
228
+ end
229
+
230
+ test_count++;
231
+ @(posedge clk);
232
+ endtask
233
+
234
+ // Main Testbench
235
+ initial begin
236
+ // Initialize signals
237
+ op_valid = 1'b0;
238
+ base_address = 64'h0;
239
+ bit_offset = 64'h0;
240
+ operation = 3'h0;
241
+ reset = 1'b0;
242
+
243
+ // Reset sequence
244
+ #20;
245
+ reset = 1'b1;
246
+ #20;
247
+
248
+ $display("\n========================================");
249
+ $display(" BIT ACCELERATOR FUNCTIONAL TEST ");
250
+ $display("========================================\n");
251
+
252
+ // Initialize memory
253
+ init_memory();
254
+
255
+ // Test 1: BIT_GET at various offsets (single word)
256
+ $display("\n--- Test Group 1: Single-Word Bit Extraction ---");
257
+
258
+ // Word 0 = 0x0123456789ABCDEF
259
+ // Bit 0 (LSB of byte 0): 1
260
+ test_bit_get(64'h00, 64'h0, 1'b1, "bit 0 of word 0");
261
+
262
+ // Bit 1: 1
263
+ test_bit_get(64'h00, 64'h1, 1'b1, "bit 1 of word 0");
264
+
265
+ // Bit 7: 0
266
+ test_bit_get(64'h00, 64'h7, 1'b0, "bit 7 of word 0");
267
+
268
+ // Bit 8 (LSB of byte 1): 1
269
+ test_bit_get(64'h00, 64'h8, 1'b1, "bit 8 of word 0");
270
+
271
+ // Bit 31: 0
272
+ test_bit_get(64'h00, 64'h1F, 1'b0, "bit 31 of word 0");
273
+
274
+ // Bit 32: 1
275
+ test_bit_get(64'h00, 64'h20, 1'b1, "bit 32 of word 0");
276
+
277
+ // Bit 63 (MSB of word): 0
278
+ test_bit_get(64'h00, 64'h3F, 1'b0, "bit 63 of word 0");
279
+
280
+ // Test 2: Cross-word boundary
281
+ $display("\n--- Test Group 2: Cross-Word Boundary ---");
282
+
283
+ // Word 1 = 0xFEDCBA9876543210
284
+ // Bit 64 (bit 0 of word 1): 0
285
+ test_bit_get(64'h00, 64'h40, 1'b0, "bit 64 (bit 0 of word 1)");
286
+
287
+ // Bit 65: 0
288
+ test_bit_get(64'h00, 64'h41, 1'b0, "bit 65 (bit 1 of word 1)");
289
+
290
+ // Test 3: Base address offset
291
+ $display("\n--- Test Group 3: Non-Zero Base Address ---");
292
+
293
+ // Base address = 0x08 (word 1)
294
+ // Bit offset = 0 (bit 0 of word 1)
295
+ test_bit_get(64'h08, 64'h0, 1'b0, "base=0x08, offset=0");
296
+
297
+ // Test 4: Modify operations
298
+ $display("\n--- Test Group 4: Modify Operations ---");
299
+
300
+ test_bit_set(64'h10, 64'h0, "BIT_SET at bit 0 of word 2");
301
+ test_bit_clear(64'h10, 64'h0, "BIT_CLEAR at bit 0 of word 2");
302
+
303
+ // Summary
304
+ $display("\n========================================");
305
+ $display(" TEST SUMMARY ");
306
+ $display("========================================");
307
+ $display("Total Tests: %0d", test_count);
308
+ $display("Passed: %0d", pass_count);
309
+ $display("Failed: %0d", fail_count);
310
+
311
+ if (fail_count == 0) begin
312
+ $display("\n✓ All tests PASSED!");
313
+ end else begin
314
+ $display("\n✗ %0d tests FAILED!", fail_count);
315
+ end
316
+ $display("========================================\n");
317
+
318
+ #100;
319
+ $finish;
320
+ end
321
+
322
+ endmodule : tb_bit_accelerator
bit_accelerator/testbenches/tb_bit_accelerator_v2.sv ADDED
@@ -0,0 +1,311 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Cycle-accurate testbench for bit_accelerator_v2.
2
+ // Inputs are driven on negedge; every posedge logs the pre-edge value of each
3
+ // signal, so log[c] is exactly what the DUT/memory saw during cycle c.
4
+ // Spec (1-cycle-latency memory): accept@a, READ_REQ@a+1, READ_RESP@a+2, RESULT_VALID@a+3.
5
+
6
+ module tb_bit_accelerator_v2;
7
+
8
+ localparam int MAXC = 4096;
9
+
10
+ logic clk = 1'b0;
11
+ logic reset;
12
+ logic op_valid, op_ready;
13
+ logic [63:0] base_address, bit_offset;
14
+ logic [2:0] operation;
15
+ logic result_valid, result_bit, error;
16
+ logic mem_valid, mem_write, mem_ready;
17
+ logic [63:0] mem_addr, mem_wdata, mem_rdata;
18
+ logic [7:0] mem_wstrb;
19
+ logic mem_rvalid = 1'b0, mem_fault = 1'b0;
20
+
21
+ bit_accelerator_v2 dut (.*);
22
+
23
+ always #5 clk = ~clk;
24
+
25
+ // ---------------- memory model (1-cycle read latency) ----------------
26
+ logic [63:0] memory [0:1023];
27
+ bit stall_en;
28
+ int stall_lo, stall_hi;
29
+ int cyc = 0;
30
+
31
+ assign mem_ready = !(stall_en && cyc >= stall_lo && cyc <= stall_hi);
32
+ bit fault_next_read = 1'b0; // answer the next accepted read with mem_fault
33
+
34
+ always_ff @(posedge clk) begin
35
+ mem_rvalid <= 1'b0;
36
+ mem_fault <= 1'b0;
37
+ if (mem_valid && mem_ready) begin
38
+ if (mem_write) begin
39
+ for (int i = 0; i < 8; i++)
40
+ if (mem_wstrb[i]) memory[mem_addr[12:3]][i*8 +: 8] <= mem_wdata[i*8 +: 8];
41
+ end else if (fault_next_read) begin
42
+ mem_fault <= 1'b1;
43
+ fault_next_read <= 1'b0;
44
+ end else begin
45
+ mem_rvalid <= 1'b1;
46
+ mem_rdata <= memory[mem_addr[12:3]];
47
+ end
48
+ end
49
+ end
50
+
51
+ // ---------------- per-cycle log ----------------
52
+ logic l_opv [0:MAXC-1], l_opr [0:MAXC-1];
53
+ logic l_mv [0:MAXC-1], l_mw [0:MAXC-1], l_mr [0:MAXC-1];
54
+ logic l_rv [0:MAXC-1], l_res [0:MAXC-1], l_bit [0:MAXC-1], l_err [0:MAXC-1];
55
+ logic [63:0] l_wd [0:MAXC-1];
56
+
57
+ always @(posedge clk) begin
58
+ l_opv[cyc] = op_valid; l_opr[cyc] = op_ready;
59
+ l_mv[cyc] = mem_valid; l_mw[cyc] = mem_write; l_mr[cyc] = mem_ready;
60
+ l_rv[cyc] = mem_rvalid; l_res[cyc] = result_valid; l_bit[cyc] = result_bit;
61
+ l_err[cyc] = error;
62
+ l_wd[cyc] = mem_wdata;
63
+ cyc <= cyc + 1;
64
+ end
65
+
66
+ // ---------------- checking helpers ----------------
67
+ int fails = 0, checks = 0;
68
+
69
+ task automatic check(input bit cond, input string msg);
70
+ checks++;
71
+ if (!cond) begin
72
+ fails++;
73
+ $display(" FAIL: %s", msg);
74
+ end
75
+ endtask
76
+
77
+ task automatic init_mem();
78
+ for (int i = 0; i < 1024; i++) memory[i] = {32'hA5A50000 | i[15:0], 32'h0000F00D | (i[15:0] << 16)};
79
+ memory[0] = 64'h0000_0000_0000_0020; // bit 5 set only
80
+ memory[1] = 64'h0000_0000_0000_0000;
81
+ endtask
82
+
83
+ task automatic do_reset();
84
+ @(negedge clk);
85
+ reset = 1'b1; op_valid = 1'b0;
86
+ @(negedge clk);
87
+ reset = 1'b0;
88
+ @(negedge clk);
89
+ endtask
90
+
91
+ // Issue one op; returns the cycle index at which it was accepted.
92
+ task automatic issue(input logic [2:0] op, input logic [63:0] base, input logic [63:0] off,
93
+ output int acc);
94
+ @(negedge clk);
95
+ op_valid = 1'b1; operation = op; base_address = base; bit_offset = off;
96
+ acc = cyc; // op_valid/op_ready are sampled at the next posedge, cycle == cyc
97
+ @(negedge clk);
98
+ op_valid = 1'b0;
99
+ endtask
100
+
101
+ task automatic wait_cycles(input int n);
102
+ repeat (n) @(negedge clk);
103
+ endtask
104
+
105
+ function automatic int count_results(input int lo, input int hi);
106
+ int n = 0;
107
+ for (int c = lo; c <= hi; c++) if (l_res[c]) n++;
108
+ return n;
109
+ endfunction
110
+
111
+ // ---------------- tests ----------------
112
+ task automatic t_get(input string name, input logic [63:0] base, input logic [63:0] off, input bit exp_bit);
113
+ int a;
114
+ $display("TEST %s", name);
115
+ do_reset();
116
+ issue(3'b000, base, off, a);
117
+ wait_cycles(10);
118
+ check(l_opv[a] && l_opr[a], "op accepted at a");
119
+ check(l_mv[a+1] && !l_mw[a+1], "READ_REQUEST at a+1");
120
+ check(!l_mv[a+2], "no second request at a+2");
121
+ check(l_rv[a+2], "READ_RESPONSE at a+2");
122
+ check(l_res[a+3], "RESULT_VALID at a+3");
123
+ check(l_bit[a+3] == exp_bit, "result_bit value");
124
+ check(!l_res[a+4], "result_valid is one-cycle (low at a+4)");
125
+ check(count_results(a, a+10) == 1, "exactly one result pulse");
126
+ check(l_opr[a+4] && !l_opr[a+1] && !l_opr[a+3], "op_ready low while busy, high after result");
127
+ endtask
128
+
129
+ task automatic t_modify(input string name, input logic [2:0] op, input logic [63:0] base,
130
+ input logic [63:0] off, input logic [63:0] exp_word);
131
+ int a;
132
+ logic [63:0] widx;
133
+ widx = ((base << 3) + off) >> 6;
134
+ $display("TEST %s", name);
135
+ do_reset();
136
+ issue(op, base, off, a);
137
+ wait_cycles(12);
138
+ check(l_mv[a+1] && !l_mw[a+1], "READ_REQUEST at a+1");
139
+ check(l_rv[a+2], "READ_RESPONSE at a+2");
140
+ check(!l_mv[a+3], "MODIFY: no mem request at a+3");
141
+ check(l_mv[a+4] && l_mw[a+4] && l_mr[a+4], "WRITE accepted (valid&&write&&ready) at a+4");
142
+ check(!l_mv[a+5], "no request after accepted write at a+5");
143
+ check(l_res[a+6], "RESULT_VALID at a+6");
144
+ check(count_results(a, a+12) == 1, "exactly one result pulse");
145
+ check(memory[widx[9:0]] == exp_word, "memory word after RMW");
146
+ endtask
147
+
148
+ task automatic t_write_stall();
149
+ int a;
150
+ logic [63:0] mem0_pre;
151
+ $display("TEST write stall (mem_ready low a+4..a+6)");
152
+ do_reset();
153
+ mem0_pre = memory[0];
154
+ @(negedge clk);
155
+ stall_en = 1'b1; stall_lo = cyc + 1 + 4; stall_hi = cyc + 1 + 6; // issue() accepts at cyc+1
156
+ issue(3'b010, 64'd0, 64'd0, a);
157
+ check(a + 4 == stall_lo, "stall window aligned to write request");
158
+ wait_cycles(14);
159
+ stall_en = 1'b0;
160
+ check(l_mv[a+4] && l_mw[a+4] && !l_mr[a+4], "write request held, not accepted a+4");
161
+ check(l_mv[a+5] && l_mw[a+5] && !l_mr[a+5], "write request held a+5");
162
+ check(l_mv[a+6] && l_mw[a+6] && !l_mr[a+6], "write request held a+6");
163
+ check(l_wd[a+4] == l_wd[a+5] && l_wd[a+5] == l_wd[a+6], "wdata stable during stall");
164
+ check(l_mv[a+7] && l_mw[a+7] && l_mr[a+7], "write accepted at a+7");
165
+ check(!l_mv[a+8], "no request after accept");
166
+ check(count_results(a, a+7) == 0, "no result mem0_pre write accepted");
167
+ check(l_res[a+9], "RESULT_VALID at a+9 (2 cycles after accept)");
168
+ check(count_results(a, a+14) == 1, "exactly one result pulse");
169
+ check(memory[0] == (mem0_pre | 64'h1), "write committed once");
170
+ endtask
171
+
172
+ task automatic t_read_stall();
173
+ int a;
174
+ $display("TEST read stall (mem_ready low a+1..a+2)");
175
+ do_reset();
176
+ @(negedge clk);
177
+ stall_en = 1'b1; stall_lo = cyc + 1 + 1; stall_hi = cyc + 1 + 2;
178
+ issue(3'b000, 64'd0, 64'd5, a);
179
+ wait_cycles(10);
180
+ stall_en = 1'b0;
181
+ check(l_mv[a+1] && !l_mr[a+1] && l_mv[a+2] && !l_mr[a+2], "read request held during stall");
182
+ check(l_mv[a+3] && l_mr[a+3], "read accepted at a+3");
183
+ check(l_rv[a+4], "read response at a+4");
184
+ check(l_res[a+5] && l_bit[a+5], "RESULT_VALID at a+5 with bit=1");
185
+ check(count_results(a, a+10) == 1, "exactly one result pulse");
186
+ endtask
187
+
188
+ // Reset asserted for one cycle at cycle (a + k): operation must be cancelled.
189
+ task automatic t_reset_at(input int k, input string where);
190
+ int a;
191
+ logic [63:0] mem0_pre;
192
+ $display("TEST reset cancels op during %s (reset@a+%0d)", where, k);
193
+ do_reset();
194
+ mem0_pre = memory[0];
195
+ issue(3'b010, 64'd0, 64'd0, a);
196
+ while (cyc < a + k) @(negedge clk);
197
+ reset = 1'b1;
198
+ @(negedge clk);
199
+ reset = 1'b0;
200
+ wait_cycles(12);
201
+ check(count_results(a, a+16) == 0, "no result_valid for cancelled op");
202
+ check(!mem_valid && !result_valid, "idle outputs after reset");
203
+ check(op_ready, "op_ready after reset");
204
+ if (k <= 4)
205
+ check(memory[0] == mem0_pre, "no write committed (cancelled before write accepted)");
206
+ // a fresh op must work normally afterwards
207
+ begin
208
+ int b;
209
+ issue(3'b000, 64'd0, 64'd5, b);
210
+ wait_cycles(8);
211
+ check(l_res[b+3] && l_bit[b+3], "fresh op after reset completes normally");
212
+ end
213
+ endtask
214
+
215
+ // Read fault: the op ends at a+3 with error=1 in the result cycle and never writes.
216
+ task automatic t_read_fault(input string name, input logic [2:0] op);
217
+ int a, b;
218
+ logic [63:0] mem0_pre;
219
+ $display("TEST read fault on %s", name);
220
+ do_reset();
221
+ mem0_pre = memory[0];
222
+ @(negedge clk);
223
+ fault_next_read = 1'b1;
224
+ issue(op, 64'd0, 64'd5, a);
225
+ wait_cycles(10);
226
+ check(l_mv[a+1] && !l_mw[a+1], "READ_REQUEST at a+1");
227
+ check(!l_rv[a+2], "no read data on a faulted read");
228
+ check(l_res[a+3], "RESULT_VALID at a+3");
229
+ check(l_err[a+3], "error high in the result cycle");
230
+ check(count_results(a, a+10) == 1, "exactly one result pulse");
231
+ for (int c = a + 1; c <= a + 10; c++)
232
+ check(!(l_mv[c] && l_mw[c]), "no write after a read fault");
233
+ check(memory[0] == mem0_pre, "memory unchanged after a read fault");
234
+ // The next operation clears error.
235
+ issue(3'b000, 64'd0, 64'd5, b);
236
+ wait_cycles(8);
237
+ check(l_res[b+3] && !l_err[b+3] && l_bit[b+3], "next op completes with error=0");
238
+ endtask
239
+
240
+ // Opcodes 101..111 are not defined; v2 executes them as a read with no write.
241
+ task automatic t_undefined_opcode(input logic [2:0] op);
242
+ int a;
243
+ logic [63:0] mem0_pre;
244
+ $display("TEST undefined opcode %b reads and never writes", op);
245
+ do_reset();
246
+ mem0_pre = memory[0];
247
+ issue(op, 64'd0, 64'd5, a);
248
+ wait_cycles(10);
249
+ check(l_res[a+3] && l_bit[a+3] && !l_err[a+3], "completes like GET at a+3");
250
+ for (int c = a + 1; c <= a + 10; c++)
251
+ check(!(l_mv[c] && l_mw[c]), "no write for an undefined opcode");
252
+ check(memory[0] == mem0_pre, "memory unchanged");
253
+ endtask
254
+
255
+ initial begin
256
+ reset = 1'b1; op_valid = 1'b0; operation = '0; base_address = '0; bit_offset = '0;
257
+ stall_en = 1'b0; stall_lo = 0; stall_hi = 0;
258
+ init_mem();
259
+
260
+ t_get("GET bit5 (set)", 64'd0, 64'd5, 1'b1);
261
+ t_get("GET bit4 (clear)", 64'd0, 64'd4, 1'b0);
262
+ t_get("GET word1 bit 0 via off=64", 64'd0, 64'd64, 1'b0);
263
+
264
+ t_modify("SET bit0", 3'b010, 64'd0, 64'd0, 64'h21);
265
+ init_mem();
266
+ t_modify("CLEAR bit5", 3'b011, 64'd0, 64'd5, 64'h00);
267
+ init_mem();
268
+ t_modify("TOGGLE bit5", 3'b100, 64'd0, 64'd5, 64'h00);
269
+ init_mem();
270
+ t_modify("SET cross-word (off=70 -> word1 bit6)", 3'b010, 64'd0, 64'd70, 64'h40);
271
+ init_mem();
272
+ t_modify("SET base=8 off=3 -> word1 bit3", 3'b010, 64'd8, 64'd3, 64'h08);
273
+ init_mem();
274
+
275
+ t_write_stall();
276
+ init_mem();
277
+ t_read_stall();
278
+ init_mem();
279
+
280
+ t_reset_at(1, "READ_REQUEST");
281
+ init_mem();
282
+ t_reset_at(2, "READ_WAIT");
283
+ init_mem();
284
+ t_reset_at(3, "MODIFY");
285
+ init_mem();
286
+ t_reset_at(4, "WRITE_REQUEST");
287
+ init_mem();
288
+ t_reset_at(5, "WRITE_WAIT");
289
+ init_mem();
290
+
291
+ t_read_fault("GET", 3'b000);
292
+ init_mem();
293
+ t_read_fault("SET", 3'b010);
294
+ init_mem();
295
+ t_read_fault("TOGGLE", 3'b100);
296
+ init_mem();
297
+ t_undefined_opcode(3'b101);
298
+ t_undefined_opcode(3'b111);
299
+
300
+ $display("\nchecks=%0d fails=%0d", checks, fails);
301
+ if (fails != 0) $fatal(1, "FAILED");
302
+ $display("ALL PASS");
303
+ $finish;
304
+ end
305
+
306
+ initial begin
307
+ #2000000;
308
+ $fatal(1, "TIMEOUT");
309
+ end
310
+
311
+ endmodule
docs/verification.md ADDED
@@ -0,0 +1,58 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # Verification Contract
2
+
3
+ Applies to `rtl/bit_accelerator.sv`.
4
+
5
+ ## Interface
6
+
7
+ - Reset is synchronous and active-high. Reset cancels any uncompleted operation
8
+ and suppresses its result. `op_ready` is low while `reset` is high.
9
+ - An operation is accepted on a cycle with `op_valid && op_ready`. `op_ready`
10
+ stays low until the operation's result pulse.
11
+ - A read request completes on `mem_valid && !mem_write && mem_ready`; its data
12
+ completes on `mem_rvalid`. A read fault is signalled with `mem_fault` instead
13
+ of `mem_rvalid`.
14
+ - A write request completes on `mem_valid && mem_write && mem_ready`. The cycle
15
+ after the write handshake, `mem_fault` reports a write fault.
16
+ - `mem_addr` is `((base_address << 3) + bit_offset) >> 6 << 3` (64-bit
17
+ arithmetic); `mem_wstrb` is all ones.
18
+ - `result_valid` is a one-cycle pulse. `error` and `result_bit` are valid in the
19
+ same cycle. On `error`, `result_bit` keeps its previous value.
20
+
21
+ ## Operations
22
+
23
+ | Opcode | Op | Writes | `result_bit` |
24
+ |---|---|---|---|
25
+ | 000 | GET | no | bit value |
26
+ | 001 | TEST | no | bit value |
27
+ | 010 | SET | yes | 1 |
28
+ | 011 | CLEAR | yes | 0 |
29
+ | 100 | TOGGLE | yes | new bit value |
30
+ | 101-111 | undefined | no | `error = 1` |
31
+
32
+ A read fault ends the operation with `error = 1` and no write. A write fault
33
+ reports `error = 1`; whether the memory kept the write is up to the memory.
34
+
35
+ ## Evidence
36
+
37
+ | Check | Tool | Result |
38
+ |---|---|---|
39
+ | Lint | `verilator --lint-only -Wall` | clean |
40
+ | Simulation | `verification/tb_bit_accelerator.sv`, Icarus 12 and Verilator 5.020 | 0 failures; 23 directed operations, 12 reset-cancellation cases, 2000 random operations per seed with backpressure, read latency 0-3 and fault injection |
41
+ | Mutation | 7 hand-made RTL mutants (wrong bit index, wrong address, SET as XOR, ...) | all detected |
42
+ | Proofs | `formal/*.mlw`, Why3 1.6 + Z3 4.8.12 | 38/38 goals valid |
43
+ | Timing model | `spice/bit_extract.sp`, ngspice 42 | tpd ≈ 94 ps (RC model, not extracted silicon) |
44
+ | FPGA wrapper | `fpga/tb/tb_fpga_top.sv` over the UART: RTL (Icarus, Verilator), iCE40 and ECP5 gate-level netlists | 0 failures on each |
45
+ | Host tool | `fpga/sim/cosim.sh`: `bitacc selftest` against the RTL through a pseudo-terminal | 2000 operations, 0 mismatches |
46
+ | FPGA place-and-route | nextpnr, 5 seeds | iCE40UP5K 39.06 MHz, ECP5-25F 73.22 MHz; both meet board clocks |
47
+ | ASIC synthesis | Yosys + ABC on sky130_fd_sc_hd, OpenSTA | 1538 cells, 10,063 µm², netlist proved equal to RTL, 500 MHz pre-layout |
48
+
49
+ `formal/bit_address.mlw` proves that the RTL's shift/mask datapath equals the
50
+ integer address specification when `(base << 3) + offset` does not overflow.
51
+ Its trusted base is four facts from the Why3 bit-vector library (listed in the
52
+ file), restated because the SMT drivers do not pass them to the solver.
53
+ `formal/bit_extract.mlw` proves GET/SET/CLEAR/TOGGLE on 64-bit words change
54
+ exactly the target bit.
55
+
56
+ The proofs are about the datapath expressions; the state machine is checked by
57
+ simulation. Random seeds reproduce within one simulator only (Icarus and
58
+ Verilator implement `$random` differently).
dual license ADDED
@@ -0,0 +1,171 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ SNAPKITTY BIT HARDWARE SOURCE LICENSE
2
+
3
+ Version 1.0
4
+
5
+ Copyright © 2026 SnapKitty Collective. All rights reserved.
6
+
7
+ 1. Definitions
8
+
9
+ “Software” means software distributed with this project.
10
+
11
+ “Hardware” means RTL, HDL, netlists, hardware descriptions, circuit descriptions, formal specifications, verification artifacts, and other hardware-design materials contained in this project.
12
+
13
+ “Core” means the bit-string accelerator implementation and its directly derived hardware implementations.
14
+
15
+ “Licensee” means any person or organization exercising rights granted by this License.
16
+
17
+ “Modified Core” means a modified or derivative version of the Core.
18
+
19
+ 2. Copyright Permission
20
+
21
+ Subject to the terms of this License, SnapKitty Collective grants Licensee a worldwide, non-exclusive, royalty-free license to:
22
+
23
+ - use the Hardware;
24
+ - study the Hardware;
25
+ - reproduce the Hardware;
26
+ - modify the Hardware;
27
+ - create derivative works;
28
+ - compile, synthesize, simulate, and manufacture products incorporating the Hardware;
29
+ - use the Hardware commercially.
30
+
31
+ 3. Commercial Use
32
+
33
+ Commercial use is expressly permitted.
34
+
35
+ Licensee may:
36
+
37
+ - manufacture integrated circuits;
38
+ - manufacture FPGA implementations;
39
+ - manufacture ASIC implementations;
40
+ - sell hardware incorporating the Core;
41
+ - license products incorporating the Core;
42
+ - provide commercial services using the Core;
43
+ - integrate the Core into commercial systems.
44
+
45
+ No additional royalty is owed to SnapKitty Collective solely because the Core is used commercially.
46
+
47
+ 4. Modification and Redistribution
48
+
49
+ Modified versions of the Core may be created.
50
+
51
+ If a Modified Core is distributed publicly, the distributor must:
52
+
53
+ 1. preserve this License;
54
+ 2. retain existing copyright notices;
55
+ 3. identify material modifications;
56
+ 4. provide the corresponding modified Core source;
57
+ 5. provide the same rights granted by this License for the Modified Core.
58
+
59
+ A distributor may not impose additional restrictions that prevent recipients from exercising the rights granted by this License.
60
+
61
+ 5. Proprietary Systems
62
+
63
+ Use of the Core inside a larger system does not require the larger system to be licensed under this License.
64
+
65
+ A proprietary product may contain or interface with the Core.
66
+
67
+ For example:
68
+
69
+ Proprietary Product
70
+ │
71
+ ├── Proprietary Logic
72
+ ├── Proprietary Firmware
73
+ ├── Proprietary Software
74
+ │
75
+ └── SnapKitty Bit Accelerator
76
+ │
77
+ └── licensed under this License
78
+
79
+ Only the Core and Modified Core remain subject to the source-sharing requirements of this License.
80
+
81
+ 6. Generated Hardware
82
+
83
+ Synthesis products generated from the Core, including:
84
+
85
+ - FPGA bitstreams;
86
+ - ASIC netlists;
87
+ - gate-level representations;
88
+ - placed-and-routed designs;
89
+ - manufactured chips;
90
+
91
+ may be commercially distributed.
92
+
93
+ Distribution of a generated hardware artifact does not by itself require distribution of unrelated proprietary portions of the containing system.
94
+
95
+ 7. Attribution
96
+
97
+ Redistributions of the Core must preserve reasonable attribution to:
98
+
99
+ SnapKitty Collective
100
+
101
+ Copyright notices and this License must remain included with source distributions.
102
+
103
+ 8. Patent Grant
104
+
105
+ Each contributor grants Licensee a worldwide, non-exclusive, royalty-free patent license to make, have made, use, sell, offer for sale, import, and otherwise transfer the Core, but only for patent claims necessarily infringed by that contributor's contribution to the Core.
106
+
107
+ If Licensee initiates patent litigation alleging that the Core itself infringes a patent, the patent license granted to that Licensee under this section terminates as of the date the litigation is initiated.
108
+
109
+ 9. No Trademark License
110
+
111
+ This License does not grant permission to use:
112
+
113
+ SnapKitty
114
+ SnapKitty Collective
115
+ SnapKitty West
116
+
117
+ or associated trademarks, logos, or branding except as reasonably necessary to identify the origin of the licensed work.
118
+
119
+ 10. No Warranty
120
+
121
+ THE HARDWARE AND SOFTWARE ARE PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, TITLE, OR NON-INFRINGEMENT.
122
+
123
+ LICENSEE ASSUMES ALL RISK ASSOCIATED WITH THE USE, SYNTHESIS, MANUFACTURE, DEPLOYMENT, AND OPERATION OF THE HARDWARE.
124
+
125
+ 11. Limitation of Liability
126
+
127
+ TO THE MAXIMUM EXTENT PERMITTED BY LAW, THE COPYRIGHT HOLDERS AND CONTRIBUTORS SHALL NOT BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES ARISING FROM USE OF THE HARDWARE OR SOFTWARE.
128
+
129
+ 12. No Certification
130
+
131
+ Use of this Hardware does not imply that SnapKitty Collective certifies:
132
+
133
+ - manufactured chips;
134
+ - FPGA implementations;
135
+ - safety-critical systems;
136
+ - security properties;
137
+ - regulatory compliance;
138
+ - performance characteristics;
139
+ - suitability for any particular application.
140
+
141
+ 13. License Termination
142
+
143
+ The rights granted under this License terminate automatically if Licensee materially violates its terms.
144
+
145
+ Rights are reinstated automatically if the violation is cured within thirty (30) days after discovery or notification of the violation.
146
+
147
+ Termination does not terminate licenses already properly granted to recipients who are not themselves in violation of this License.
148
+
149
+ 14. Entire License
150
+
151
+ This License constitutes the complete license governing the Core unless a separate written agreement expressly supersedes it.
152
+
153
+ Nothing in this License limits rights that Licensee may have independently under applicable copyright, patent, or other law.
154
+
155
+ ---
156
+
157
+ SNAPKITTY BIT HARDWARE SOURCE LICENSE v1.0
158
+
159
+ Commercial use: PERMITTED
160
+
161
+ Modification: PERMITTED
162
+
163
+ Commercial manufacturing: PERMITTED
164
+
165
+ FPGA/ASIC implementation: PERMITTED
166
+
167
+ Commercial sale: PERMITTED
168
+
169
+ Modified Core redistribution: SOURCE + SAME LICENSE REQUIRED
170
+
171
+ Larger proprietary systems: PERMITTED
formal/bit_address.mlw ADDED
@@ -0,0 +1,111 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ (* Address mapping of rtl/bit_accelerator.sv.
2
+
3
+ Part 1 states the mapping over unbounded integers.
4
+ Part 2 states the RTL's 64-bit datapath over bit-vectors and proves it
5
+ implements Part 1 whenever (base << 3) + offset does not overflow. *)
6
+
7
+ module BitAddress
8
+ use int.Int
9
+ use int.EuclideanDivision
10
+
11
+ constant word_bits : int = 64
12
+
13
+ (* base is a byte address, offset a bit offset; result is a bit address. *)
14
+ function effective_bit (base offset : int) : int = base * 8 + offset
15
+ function word_index (b : int) : int = div b word_bits
16
+ function bit_index (b : int) : int = mod b word_bits
17
+ function word_byte_address (b : int) : int = word_index b * 8
18
+
19
+ lemma decomposition :
20
+ forall b : int. b = word_index b * word_bits + bit_index b
21
+
22
+ lemma bit_index_bounds :
23
+ forall b : int. 0 <= bit_index b < word_bits
24
+
25
+ lemma word_byte_address_aligned :
26
+ forall b : int. mod (word_byte_address b) 8 = 0
27
+
28
+ (* (word, bit) identifies a bit address uniquely. *)
29
+ lemma decomposition_injective :
30
+ forall b1 b2 : int.
31
+ word_index b1 = word_index b2 -> bit_index b1 = bit_index b2 -> b1 = b2
32
+
33
+ (* Offsets 0..63 from a word-aligned base stay in that word, in order. *)
34
+ lemma aligned_base_same_word :
35
+ forall base k : int. mod base 8 = 0 -> 0 <= k < word_bits ->
36
+ word_index (effective_bit base k) = div base 8 /\
37
+ bit_index (effective_bit base k) = k
38
+
39
+ (* Adding 64 to the bit address moves to the next word, same bit. *)
40
+ lemma next_word :
41
+ forall b : int.
42
+ word_index (b + word_bits) = word_index b + 1 /\
43
+ bit_index (b + word_bits) = bit_index b
44
+
45
+ (* Offsets 0 and 64 from any base land in adjacent words. *)
46
+ lemma offset_64_next_word :
47
+ forall base : int.
48
+ word_index (effective_bit base 64) = word_index (effective_bit base 0) + 1
49
+ end
50
+
51
+ module RtlDatapath
52
+ use int.Int
53
+ use int.EuclideanDivision
54
+ use bv.BV64
55
+ use BitAddress
56
+
57
+ (* The RTL expressions, verbatim in bit-vector form. *)
58
+ function eff_bit (base offset : t) : t = add (lsl_bv base (3 : t)) offset
59
+ function bit_idx (e : t) : t = bw_and e (63 : t)
60
+ function req_addr (e : t) : t = lsl_bv (lsr_bv e (6 : t)) (3 : t)
61
+
62
+ lemma bit_idx_lt_64 :
63
+ forall e : t. ult (bit_idx e) (64 : t)
64
+
65
+ lemma req_addr_aligned :
66
+ forall e : t. bw_and (req_addr e) (7 : t) = (0 : t)
67
+
68
+ (* The word address and bit index recompose the effective bit address. *)
69
+ lemma rtl_decomposition :
70
+ forall e : t. add (lsl_bv (lsr_bv e (6 : t)) (6 : t)) (bit_idx e) = e
71
+
72
+ (* The shift/mask forms equal division, remainder and multiplication. *)
73
+ lemma bit_idx_is_urem :
74
+ forall e : t. bit_idx e = urem e (64 : t)
75
+
76
+ lemma req_addr_is_udiv_mul :
77
+ forall e : t. req_addr e = mul (udiv e (64 : t)) (8 : t)
78
+
79
+ lemma shl3_is_mul8 :
80
+ forall b : t. lsl_bv b (3 : t) = mul b (8 : t)
81
+
82
+ (* Trusted base: four specialisations of facts in the Why3 standard library
83
+ module bv.BV64 (axioms to_uint_urem and to_uint_udiv at divisor 64, lemmas
84
+ to_uint_mul_bounded at factor 8 and to_uint_add_bounded). The SMT drivers
85
+ map urem/udiv/mul/add to native bit-vector operations and do not pass the
86
+ library's integer axioms on, so these instances are restated here. Each is
87
+ true in SMT-LIB bit-vector semantics. Everything else in this file is
88
+ proved, not assumed. *)
89
+ axiom urem_64 : forall e : t. t'int (urem e (64 : t)) = mod (t'int e) 64
90
+ axiom udiv_64 : forall e : t. t'int (udiv e (64 : t)) = div (t'int e) 64
91
+ axiom mul_8_bounded :
92
+ forall a : t. t'int a * 8 < two_power_size -> t'int (mul a (8 : t)) = t'int a * 8
93
+ axiom add_bounded :
94
+ forall a b : t. t'int a + t'int b < two_power_size ->
95
+ t'int (add a b) = t'int a + t'int b
96
+
97
+ lemma udiv_64_bound : forall e : t. 0 <= div (t'int e) 64 * 8 < two_power_size
98
+
99
+ (* Bridge to the integer specification. *)
100
+ lemma bit_idx_is_mod :
101
+ forall e : t. t'int (bit_idx e) = bit_index (t'int e)
102
+
103
+ lemma req_addr_is_word_byte_address :
104
+ forall e : t. t'int (req_addr e) = word_byte_address (t'int e)
105
+
106
+ (* Without overflow the 64-bit sum equals the integer effective address. *)
107
+ lemma eff_bit_no_overflow :
108
+ forall base offset : t.
109
+ t'int base * 8 + t'int offset < two_power_size ->
110
+ t'int (eff_bit base offset) = effective_bit (t'int base) (t'int offset)
111
+ end
formal/bit_extract.mlw ADDED
@@ -0,0 +1,50 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ (* Single-bit read and read-modify-write semantics of rtl/bit_accelerator.sv,
2
+ stated over 64-bit words. k is the bit index (bit_idx_q), k < 64. *)
3
+
4
+ module BitExtract
5
+ use bv.BV64
6
+
7
+ function one_hot (k : t) : t = lsl_bv one k (* shifted_one *)
8
+ function op_set (w k : t) : t = bw_or w (one_hot k)
9
+ function op_clear (w k : t) : t = bw_and w (bw_not (one_hot k))
10
+ function op_toggle (w k : t) : t = bw_xor w (one_hot k)
11
+
12
+ (* GET/TEST: mem_rdata[k] is the k-th bit of the word. *)
13
+ lemma get_is_bit :
14
+ forall w k : t. ult k (64 : t) ->
15
+ (nth_bv w k <-> bw_and (lsr_bv w k) one = one)
16
+
17
+ lemma one_hot_single_bit :
18
+ forall k j : t. ult k (64 : t) -> ult j (64 : t) ->
19
+ (nth_bv (one_hot k) j <-> j = k)
20
+
21
+ (* SET makes bit k one and leaves every other bit unchanged. *)
22
+ lemma set_target :
23
+ forall w k : t. ult k (64 : t) -> nth_bv (op_set w k) k
24
+ lemma set_frame :
25
+ forall w k j : t. ult k (64 : t) -> ult j (64 : t) -> j <> k ->
26
+ (nth_bv (op_set w k) j <-> nth_bv w j)
27
+
28
+ (* CLEAR makes bit k zero and leaves every other bit unchanged. *)
29
+ lemma clear_target :
30
+ forall w k : t. ult k (64 : t) -> not (nth_bv (op_clear w k) k)
31
+ lemma clear_frame :
32
+ forall w k j : t. ult k (64 : t) -> ult j (64 : t) -> j <> k ->
33
+ (nth_bv (op_clear w k) j <-> nth_bv w j)
34
+
35
+ (* TOGGLE inverts bit k and leaves every other bit unchanged. *)
36
+ lemma toggle_target :
37
+ forall w k : t. ult k (64 : t) ->
38
+ (nth_bv (op_toggle w k) k <-> not (nth_bv w k))
39
+ lemma toggle_frame :
40
+ forall w k j : t. ult k (64 : t) -> ult j (64 : t) -> j <> k ->
41
+ (nth_bv (op_toggle w k) j <-> nth_bv w j)
42
+
43
+ (* Algebraic laws. *)
44
+ lemma set_idempotent :
45
+ forall w k : t. ult k (64 : t) -> op_set (op_set w k) k = op_set w k
46
+ lemma clear_idempotent :
47
+ forall w k : t. ult k (64 : t) -> op_clear (op_clear w k) k = op_clear w k
48
+ lemma toggle_involution :
49
+ forall w k : t. ult k (64 : t) -> op_toggle (op_toggle w k) k = w
50
+ end
formal/lane_map.mlw ADDED
@@ -0,0 +1,176 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ (* Lane mapping of BULK in pcie/rtl/bitacc_engine.sv.
2
+
3
+ The bit store has L lanes; word w lives in lane (w mod L) at local address
4
+ (w div L). BULK pairs dst word D + k with src word S + k for k = 0 .. n-1,
5
+ L elements per step j. Per lane i the RTL computes, once per operation:
6
+
7
+ r i = (i - S) mod L src element offset (RTL: LW'(i) - S[LW-1:0])
8
+ sa i = (S + r i) div L src local base (RTL: sa)
9
+ q m = (m - D) mod L dst element offset (RTL: q_off)
10
+ da m = (D + q m) div L dst local base (RTL: da)
11
+ delta = (D - S) mod L rotation (RTL: r_delta)
12
+
13
+ In step j, lane i reads src local address j + sa i, which holds element
14
+ k = j*L + r i; dst lane m reads and writes local address j + da m, holding
15
+ element j*L + q m, and takes its src word from lane (m - delta) mod L.
16
+
17
+ Proved here, for every L > 0 (the RTL uses L = 2^LW, where LW-bit
18
+ subtraction is subtraction mod L, Part 1):
19
+ - lane i's src read is word S + k of lane i (Part 2);
20
+ - every element k >= 0 is read by exactly one lane, in step k div L (Part 2);
21
+ - the rotation delivers element k to the lane and local address of word
22
+ D + k, i.e. dst lane m and src lane (m - delta) mod L hold the same k
23
+ (Part 3).
24
+ Bounds (k < n, addresses inside the store) are checked by the RTL's kvalid
25
+ and the decode-time range checks, and tested in pcie/tb. *)
26
+
27
+ module LaneMap
28
+ use int.Int
29
+ use int.EuclideanDivision
30
+
31
+ constant l : int
32
+ axiom l_pos : l > 0
33
+
34
+ (* Each lemma is a lemma function whose assertions name the quotient
35
+ witnesses, so that every step is linear arithmetic plus one instance of
36
+ the standard library's Div_mod, Div_unique, Div_mult or Mod_mult. *)
37
+
38
+ (* ---------------------------------------------------------------- Part 1: residues *)
39
+ let lemma mod_add_multiple (a t : int)
40
+ ensures { mod (a + t * l) l = mod a l }
41
+ = assert { a + t * l = l * t + a }
42
+
43
+ (* Linear step of rotation_pairs_elements, kept apart so that the prover
44
+ sees it without the residue lemmas in its context. *)
45
+ let lemma rotation_arith (m d s t e : int)
46
+ requires { d - s = l * t + e }
47
+ ensures { m - e + (- s) = (m - d) + t * l }
48
+ = ()
49
+
50
+ let lemma rotation_mod (m d s t e : int)
51
+ requires { d - s = l * t + e }
52
+ ensures { mod (m - e + (- s)) l = mod (m - d) l }
53
+ = rotation_arith m d s t e;
54
+ mod_add_multiple (m - d) t
55
+
56
+ let lemma div_add_multiple (a t : int)
57
+ ensures { div (a + t * l) l = div a l + t }
58
+ = assert { a + t * l = l * t + a }
59
+
60
+ let lemma mod_small (a : int)
61
+ requires { 0 <= a < l }
62
+ ensures { mod a l = a }
63
+ = assert { div a l = 0 };
64
+ assert { a = l * div a l + mod a l }
65
+
66
+ let lemma mod_sum_left (a b : int)
67
+ ensures { mod (mod a l + b) l = mod (a + b) l }
68
+ = assert { a = l * div a l + mod a l };
69
+ assert { a + b = (mod a l + b) + div a l * l };
70
+ mod_add_multiple (mod a l + b) (div a l)
71
+
72
+ let lemma mod_sum_right (a b : int)
73
+ ensures { mod (a + mod b l) l = mod (a + b) l }
74
+ = mod_sum_left b a;
75
+ assert { mod b l + a = a + mod b l /\ b + a = a + b }
76
+
77
+ (* LW-bit subtraction of residues (the RTL's r, q_off, r_delta) is the
78
+ residue of the difference when L = 2^LW. *)
79
+ let lemma mod_sub_residues (a b : int)
80
+ ensures { mod (mod a l - mod b l) l = mod (a - b) l }
81
+ = assert { a = l * div a l + mod a l };
82
+ assert { b = l * div b l + mod b l };
83
+ assert { a - b = (mod a l - mod b l) + (div a l - div b l) * l };
84
+ mod_add_multiple (mod a l - mod b l) (div a l - div b l)
85
+
86
+ (* ---------------------------------------------------------------- Part 2: src side *)
87
+ function r (s i : int) : int = mod (i - s) l
88
+ function sa (s i : int) : int = div (s + r s i) l
89
+ function k_src (s i j : int) : int = j * l + r s i
90
+
91
+ lemma r_bounds : forall s i : int. 0 <= r s i < l
92
+
93
+ (* Lane i's element of step j lives in lane i ... *)
94
+ let lemma src_lane (s i j : int)
95
+ requires { 0 <= i < l }
96
+ ensures { mod (s + k_src s i j) l = i }
97
+ = assert { i - s = l * div (i - s) l + r s i };
98
+ assert { s + k_src s i j = i + (j - div (i - s) l) * l };
99
+ mod_add_multiple i (j - div (i - s) l);
100
+ mod_small i
101
+
102
+ (* ... at local address j + sa i. *)
103
+ let lemma src_local (s i j : int)
104
+ ensures { div (s + k_src s i j) l = j + sa s i }
105
+ = assert { s + k_src s i j = (s + r s i) + j * l };
106
+ div_add_multiple (s + r s i) j
107
+
108
+ (* Every element k is the element of lane (s + k) mod L in step k div L ... *)
109
+ let lemma src_covers (s k : int)
110
+ ensures { k_src s (mod (s + k) l) (div k l) = k }
111
+ = mod_sum_left (s + k) (- s);
112
+ assert { s + k + (- s) = k };
113
+ assert { k = l * div k l + mod k l }
114
+
115
+ (* ... and of no other lane in that step. *)
116
+ let lemma src_unique (s i1 i2 j : int)
117
+ requires { 0 <= i1 < l /\ 0 <= i2 < l }
118
+ requires { k_src s i1 j = k_src s i2 j }
119
+ ensures { i1 = i2 }
120
+ = src_lane s i1 j;
121
+ src_lane s i2 j
122
+
123
+ (* The element of step j is in [j L, j L + L): different steps hold
124
+ different elements. *)
125
+ let lemma src_step (s i j : int)
126
+ ensures { div (k_src s i j) l = j }
127
+ = assert { j * l <= k_src s i j < j * l + l }
128
+
129
+ let lemma src_steps_disjoint (s i1 i2 j1 j2 : int)
130
+ requires { k_src s i1 j1 = k_src s i2 j2 }
131
+ ensures { j1 = j2 }
132
+ = src_step s i1 j1;
133
+ src_step s i2 j2
134
+
135
+ (* ---------------------------------------------------------------- Part 3: dst side, rotation *)
136
+ (* The dst offsets have the same form as the src offsets, with d for s. *)
137
+ function q (d m : int) : int = r d m
138
+ function da (d m : int) : int = sa d m
139
+ function k_dst (d m j : int) : int = k_src d m j
140
+ function delta (d s : int) : int = mod (d - s) l
141
+ function src_lane_for (d s m : int) : int = mod (m - delta d s) l
142
+
143
+ (* Dst lane m's element of step j is word d + k of lane m, at j + da m. *)
144
+ let lemma dst_lane (d m j : int)
145
+ requires { 0 <= m < l }
146
+ ensures { mod (d + k_dst d m j) l = m }
147
+ = src_lane d m j
148
+
149
+ let lemma dst_local (d m j : int)
150
+ ensures { div (d + k_dst d m j) l = j + da d m }
151
+ = src_local d m j
152
+
153
+ (* The src lane the rotation selects is a lane ... *)
154
+ lemma rotation_in_range :
155
+ forall d s m : int. 0 <= src_lane_for d s m < l
156
+
157
+ (* ... and it holds the same element k as dst lane m, in every step. *)
158
+ let lemma rotation_pairs_elements (d s m j : int)
159
+ ensures { k_src s (src_lane_for d s m) j = k_dst d m j }
160
+ = let t = div (d - s) l in
161
+ let e = delta d s in
162
+ assert { r s (src_lane_for d s m) = mod (mod (m - e) l + (- s)) l };
163
+ mod_sum_left (m - e) (- s);
164
+ assert { r s (src_lane_for d s m) = mod (m - e + (- s)) l };
165
+ assert { d - s = l * t + e };
166
+ rotation_mod m d s t e
167
+
168
+ (* Element k from src lane i goes to dst lane (i + delta) mod L. *)
169
+ let lemma rotation_target (d s i j : int)
170
+ requires { 0 <= i < l }
171
+ ensures { mod (d + k_src s i j) l = mod (i + delta d s) l }
172
+ = assert { i - s = l * div (i - s) l + r s i };
173
+ assert { d + k_src s i j = (i + (d - s)) + (j - div (i - s) l) * l };
174
+ mod_add_multiple (i + (d - s)) (j - div (i - s) l);
175
+ mod_sum_right i (d - s)
176
+ end
fpga/Makefile ADDED
@@ -0,0 +1,115 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # FPGA build for the bit-string accelerator.
2
+ #
3
+ # make sim UART-level testbench on the RTL (Icarus + Verilator)
4
+ # make lint verilator -Wall on both board tops
5
+ # make icebreaker bitstream for iCEBreaker (iCE40UP5K) -> build/icebreaker.bin
6
+ # make ulx3s bitstream for ULX3S (ECP5 25F) -> build/ulx3s.bit
7
+ # make gl-sim testbench on post-synthesis netlists (iCE40, ECP5)
8
+ # make cosim host tool (host/) against the RTL through a pseudo-terminal
9
+ # make prog-icebreaker / prog-ulx3s program a connected board
10
+ # make all lint, sim, cosim, gl-sim and both bitstreams
11
+ #
12
+ # Tools: yosys, nextpnr-ice40, nextpnr-ecp5, icepack (icestorm), ecppack
13
+ # (prjtrellis), iverilog, verilator; iceprog / openFPGALoader to program.
14
+
15
+ YOSYS ?= yosys
16
+ IVERILOG ?= iverilog
17
+ VVP ?= vvp
18
+ VERILATOR ?= verilator
19
+ BUILD ?= build
20
+ SEED ?= 1
21
+ ULX3S_DEVICE ?= 25k # 12k, 25k, 45k or 85k to match the board
22
+ YOSYS_DAT ?= /usr/share/yosys # Yosys data dir with ice40/ and ecp5/ cell models
23
+
24
+ CORE := ../rtl/bit_accelerator.sv rtl/uart_rx.sv rtl/uart_tx.sv rtl/word_memory.sv rtl/fpga_top.sv
25
+ TB := tb/tb_fpga_top.sv
26
+
27
+ .PHONY: all sim sim-icarus sim-verilator lint icebreaker ulx3s gl-sim gl-sim-ice40 gl-sim-ecp5 \
28
+ cosim host prog-icebreaker prog-ulx3s clean
29
+ .DEFAULT_GOAL := all
30
+
31
+ all: lint sim cosim gl-sim icebreaker ulx3s
32
+
33
+ $(BUILD):
34
+ mkdir -p $@
35
+
36
+ # ------------------------------------------------------------------ RTL checks
37
+ sim: sim-icarus sim-verilator
38
+
39
+ sim-icarus: | $(BUILD)
40
+ $(IVERILOG) -g2012 -o $(BUILD)/tb_fpga.vvp $(CORE) $(TB)
41
+ $(VVP) -n $(BUILD)/tb_fpga.vvp
42
+
43
+ sim-verilator: | $(BUILD)
44
+ $(VERILATOR) --binary --timing --timescale 1ns/1ps -Wno-fatal -Wno-lint --top-module tb_fpga_top \
45
+ -Mdir $(BUILD)/verilator $(CORE) $(TB) >/dev/null
46
+ $(BUILD)/verilator/Vtb_fpga_top
47
+
48
+ lint:
49
+ $(VERILATOR) --lint-only -Wall $(CORE) rtl/power_on_reset.sv boards/icebreaker_top.sv --top-module icebreaker_top
50
+ $(VERILATOR) --lint-only -Wall $(CORE) rtl/power_on_reset.sv boards/ulx3s_top.sv --top-module ulx3s_top
51
+
52
+ # ------------------------------------------------------------------ host tool
53
+ host:
54
+ cd host && cargo fmt --check && cargo clippy --all-targets -- -D warnings && cargo test
55
+
56
+ cosim: host
57
+ BUILD=$(BUILD) sim/cosim.sh 2000 1
58
+
59
+ # ------------------------------------------------------------------ iCEBreaker
60
+ icebreaker: $(BUILD)/icebreaker.bin
61
+
62
+ $(BUILD)/icebreaker.json: $(CORE) rtl/power_on_reset.sv boards/icebreaker_top.sv | $(BUILD)
63
+ $(YOSYS) -q -l $(BUILD)/icebreaker_synth.log -p "read_verilog -sv $^; synth_ice40 -top icebreaker_top -json $@"
64
+
65
+ $(BUILD)/icebreaker.asc: $(BUILD)/icebreaker.json boards/icebreaker.pcf
66
+ nextpnr-ice40 --up5k --package sg48 --json $< --pcf boards/icebreaker.pcf --asc $@ \
67
+ --freq 12 --seed $(SEED) -l $(BUILD)/icebreaker_pnr.log -q
68
+
69
+ $(BUILD)/icebreaker.bin: $(BUILD)/icebreaker.asc
70
+ icepack $< $@
71
+ @grep -E "Max frequency|ICESTORM_LC:|ICESTORM_RAM:" $(BUILD)/icebreaker_pnr.log | tail -3
72
+
73
+ prog-icebreaker: $(BUILD)/icebreaker.bin
74
+ iceprog $<
75
+
76
+ # ------------------------------------------------------------------ ULX3S
77
+ ulx3s: $(BUILD)/ulx3s.bit
78
+
79
+ $(BUILD)/ulx3s.json: $(CORE) rtl/power_on_reset.sv boards/ulx3s_top.sv | $(BUILD)
80
+ $(YOSYS) -q -l $(BUILD)/ulx3s_synth.log -p "read_verilog -sv $^; synth_ecp5 -top ulx3s_top -json $@"
81
+
82
+ $(BUILD)/ulx3s.config: $(BUILD)/ulx3s.json boards/ulx3s.lpf
83
+ nextpnr-ecp5 --$(strip $(ULX3S_DEVICE)) --package CABGA381 --json $< --lpf boards/ulx3s.lpf \
84
+ --textcfg $@ --seed $(SEED) -l $(BUILD)/ulx3s_pnr.log -q
85
+
86
+ $(BUILD)/ulx3s.bit: $(BUILD)/ulx3s.config
87
+ ecppack --compress $< $@
88
+ @grep -E "Max frequency|TRELLIS_COMB:|DP16KD:" $(BUILD)/ulx3s_pnr.log | tail -3
89
+
90
+ prog-ulx3s: $(BUILD)/ulx3s.bit
91
+ openFPGALoader --board ulx3s $<
92
+
93
+ # ------------------------------------------------------------------ gate level
94
+ # The netlists are built with CLKS_PER_BIT = 8 so the UART testbench runs fast.
95
+ gl-sim: gl-sim-ice40 gl-sim-ecp5
96
+
97
+ gl-sim-ice40: | $(BUILD)
98
+ $(YOSYS) -q -p "read_verilog -sv $(CORE); chparam -set CLKS_PER_BIT 8 fpga_top; \
99
+ synth_ice40 -top fpga_top; write_verilog -noattr $(BUILD)/fpga_top_ice40_gl.v"
100
+ $(IVERILOG) -g2012 -DGATE_LEVEL -o $(BUILD)/gl_ice40.vvp \
101
+ $(BUILD)/fpga_top_ice40_gl.v $(strip $(YOSYS_DAT))/ice40/cells_sim.v $(TB)
102
+ $(VVP) -n $(BUILD)/gl_ice40.vvp
103
+
104
+ # Yosys ships DP16KD (ECP5 block RAM) only as a black box, so this netlist
105
+ # keeps the memory in LUT RAM (-nobram); everything else is the real mapping.
106
+ gl-sim-ecp5: | $(BUILD)
107
+ $(YOSYS) -q -p "read_verilog -sv $(CORE); chparam -set CLKS_PER_BIT 8 fpga_top; \
108
+ synth_ecp5 -nobram -top fpga_top; write_verilog -noattr $(BUILD)/fpga_top_ecp5_gl.v"
109
+ $(IVERILOG) -g2012 -DGATE_LEVEL -I$(strip $(YOSYS_DAT))/ecp5 -o $(BUILD)/gl_ecp5.vvp \
110
+ $(BUILD)/fpga_top_ecp5_gl.v $(strip $(YOSYS_DAT))/ecp5/cells_sim.v $(TB)
111
+ $(VVP) -n $(BUILD)/gl_ecp5.vvp
112
+
113
+ clean:
114
+ rm -rf $(BUILD)
115
+ cd host && cargo clean
fpga/README.md ADDED
@@ -0,0 +1,99 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # FPGA build
2
+
3
+ Runs `rtl/bit_accelerator.sv` on real FPGA boards. The core's 64-bit buses do
4
+ not fit on package pins, so `rtl/fpga_top.sv` wraps it with:
5
+
6
+ - 256 × 64-bit words of block RAM (byte addresses 0-2047). Any other address
7
+ answers with `mem_fault`, so the error path works on hardware.
8
+ - A UART command interface, 115200 baud 8N1.
9
+
10
+ | Board | FPGA | Clock | Top | Constraints |
11
+ |---|---|---|---|---|
12
+ | iCEBreaker | iCE40UP5K-SG48 | 12 MHz | `boards/icebreaker_top.sv` | `boards/icebreaker.pcf` |
13
+ | ULX3S | ECP5 LFE5U-25F CABGA381 | 25 MHz | `boards/ulx3s_top.sv` | `boards/ulx3s.lpf` |
14
+
15
+ LEDs: iCEBreaker red = last operation reported an error, green = heartbeat.
16
+ ULX3S `led[0]` = error, `led[1]` = busy, `led[7]` = heartbeat. The button resets.
17
+
18
+ ## Build and program
19
+
20
+ Ubuntu 24.04: `sudo apt-get install yosys nextpnr-ice40 nextpnr-ecp5 fpga-icestorm fpga-trellis iverilog verilator`.
21
+
22
+ ```sh
23
+ make icebreaker # build/icebreaker.bin
24
+ make prog-icebreaker # iceprog
25
+ make ulx3s # build/ulx3s.bit (ULX3S_DEVICE=12k|25k|45k|85k to match your board)
26
+ make prog-ulx3s # openFPGALoader --board ulx3s
27
+ ```
28
+
29
+ Then, from the host (`cd host && cargo build --release`):
30
+
31
+ ```sh
32
+ bitacc --port /dev/ttyUSB1 ping # pong
33
+ bitacc --port /dev/ttyUSB1 write 0 0x8000000000000001
34
+ bitacc --port /dev/ttyUSB1 exec get 0 63 # 1
35
+ bitacc --port /dev/ttyUSB1 exec toggle 0 5 # 1
36
+ bitacc --port /dev/ttyUSB1 read 0 # 0x8000000000000021
37
+ bitacc --port /dev/ttyUSB1 exec get 4096 0 # error (outside the RAM)
38
+ bitacc --port /dev/ttyUSB1 selftest 10000 # acceptance test, must report 0 mismatches
39
+ ```
40
+
41
+ The iCEBreaker's UART is the FTDI's second interface (usually `/dev/ttyUSB1`).
42
+ On the ULX3S it is the only FTDI port (usually `/dev/ttyUSB0`).
43
+
44
+ `selftest` writes random data to all 256 words. It then runs random operations
45
+ (including out-of-range addresses and undefined opcodes) and checks every
46
+ status and the final RAM contents against a host model of the RTL.
47
+
48
+ ## Protocol
49
+
50
+ All multi-byte fields are little-endian.
51
+
52
+ | Host → FPGA | FPGA → host | |
53
+ |---|---|---|
54
+ | `'P'` | `'B'` | ping |
55
+ | `'W'` idx[1] data[8] | `'K'` | write word |
56
+ | `'R'` idx[1] | data[8] | read word |
57
+ | `'X'` op[1] base[8] offset[8] | `0xA0 \| error<<1 \| bit` | run one operation |
58
+ | anything else | `'?'` | |
59
+
60
+ ## Results
61
+
62
+ Yosys 0.33, nextpnr 0.6, place-and-route seeds 1-5:
63
+
64
+ | Board | Logic | Block RAM | Fmax (worst of 5 seeds) | Board clock |
65
+ |---|---|---|---|---|
66
+ | iCEBreaker | 1138 / 5280 LC (21%) | 4 / 30 | 39.06 MHz | 12 MHz |
67
+ | ULX3S 25F | 1171 / 24288 LUT4 (4%), 725 FF | 2 / 56 DP16KD | 73.22 MHz | 25 MHz |
68
+
69
+ ## Verification
70
+
71
+ | Check | Command | Result |
72
+ |---|---|---|
73
+ | Lint, both board tops | `make lint` | `verilator -Wall` clean |
74
+ | UART-level testbench on RTL, Icarus + Verilator | `make sim` | 0 failures (7554 checks under Icarus, 7407 under Verilator; their random streams differ) |
75
+ | Same testbench on the iCE40 gate-level netlist (with the `SB_RAM40_4K` model) | `make gl-sim-ice40` | 7554 checks, 0 failures |
76
+ | Same testbench on the ECP5 gate-level netlist | `make gl-sim-ecp5` | 7554 checks, 0 failures |
77
+ | Host tool against the RTL through a pseudo-terminal | `make cosim` | `selftest` 2000 ops, 0 mismatches |
78
+
79
+ The testbench drives the serial line bit by bit. It checks pings, unknown
80
+ commands, all 256 words, directed operations (word crossing, last bit of RAM,
81
+ out-of-range reads, undefined opcodes) and 300 random operations against a
82
+ reference model. It also checks that TX idles high from power-up. Six of seven
83
+ hand-made faults in `fpga_top`/`uart_tx` are detected. The seventh (no
84
+ write-fault response) cannot occur: a write only follows a successful read of
85
+ the same word.
86
+
87
+ Two problems were found and fixed on the way:
88
+ - **TX powered up low.** FPGA flip-flops power up low, so TX started low and a
89
+ host would read a junk byte.
90
+ - **Testbench race.** The testbench released reset on a clock edge, so the
91
+ gate-level netlist saw a partial reset.
92
+
93
+ Limits:
94
+ - **Not run on a physical board.** Pin assignments are taken from each board's
95
+ reference constraints and have not been checked against a board.
96
+ - **ECP5 block RAM is not covered at gate level.** Yosys 0.33 ships `DP16KD`
97
+ only as a black box, so `gl-sim-ecp5` maps the memory to LUT RAM (`-nobram`).
98
+ The `DP16KD` mapping is covered by place-and-route only. The iCE40
99
+ gate-level run does include block RAM.
fpga/boards/icebreaker.pcf ADDED
@@ -0,0 +1,7 @@
 
 
 
 
 
 
 
 
1
+ # iCEBreaker v1.0 (iCE40UP5K-SG48). Pin numbers from the iCEBreaker examples.
2
+ set_io -nowarn CLK 35
3
+ set_io -nowarn BTN_N 10
4
+ set_io -nowarn RX 6
5
+ set_io -nowarn TX 9
6
+ set_io -nowarn LEDR_N 11
7
+ set_io -nowarn LEDG_N 37
fpga/boards/icebreaker_top.sv ADDED
@@ -0,0 +1,22 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // iCEBreaker (Lattice iCE40UP5K-SG48, 12 MHz). UART on the FTDI second channel
2
+ // at 115200 baud. Red LED: last operation reported an error. Green LED: heartbeat.
3
+ module icebreaker_top (
4
+ input logic CLK,
5
+ input logic BTN_N,
6
+ input logic RX,
7
+ output logic TX,
8
+ output logic LEDR_N,
9
+ output logic LEDG_N
10
+ );
11
+ logic reset, led_busy, led_error;
12
+ logic [23:0] beat = '0;
13
+
14
+ power_on_reset u_por (.clk(CLK), .button(!BTN_N), .reset);
15
+
16
+ fpga_top #(.CLKS_PER_BIT(104)) u_top ( // 12 MHz / 115200 = 104.2
17
+ .clk(CLK), .reset, .uart_rx(RX), .uart_tx(TX), .led_busy, .led_error);
18
+
19
+ always_ff @(posedge CLK) beat <= beat + 1'b1;
20
+ assign LEDR_N = !led_error;
21
+ assign LEDG_N = !(beat[23] || led_busy);
22
+ endmodule
fpga/boards/ulx3s.lpf ADDED
@@ -0,0 +1,35 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # ULX3S v3.x. Sites from the ULX3S reference constraint file (ulx3s_v20.lpf).
2
+ BLOCK RESETPATHS;
3
+ BLOCK ASYNCPATHS;
4
+
5
+ LOCATE COMP "clk_25mhz" SITE "G2";
6
+ IOBUF PORT "clk_25mhz" PULLMODE=NONE IO_TYPE=LVCMOS33;
7
+ FREQUENCY PORT "clk_25mhz" 25 MHZ;
8
+
9
+ LOCATE COMP "ftdi_rxd" SITE "L4"; # FPGA transmits to FTDI
10
+ LOCATE COMP "ftdi_txd" SITE "M1"; # FPGA receives from FTDI
11
+ IOBUF PORT "ftdi_rxd" PULLMODE=UP IO_TYPE=LVCMOS33 DRIVE=4;
12
+ IOBUF PORT "ftdi_txd" PULLMODE=UP IO_TYPE=LVCMOS33;
13
+
14
+ LOCATE COMP "btn[0]" SITE "D6"; # BTN_PWRn, active low
15
+ IOBUF PORT "btn[0]" PULLMODE=UP IO_TYPE=LVCMOS33;
16
+
17
+ LOCATE COMP "led[0]" SITE "B2";
18
+ LOCATE COMP "led[1]" SITE "C2";
19
+ LOCATE COMP "led[2]" SITE "C1";
20
+ LOCATE COMP "led[3]" SITE "D2";
21
+ LOCATE COMP "led[4]" SITE "D1";
22
+ LOCATE COMP "led[5]" SITE "E2";
23
+ LOCATE COMP "led[6]" SITE "E1";
24
+ LOCATE COMP "led[7]" SITE "H3";
25
+ IOBUF PORT "led[0]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
26
+ IOBUF PORT "led[1]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
27
+ IOBUF PORT "led[2]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
28
+ IOBUF PORT "led[3]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
29
+ IOBUF PORT "led[4]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
30
+ IOBUF PORT "led[5]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
31
+ IOBUF PORT "led[6]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
32
+ IOBUF PORT "led[7]" PULLMODE=NONE IO_TYPE=LVCMOS33 DRIVE=4;
33
+
34
+ LOCATE COMP "wifi_gpio0" SITE "L2";
35
+ IOBUF PORT "wifi_gpio0" PULLMODE=UP IO_TYPE=LVCMOS33 DRIVE=4;
fpga/boards/ulx3s_top.sv ADDED
@@ -0,0 +1,23 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // ULX3S (Lattice ECP5 LFE5U-25F/45F/85F, 25 MHz). UART through the on-board FTDI
2
+ // at 115200 baud. led[0]: last operation reported an error, led[1]: busy,
3
+ // led[7]: heartbeat. btn[0] (PWR, active low) resets.
4
+ module ulx3s_top (
5
+ input logic clk_25mhz,
6
+ input logic [0:0] btn,
7
+ input logic ftdi_txd, // FTDI -> FPGA
8
+ output logic ftdi_rxd, // FPGA -> FTDI
9
+ output logic [7:0] led,
10
+ output logic wifi_gpio0 // held high so the ESP32 does not take over
11
+ );
12
+ logic reset, led_busy, led_error;
13
+ logic [24:0] beat = '0;
14
+
15
+ power_on_reset u_por (.clk(clk_25mhz), .button(!btn[0]), .reset);
16
+
17
+ fpga_top #(.CLKS_PER_BIT(217)) u_top ( // 25 MHz / 115200 = 217.0
18
+ .clk(clk_25mhz), .reset, .uart_rx(ftdi_txd), .uart_tx(ftdi_rxd), .led_busy, .led_error);
19
+
20
+ always_ff @(posedge clk_25mhz) beat <= beat + 1'b1;
21
+ assign led = {beat[24], 5'd0, led_busy, led_error};
22
+ assign wifi_gpio0 = 1'b1;
23
+ endmodule
fpga/host/Cargo.lock ADDED
@@ -0,0 +1,7 @@
 
 
 
 
 
 
 
 
1
+ # This file is automatically @generated by Cargo.
2
+ # It is not intended for manual editing.
3
+ version = 4
4
+
5
+ [[package]]
6
+ name = "bitacc"
7
+ version = "0.1.0"
fpga/host/Cargo.toml ADDED
@@ -0,0 +1,10 @@
 
 
 
 
 
 
 
 
 
 
 
1
+ [package]
2
+ name = "bitacc"
3
+ version = "0.1.0"
4
+ edition = "2024"
5
+ rust-version = "1.85"
6
+ description = "Host tool for the bit-string accelerator FPGA build (UART protocol)"
7
+ license = "EPL-2.0"
8
+ publish = false
9
+
10
+ [dependencies]
fpga/host/src/main.rs ADDED
@@ -0,0 +1,283 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ //! bitacc: drive the bit-string accelerator FPGA build over its UART.
2
+ //!
3
+ //! bitacc --port /dev/ttyUSB1 ping
4
+ //! bitacc --port /dev/ttyUSB1 write <index> <value>
5
+ //! bitacc --port /dev/ttyUSB1 read <index>
6
+ //! bitacc --port /dev/ttyUSB1 exec <get|test|set|clear|toggle|0..7> <base> <offset>
7
+ //! bitacc --port /dev/ttyUSB1 selftest [operations] [seed]
8
+ //!
9
+ //! Options: --baud N (default 115200), --words N (RAM size: 256 for the FPGA
10
+ //! build, 4 for the Tiny Tapeout chip).
11
+ //! Numbers are decimal or 0x-prefixed hex. The port is configured with `stty`
12
+ //! (115200 8N1 raw, 1 s read timeout); Linux and macOS.
13
+
14
+ mod protocol;
15
+
16
+ use protocol::*;
17
+ use std::fs::{File, OpenOptions};
18
+ use std::io::{Read, Write};
19
+ use std::process::{Command, ExitCode};
20
+
21
+ struct Port {
22
+ file: File,
23
+ }
24
+
25
+ impl Port {
26
+ fn open(path: &str, baud: u32) -> Result<Port, String> {
27
+ let flag = if cfg!(target_os = "macos") {
28
+ "-f"
29
+ } else {
30
+ "-F"
31
+ };
32
+ let status = Command::new("stty")
33
+ .args([
34
+ flag,
35
+ path,
36
+ &baud.to_string(),
37
+ "raw",
38
+ "-echo",
39
+ "cs8",
40
+ "-cstopb",
41
+ "-parenb",
42
+ ])
43
+ .args(["-crtscts", "min", "0", "time", "10"])
44
+ .status()
45
+ .map_err(|e| format!("running stty: {e}"))?;
46
+ if !status.success() {
47
+ return Err(format!("stty could not configure {path}"));
48
+ }
49
+ let file = OpenOptions::new()
50
+ .read(true)
51
+ .write(true)
52
+ .open(path)
53
+ .map_err(|e| format!("opening {path}: {e}"))?;
54
+ let mut port = Port { file };
55
+ port.drain();
56
+ Ok(port)
57
+ }
58
+
59
+ /// Discard bytes left over from a previous session.
60
+ fn drain(&mut self) {
61
+ let mut buf = [0u8; 256];
62
+ while matches!(self.file.read(&mut buf), Ok(n) if n > 0) {}
63
+ }
64
+
65
+ fn send(&mut self, bytes: &[u8]) -> Result<(), String> {
66
+ self.file
67
+ .write_all(bytes)
68
+ .map_err(|e| format!("write: {e}"))
69
+ }
70
+
71
+ fn recv(&mut self, n: usize) -> Result<Vec<u8>, String> {
72
+ let mut out = vec![0u8; n];
73
+ let mut got = 0;
74
+ while got < n {
75
+ match self.file.read(&mut out[got..]) {
76
+ Ok(0) => return Err(format!("timeout: got {got} of {n} reply bytes")),
77
+ Ok(k) => got += k,
78
+ Err(e) => return Err(format!("read: {e}")),
79
+ }
80
+ }
81
+ Ok(out)
82
+ }
83
+
84
+ fn ping(&mut self) -> Result<(), String> {
85
+ self.send(&[PING])?;
86
+ match self.recv(1)?[0] {
87
+ PONG => Ok(()),
88
+ b => Err(unexpected("ping", b)),
89
+ }
90
+ }
91
+
92
+ fn write_word(&mut self, index: u8, value: u64) -> Result<(), String> {
93
+ self.send(&write_frame(index, value))?;
94
+ match self.recv(1)?[0] {
95
+ WRITE_ACK => Ok(()),
96
+ b => Err(unexpected("write", b)),
97
+ }
98
+ }
99
+
100
+ fn read_word(&mut self, index: u8) -> Result<u64, String> {
101
+ self.send(&read_frame(index))?;
102
+ let b = self.recv(8)?;
103
+ Ok(u64::from_le_bytes(b.try_into().expect("8 bytes")))
104
+ }
105
+
106
+ fn exec(&mut self, opcode: u8, base: u64, offset: u64) -> Result<Status, String> {
107
+ self.send(&exec_frame(opcode, base, offset))?;
108
+ parse_status(self.recv(1)?[0])
109
+ }
110
+ }
111
+
112
+ fn num(s: &str) -> Result<u64, String> {
113
+ let r = match s.strip_prefix("0x").or_else(|| s.strip_prefix("0X")) {
114
+ Some(h) => u64::from_str_radix(&h.replace('_', ""), 16),
115
+ None => s.replace('_', "").parse(),
116
+ };
117
+ r.map_err(|_| format!("not a number: {s}"))
118
+ }
119
+
120
+ fn opcode(s: &str) -> Result<u8, String> {
121
+ if let Some(op) = Op::parse(s) {
122
+ return Ok(op as u8);
123
+ }
124
+ match num(s)? {
125
+ n @ 0..=7 => Ok(n as u8),
126
+ _ => Err(format!(
127
+ "opcode must be get/test/set/clear/toggle or 0..7: {s}"
128
+ )),
129
+ }
130
+ }
131
+
132
+ fn index(s: &str, words: usize) -> Result<u8, String> {
133
+ let n = num(s)?;
134
+ u8::try_from(n)
135
+ .ok()
136
+ .filter(|&i| (i as usize) < words)
137
+ .ok_or_else(|| format!("index must be 0..{}: {s}", words - 1))
138
+ }
139
+
140
+ struct Rng(u64);
141
+ impl Rng {
142
+ fn next(&mut self) -> u64 {
143
+ self.0 ^= self.0 << 13;
144
+ self.0 ^= self.0 >> 7;
145
+ self.0 ^= self.0 << 17;
146
+ self.0
147
+ }
148
+ }
149
+
150
+ /// Fill the RAM, run random operations, and compare every status and the final
151
+ /// RAM contents against the host model. This is the on-hardware acceptance test.
152
+ fn selftest(port: &mut Port, words: usize, ops: u64, seed: u64) -> Result<(), String> {
153
+ let mut rng = Rng(seed.max(1));
154
+ let mut ram = vec![0u64; words];
155
+ port.ping()?;
156
+ for (i, w) in ram.iter_mut().enumerate() {
157
+ *w = rng.next();
158
+ port.write_word(i as u8, *w)?;
159
+ }
160
+ let mut mismatches = 0u64;
161
+ for n in 0..ops {
162
+ let r = rng.next();
163
+ let mut op = (r % 8) as u8;
164
+ if op > 4 && r % 3 != 0 {
165
+ op -= 4; // mostly defined opcodes
166
+ }
167
+ let (base, offset) = if r % 10 == 0 {
168
+ (rng.next(), rng.next()) // mostly out of range: exercises faults
169
+ } else {
170
+ (
171
+ rng.next() % (words as u64 * 8),
172
+ rng.next() % (words as u64 * 64),
173
+ )
174
+ };
175
+ let want = model_exec(&mut ram, op, base, offset);
176
+ let got = port.exec(op, base, offset)?;
177
+ if got.error != want.error || (!want.error && got.bit != want.bit) {
178
+ mismatches += 1;
179
+ eprintln!(
180
+ "op {n}: exec {op} base {base:#x} offset {offset:#x}: got {got:?}, expected {want:?}"
181
+ );
182
+ }
183
+ }
184
+ for (i, &w) in ram.iter().enumerate() {
185
+ let got = port.read_word(i as u8)?;
186
+ if got != w {
187
+ mismatches += 1;
188
+ eprintln!("word {i}: got {got:#018x}, expected {w:#018x}");
189
+ }
190
+ }
191
+ println!("selftest: {ops} operations, {words} words checked, {mismatches} mismatches");
192
+ if mismatches == 0 {
193
+ Ok(())
194
+ } else {
195
+ Err("selftest FAILED".into())
196
+ }
197
+ }
198
+
199
+ fn run(args: &[String]) -> Result<(), String> {
200
+ let mut port_path = None;
201
+ let mut baud = 115_200u32;
202
+ let mut words = WORDS;
203
+ let mut rest = Vec::new();
204
+ let mut it = args.iter();
205
+ while let Some(a) = it.next() {
206
+ match a.as_str() {
207
+ "--port" => port_path = it.next().cloned(),
208
+ "--baud" => baud = num(it.next().ok_or("--baud needs a value")?)? as u32,
209
+ "--words" => {
210
+ words = num(it.next().ok_or("--words needs a value")?)? as usize;
211
+ if !(1..=256).contains(&words) {
212
+ return Err("--words must be 1..256".into());
213
+ }
214
+ }
215
+ "-h" | "--help" => {
216
+ println!(
217
+ "{}",
218
+ include_str!("main.rs")
219
+ .lines()
220
+ .take(13)
221
+ .map(|l| l.trim_start_matches("//!"))
222
+ .collect::<Vec<_>>()
223
+ .join("\n")
224
+ );
225
+ return Ok(());
226
+ }
227
+ _ => rest.push(a.as_str()),
228
+ }
229
+ }
230
+ let path = port_path.ok_or("missing --port <serial device>")?;
231
+ let mut port = Port::open(&path, baud)?;
232
+ match rest.as_slice() {
233
+ ["ping"] => {
234
+ port.ping()?;
235
+ println!("pong");
236
+ }
237
+ ["write", i, v] => port.write_word(index(i, words)?, num(v)?)?,
238
+ ["read", i] => println!("{:#018x}", port.read_word(index(i, words)?)?),
239
+ ["exec", op, base, offset] => {
240
+ let s = port.exec(opcode(op)?, num(base)?, num(offset)?)?;
241
+ if s.error {
242
+ println!("error");
243
+ } else {
244
+ println!("{}", s.bit as u8);
245
+ }
246
+ }
247
+ ["selftest"] => selftest(&mut port, words, 1000, 1)?,
248
+ ["selftest", n] => selftest(&mut port, words, num(n)?, 1)?,
249
+ ["selftest", n, seed] => selftest(&mut port, words, num(n)?, num(seed)?)?,
250
+ _ => return Err("unknown command; see --help".into()),
251
+ }
252
+ Ok(())
253
+ }
254
+
255
+ fn main() -> ExitCode {
256
+ let args: Vec<String> = std::env::args().skip(1).collect();
257
+ match run(&args) {
258
+ Ok(()) => ExitCode::SUCCESS,
259
+ Err(e) => {
260
+ eprintln!("bitacc: {e}");
261
+ ExitCode::FAILURE
262
+ }
263
+ }
264
+ }
265
+
266
+ #[cfg(test)]
267
+ mod tests {
268
+ use super::*;
269
+
270
+ #[test]
271
+ fn parses_numbers_and_opcodes() {
272
+ assert_eq!(num("0x10").unwrap(), 16);
273
+ assert_eq!(num("1_000").unwrap(), 1000);
274
+ assert!(num("zz").is_err());
275
+ assert_eq!(opcode("set").unwrap(), 2);
276
+ assert_eq!(opcode("7").unwrap(), 7);
277
+ assert!(opcode("8").is_err());
278
+ assert_eq!(index("255", 256).unwrap(), 255);
279
+ assert!(index("256", 256).is_err());
280
+ assert_eq!(index("3", 4).unwrap(), 3);
281
+ assert!(index("4", 4).is_err());
282
+ }
283
+ }
fpga/host/src/protocol.rs ADDED
@@ -0,0 +1,204 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ //! Byte-level protocol of `fpga/rtl/fpga_top.sv`. Multi-byte fields are little-endian.
2
+
3
+ /// Opcodes accepted by the accelerator.
4
+ #[derive(Clone, Copy, Debug, PartialEq, Eq)]
5
+ pub enum Op {
6
+ Get = 0,
7
+ Test = 1,
8
+ Set = 2,
9
+ Clear = 3,
10
+ Toggle = 4,
11
+ }
12
+
13
+ impl Op {
14
+ pub fn parse(s: &str) -> Option<Op> {
15
+ match s.to_ascii_lowercase().as_str() {
16
+ "get" => Some(Op::Get),
17
+ "test" => Some(Op::Test),
18
+ "set" => Some(Op::Set),
19
+ "clear" => Some(Op::Clear),
20
+ "toggle" => Some(Op::Toggle),
21
+ _ => None,
22
+ }
23
+ }
24
+ }
25
+
26
+ pub const PING: u8 = b'P';
27
+ pub const PONG: u8 = b'B';
28
+ pub const WRITE: u8 = b'W';
29
+ pub const WRITE_ACK: u8 = b'K';
30
+ pub const READ: u8 = b'R';
31
+ pub const EXEC: u8 = b'X';
32
+ pub const UNKNOWN: u8 = b'?';
33
+ pub const STATUS_TAG: u8 = 0xA0;
34
+ pub const STATUS_TAG_MASK: u8 = 0xFC;
35
+
36
+ /// Number of 64-bit words in the FPGA build's RAM; byte addresses 0..WORDS*8 are in
37
+ /// range. The Tiny Tapeout chip has 4 (`--words 4`).
38
+ pub const WORDS: usize = 256;
39
+
40
+ pub fn write_frame(index: u8, value: u64) -> Vec<u8> {
41
+ let mut f = vec![WRITE, index];
42
+ f.extend_from_slice(&value.to_le_bytes());
43
+ f
44
+ }
45
+
46
+ pub fn read_frame(index: u8) -> Vec<u8> {
47
+ vec![READ, index]
48
+ }
49
+
50
+ /// `opcode` is sent as given (3 bits), so undefined opcodes 5..=7 can be exercised.
51
+ pub fn exec_frame(opcode: u8, base: u64, offset: u64) -> Vec<u8> {
52
+ let mut f = vec![EXEC, opcode & 0x07];
53
+ f.extend_from_slice(&base.to_le_bytes());
54
+ f.extend_from_slice(&offset.to_le_bytes());
55
+ f
56
+ }
57
+
58
+ /// Result of one accelerator operation.
59
+ #[derive(Clone, Copy, Debug, PartialEq, Eq)]
60
+ pub struct Status {
61
+ pub error: bool,
62
+ /// Meaningful only when `error` is false.
63
+ pub bit: bool,
64
+ }
65
+
66
+ /// Describe a reply byte that was not the one expected.
67
+ pub fn unexpected(what: &str, byte: u8) -> String {
68
+ if byte == UNKNOWN {
69
+ format!("{what}: the FPGA did not recognize the command (reply '?')")
70
+ } else {
71
+ format!("{what}: unexpected reply 0x{byte:02x}")
72
+ }
73
+ }
74
+
75
+ pub fn parse_status(byte: u8) -> Result<Status, String> {
76
+ if byte & STATUS_TAG_MASK != STATUS_TAG {
77
+ return Err(format!("unexpected status byte 0x{byte:02x}"));
78
+ }
79
+ Ok(Status {
80
+ error: byte & 0x02 != 0,
81
+ bit: byte & 0x01 != 0,
82
+ })
83
+ }
84
+
85
+ /// Host-side reference model of one operation on a RAM image, matching the RTL:
86
+ /// effective bit = (base << 3) + offset (mod 2^64), byte address = (bit >> 6) << 3,
87
+ /// out-of-range addresses and undefined opcodes report an error and do not write.
88
+ pub fn model_exec(ram: &mut [u64], opcode: u8, base: u64, offset: u64) -> Status {
89
+ let eff = (base << 3).wrapping_add(offset);
90
+ let word = eff >> 6;
91
+ let bit = (eff & 63) as u32;
92
+ if word >= ram.len() as u64 || opcode > 4 {
93
+ return Status {
94
+ error: true,
95
+ bit: false,
96
+ };
97
+ }
98
+ let w = &mut ram[word as usize];
99
+ let old = (*w >> bit) & 1 == 1;
100
+ let mask = 1u64 << bit;
101
+ let new_bit = match opcode {
102
+ 2 => {
103
+ *w |= mask;
104
+ true
105
+ }
106
+ 3 => {
107
+ *w &= !mask;
108
+ false
109
+ }
110
+ 4 => {
111
+ *w ^= mask;
112
+ !old
113
+ }
114
+ _ => old,
115
+ };
116
+ Status {
117
+ error: false,
118
+ bit: new_bit,
119
+ }
120
+ }
121
+
122
+ #[cfg(test)]
123
+ mod tests {
124
+ use super::*;
125
+
126
+ #[test]
127
+ fn frames_are_little_endian() {
128
+ assert_eq!(
129
+ write_frame(3, 0x0102_0304_0506_0708),
130
+ vec![b'W', 3, 8, 7, 6, 5, 4, 3, 2, 1]
131
+ );
132
+ assert_eq!(read_frame(255), vec![b'R', 255]);
133
+ let x = exec_frame(Op::Toggle as u8, 0x11, 0x2233);
134
+ assert_eq!(x.len(), 18);
135
+ assert_eq!(&x[..2], &[b'X', 4]);
136
+ assert_eq!(&x[2..10], &0x11u64.to_le_bytes());
137
+ assert_eq!(&x[10..], &0x2233u64.to_le_bytes());
138
+ }
139
+
140
+ #[test]
141
+ fn status_byte() {
142
+ assert_eq!(
143
+ parse_status(0xA0),
144
+ Ok(Status {
145
+ error: false,
146
+ bit: false
147
+ })
148
+ );
149
+ assert_eq!(
150
+ parse_status(0xA1),
151
+ Ok(Status {
152
+ error: false,
153
+ bit: true
154
+ })
155
+ );
156
+ assert!(parse_status(0xA2).unwrap().error);
157
+ assert!(parse_status(b'K').is_err());
158
+ assert!(parse_status(0xB1).is_err());
159
+ }
160
+
161
+ #[test]
162
+ fn model_matches_rtl_rules() {
163
+ let mut ram = [0u64; WORDS];
164
+ ram[0] = 0x8000_0000_0000_0001;
165
+ assert_eq!(
166
+ model_exec(&mut ram, 0, 0, 63),
167
+ Status {
168
+ error: false,
169
+ bit: true
170
+ }
171
+ );
172
+ assert_eq!(
173
+ model_exec(&mut ram, 2, 8, 6),
174
+ Status {
175
+ error: false,
176
+ bit: true
177
+ }
178
+ );
179
+ assert_eq!(ram[1], 0x40);
180
+ // (7 << 3) + 9 = bit 65 = word 1, bit 1: was 0, toggles to 1.
181
+ assert_eq!(
182
+ model_exec(&mut ram, 4, 7, 9),
183
+ Status {
184
+ error: false,
185
+ bit: true
186
+ }
187
+ );
188
+ assert_eq!(ram[1], 0x42);
189
+ assert!(model_exec(&mut ram, 0, 2048, 0).error); // byte 2048 is past the RAM
190
+ assert!(model_exec(&mut ram, 5, 0, 0).error); // undefined opcode
191
+ assert!(model_exec(&mut ram, 0, u64::MAX, 0).error);
192
+
193
+ let mut small = [0u64; 4]; // Tiny Tapeout RAM: bytes 0..31
194
+ assert!(!model_exec(&mut small, 2, 31, 7).error);
195
+ assert_eq!(small[3], 1 << 63);
196
+ assert!(model_exec(&mut small, 0, 32, 0).error);
197
+ }
198
+
199
+ #[test]
200
+ fn op_names() {
201
+ assert_eq!(Op::parse("TOGGLE"), Some(Op::Toggle));
202
+ assert_eq!(Op::parse("nope"), None);
203
+ }
204
+ }
fpga/rtl/fpga_top.sv ADDED
@@ -0,0 +1,162 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Board-independent hardware top: bit_accelerator + 256 x 64-bit block RAM,
2
+ // controlled over a UART (8N1). All multi-byte fields are little-endian.
3
+ //
4
+ // host -> FPGA FPGA -> host
5
+ // 'P' 'B' ping
6
+ // 'W' idx[1] data[8] 'K' write word idx
7
+ // 'R' idx[1] data[8] read word idx
8
+ // 'X' op[1] base[8] offset[8] 0xA0 | error<<1 | bit run one operation
9
+ // anything else '?'
10
+ //
11
+ // The accelerator sees the RAM at byte addresses 0 .. DEPTH*8-1. Any other
12
+ // address answers with mem_fault, so the error path works on hardware.
13
+ module fpga_top #(
14
+ parameter int CLKS_PER_BIT = 104, // clock Hz / baud
15
+ parameter int DEPTH = 256 // words; power of two
16
+ )(
17
+ input logic clk,
18
+ input logic reset, // synchronous, active high
19
+ input logic uart_rx,
20
+ output logic uart_tx,
21
+ output logic led_busy, // operation in progress
22
+ output logic led_error // last operation reported error
23
+ );
24
+ localparam int AW = $clog2(DEPTH);
25
+
26
+ // ------------------------------------------------------------- UART
27
+ logic rx_valid;
28
+ logic [7:0] rx_data;
29
+ logic tx_start, tx_ready;
30
+ logic [7:0] tx_data;
31
+
32
+ localparam logic [9:0] CPB = 10'(CLKS_PER_BIT);
33
+ uart_rx u_rx (
34
+ .clk, .reset, .cpb(CPB), .rx(uart_rx), .valid(rx_valid), .data(rx_data));
35
+ uart_tx u_tx (
36
+ .clk, .reset, .cpb(CPB), .start(tx_start), .data(tx_data), .ready(tx_ready), .tx(uart_tx));
37
+
38
+ // ------------------------------------------------------------- accelerator
39
+ logic op_valid, op_ready;
40
+ logic [63:0] base_q, offset_q;
41
+ logic [2:0] opcode_q;
42
+ logic result_valid, result_bit, acc_error;
43
+ logic mem_valid, mem_write, mem_ready, mem_rvalid, mem_fault;
44
+ logic [63:0] mem_addr, mem_wdata, mem_rdata;
45
+ logic [7:0] mem_wstrb;
46
+
47
+ bit_accelerator u_acc (
48
+ .clk, .reset,
49
+ .op_valid, .op_ready,
50
+ .base_address(base_q), .bit_offset(offset_q), .operation(opcode_q),
51
+ .result_valid, .result_bit, .error(acc_error),
52
+ .mem_valid, .mem_write, .mem_addr, .mem_wdata, .mem_wstrb,
53
+ .mem_ready, .mem_rvalid, .mem_rdata, .mem_fault);
54
+
55
+ // ------------------------------------------------------------- memory
56
+ logic ram_we;
57
+ logic [AW-1:0] ram_addr;
58
+ logic [63:0] ram_wdata, ram_rdata;
59
+
60
+ word_memory #(.DEPTH(DEPTH)) u_ram (
61
+ .clk, .we(ram_we), .addr(ram_addr), .wdata(ram_wdata), .rdata(ram_rdata));
62
+
63
+ typedef enum logic [3:0] {
64
+ S_CMD, S_ARGS, S_HOST_WRITE, S_HOST_READ, S_HOST_READ_DATA,
65
+ S_LOAD, S_START, S_EXEC, S_SEND
66
+ } state_t;
67
+ state_t state;
68
+
69
+ logic [7:0] cmd;
70
+ logic [4:0] nargs, argi; // argument bytes expected / received
71
+ logic [7:0] args [0:16];
72
+ logic [7:0] reply [0:7];
73
+ logic [3:0] nreply, replyi;
74
+ logic in_range;
75
+
76
+ logic unused_ok;
77
+ assign unused_ok = &{1'b0, mem_wstrb, mem_addr[2:0]}; // whole-word access, strobes all ones
78
+
79
+ // The accelerator owns the RAM port only in S_EXEC; the host commands use it otherwise.
80
+ assign in_range = (mem_addr[63:AW+3] == '0);
81
+ assign mem_ready = (state == S_EXEC);
82
+ assign mem_rdata = ram_rdata;
83
+ assign ram_we = (state == S_EXEC) ? (mem_valid && mem_write && in_range)
84
+ : (state == S_HOST_WRITE);
85
+ assign ram_addr = (state == S_EXEC) ? mem_addr[AW+2:3] : args[0][AW-1:0];
86
+ assign ram_wdata = (state == S_EXEC) ? mem_wdata
87
+ : {args[8], args[7], args[6], args[5],
88
+ args[4], args[3], args[2], args[1]};
89
+ assign op_valid = (state == S_START);
90
+ assign tx_data = reply[replyi[2:0]];
91
+ assign tx_start = (state == S_SEND) && tx_ready && (replyi < nreply);
92
+ assign led_busy = (state == S_START) || (state == S_EXEC);
93
+
94
+ always_ff @(posedge clk) begin
95
+ if (reset) begin
96
+ state <= S_CMD; cmd <= '0; nargs <= '0; argi <= '0;
97
+ nreply <= '0; replyi <= '0; led_error <= 1'b0;
98
+ base_q <= '0; offset_q <= '0; opcode_q <= '0;
99
+ mem_rvalid <= 1'b0; mem_fault <= 1'b0;
100
+ end else begin
101
+ mem_rvalid <= 1'b0;
102
+ mem_fault <= 1'b0;
103
+ case (state)
104
+ S_CMD: if (rx_valid) begin
105
+ cmd <= rx_data; argi <= '0; replyi <= '0;
106
+ case (rx_data)
107
+ 8'h50: begin reply[0] <= 8'h42; nreply <= 4'd1; state <= S_SEND; end // 'P'
108
+ 8'h57: begin nargs <= 5'd9; state <= S_ARGS; end // 'W'
109
+ 8'h52: begin nargs <= 5'd1; state <= S_ARGS; end // 'R'
110
+ 8'h58: begin nargs <= 5'd17; state <= S_ARGS; end // 'X'
111
+ default: begin reply[0] <= 8'h3F; nreply <= 4'd1; state <= S_SEND; end
112
+ endcase
113
+ end
114
+ S_ARGS: if (rx_valid) begin
115
+ args[argi] <= rx_data;
116
+ argi <= argi + 1'b1;
117
+ if (argi + 1'b1 == nargs) begin
118
+ case (cmd)
119
+ 8'h57: state <= S_HOST_WRITE;
120
+ 8'h52: state <= S_HOST_READ;
121
+ default: state <= S_LOAD;
122
+ endcase
123
+ end
124
+ end
125
+ S_HOST_WRITE: begin // ram_we is high this cycle
126
+ reply[0] <= 8'h4B; nreply <= 4'd1; state <= S_SEND;
127
+ end
128
+ S_HOST_READ: state <= S_HOST_READ_DATA; // address presented this cycle
129
+ S_HOST_READ_DATA: begin
130
+ for (int i = 0; i < 8; i++) reply[i] <= ram_rdata[8*i +: 8];
131
+ nreply <= 4'd8; state <= S_SEND;
132
+ end
133
+ S_LOAD: begin // operands are stable before op_valid
134
+ opcode_q <= args[0][2:0];
135
+ base_q <= {args[8], args[7], args[6], args[5], args[4], args[3], args[2], args[1]};
136
+ offset_q <= {args[16], args[15], args[14], args[13], args[12], args[11], args[10], args[9]};
137
+ state <= S_START;
138
+ end
139
+ S_START: if (op_ready) state <= S_EXEC; // op_valid is high in S_START
140
+ S_EXEC: begin
141
+ // Memory slave: always ready, one-cycle read latency, fault out of range.
142
+ if (mem_valid && !mem_write) begin
143
+ if (in_range) mem_rvalid <= 1'b1; else mem_fault <= 1'b1;
144
+ end
145
+ // Unreachable here (a write always follows a successful read of the same
146
+ // word) but kept so the slave honours the interface contract.
147
+ if (mem_valid && mem_write && !in_range) mem_fault <= 1'b1;
148
+ if (result_valid) begin
149
+ reply[0] <= 8'hA0 | {6'd0, acc_error, result_bit};
150
+ led_error <= acc_error;
151
+ nreply <= 4'd1; state <= S_SEND;
152
+ end
153
+ end
154
+ S_SEND: begin
155
+ if (tx_start) replyi <= replyi + 1'b1;
156
+ else if (replyi == nreply && tx_ready) state <= S_CMD;
157
+ end
158
+ default: state <= S_CMD;
159
+ endcase
160
+ end
161
+ end
162
+ endmodule
fpga/rtl/power_on_reset.sv ADDED
@@ -0,0 +1,19 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Synchronous reset: held for 2^CW cycles after configuration and while the
2
+ // (already active-high) button input is pressed. The button is synchronized.
3
+ module power_on_reset #(
4
+ parameter int CW = 8
5
+ )(
6
+ input logic clk,
7
+ input logic button,
8
+ output logic reset
9
+ );
10
+ logic [CW-1:0] count = '0;
11
+ logic b_m = 1'b0, b_s = 1'b0;
12
+ always_ff @(posedge clk) begin
13
+ b_m <= button;
14
+ b_s <= b_m;
15
+ if (b_s) count <= '0;
16
+ else if (!(&count)) count <= count + 1'b1;
17
+ end
18
+ assign reset = !(&count);
19
+ endmodule
fpga/rtl/uart_rx.sv ADDED
@@ -0,0 +1,49 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // 8N1 UART receiver. cpb = clocks per bit = clock frequency / baud rate (>= 4).
2
+ // valid pulses for one cycle with the received byte in data.
3
+ module uart_rx #(
4
+ parameter int CW = 10 // width of cpb
5
+ )(
6
+ input logic clk,
7
+ input logic reset,
8
+ input logic [CW-1:0] cpb,
9
+ input logic rx,
10
+ output logic valid,
11
+ output logic [7:0] data
12
+ );
13
+ logic [CW-1:0] FULL, HALF;
14
+ assign FULL = cpb - 1'b1;
15
+ assign HALF = cpb >> 1;
16
+
17
+ logic rx_m, rx_s; // two-flop synchronizer
18
+ logic [1:0] state; // 0 idle, 1 start, 2 data, 3 stop
19
+ logic [CW-1:0] cnt;
20
+ logic [2:0] bitn;
21
+
22
+ always_ff @(posedge clk) begin
23
+ rx_m <= rx;
24
+ rx_s <= rx_m;
25
+ valid <= 1'b0;
26
+ if (reset) begin
27
+ state <= 2'd0; cnt <= '0; bitn <= '0; data <= '0;
28
+ rx_m <= 1'b1; rx_s <= 1'b1;
29
+ end else begin
30
+ case (state)
31
+ 2'd0: if (!rx_s) begin state <= 2'd1; cnt <= HALF; end
32
+ 2'd1: if (cnt == 0) begin
33
+ if (!rx_s) begin state <= 2'd2; cnt <= FULL; bitn <= '0; end
34
+ else state <= 2'd0; // glitch, not a start bit
35
+ end else cnt <= cnt - 1'b1;
36
+ 2'd2: if (cnt == 0) begin
37
+ data <= {rx_s, data[7:1]};
38
+ cnt <= FULL;
39
+ if (bitn == 3'd7) state <= 2'd3;
40
+ bitn <= bitn + 1'b1;
41
+ end else cnt <= cnt - 1'b1;
42
+ default: if (cnt == 0) begin
43
+ state <= 2'd0;
44
+ valid <= rx_s; // drop bytes with a bad stop bit
45
+ end else cnt <= cnt - 1'b1;
46
+ endcase
47
+ end
48
+ end
49
+ endmodule
fpga/rtl/uart_tx.sv ADDED
@@ -0,0 +1,48 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // 8N1 UART transmitter. Load with start when ready is high.
2
+ module uart_tx #(
3
+ parameter int CW = 10 // width of cpb
4
+ )(
5
+ input logic clk,
6
+ input logic reset,
7
+ input logic [CW-1:0] cpb, // clocks per bit (>= 4)
8
+ input logic start,
9
+ input logic [7:0] data,
10
+ output logic ready,
11
+ output logic tx
12
+ );
13
+ logic [CW-1:0] FULL;
14
+ assign FULL = cpb - 1'b1;
15
+
16
+ // LSB first: start, data[7:0], stop, then one guard bit so ready rises only
17
+ // after the stop bit has lasted a full bit time.
18
+ logic [10:0] shreg;
19
+ logic [3:0] left; // bit times still to send
20
+ logic [CW-1:0] cnt;
21
+ // The line is stored inverted: FPGA flip-flops power up low, so tx is idle
22
+ // high from configuration, before the first reset edge (a low line would be a
23
+ // start bit, i.e. a junk byte, to the host). No initial value is needed.
24
+ logic tx_n;
25
+ assign tx = !tx_n;
26
+
27
+ assign ready = (left == 0);
28
+
29
+ always_ff @(posedge clk) begin
30
+ if (reset) begin
31
+ tx_n <= 1'b0; left <= '0; cnt <= '0; shreg <= '1;
32
+ end else if (left == 0) begin
33
+ tx_n <= 1'b0;
34
+ if (start) begin
35
+ shreg <= {2'b11, data, 1'b0};
36
+ left <= 4'd11;
37
+ cnt <= '0;
38
+ end
39
+ end else if (cnt == 0) begin
40
+ tx_n <= !shreg[0];
41
+ shreg <= {1'b1, shreg[10:1]};
42
+ left <= left - 1'b1;
43
+ cnt <= FULL;
44
+ end else begin
45
+ cnt <= cnt - 1'b1;
46
+ end
47
+ end
48
+ endmodule
fpga/rtl/word_memory.sv ADDED
@@ -0,0 +1,16 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ // Single-port 64-bit word memory with synchronous read (maps to block RAM).
2
+ module word_memory #(
3
+ parameter int DEPTH = 256
4
+ )(
5
+ input logic clk,
6
+ input logic we,
7
+ input logic [$clog2(DEPTH)-1:0] addr,
8
+ input logic [63:0] wdata,
9
+ output logic [63:0] rdata
10
+ );
11
+ logic [63:0] mem [0:DEPTH-1];
12
+ always_ff @(posedge clk) begin
13
+ if (we) mem[addr] <= wdata;
14
+ rdata <= mem[addr];
15
+ end
16
+ endmodule
fpga/sim/cosim.sh ADDED
@@ -0,0 +1,29 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ #!/usr/bin/env bash
2
+ # End-to-end check of the host tool against the RTL: builds fpga_top with
3
+ # Verilator, bridges its UART to a pseudo-terminal (sim/uart_pty.cpp), and runs
4
+ # `bitacc selftest` through that terminal exactly as it would run on a board.
5
+ # Usage: sim/cosim.sh [operations] [seed]
6
+ set -euo pipefail
7
+ cd "$(dirname "$0")/.."
8
+ OPS=${1:-2000}
9
+ SEED=${2:-1}
10
+ BUILD=${BUILD:-build}
11
+ mkdir -p "$BUILD"
12
+ rm -rf "$BUILD/pty"
13
+ verilator --cc --exe --build -O2 --timescale 1ns/1ps -Wno-fatal -Wno-lint -GCLKS_PER_BIT=8 --top-module fpga_top \
14
+ -Mdir "$BUILD/pty" -CFLAGS -DCPB=8 -LDFLAGS -lutil \
15
+ ../rtl/bit_accelerator.sv rtl/uart_rx.sv rtl/uart_tx.sv rtl/word_memory.sv rtl/fpga_top.sv \
16
+ "$PWD/sim/uart_pty.cpp" > "$BUILD/pty_build.log"
17
+ (cd host && cargo build --quiet --release)
18
+
19
+ rm -f "$BUILD/pty.path"
20
+ "$BUILD/pty/Vfpga_top" "$BUILD/pty.path" &
21
+ SIM=$!
22
+ trap 'kill $SIM 2>/dev/null || true; wait $SIM 2>/dev/null || true' EXIT
23
+ for _ in $(seq 100); do [ -s "$BUILD/pty.path" ] && break; sleep 0.1; done
24
+ PORT=$(cat "$BUILD/pty.path")
25
+ BITACC=host/target/release/bitacc
26
+
27
+ "$BITACC" --port "$PORT" ping
28
+ test "$("$BITACC" --port "$PORT" exec 6 0 0)" = error
29
+ "$BITACC" --port "$PORT" selftest "$OPS" "$SEED"