mirror of https://github.com/YosysHQ/yosys.git
Remove too fragile smtlib2_module test
This compares the write_smt2 output pretty much verbatim, which contains auto generated private names and fixes an arbitrary ordering. The tested functionality is also covered by SBY tests which actually interpret the write_smt2 output using an SMT solver and thus are much more robust, so we can safely remove this test.
This commit is contained in:
Jannis Harder
parent
9f27923782
commit
2baa578d94
|
|
@ -1,96 +0,0 @@
|
|||
; SMT-LIBv2 description generated by Yosys $VERSION
|
||||
; yosys-smt2-module smtlib2
|
||||
(declare-sort |smtlib2_s| 0)
|
||||
(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
|
||||
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
|
||||
; yosys-smt2-input a 8
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
|
||||
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
|
||||
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
|
||||
; yosys-smt2-input b 8
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
|
||||
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
|
||||
; yosys-smt2-output add 8
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
|
||||
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
|
||||
(|a| (|smtlib2_n a| state))
|
||||
(|b| (|smtlib2_n b| state))
|
||||
)
|
||||
(bvadd a b)
|
||||
))
|
||||
; yosys-smt2-output eq 1
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
|
||||
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
|
||||
(|a| (|smtlib2_n a| state))
|
||||
(|b| (|smtlib2_n b| state))
|
||||
)
|
||||
(= a b)
|
||||
))
|
||||
; yosys-smt2-output sub 8
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
|
||||
(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
|
||||
(|a| (|smtlib2_n a| state))
|
||||
(|b| (|smtlib2_n b| state))
|
||||
)
|
||||
(bvadd a (bvneg b))
|
||||
))
|
||||
(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
|
||||
(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
|
||||
(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
|
||||
(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
|
||||
(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
|
||||
; yosys-smt2-module uut
|
||||
(declare-sort |uut_s| 0)
|
||||
(declare-fun |uut_is| (|uut_s|) Bool)
|
||||
; yosys-smt2-cell smtlib2 s
|
||||
; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"}
|
||||
(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
|
||||
(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
|
||||
(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
|
||||
(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
|
||||
; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
|
||||
(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
|
||||
; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
|
||||
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
|
||||
(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
|
||||
(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
|
||||
(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
|
||||
; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
|
||||
(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
|
||||
(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
|
||||
(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
|
||||
; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
|
||||
(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
|
||||
(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
|
||||
(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
|
||||
; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
|
||||
(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
|
||||
(define-fun |uut_a| ((state |uut_s|)) Bool (and
|
||||
(|uut_a 0| state)
|
||||
(|uut_a 1| state)
|
||||
(|uut_a 2| state)
|
||||
(|smtlib2_a| (|uut_h s| state))
|
||||
))
|
||||
(define-fun |uut_u| ((state |uut_s|)) Bool
|
||||
(|smtlib2_u| (|uut_h s| state))
|
||||
)
|
||||
(define-fun |uut_i| ((state |uut_s|)) Bool
|
||||
(|smtlib2_i| (|uut_h s| state))
|
||||
)
|
||||
(define-fun |uut_h| ((state |uut_s|)) Bool (and
|
||||
(= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
|
||||
(= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
|
||||
(= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
|
||||
(= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
|
||||
(= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
|
||||
(= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
|
||||
(|smtlib2_h| (|uut_h s| state))
|
||||
))
|
||||
(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
|
||||
(= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
|
||||
(= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
|
||||
(|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
|
||||
)) ; end of module uut
|
||||
; yosys-smt2-topmod uut
|
||||
; end of yosys output
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
set -ex
|
||||
../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
|
||||
sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/ *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
|
||||
diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
(* smtlib2_module *)
|
||||
module smtlib2(a, b, add, sub, eq);
|
||||
input [7:0] a, b;
|
||||
(* smtlib2_comb_expr = "(bvadd a b)" *)
|
||||
output [7:0] add;
|
||||
(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
|
||||
output [7:0] sub;
|
||||
(* smtlib2_comb_expr = "(= a b)" *)
|
||||
output eq;
|
||||
endmodule
|
||||
|
||||
(* top *)
|
||||
module uut;
|
||||
wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2;
|
||||
wire eq;
|
||||
|
||||
assign add2 = a + b;
|
||||
assign sub2 = a - b;
|
||||
|
||||
smtlib2 s (
|
||||
.a(a),
|
||||
.b(b),
|
||||
.add(add),
|
||||
.sub(sub),
|
||||
.eq(eq)
|
||||
);
|
||||
|
||||
always @* begin
|
||||
assert(add == add2);
|
||||
assert(sub == sub2);
|
||||
assert(eq == (a == b));
|
||||
end
|
||||
endmodule
|
||||
Loading…
Reference in New Issue