Skip to content

Commit 8108a61

Browse files
kroeningkroening
committed
nuterm using libtorch
1 parent 66a241c commit 8108a61

22 files changed

+1473
-0
lines changed

‎.github/workflows/pull-request-checks.yaml

+49
Original file line numberDiff line numberDiff line change
@@ -191,3 +191,52 @@ jobs:
191191
run: make -C regression/verilog test-z3
192192
- name: Print ccache stats
193193
run: ccache -s
194+
195+
# This job takes approximately 1 minute
196+
check-ubuntu-22_04-nuterm:
197+
runs-on: ubuntu-22.04
198+
steps:
199+
- uses: actions/checkout@v3
200+
with:
201+
submodules: recursive
202+
- name: Fetch dependencies
203+
env:
204+
# This is needed in addition to -yq to prevent apt-get from asking for
205+
# user input
206+
DEBIAN_FRONTEND: noninteractive
207+
run: |
208+
sudo apt-get update
209+
sudo apt-get install --no-install-recommends -yq gcc g++ ccache cmake
210+
- name: Prepare ccache
211+
uses: actions/cache@v3
212+
with:
213+
path: .ccache
214+
key: ${{ runner.os }}-22.04-nuterm-${{ github.ref }}-${{ github.sha }}-PR
215+
restore-keys: |
216+
${{ runner.os }}-22.04-nuterm-${{ github.ref }}
217+
${{ runner.os }}-22.04-nuterm
218+
- name: ccache environment
219+
run: |
220+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
221+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
222+
- name: Zero ccache stats and limit in size
223+
run: ccache -z --max-size=500M
224+
- name: Get pytorch
225+
run: |
226+
cd src/nuterm
227+
wget -q https://download.pytorch.org/libtorch/cpu/libtorch-cxx11-abi-shared-with-deps-2.1.2%2Bcpu.zip
228+
unzip -q *.zip
229+
- name: Build with cmake
230+
run: |
231+
cd src/nuterm
232+
LIBTORCH=`pwd`/libtorch
233+
mkdir build
234+
cd build
235+
cmake -DCMAKE_PREFIX_PATH=$LIBTORCH -DCMAKE_CXX_COMPILER_LAUNCHER=ccache ..
236+
cmake --build . --config Release
237+
- name: Run the unit tests
238+
run: src/nuterm/build/pytorch_tests
239+
- name: Run the system tests
240+
run: make -C regression/nuterm
241+
- name: Print ccache stats
242+
run: ccache -s

‎regression/nuterm/Makefile

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
default: test
2+
3+
TEST_PL = ../../lib/cbmc/regression/test.pl
4+
5+
test:
6+
@$(TEST_PL) -c ../../../src/nuterm/build/nuterm
7+

‎regression/nuterm/counters/counter1.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
counter1
3+
4+
^weight main.clk = 0 .*$
5+
^weight main.counter = 1 .*$
6+
^RESULT: main.counter-1$
7+
^bias: -1 .*$
8+
^EXIT=0$
9+
^SIGNAL=0$

‎regression/nuterm/counters/counter1.v

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main(input clk);
2+
3+
reg [31:0] counter;
4+
5+
always @(posedge clk)
6+
if(counter != 0)
7+
counter = counter - 1;
8+
9+
endmodule

‎regression/nuterm/counters/counter1/trace.1

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
0main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
1main.clk
18+
#2
19+
b00001111111111111111111111111110 main.counter
20+
#3
21+
b00001111111111111111111111111101 main.counter
22+
0main.clk
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
1main.clk
26+
#5
27+
b00001111111111111111111111111011 main.counter
28+
#6
29+
b00001111111111111111111111111010 main.counter
30+
#7
31+
b00001111111111111111111111111001 main.counter
32+
#8
33+
b00001111111111111111111111111000 main.counter
34+
#9
35+
b00001111111111111111111111110111 main.counter
36+
#10
37+
b00001111111111111111111111110110 main.counter

‎regression/nuterm/counters/counter1/trace.10

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
0main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
1main.clk
18+
#2
19+
b00001111111111111111111111111110 main.counter
20+
0main.clk
21+
#3
22+
b00001111111111111111111111111101 main.counter
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
1main.clk
26+
#5
27+
b00001111111111111111111111111011 main.counter
28+
0main.clk
29+
#6
30+
b00001111111111111111111111111010 main.counter
31+
#7
32+
b00001111111111111111111111111001 main.counter
33+
#8
34+
b00001111111111111111111111111000 main.counter
35+
1main.clk
36+
#9
37+
b00001111111111111111111111110111 main.counter
38+
#10
39+
b00001111111111111111111111110110 main.counter
40+
0main.clk

‎regression/nuterm/counters/counter1/trace.2

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
0main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
#2
18+
b00001111111111111111111111111110 main.counter
19+
1main.clk
20+
#3
21+
b00001111111111111111111111111101 main.counter
22+
0main.clk
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
#5
26+
b00001111111111111111111111111011 main.counter
27+
#6
28+
b00001111111111111111111111111010 main.counter
29+
#7
30+
b00001111111111111111111111111001 main.counter
31+
#8
32+
b00001111111111111111111111111000 main.counter
33+
1main.clk
34+
#9
35+
b00001111111111111111111111110111 main.counter
36+
0main.clk
37+
#10
38+
b00001111111111111111111111110110 main.counter
39+
1main.clk

‎regression/nuterm/counters/counter1/trace.3

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
1main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
0main.clk
18+
#2
19+
b00001111111111111111111111111110 main.counter
20+
#3
21+
b00001111111111111111111111111101 main.counter
22+
1main.clk
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
#5
26+
b00001111111111111111111111111011 main.counter
27+
#6
28+
b00001111111111111111111111111010 main.counter
29+
#7
30+
b00001111111111111111111111111001 main.counter
31+
0main.clk
32+
#8
33+
b00001111111111111111111111111000 main.counter
34+
1main.clk
35+
#9
36+
b00001111111111111111111111110111 main.counter
37+
0main.clk
38+
#10
39+
b00001111111111111111111111110110 main.counter
40+
1main.clk

‎regression/nuterm/counters/counter1/trace.4

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
0main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
1main.clk
18+
#2
19+
b00001111111111111111111111111110 main.counter
20+
#3
21+
b00001111111111111111111111111101 main.counter
22+
0main.clk
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
1main.clk
26+
#5
27+
b00001111111111111111111111111011 main.counter
28+
#6
29+
b00001111111111111111111111111010 main.counter
30+
0main.clk
31+
#7
32+
b00001111111111111111111111111001 main.counter
33+
#8
34+
b00001111111111111111111111111000 main.counter
35+
1main.clk
36+
#9
37+
b00001111111111111111111111110111 main.counter
38+
0main.clk
39+
#10
40+
b00001111111111111111111111110110 main.counter
41+
1main.clk

‎regression/nuterm/counters/counter1/trace.5

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
1main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
#2
18+
b00001111111111111111111111111110 main.counter
19+
#3
20+
b00001111111111111111111111111101 main.counter
21+
#4
22+
b00001111111111111111111111111100 main.counter
23+
0main.clk
24+
#5
25+
b00001111111111111111111111111011 main.counter
26+
1main.clk
27+
#6
28+
b00001111111111111111111111111010 main.counter
29+
0main.clk
30+
#7
31+
b00001111111111111111111111111001 main.counter
32+
1main.clk
33+
#8
34+
b00001111111111111111111111111000 main.counter
35+
#9
36+
b00001111111111111111111111110111 main.counter
37+
#10
38+
b00001111111111111111111111110110 main.counter

‎regression/nuterm/counters/counter1/trace.6

+42
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
$date
2+
Sun Jan 7 16:33:39 2024
3+
$end
4+
$timescale
5+
1ns
6+
$end
7+
$scope module main $end
8+
$var reg 32 main.counter main.counter [31:0] $end
9+
$var wire 1 main.clk main.clk $end
10+
$upscope $end
11+
$enddefinitions $end
12+
#0
13+
b00010000000000000000000000000000 main.counter
14+
0main.clk
15+
#1
16+
b00001111111111111111111111111111 main.counter
17+
1main.clk
18+
#2
19+
b00001111111111111111111111111110 main.counter
20+
0main.clk
21+
#3
22+
b00001111111111111111111111111101 main.counter
23+
#4
24+
b00001111111111111111111111111100 main.counter
25+
1main.clk
26+
#5
27+
b00001111111111111111111111111011 main.counter
28+
#6
29+
b00001111111111111111111111111010 main.counter
30+
0main.clk
31+
#7
32+
b00001111111111111111111111111001 main.counter
33+
1main.clk
34+
#8
35+
b00001111111111111111111111111000 main.counter
36+
0main.clk
37+
#9
38+
b00001111111111111111111111110111 main.counter
39+
1main.clk
40+
#10
41+
b00001111111111111111111111110110 main.counter
42+
0main.clk

0 commit comments

Comments
 (0)