Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation

1. Load the libraries
2. Cyclic Systems
3. Acyclic systems

This webpage contains detailed experimental results for the paper Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation that was submitted to TACAS 2022.

1 Load the libraries

Load the R libraries that are necessary for analysis of the results.

library(ggplot2)
library(tidyr)
library(dplyr)
library(readr)
theme_set(theme_light())
theme_update(text = element_text(size=20))
options(scipen=999)

2 Cyclic Systems

2.1 Load the data

ladder <- read_csv(file="results_ladder.csv")
radiator <- read_csv(file="results_radiator.csv")
random <- read_csv(file="results_random.csv")

# set timeout for failed solvers
timeout <- 3600000
ladder <- ladder %>% mutate(mcss=ifelse(time > timeout, 0, mcss), time=ifelse(mcss == 0, NA, time))
radiator <- radiator %>% mutate(mcss=ifelse(time > timeout, 0, mcss), time=ifelse(mcss == 0, NA, time))
random <- random %>% mutate(mcss=ifelse(time > timeout, 0, mcss), time=ifelse(mcss == 0, NA, time))

2.2 Cut set counts

Summarize the number of minimal cut sets for each combination of architecture, number of voters, and size.

2.2.1 Ladder

For brevity, only each tenth result is shown.

ladder %>%
  filter(mcss != "") %>%
  group_by(size, voters) %>%
  summarize(mcss = max(mcss)) %>%
  pivot_wider(names_from = c(voters), values_from = mcss) %>%
  filter(size == 1 | size %% 10 == 0)

size	1	2	3
1	6	8	12
10	42	166	432
20	82	346	912
30	122	526	1392
40	162	706	1872
50	202	886	2352
60	242	1066	2832
70	282	1246	3312
80	322	1426	3792
90	362	1606	4272
100	402	1786	4752

Check whether there is any result for which the approaches disagree on the MCS counts, i.e., some of the results is wrong.

ladder %>%
  filter(mcss != "" & mcss != 0) %>% # remove runs that failed to compute cuts sets
  group_by(size, voters) %>%
  summarize(results = n_distinct(mcss)) %>%
  filter(results > 1) # keep inputs with more than one result

size

voters

results

2.2.2 Radiator

radiator %>%
  filter(mcss != "") %>%
  group_by(size, voters) %>%
  summarize(mcss = max(mcss)) %>%
  pivot_wider(names_from = c(voters), values_from = mcss) %>%
  filter(size < 10 | size %% 10 == 0)

size	1	2	3
1	5	9	18
2	9	25	60
3	13	41	102
4	17	57	144
5	21	73	186
6	25	89	nil
7	29	105	0
8	33	121	nil
9	37	137	nil
10	41	153	nil
20	81	nil	nil
30	121	nil	nil
40	161	nil	nil
50	201	nil	nil

Check whether there is any result for which the approaches disagree on the MCS counts, i.e., some of the results is wrong.

radiator %>%
  filter(mcss != "" & mcss != 0) %>% # remove runs that failed to compute cuts sets
  group_by(size, voters) %>%
  summarize(results = n_distinct(mcss)) %>%
  filter(results > 1) # keep inputs with more than one result

size

voters

results

2.2.3 Random

Check whether there is any result for which the approaches disagree on the MCS counts, i.e., some of the results is wrong.

random %>%
  filter(mcss != "" & mcss != 0) %>% # remove runs that failed to compute cuts sets
  group_by(seed) %>%
  summarize(results = n_distinct(mcss)) %>%
  filter(results > 1) # keep inputs with more than one result

seed

results

2.3 Scalable systems

Analyze the runtimes of all approaches, divided by the architecture and the number of voters.

2.3.1 Tables

Ladder

ladder %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = c(method, voters), values_from = time, names_glue = "{method}_{voters}v") %>%
  arrange(size)

size	fpg_1v	fpg_2v	fpg_3v	smv_1v	smv_2v	smv_3v
1	0.11	0.11	0.12	0.15	0.16	0.23
2	0.1	0.12	0.14	0.67	2.06	10.88
3	0.11	0.12	0.19	3.53	42.89	250.26
4	0.12	0.16	0.25	17.27	348.67	nil
5	0.12	0.18	0.33	56.7	3239.96	nil
6	0.13	0.18	0.43	145.16	nil	nil
7	0.14	0.22	0.54	392.98	nil	nil
8	0.14	0.23	0.66	501.05	nil	nil
9	0.14	0.26	0.86	1767.04	nil	nil
10	0.15	0.32	1.01	3364.92	nil	nil
11	0.16	0.34	1.19	nil	nil	nil
12	0.16	0.37	1.44	nil	nil	nil
13	0.18	0.42	1.7	nil	nil	nil
14	0.19	0.47	1.85	nil	nil	nil
15	0.2	0.51	2.08	nil	nil	nil
16	0.21	0.56	2.39	nil	nil	nil
17	0.23	0.69	2.87	nil	nil	nil
18	0.25	0.74	3.3	nil	nil	nil
19	0.26	0.74	3.48	nil	nil	nil
20	0.28	0.88	4.14	nil	nil	nil
21	0.3	0.92	4.15	nil	nil	nil
22	0.3	0.94	5.22	nil	nil	nil
23	0.3	1.02	5.28	nil	nil	nil
24	0.35	1.16	5.89	nil	nil	nil
25	0.35	1.24	6.24	nil	nil	nil
26	0.37	1.31	7.08	nil	nil	nil
27	0.38	1.54	7.64	nil	nil	nil
28	0.41	1.59	8.14	nil	nil	nil
29	0.44	1.94	8.76	nil	nil	nil
30	0.46	1.67	9.61	nil	nil	nil
31	0.5	2.07	10.35	nil	nil	nil
32	0.53	2.17	10.44	nil	nil	nil
33	0.51	2.03	11.3	nil	nil	nil
34	0.62	2.38	12.3	nil	nil	nil
35	0.62	2.59	13.1	nil	nil	nil
36	0.78	2.4	12.84	nil	nil	nil
37	0.66	2.51	13.28	nil	nil	nil
38	0.66	2.67	15.06	nil	nil	nil
39	0.67	3.09	16.47	nil	nil	nil
40	0.78	3.35	17.26	nil	nil	nil
41	0.75	3.42	19.3	nil	nil	nil
42	0.89	3.88	21.1	nil	nil	nil
43	0.84	4.01	20.65	nil	nil	nil
44	0.9	4.7	21.45	nil	nil	nil
45	0.98	4.44	23.61	nil	nil	nil
46	1.05	4.77	22.49	nil	nil	nil
47	0.91	4.85	25.24	nil	nil	nil
48	1.11	4.55	26.11	nil	nil	nil
49	1.1	4.78	23.05	nil	nil	nil
50	1.14	5.73	25.34	nil	nil	nil
51	1.06	5.86	28.07	nil	nil	nil
52	1.13	6.92	34.73	nil	nil	nil
53	1.35	6.2	33.08	nil	nil	nil
54	1.28	6.53	33.9	nil	nil	nil
55	1.25	6.22	34.17	nil	nil	nil
56	1.5	7.73	37.13	nil	nil	nil
57	1.43	7.64	36.55	nil	nil	nil
58	1.61	8	39.96	nil	nil	nil
59	1.82	8.04	41.28	nil	nil	nil
60	1.46	8.71	40.9	nil	nil	nil
61	1.86	9.2	44.24	nil	nil	nil
62	1.61	8.29	44.78	nil	nil	nil
63	1.75	9.56	44.02	nil	nil	nil
64	1.85	10.1	43.24	nil	nil	nil
65	1.95	9.32	46.06	nil	nil	nil
66	1.84	9.18	49.34	nil	nil	nil
67	1.99	10.2	55.14	nil	nil	nil
68	2.24	10.47	55.76	nil	nil	nil
69	2.22	10.12	54.38	nil	nil	nil
70	2.25	10.64	60.18	nil	nil	nil
71	2.26	11.96	55.72	nil	nil	nil
72	2.4	11.23	59.1	nil	nil	nil
73	2.78	19.02	63.95	nil	nil	nil
74	2.15	11.83	71.86	nil	nil	nil
75	2.62	13.19	68.98	nil	nil	nil
76	2.72	13.93	69.31	nil	nil	nil
77	2.43	14.14	70.81	nil	nil	nil
78	3.11	14.93	73.57	nil	nil	nil
79	2.71	13.75	78.73	nil	nil	nil
80	2.79	14.7	85.87	nil	nil	nil
81	2.62	15.86	87.4	nil	nil	nil
82	3.02	16.58	80.14	nil	nil	nil
83	3.17	17.23	86.82	nil	nil	nil
84	3.2	17.45	88.55	nil	nil	nil
85	3.36	16.46	88.94	nil	nil	nil
86	3.58	19.12	95.52	nil	nil	nil
87	3.5	19.04	93.07	nil	nil	nil
88	3.35	19.2	101.92	nil	nil	nil
89	3.43	18.6	102.9	nil	nil	nil
90	3.89	22.07	114.76	nil	nil	nil
91	3.85	26.74	102.06	nil	nil	nil
92	3.85	20.97	114.17	nil	nil	nil
93	4.05	21.16	106.43	nil	nil	nil
94	4.13	20.78	123.33	nil	nil	nil
95	4.35	20.6	122.22	nil	nil	nil
96	4.03	24.73	126.56	nil	nil	nil
97	4.6	24	111.73	nil	nil	nil
98	4.3	24.61	123.65	nil	nil	nil
99	4.83	27.01	126.27	nil	nil	nil
100	4.68	26.93	129.16	nil	nil	nil

Radiator

radiator %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = c(method, voters), values_from = time, names_glue = "{method}_{voters}v") %>%
  arrange(size)

size	fpg_1v	fpg_2v	fpg_3v	smv_1v	smv_2v	smv_3v
1	0.12	0.2	0.2	0.27	0.55	0.96
2	0.2	0.2	0.48	4.28	30.41	115.16
3	0.21	0.24	5.86	25.37	1245.76	nil
4	0.22	0.3	18.54	96.81	nil	nil
5	0.22	0.56	1416.32	869.45	nil	nil
6	0.22	0.39	nil	3195.01	nil	nil
7	0.23	1.01	nil	nil	nil	nil
8	0.17	1.69	nil	nil	nil	nil
9	0.18	1.27	nil	nil	nil	nil
10	0.19	2.65	nil	nil	nil	nil
11	0.2	5.64	nil	nil	nil	nil
12	0.22	7.89	nil	nil	nil	nil
13	0.23	nil	nil	nil	nil	nil
14	0.26	68.56	nil	nil	nil	nil
15	0.29	200.3	nil	nil	nil	nil
16	0.29	454.72	nil	nil	nil	nil
17	0.33	nil	nil	nil	nil	nil
18	0.33	nil	nil	nil	nil	nil
19	0.36	nil	nil	nil	nil	nil
20	0.38	nil	nil	nil	nil	nil
21	0.4	nil	nil	nil	nil	nil
22	0.4	nil	nil	nil	nil	nil
23	0.5	nil	nil	nil	nil	nil
24	0.48	nil	nil	nil	nil	nil
25	0.49	nil	nil	nil	nil	nil
26	0.51	nil	nil	nil	nil	nil
27	0.62	nil	nil	nil	nil	nil
28	0.73	nil	nil	nil	nil	nil
29	0.73	nil	nil	nil	nil	nil
30	0.72	nil	nil	nil	nil	nil
31	0.92	nil	nil	nil	nil	nil
32	0.84	nil	nil	nil	nil	nil
33	0.84	nil	nil	nil	nil	nil
34	0.95	nil	nil	nil	nil	nil
35	1.1	nil	nil	nil	nil	nil
36	0.93	nil	nil	nil	nil	nil
37	1.14	nil	nil	nil	nil	nil
38	1.24	nil	nil	nil	nil	nil
39	1.12	nil	nil	nil	nil	nil
40	1.41	nil	nil	nil	nil	nil
41	1.3	nil	nil	nil	nil	nil
42	1.41	nil	nil	nil	nil	nil
43	1.52	nil	nil	nil	nil	nil
44	1.72	nil	nil	nil	nil	nil
45	1.53	nil	nil	nil	nil	nil
46	1.71	nil	nil	nil	nil	nil
47	1.84	nil	nil	nil	nil	nil
48	1.6	nil	nil	nil	nil	nil
49	2.18	nil	nil	nil	nil	nil
50	1.88	nil	nil	nil	nil	nil

2.3.2 Plots

Plot the previous results.

Ladder

timeout <- 3600

plot <- ladder %>%
  filter(mcss != 0) %>%
  mutate(method = recode(method, fpg="FPG", smv="ParamIC3")) %>%
  ggplot(aes(x=size, y=time/1000, color=method)) +
  geom_point() +
  scale_x_continuous(name="Size of the architecture") +
  scale_y_continuous(name="Time (s)", trans="log10",
                     limits=c(0.09, timeout),
                     breaks=c(0.1, 1, 10, 100, 1000, timeout),
                     label=c("0.1", "1", "10", "100", "1000", "T/O")) +
  scale_color_discrete(name = "Method") +
  annotation_logticks(sides="l", mid = unit(2.5,"mm"), long=unit(4,"mm")) +
  facet_grid(cols=vars(voters))
plot

Generate PDF version of the plot, which is used in the paper.

plot

scalable_time_radiator.pdf

Radiator

timeout <- 3600

plot <- radiator %>%
  filter(mcss != 0) %>%
  mutate(method = recode(method, fpg="FPG", smv="ParamIC3")) %>%
  ggplot(aes(x=size, y=time/1000, color=method)) +
  geom_point() +
  scale_x_continuous(name="Size of the architecture") +
  scale_y_continuous(name="Time (s)", trans="log10",
                     limits=c(0.09, timeout),
                     breaks=c(0.1, 1, 10, 100, 1000, timeout),
                     label=c("0.1", "1", "10", "100", "1000", "T/O")) +
  scale_color_discrete(name = "Method") +
  annotation_logticks(sides="l", mid = unit(2.5,"mm"), long=unit(4,"mm")) +
  facet_grid(cols=vars(voters))
plot

Generate PDF version of the plot, which is used in the paper.

plot

scalable_time_radiator.pdf

2.4 Random systems

timeout <- 3600000

random_wide <- random %>%
  select(method, seed, time) %>%
  mutate(time = if_else(time >= timeout | is.na(time), timeout, time)) %>%
  pivot_wider(names_from=method, values_from=time, values_fill=3600000)

Solved by neither FPG, nor SMV:

random_wide %>%
  filter(smv == timeout & fpg == timeout) %>%
  arrange(seed) %>% nrow()

x
66

Solved by FPG, unsolved by SMV:

random_wide %>%
  filter(smv == timeout & fpg != timeout) %>%
  arrange(seed) %>% nrow()

x
59

Solved by SMV, unsolved by FPG:

random_wide %>%
  filter(smv != timeout & fpg == timeout) %>%
  arrange(seed) %>% nrow()

x
0

timeout <- 3600

plot <- random %>%
  select(method, seed, time) %>%
  mutate(time = if_else(time >= timeout*1000 | is.na(time), timeout*1000, time)) %>%
  pivot_wider(names_from=method, values_from=time, values_fill=3600000) %>%
  ggplot(aes(x=fpg/1000, y=smv/1000)) +
  geom_point() +
  scale_x_continuous("Time FPG (s)", trans="log10",
                     limits=c(0.05, timeout),
                     breaks=c(0.1, 1, 10, 100, 1000, timeout),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  scale_y_continuous("Time ParamIC3 (s)", trans="log10",
                     limits=c(0.05, timeout),
                     breaks=c(0.1, 1, 10, 100, 1000, timeout),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  geom_abline(slope=1, color = "darkgray") +
  geom_abline(slope=1, intercept=1, color = "gray") +
  geom_abline(slope=1, intercept=-1, color = "gray") +
  geom_abline(slope=1, intercept=2, color = "lightgray") +
  geom_abline(slope=1, intercept=-2, color = "lightgray")
plot

Generate PDF version of the plot, which is used in the paper.

plot

scalable_time_random.pdf

3 Acyclic systems

3.1 Load the data

scalable_acyclic <- read_csv(file="results_scalable_acyclic.csv")
random_acyclic <- read_csv(file="results_random_acyclic.csv")

# merge abstraction and solver into one field and set timeout for failed solvers
scalable_acyclic <- scalable_acyclic %>% mutate(method = paste(abstraction, solver, sep="-"), time=ifelse(mcss == 0, NA, time))
random_acyclic <- random_acyclic %>% mutate(method = paste(abstraction, solver, sep="-"), time=ifelse(mcss == 0, NA, time))

3.2 Cut set counts

Summarize the number of minimal cut sets for each combination of architecture, number of voters, and size. For brevity, only each tenth result is shown.

scalable_acyclic %>%
  filter(mcss != "") %>%
  group_by(arch, size, voters) %>%
  summarize(mcss = max(mcss)) %>%
  pivot_wider(names_from = c(voters, arch), values_from = mcss) %>%
  filter(size == 1 | size %% 10 == 0)

size	1_linear	2_linear	3_linear	1_rectangular	2_rectangular	3_rectangular
10	40	58	114	160	277	657
20	80	118	234	320	557	1317
30	120	178	354	480	837	1977
40	160	238	474	640	1117	2637
50	200	298	594	800	1397	3297
60	240	358	714	960	1677	3957
70	280	418	834	1120	1957	4617
80	320	478	954	1280	2237	5277
90	360	538	1074	1440	2517	5937
100	400	598	1194	1600	2797	6597
110	440	658	1314	1760	3077	7257
120	480	718	1434	1920	3357	7917
130	520	778	1554	2080	3637	8577
140	560	838	1674	2240	3917	9237
150	600	898	1794	2400	4197	9897
160	640	958	1914	2560	4477	10557
170	680	1018	2034	2720	4757	11217
180	720	1078	2154	2880	5037	11877
190	760	1138	2274	3040	5317	12537
200	800	1198	2394	3200	5597	13197
210	840	1258	2514	3360	5877	13857
220	880	1318	2634	3520	6157	14517
230	920	1378	2754	3680	6437	15177
240	960	1438	2874	3840	6717	15837
250	1000	1498	2994	4000	6997	16497
260	1040	1558	3114	4160	7277	17157
270	1080	1618	3234	4320	7557	17817
280	1120	1678	3354	4480	7837	18477
290	1160	1738	3474	4640	8117	19137
300	1200	1798	3594	4800	8397	19797

Check whether there is any result for which the approaches disagree on the MCS counts, i.e., some of the results is wrong.

scalable_acyclic %>%
  filter(mcss != "" & mcss != 0) %>% # remove runs that failed to compute cuts sets
  group_by(arch, size, voters) %>%
  summarize(results = n_distinct(mcss)) %>%
  filter(results > 1) # keep inputs with more than one result

arch

size

voters

results

3.3 Overall runtimes

Analyze the runtimes of all approaches, divided by the architecture and the number of voters.

3.3.1 Tables

In both of the tables, again only each tenth result is shown for brevity.

Linear

1 voter

scalable_acyclic %>%
  filter(arch == "linear" & voters == 1) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	1	0.19	0.17	0.28	0.33
20	1	0.21	0.2	0.36	0.41
30	1	0.26	0.23	0.48	0.54
40	1	0.36	0.27	0.62	0.69
50	1	0.58	0.33	0.83	0.86
60	1	0.81	0.4	1.08	1.01
70	1	1.25	0.49	1.51	1.27
80	1	1.74	0.59	2	1.53
90	1	2.11	0.67	2.7	1.74
100	1	2.89	0.8	3.32	2.06
110	1	3.94	0.96	4.89	2.51
120	1	4.36	1.1	4.9	2.64
130	1	5.93	1.25	6.03	3.25
140	1	7.29	1.45	6.95	3.51
150	1	8.89	1.64	8.73	4.22
160	1	9.93	1.79	10.52	4.3
170	1	13.65	2.15	12.71	5.39
180	1	16.05	2.39	15.06	5.98
190	1	22.66	2.7	15.57	5.86
200	1	21.36	2.97	19.24	7.25
210	1	23.46	3	27.16	7.73
220	1	27.54	3.39	24.82	8.05
230	1	30.69	4.04	36.71	9.2
240	1	34.14	4.14	30.8	9.6
250	1	36.96	4.37	36.54	10.61
260	1	42.65	5.2	41.22	11.1
270	1	50.31	5.3	43.86	12.34
280	1	57.39	5.71	54.96	12.93
290	1	65.55	6.2	63.58	14.52
300	1	87.49	6.88	72.67	15.83

2 voters

scalable_acyclic %>%
  filter(arch == "linear" & voters == 2) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	2	0.19	0.18	0.32	0.38
20	2	0.25	0.22	0.45	0.58
30	2	0.4	0.28	0.7	0.86
40	2	0.66	0.36	1.12	1.13
50	2	1.14	0.47	1.88	1.53
60	2	1.85	0.6	2.82	2.02
70	2	2.72	0.78	4.03	2.6
80	2	3.71	0.97	5.3	3.17
90	2	5.1	1.14	6.95	3.9
100	2	7.43	1.46	9.64	4.57
110	2	8.95	1.7	11.8	5.8
120	2	14.83	2.04	18.66	7.21
130	2	15.96	2.48	17.82	8.33
140	2	19.11	2.81	25.03	9.31
150	2	23.16	3.26	33.78	10.65
160	2	26.75	3.51	35.37	11.63
170	2	33.7	4.23	42.95	13.35
180	2	38.5	4.9	57.01	14.93
190	2	42.16	5.38	80.4	15.73
200	2	49.45	5.56	94.83	17.94
210	2	80.92	6.72	105.94	20.68
220	2	68.05	7.4	129.06	21.11
230	2	102.61	8.5	175.98	24.16
240	2	97.29	8.93	202.92	26.82
250	2	104.4	9.44	214.63	27.54
260	2	117.53	10.07	271.06	31.1
270	2	133.23	11.87	306.21	34.11
280	2	139.12	12.56	318.31	35.18
290	2	168.77	12.66	348.59	38.15
300	2	188.87	15.06	413.25	41.74

3 voters

scalable_acyclic %>%
  filter(arch == "linear" & voters == 3) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	3	0.2	0.2	0.4	0.49
20	3	0.41	0.28	0.88	0.95
30	3	0.88	0.42	2.03	1.59
40	3	1.67	0.62	3.92	2.41
50	3	3.16	0.88	6.43	3.54
60	3	5.26	1.22	10.62	4.8
70	3	8.33	1.49	19.33	7.16
80	3	12.37	1.96	27.02	9.21
90	3	16.12	2.47	43.71	11.13
100	3	23.54	3.1	56.12	14.36
110	3	29.66	3.68	80.78	16.54
120	3	38.05	4.3	107.61	19.51
130	3	50.13	5.11	141.02	23.88
140	3	64.1	6.18	182.63	27.56
150	3	78.21	6.98	223.1	31.8
160	3	97.69	8.61	264.41	35.23
170	3	110.28	8.99	344.63	40.2
180	3	175.64	10.6	542.04	54.43
190	3	166.8	11.63	513.17	52.1
200	3	185.2	12.63	600.95	55.86
210	3	226.3	15.58	688	61.2
220	3	237.34	16.21	736.81	68.33
230	3	303.75	18.71	918.73	77.77
240	3	322.58	19.73	1271.33	92.99
250	3	493.68	24.55	1206.33	90.68
260	3	543.56	24.13	1349.63	100.57
270	3	622.22	25.96	1527.57	122.09
280	3	552.4	28.84	1722.36	113.21
290	3	585.2	30.05	1814.59	120.2
300	3	767.11	31.54	2115.85	142.88

Rectangular

1 voter

scalable_acyclic %>%
  filter(arch == "rectangular" & voters == 1) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	1	0.4	0.28	0.83	0.92
20	1	1.75	0.6	2.43	2.03
30	1	5.5	1.15	5.52	3.64
40	1	15.14	2.03	11.94	6.32
50	1	21.48	2.95	18.96	8.53
60	1	37.5	4.15	43.34	14.6
70	1	73.48	6.15	82.72	18.64
80	1	113.14	8.48	125.33	26.37
90	1	124.52	10.29	199.46	27.38
100	1	172.69	12.77	271.4	34.63
110	1	240.1	16.51	387.55	43.49
120	1	313.9	20.9	521.65	51.05
130	1	400.94	25.25	879.63	60.03
140	1	490.64	29.6	1127.71	67.52
150	1	606.21	35.71	1438.47	79.97
160	1	784.52	38.55	1300.91	89.27
170	1	952.51	47.24	1606.91	105.19
180	1	1139.82	51.16	1948.65	113.36
190	1	1374.62	59.28	3105	135.08
200	1	2132.72	67.93	2673.6	149.71
210	1	1957.57	78.34	3054.41	163.12
220	1	2315.68	86.31	3476.79	185.31
230	1	3760.86	98.28	nil	204.82
240	1	3308.09	106.32	nil	220.85
250	1	nil	119.14	nil	nil
260	1	nil	128.72	nil	nil
270	1	nil	144.94	nil	nil
280	1	nil	165.23	nil	nil
290	1	nil	171	nil	nil
300	1	nil	187.35	nil	nil

2 voters

scalable_acyclic %>%
  filter(arch == "rectangular" & voters == 2) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	2	1.02	0.4	1.81	1.65
20	2	6.43	1.06	8.54	5.11
30	2	19.61	2.29	26.51	10.56
40	2	46.49	3.87	69.05	18.44
50	2	88.04	6.55	138.66	27.84
60	2	154.18	9.67	261.88	39.55
70	2	244.51	12.72	417.02	54.05
80	2	382.18	18.78	627.3	71.65
90	2	546.05	23.6	925.62	92.42
100	2	769.98	30.18	1229.57	108.65
110	2	1058.02	38.66	1656.52	133.38
120	2	1402.95	45.95	3001.97	162.28
130	2	1793.59	54.11	2951.9	198.49
140	2	2370.63	66.66	3548.04	222.56
150	2	nil	79	nil	254.88
160	2	nil	90.6	nil	294.6
170	2	nil	105.89	nil	343.44
180	2	nil	122.96	nil	445.55
190	2	nil	138.5	nil	433.72
200	2	nil	155.63	nil	493.23
210	2	nil	183	nil	566.23
220	2	nil	206.12	nil	626.32
230	2	nil	228.08	nil	682.49
240	2	nil	257.26	nil	740.85
250	2	nil	284.5	nil	nil
260	2	nil	314.87	nil	nil
270	2	nil	342.72	nil	nil
280	2	nil	386.11	nil	nil
290	2	nil	404.35	nil	nil
300	2	nil	457.59	nil	nil

3 voters

scalable_acyclic %>%
  filter(arch == "rectangular" & voters == 3 & !is.na(time)) %>%
  select(size, voters, method, time) %>%
  mutate(time = round(time / 1000, 2)) %>%
  arrange(method, voters) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  arrange(voters, size) %>%
  filter(size == 1 | size %% 10 == 0)

size	voters	fp-bdd	fp-xpg	pa-bdd	pa-xpg
10	3	5.95	0.79	17.41	5.43
20	3	40	2.56	88.5	15.32
30	3	177.68	5.71	410.83	43.63
40	3	310.39	12.06	748.54	64.02
50	3	642.13	18.44	1447.92	103.31
60	3	1146.31	27.91	2551.46	148.59
70	3	2463.2	38.59	nil	214.42
80	3	2798.28	53.44	nil	269.64
90	3	nil	69.57	nil	434.98
100	3	nil	90.5	nil	443.16
110	3	nil	117.7	nil	554.09
120	3	nil	138.9	nil	667.66
130	3	nil	168.78	nil	756.02
140	3	nil	198.62	nil	1107.76
150	3	nil	234.29	nil	1039.81
160	3	nil	274.21	nil	1215.92
170	3	nil	330.07	nil	1716.8
180	3	nil	379.56	nil	1520.46
190	3	nil	438.64	nil	1806.2
200	3	nil	490.33	nil	2420.66
210	3	nil	562.5	nil	2655.67
220	3	nil	625.78	nil	2974.36
230	3	nil	712.38	nil	2963.95
240	3	nil	778.29	nil	nil
250	3	nil	866.53	nil	nil
260	3	nil	975.3	nil	nil
270	3	nil	1063.09	nil	nil
280	3	nil	1178.65	nil	nil
290	3	nil	1261.48	nil	nil
300	3	nil	1395.53	nil	nil

3.3.2 Plots

Plot the previous results.

plot <- scalable_acyclic %>%
  filter(size <= 200) %>%
  mutate(method = recode(method, `fp-bdd`="FP-BDD", `fp-xpg`="FP-SAT", `pa-bdd`="PA-BDD", `pa-xpg`="PA-SAT")) %>%
  filter(mcss != 0) %>%
  ggplot(aes(x=size, y=time/1000, color=method)) +
  geom_point() +
  scale_x_continuous(name="Size of the architecture") +
  scale_y_continuous(name="Time (s)", trans="log10",
                     limits=c(0.09, 3600),
                     breaks=c(0.1, 1, 10, 100, 1000, 3600),
                     label=c("0.1", "1", "10", "100", "1000", "T/O")) +
  scale_color_discrete(name = "Method") +
  annotation_logticks(sides="l", mid = unit(2.5,"mm"), long=unit(4,"mm")) +
  facet_grid(vars(arch), vars(voters))
plot

Generate PDF version of the plot, which is used in the paper.

plot

scalable_time.pdf

3.3.3 Random

plot <- random_acyclic %>%
  select(method, time, size, seed) %>%
  mutate(time = round(time / 1000, 4)) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  ggplot(aes(x=`pa-bdd`, y=`fp-xpg`)) +
  geom_point() +
  scale_x_continuous(name="Time PA-BDD (s)", trans="log10",
                     limits=c(0.05, 3600),
                     breaks=c(0.1, 1, 10, 100, 1000, 3600),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  scale_y_continuous(name="Time FP-SAT (s)", trans="log10",
                     limits=c(0.05, 3600),
                     breaks=c(0.1, 1, 10, 100, 1000, 3600),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  geom_abline(slope=1, color = "darkgray") +
  geom_abline(slope=1, intercept=1, color = "gray") +
  geom_abline(slope=1, intercept=-1, color = "gray") +
  geom_abline(slope=1, intercept=2, color = "lightgray") +
  geom_abline(slope=1, intercept=-2, color = "lightgray")
plot

Generate PDF version of the plot, which is used in the paper.

plot

solving_time_random_pa_bdd_fp_xpg.pdf

plot <- random_acyclic %>%
  select(method, time, size, seed) %>%
  mutate(time = round(time / 1000, 4)) %>%
  pivot_wider(names_from = method, values_from = time) %>%
  ggplot(aes(x=`pa-xpg`, y=`fp-xpg`)) +
  geom_point() +
  scale_x_continuous(name="Time PA-SAT (s)", trans="log10",
                     limits=c(0.05, 3600),
                     breaks=c(0.1, 1, 10, 100, 1000, 3600),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  scale_y_continuous(name="Time FP-SAT (s)", trans="log10",
                     limits=c(0.05, 3600),
                     breaks=c(0.1, 1, 10, 100, 1000, 3600),
                     label=c("0.1", "1", "10", "100", "1000", "T/O"),
                     ) +
  geom_abline(slope=1, color = "darkgray") +
  geom_abline(slope=1, intercept=1, color = "gray") +
  geom_abline(slope=1, intercept=-1, color = "gray") +
  geom_abline(slope=1, intercept=2, color = "lightgray") +
  geom_abline(slope=1, intercept=-2, color = "lightgray")
plot

plot

solving_time_random_pa_xpg_fp_xpg.pdf

size	1	2	3
1	5	9	18
2	9	25	60
3	13	41	102
4	17	57	144
5	21	73	186
6	25	89	nil
7	29	105	0
8	33	121	nil
9	37	137	nil
10	41	153	nil
20	81	nil	nil
30	121	nil	nil
40	161	nil	nil
50	201	nil	nil

size	1	2	3
1	5	9	18
2	9	25	60
3	13	41	102
4	17	57	144
5	21	73	186
6	25	89	nil
7	29	105	0
8	33	121	nil
9	37	137	nil
10	41	153	nil
20	81	nil	nil
30	121	nil	nil
40	161	nil	nil
50	201	nil	nil

Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation

Table of Contents

1 Load the libraries

2 Cyclic Systems

2.1 Load the data

2.2 Cut set counts

2.2.1 Ladder

2.2.2 Radiator

2.2.3 Random

2.3 Scalable systems

2.3.1 Tables

2.3.2 Plots

2.4 Random systems

3 Acyclic systems

3.1 Load the data

3.2 Cut set counts

3.3 Overall runtimes

3.3.1 Tables

3.3.2 Plots

3.3.3 Random

size	1	2	3
1	5	9	18
2	9	25	60
3	13	41	102
4	17	57	144
5	21	73	186
6	25	89	nil
7	29	105	0
8	33	121	nil
9	37	137	nil
10	41	153	nil
20	81	nil	nil
30	121	nil	nil
40	161	nil	nil
50	201	nil	nil