-
Notifications
You must be signed in to change notification settings - Fork 2
/
riscv.thm
executable file
·80 lines (68 loc) · 2.62 KB
/
riscv.thm
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
<?xml version="1.0"?>
<alloy>
<view>
<defaultnode/>
<defaultedge/>
<node>
<type name="AMO"/>
<type name="Event"/>
<type name="Fence"/>
<type name="FenceTSO"/>
<type name="Int"/>
<type name="LoadNormal"/>
<type name="LoadReserve"/>
<type name="MemoryEvent"/>
<type name="NOP"/>
<type name="StoreConditional"/>
<type name="StoreNormal"/>
<type name="String"/>
<type name="univ"/>
<type name="seq/Int"/>
<set name="$lkmm_rel_acq_a" type="Event"/>
<set name="$lkmm_rel_acq_b" type="Event"/>
<set name="$lkmm_rel_acq_c" type="Event"/>
<set name="$lkmm_rel_acq_d" type="Event"/>
<set name="$lkmm_rel_acq_e" type="Event"/>
<set name="$lkmm_rel_acq_f" type="Event"/>
<set name="$lkmm_rel_acq_x" type="Address"/>
<set name="$lkmm_rel_acq_y" type="Address"/>
<set name="$lkmm_rel_acq_z" type="Address"/>
</node>
<node color="Blue">
<set name="$Init" type="Event"/>
</node>
<node color="Green">
<type name="Hart"/>
</node>
<node showlabel="no">
<set name="$FencePRSR" type="Fence"/>
<set name="$FencePRSW" type="Fence"/>
<set name="$Load" type="Event"/>
<set name="$NonInit" type="Event"/>
<set name="$RCsc" type="MemoryEvent"/>
<set name="$Release" type="MemoryEvent"/>
<set name="$Store" type="Event"/>
</node>
<node visible="no">
<type name="Address"/>
</node>
<edge visible="no">
<relation name="$fr"> <type name="Event"/> <type name="Event"/> </relation>
<relation name="$po_loc"> <type name="Event"/> <type name="Event"/> </relation>
<relation name="$ppo"> <type name="Event"/> <type name="Event"/> </relation>
<relation name="$ppo_fence"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
<relation name="$rfi"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
</edge>
<edge visible="no" attribute="yes">
<relation name="acquireRCpc"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
<relation name="acquireRCsc"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
<relation name="address"> <type name="MemoryEvent"/> <type name="Address"/> </relation>
<relation name="pr"> <type name="Fence"/> <type name="Fence"/> </relation>
<relation name="pw"> <type name="Fence"/> <type name="Fence"/> </relation>
<relation name="releaseRCpc"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
<relation name="releaseRCsc"> <type name="MemoryEvent"/> <type name="MemoryEvent"/> </relation>
<relation name="sr"> <type name="Fence"/> <type name="Fence"/> </relation>
<relation name="sw"> <type name="Fence"/> <type name="Fence"/> </relation>
</edge>
</view>
</alloy>