1 of 42

AllSAT for Combinational Circuits

Yogev Shalmon, Intel & The Open University of Israel

Dror Fried, The Open University of Israel

Alexander Nadel, Intel & Technion, Israel

SAT’23, Alghero, Italy

July 5, 2023

1

7/4/2023

2 of 42

Static Timing Analysis (STA)

Validates the timing performance of a circuit
STA is a crucial step in circuit design process

2

7/4/2023

3 of 42

Intel’s STA Flow

3

7/4/2023

4 of 42

The AllSAT-CT Problem

What is the AllSAT-CT problem?

4

7/4/2023


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

5 of 42

Disjoint vs Non-Disjoint Solutions

5

7/4/2023

Disjoint

Non-Disjoint

6 of 42

Disjoint vs Non-Disjoint Solutions

6

7/4/2023

Disjoint

Non-Disjoint

7 of 42

Solution Generalization

Obtaining small partial solutions results in more compact DNF
A simple approach is to generalize an existing solution

In Boolean logic, by unassigning variables

7

7/4/2023


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

8 of 42

Solution Generalization

Obtaining small partial solutions results in more compact DNF
A simple approach is to generalize an existing solution

In Boolean logic, by unassigning variables

8

7/4/2023

Generalization


0	0	0	1
0	0	1	1
0	1	0	1
0	1	1	1
1	0	0	1
1	0	1	1
1	1	0	1
1	1	1	0

9 of 42

Naïve Approach for AllSAT-CT

How one can solve the AllSAT-CT problem?

9

7/4/2023

Easy:

Convert to a CNF formula (i.e., Tseitin encoding)
Solve AllSAT for CNF (AllSAT-CNF)

[TS, JEA’16; ZPS, ASE’20; LMZY, IJCAI’22]

Result is in Disjunctive Normal Form (DNF)

Either Disjoint (no overlap) or Non-Disjoint (may overlap)

10 of 42

Why AllSAT-CNF?

10

7/4/2023

SAT solvers operate at CNF level
Received substantially more attention than AllSAT-CT

[KMSJ, SAT’03; DJSY, AI’16; LBGV, MSR’13]

Problem:

Reducing AllSAT-CT to AllSAT-CNF does not scale well

Our Key observation:

Generalization in Boolean logic is inherently inefficient

11 of 42

Our Dedicated AllSAT-CT Solutions

Utilize ternary logic instead of Boolean
blocking-clause-based
Input: combinational circuit (AIGER)

TALE:

Ternary logic simulation-based

MARS:

Dual-rail & MaxSAT

DUTY:

TALE + MARS

Implemented in an open-source tool HALL (Haifa AllSAT)

https://github.com/yogevshalmon/allsat-circuits

11

7/4/2023

12 of 42

Blocking AllSAT-CT Algorithm Template

12

7/4/2023

13 of 42

Blocking AllSAT-CT Algorithm Template

13

7/4/2023

14 of 42

TALE

Encoding:

Convert AllSAT-CT to AllSAT-CNF with the Tseitin encoding

Generalization:

Utilizes the original circuit structure
Based on ternary-simulation from PDR model checking alg. [EMR, FMCAD’11]
Depends on the variable order

Blocking (adding blocking clause):

Standard method: the negated generalized solution

Result:

The resulting DNF is Non-Disjoint

14

7/4/2023

15 of 42

Ternary Logic

15

7/4/2023

16 of 42

TALE Generalization: Ternary Simulation

16

7/4/2023

17 of 42

TALE Generalization: Ternary Simulation

17

7/4/2023

18 of 42

TALE Generalization: Ternary Simulation

18

7/4/2023

19 of 42

TALE Generalization: Ternary Simulation

19

7/4/2023

20 of 42

TALE Generalization: Ternary Simulation

20

7/4/2023

21 of 42

TALE Blocking

21

7/4/2023

22 of 42

Generalization in Boolean vs Ternary Logic

22

7/4/2023

23 of 42

MARS

Encoding:

Convert AllSAT-CT to AllSAT-CNF with the dual-rail encoding

Generalization:

Does not utilize the original circuit structure
Based on Anytime MaxSAT-inspired heuristics [Nadel, J. Satisfiabilty’20]

Blocking:

Dedicated methods for non-disjoint or disjoint

Result:

The resulting DNF can be either Non-Disjoint or Disjoint

23

7/4/2023

24 of 42

The Dual-Rail Encoding

24

7/4/2023

25 of 42

Dual-Rail and Exact MaxSAT

25

7/4/2023

26 of 42

MARS Generalization

Approximate MaxSAT with SAT

Generalization is based on Anytime MaxSAT-inspired heuristics

The heuristics:

Boost the score of the target variables once (TSB heuristic)
Always choose 0 as the polarity of the target variables (optimistic heuristics)

26

7/4/2023

27 of 42

MARS Blocking

27

7/4/2023

28 of 42

DUTY

Combines MARS + TALE
The algorithm is MARS, enhanced by:

The ternary simulation-based generalization method of TALE

The resulting DNF is Non-Disjoint

28

7/4/2023

29 of 42

Experimental Results

We compare HALL against existing AllSAT-CNF solvers

Benchmarks are combinational circuit (AIGER)

Each circuit is also converted to CNF (with standard encoding)

We evaluate runtime (Timeout of 3600s) and DNF size (number of cubes)

Also:

Multiple outputs combine to single-output (e.g., or, xor)
We separated Disjoint from Non-Disjoint solvers

29

7/4/2023

30 of 42

Benchmarks

Static Timing Analysis (STA) industrial set:

A general family (formula) with increasing size
sta_gen

EPFL combinational benchmark suite:

arithmetic_or, arithmetic_xor, random_control_or, random_control_xor

Random combinational circuit:

large_cir_or

30

7/4/2023

For our STA problem:

Result can be disjoint or non-disjoint

31 of 42

Solvers

31

7/4/2023

AllSAT-CNF (Toda [TS, JEA’16]):

BC (Non-Disjoint)
NBC (Disjoint)
BDD (Disjoint)

AllSAT-CT (HALL):

TALE (Non-Disjoint)
MARS (Disjoint and Non-Disjoint)
DUTY (Non-Disjoint)

32 of 42

Evaluation of the STA Benchmark Set

32

7/4/2023

N (Input size)	Disjoint
	MARS		NBC		BDD
	Time	Size	Time	Size	Time	Size
9	< 1	10	< 1	224	< 1	224
17	< 1	59	< 1	89600	< 1	89600
25	< 1	253	2.111	27582464	48.26	27582464
33	< 1	1315	570.897	7729971200	MO	-
37	9.808	59538	TO	-	MO	-
41	TO	-	TO	-	MO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

33 of 42

Evaluation of the STA Benchmark Set

33

7/4/2023

N (Input size)	Disjoint
	MARS		NBC		BDD
	Time	Size	Time	Size	Time	Size
9	< 1	10	< 1	224	< 1	224
17	< 1	59	< 1	89600	< 1	89600
25	< 1	253	2.111	27582464	48.26	27582464
33	< 1	1315	570.897	7729971200	MO	-
37	9.808	59538	TO	-	MO	-
41	TO	-	TO	-	MO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

34 of 42

Evaluation of the STA Benchmark Set

34

7/4/2023

N (Input size)	Disjoint
	MARS		NBC		BDD
	Time	Size	Time	Size	Time	Size
9	< 1	10	< 1	224	< 1	224
17	< 1	59	< 1	89600	< 1	89600
25	< 1	253	2.111	27582464	48.26	27582464
33	< 1	1315	570.897	7729971200	MO	-
37	9.808	59538	TO	-	MO	-
41	TO	-	TO	-	MO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

35 of 42

Evaluation of the STA Benchmark Set

35

7/4/2023

N (Input size)	Non-Disjoint
	TALE		MARS		DUTY		BC
	Time	Size	Time	Size	Time	Size	Time	Size
25	< 1	12	< 1	12	< 1	12	866.53	1026771
33	< 1	16	< 1	20	< 1	16	TO	-
2009	< 1	1004	< 1	1154	< 1	1004	TO	-
3009	< 1	1504	1.874	1990	< 1	1504	TO	-
5009	3.349	2504	9.83	3629	2.417	2504	TO	-
7009	7.886	3504	10.294	6098	4.625	3504	TO	-
9009	28.909	4504	84.817	6889	11.977	4504	TO	-
11009	56.877	5504	TO	-	23.0	5504	TO	-
13009	96.688	6504	50.361	13704	29.889	6504	TO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

36 of 42

Evaluation of the STA Benchmark Set

36

7/4/2023

N (Input size)	Non-Disjoint
	TALE		MARS		DUTY		BC
	Time	Size	Time	Size	Time	Size	Time	Size
25	< 1	12	< 1	12	< 1	12	866.53	1026771
33	< 1	16	< 1	20	< 1	16	TO	-
2009	< 1	1004	< 1	1154	< 1	1004	TO	-
3009	< 1	1504	1.874	1990	< 1	1504	TO	-
5009	3.349	2504	9.83	3629	2.417	2504	TO	-
7009	7.886	3504	10.294	6098	4.625	3504	TO	-
9009	28.909	4504	84.817	6889	11.977	4504	TO	-
11009	56.877	5504	TO	-	23.0	5504	TO	-
13009	96.688	6504	50.361	13704	29.889	6504	TO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

37 of 42

Evaluation of the STA Benchmark Set

37

7/4/2023

N (Input size)	Non-Disjoint
	TALE		MARS		DUTY		BC
	Time	Size	Time	Size	Time	Size	Time	Size
25	< 1	12	< 1	12	< 1	12	866.53	1026771
33	< 1	16	< 1	20	< 1	16	TO	-
2009	< 1	1004	< 1	1154	< 1	1004	TO	-
3009	< 1	1504	1.874	1990	< 1	1504	TO	-
5009	3.349	2504	9.83	3629	2.417	2504	TO	-
7009	7.886	3504	10.294	6098	4.625	3504	TO	-
9009	28.909	4504	84.817	6889	11.977	4504	TO	-
11009	56.877	5504	TO	-	23.0	5504	TO	-
13009	96.688	6504	50.361	13704	29.889	6504	TO	-

TO: Time-out

MO: Memory-out

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

38 of 42

Evaluation of the EPFL and Random Benchmarks

38

7/4/2023

Family	#Bench	Non-Disjoint				Disjoint
Family	#Bench	TALE	MARS	DUTY	BC	MARS	NBC	BDD
arithmetic_or	10	4	2	3	0	1	1	0
arithmetic_xor	10	0	0	0	0	0	1	0
random_control_or	10	9	9	9	4	7	4	4
random_control_xor	10	5	5	5	4	4	4	4
large_cir_or	20	16	7	16	0	7	0	0
Total	60	34	23	33	8	19	10	8

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

39 of 42

Evaluation of the EPFL and Random Benchmarks

39

7/4/2023

Family	#Bench	Non-Disjoint				Disjoint
Family	#Bench	TALE	MARS	DUTY	BC	MARS	NBC	BDD
arithmetic_or	10	4	2	3	0	1	1	0
arithmetic_xor	10	0	0	0	0	0	1	0
random_control_or	10	9	9	9	4	7	4	4
random_control_xor	10	5	5	5	4	4	4	4
large_cir_or	20	16	7	16	0	7	0	0
Total	60	34	23	33	8	19	10	8

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

40 of 42

Evaluation of the EPFL and Random Benchmarks

40

7/4/2023

Family	#Bench	Non-Disjoint				Disjoint
Family	#Bench	TALE	MARS	DUTY	BC	MARS	NBC	BDD
arithmetic_or	10	4	2	3	0	1	1	0
arithmetic_xor	10	0	0	0	0	0	1	0
random_control_or	10	9	9	9	4	7	4	4
random_control_xor	10	5	5	5	4	4	4	4
large_cir_or	20	16	7	16	0	7	0	0
Total	60	34	23	33	8	19	10	8

TALE: Ternary simulation

MARS: Dual-rail & MaxSAT

DUTY: TALE + MARS

41 of 42

Conclusion and Future Work

New dedicated AllSAT-CT algorithms

TALE (ternary-simulation)
MARS (dual-rail & MaxSAT)
DUTY (TALE+MARS)

Implemented in open-source tool HALL
HALL scales better than existing reduction to AllSAT-CNF

Future work:

Utilize other AllSAT-CNF methods (non-blocking) [GSY, FMCAD’04]
Dual value propagation in circuits [GB, AAAI’10]
Include dualiza in our experiments [MA,ICTAI‘18]

41

7/4/2023

42 of 42

Thank you for listening

Questions?