aboutsummaryrefslogtreecommitdiffstats
path: root/examples/smtbmc/Makefile
blob: 61994f942fb524c07fc77072fa3ec4013b9c829e (plain) 
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

all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9

demo1: demo1.smt2
	yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
	yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2

demo2: demo2.smt2
	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2
	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
	vvp demo2_tb +vcd=demo2_tb.vcd

demo3: demo3.smt2
	yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2

demo4: demo4.smt2
	yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2

demo5: demo5.smt2
	yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2

demo6: demo6.smt2
	yosys-smtbmc -t 1 demo6.smt2

demo7: demo7.smt2
	yosys-smtbmc -t 10 demo7.smt2

demo8: demo8.smt2
	yosys-smtbmc -s z3 -t 1 -g demo8.smt2

demo9: demo9.smt2
	yosys-smtbmc -s z3 -t 1 -g demo9.smt2

demo1.smt2: demo1.v
	yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'

demo2.smt2: demo2.v
	yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires demo2.smt2'

demo3.smt2: demo3.v
	yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires demo3.smt2'

demo4.smt2: demo4.v
	yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'

demo5.smt2: demo5.v
	yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'

demo6.smt2: demo6.v
	yosys -ql demo6.yslog -p 'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'

demo7.smt2: demo7.v
	yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2'

demo8.smt2: demo8.v
	yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2'

demo9.smt2: demo9.v
	yosys -ql demo9.yslog -p 'read_verilog -formal demo9.v; prep -top demo9 -nordff; write_smt2 -stbv -wires demo9.smt2'

clean:
	rm -f demo1.yslog demo1.smt2 demo1.vcd
	rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
	rm -f demo3.yslog demo3.smt2 demo3.vcd
	rm -f demo4.yslog demo4.smt2 demo4.vcd
	rm -f demo5.yslog demo5.smt2 demo5.vcd
	rm -f demo6.yslog demo6.smt2
	rm -f demo7.yslog demo7.smt2
	rm -f demo8.yslog demo8.smt2
	rm -f demo9.yslog demo9.smt2

.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 clean
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-17 06:11:38 +0000
d(self): raise exceptions.UnsupportedAlgorithm( "ChaCha20Poly1305 is not supported by this version of OpenSSL", exceptions._Reasons.UNSUPPORTED_CIPHER ) utils._check_bytes("key", key) if len(key) != 32: raise ValueError("ChaCha20Poly1305 key must be 32 bytes.") self._key = key @classmethod def generate_key(cls): return os.urandom(32) def encrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) return aead._encrypt( backend, self, nonce, data, associated_data, 16 ) def decrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) return aead._decrypt( backend, self, nonce, data, associated_data, 16 ) def _check_params(self, nonce, data, associated_data): utils._check_bytes("nonce", nonce) utils._check_bytes("data", data) utils._check_bytes("associated_data", associated_data) if len(nonce) != 12: raise ValueError("Nonce must be 12 bytes") class AESCCM(object): def __init__(self, key, tag_length=16): utils._check_bytes("key", key) if len(key) not in (16, 24, 32): raise ValueError("AESCCM key must be 128, 192, or 256 bits.") self._key = key if not isinstance(tag_length, int): raise TypeError("tag_length must be an integer") if tag_length not in (4, 6, 8, 12, 14, 16): raise ValueError("Invalid tag_length") self._tag_length = tag_length if not backend.aead_cipher_supported(self): raise exceptions.UnsupportedAlgorithm( "AESCCM is not supported by this version of OpenSSL", exceptions._Reasons.UNSUPPORTED_CIPHER ) @classmethod def generate_key(cls, bit_length): if not isinstance(bit_length, int): raise TypeError("bit_length must be an integer") if bit_length not in (128, 192, 256): raise ValueError("bit_length must be 128, 192, or 256") return os.urandom(bit_length // 8) def encrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) self._validate_lengths(nonce, len(data)) return aead._encrypt( backend, self, nonce, data, associated_data, self._tag_length ) def decrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) return aead._decrypt( backend, self, nonce, data, associated_data, self._tag_length ) def _validate_lengths(self, nonce, data_len): # For information about computing this, see # https://tools.ietf.org/html/rfc3610#section-2.1 l = 15 - len(nonce) if 2 ** (8 * l) < data_len: raise ValueError("Nonce too long for data") def _check_params(self, nonce, data, associated_data): utils._check_bytes("nonce", nonce) utils._check_bytes("data", data) utils._check_bytes("associated_data", associated_data) if not 7 <= len(nonce) <= 13: raise ValueError("Nonce must be between 7 and 13 bytes") class AESGCM(object): def __init__(self, key): utils._check_bytes("key", key) if len(key) not in (16, 24, 32): raise ValueError("AESGCM key must be 128, 192, or 256 bits.") self._key = key @classmethod def generate_key(cls, bit_length): if not isinstance(bit_length, int): raise TypeError("bit_length must be an integer") if bit_length not in (128, 192, 256): raise ValueError("bit_length must be 128, 192, or 256") return os.urandom(bit_length // 8) def encrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) return aead._encrypt( backend, self, nonce, data, associated_data, 16 ) def decrypt(self, nonce, data, associated_data): if associated_data is None: associated_data = b"" self._check_params(nonce, data, associated_data) return aead._decrypt( backend, self, nonce, data, associated_data, 16 ) def _check_params(self, nonce, data, associated_data): utils._check_bytes("nonce", nonce) utils._check_bytes("data", data) utils._check_bytes("associated_data", associated_data)
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-17 06:11:38 +0000