-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathwire-up-qed-module.sh
executable file
·50 lines (34 loc) · 2.27 KB
/
wire-up-qed-module.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
#!/bin/bash
# Update the topsim module to wire up the QED module
# Add "(* keep *)" pragmas to preserve certain wires for model checking
patch -i ./qed-wireup-patches/step0-topsim-changes.patch ./ridecore-src-buggy/topsim.v
# Make the instruction signal a top-level input to be selected by the
# model checker
patch -i ./qed-wireup-patches/step1-topsim-changes.patch ./ridecore-src-buggy/topsim.v
# Instantiate the instruction-constraint module to constrain the
# instruction to be a valid instruction from the ISA
patch -i ./qed-wireup-patches/step2-topsim-changes.patch ./ridecore-src-buggy/topsim.v
# Use assumption to embed constraint that there's no reset in the BTOR2
# reset sequence will be simulated before BTOR2 generated
patch -i ./qed-wireup-patches/step3-topsim-changes.patch ./ridecore-src-buggy/topsim.v
# Update the pipeline module to wire up the QED module
# Drive instruction signal from top-level input, instantiate the QED
# module to modify instructions, send the output instruction of the
# QED module through the pipeline
patch -i ./qed-wireup-patches/step0-pipeline-changes.patch ./ridecore-src-buggy/pipeline.v
# wire registers 1 and 17 out of regfile so we can access them
# in standard Verilog (Yosys doesn't support . notation for reaching into modules)
patch -i ./qed-wireup-patches/step0-ram_sync_nolatch-changes.patch ./ridecore-src-buggy/ram_sync_nolatch.v
patch -i ./qed-wireup-patches/step0-arf-changes.patch ./ridecore-src-buggy/arf.v
patch -i ./qed-wireup-patches/step1-pipeline-changes.patch ./ridecore-src-buggy/pipeline.v
# OPTIONAL: make additional modifications to speed up model checking
# Disable branch prediction
patch -i ./qed-wireup-patches/step0-pipeline_if-changes-optimization.patch ./ridecore-src-buggy/pipeline_if.v
# Reduce size of memory
patch -i ./qed-wireup-patches/step0-dmem-changes-optimization.patch ./ridecore-src-buggy/dmem.v
# Limit instruction fetch to only one instruction
patch -i ./qed-wireup-patches/step2-pipeline-changes-optimization.patch ./ridecore-src-buggy/pipeline.v
# Remove branch target buffer to get rid of neg-edge behavior. This
# optimization allows to abstract the clock and reduce the number of
# unrollings in BMC
patch -i ./qed-wireup-patches/step1-pipeline_if-changes-optimization.patch ./ridecore-src-buggy/pipeline_if.v