blob: 477c7d027f6fc3d3997a84b4dafe83b251708fb1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
initial
assume (= [mem_0] [mem_1])
assume (= [cpu_0.cpuregs] [cpu_1.cpuregs])
assume (= [trace_data_0] [trace_data_1])
always
assume (=> (not [mem_valid_0]) (not [mem_ready_0]))
assume (=> (not [mem_valid_1]) (not [mem_ready_1]))
# assume (= [mem_ready_0] [mem_ready_1])
always -1
assert (=> (= [trace_balance] #x00) (= [trace_data_0] [trace_data_1]))
|
