smt « test - sail - Formal specification language for ISAs

Mode	Name	Size
-rw-r--r--	add_overflow.sat.sail	192	log plain
-rw-r--r--	add_overflow.unsat.sail	156	log plain
-rw-r--r--	arith.unsat.sail	812	log plain
-rw-r--r--	arith_C128FL.unsat.sail	867	log plain
-rw-r--r--	arith_C64C32CB.unsat.sail	694	log plain
-rw-r--r--	arith_FFL_1.unsat.sail	301	log plain
-rw-r--r--	arith_FFL_2.unsat.sail	390	log plain
-rw-r--r--	arith_FFL_3.unsat.sail	397	log plain
-rw-r--r--	arith_FFL_4.unsat.sail	326	log plain
-rw-r--r--	arith_FFL_5.unsat.sail	413	log plain
-rw-r--r--	arith_LC32L.unsat.sail	251	log plain
-rw-r--r--	arith_LC32L_1.unsat.sail	251	log plain
-rw-r--r--	arith_LC32L_2.unsat.sail	238	log plain
-rw-r--r--	arith_LC32L_3.unsat.sail	246	log plain
-rw-r--r--	arith_LC32L_4.unsat.sail	268	log plain
-rw-r--r--	arith_LCBL.unsat.sail	830	log plain
-rw-r--r--	arith_LFL.unsat.sail	844	log plain
-rw-r--r--	assembly_mapping.sat.sail	1294	log plain
-rw-r--r--	basic_1.sat.sail	368	log plain
-rw-r--r--	basic_1.unsat.sail	382	log plain
-rw-r--r--	basic_2.sat.sail	368	log plain
-rw-r--r--	basic_2.unsat.sail	368	log plain
-rw-r--r--	ccheri_regression1.unsat.sail	622	log plain
-rw-r--r--	clear_overflow_regression.unsat.sail	2291	log plain
-rw-r--r--	concat_prop.unsat.sail	427	log plain
-rw-r--r--	concat_prop128.unsat.sail	427	log plain
-rw-r--r--	encdec.sat.sail	1275	log plain
-rw-r--r--	exception.unsat.sail	241	log plain
-rw-r--r--	exception_2.unsat.sail	310	log plain
-rw-r--r--	exception_3.unsat.sail	332	log plain
-rw-r--r--	foreach_simple.unsat.sail	173	log plain
-rw-r--r--	foreach_simple_2.unsat.sail	184	log plain
-rw-r--r--	gvector.unsat.sail	294	log plain
-rw-r--r--	gvector_trivial.unsat.sail	177	log plain
-rw-r--r--	inline_regression.unsat.sail	315	log plain
-rw-r--r--	inline_test_1.unsat.sail	348	log plain
-rw-r--r--	let_intervene.unsat.sail	211	log plain
-rw-r--r--	load_store_dep.sat.sail	275	log plain
-rw-r--r--	lt_int_irrefl.unsat.sail	107	log plain
-rw-r--r--	lt_int_trans.unsat.sail	147	log plain
-rw-r--r--	lteq_int_antisym.unsat.sail	140	log plain
-rw-r--r--	lteq_int_def.unsat.sail	140	log plain
-rw-r--r--	lteq_int_refl.unsat.sail	98	log plain
-rw-r--r--	lteq_int_trans.unsat.sail	150	log plain
-rw-r--r--	lzcnt.unsat.sail	363	log plain
-rw-r--r--	lzcnt_2.unsat.sail	386	log plain
-rw-r--r--	lzcnt_3.unsat.sail	372	log plain
-rw-r--r--	match_fail.sat.sail	148	log plain
-rw-r--r--	match_fail_query_1.sat.sail	176	log plain
-rw-r--r--	match_fail_query_2.sat.sail	173	log plain
-rw-r--r--	mem_builtins.unsat.sail	258	log plain
-rw-r--r--	minmax.unsat.sail	397	log plain
-rw-r--r--	minmax_1.sat.sail	229	log plain
-rw-r--r--	minmax_2.sat.sail	229	log plain
-rw-r--r--	order.unsat.sail	1054	log plain
-rw-r--r--	real.unsat.sail	565	log plain
-rw-r--r--	reg_ref.unsat.sail	348	log plain
-rw-r--r--	revrev_endianness.unsat.sail	756	log plain
-rw-r--r--	revrev_endianness2.unsat.sail	621	log plain
-rwxr-xr-x	run_tests.py	1755	log plain
-rw-r--r--	rv_add_0.sat.sail	4154	log plain
-rw-r--r--	rv_add_0.unsat.sail	4165	log plain
-rw-r--r--	rv_add_1.sat.sail	4105	log plain
-rw-r--r--	rv_add_1.unsat.sail	4115	log plain
-rw-r--r--	rv_add_decode.unsat.sail	633	log plain
-rw-r--r--	rv_reg_rw.unsat.sail	3448	log plain
-rw-r--r--	sail_mask.unsat.sail	188	log plain
-rw-r--r--	sail_mask_2.unsat.sail	199	log plain
-rw-r--r--	sail_mask_3.unsat.sail	214	log plain
-rw-r--r--	sail_mask_4.unsat.sail	294	log plain
-rw-r--r--	sail_mask_5.unsat.sail	294	log plain
-rw-r--r--	shift_or_concat.unsat.sail	282	log plain
-rw-r--r--	shift_or_concat128.unsat.sail	287	log plain
-rw-r--r--	shift_or_concat4.unsat.sail	277	log plain
-rw-r--r--	shift_or_concat4_2.unsat.sail	290	log plain
-rw-r--r--	shift_or_concat_1.sat.sail	282	log plain
-rw-r--r--	shift_or_concat_2.sat.sail	282	log plain
-rw-r--r--	shiftr_zero_1.sat.sail	177	log plain
-rw-r--r--	shiftr_zero_1.unsat.sail	177	log plain
-rw-r--r--	sign_extend.unsat.sail	266	log plain
-rw-r--r--	sign_extend_2.unsat.sail	265	log plain
-rw-r--r--	sqrt.sat.sail	146	log plain
-rw-r--r--	sqrt.unsat.sail	125	log plain
-rw-r--r--	store_load.sat.sail	275	log plain
-rw-r--r--	store_load_scattered.sat.sail	690	log plain
-rw-r--r--	string.sat.sail	296	log plain
-rw-r--r--	string.unsat.sail	298	log plain
d---------	test	37	log plain
-rw-r--r--	tl_let_shadow.sat.sail	143	log plain
-rw-r--r--	toplevel_let.unsat.sail	174	log plain
-rw-r--r--	toplevel_let_trivial.unsat.sail	130	log plain
-rw-r--r--	trivial.sat.sail	96	log plain
-rw-r--r--	trivial.unsat.sail	95	log plain
-rw-r--r--	trivial_assert.sat.sail	137	log plain
-rw-r--r--	trivial_assert_2.unsat.sail	160	log plain
-rw-r--r--	trivial_funcall.sat.sail	132	log plain
-rw-r--r--	trivial_return.sat.sail	111	log plain
-rw-r--r--	trivial_return.unsat.sail	118	log plain
-rw-r--r--	update_access.unsat.sail	227	log plain
-rw-r--r--	update_subrange.unsat.sail	240	log plain
-rw-r--r--	write_ref.sat.sail	510	log plain
-rw-r--r--	write_ref.unsat.sail	510	log plain
-rw-r--r--	zeros_1.sat.sail	118	log plain
-rw-r--r--	zeros_1.unsat.sail	118	log plain
-rw-r--r--	zeros_2.sat.sail	136	log plain
-rw-r--r--	zeros_2.unsat.sail	117	log plain
-rw-r--r--	zeros_3.sat.sail	148	log plain
-rw-r--r--	zeros_3.unsat.sail	138	log plain
-rw-r--r--	zeros_4.unsat.sail	138	log plain
-rw-r--r--	zeros_ones.unsat.sail	231	log plain