anishathalye / anishathalye/knox
input* assigns Bool but the rest of the SMT2 model expects `(_ BitVec 1)`
- Langage dominant
- Racket
- Étoiles
- 42
- Forks
- 2
- Métriques de merge des PR
- Aucune PR mergée en 30 j
Description
`input*` assigns a `Bool` value as a default value for all single value bitvectors when constructing `input` structure. This is a problem because in some cases the generate SMT2 model expects the value to be of type `(_ BitVec 1)`.
For example, if you translate the following program:
```SystemVerilog
module test_trans #(
parameter M = 1,
)
(
input clk,
input [(M * 1)-1: 0] x1,
input [(M * 1)-1: 0] x2,
output [((M * 1)-1):0] y,
output [((M * 1)-1):0] p
);
assign p = x1 & x2;
endmodule
```
using
```
read_verilog -sv -defer src/test_trans_p.sv
prep -flatten -top test_trans -nordff
write_smt2 -stdt run/test_trans_p.smt2
```
you get
```
; SMT-LIBv2 description generated by Yosys 0.46+124 (git sha1 d1695ad99, clang++ 14.0.0-1ubuntu1.1 -Og -fPIC)
; yosys-smt2-stdt
; yosys-smt2-module test_trans
(declare-datatype |test_trans_s| ((|test_trans_mk|
(|test_trans_is| Bool)
(|test_trans#0| Bool) ; \clk
(|test_trans#1| (_ BitVec 1)) ; \x1
(|test_trans#2| (_ BitVec 1)) ; \x2
(|test_trans#4| Bool) ; \y
)))
; yosys-smt2-input clk 1
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |test_trans_n clk| ((state |test_trans_s|)) Bool (|test_trans#0| state))
(define-fun |test_trans#3| ((state |test_trans_s|)) (_ BitVec 1) (bvand (|test_trans#1| state) (|test_trans#2| state))) ; \p
; yosys-smt2-output p 1
(define-fun |test_trans_n p| ((state |test_trans_s|)) Bool (= ((_ extract 0 0) (|test_trans#3| state)) #b1))
; yosys-smt2-input x1 1
; yosys-smt2-witness {"offset": 0, "path": ["\\x1"], "smtname": "x1", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |test_trans_n x1| ((state |test_trans_s|)) Bool (= ((_ extract 0 0) (|test_trans#1| state)) #b1))
; yosys-smt2-input x2 1
; yosys-smt2-witness {"offset": 0, "path": ["\\x2"], "smtname": "x2", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |test_trans_n x2| ((state |test_trans_s|)) Bool (= ((_ extract 0 0) (|test_trans#2| state)) #b1))
; yosys-smt2-output y 1
(define-fun |test_trans_n y| ((state |test_trans_s|)) Bool (|test_trans#4| state))
(define-fun |test_trans_a| ((state |test_trans_s|)) Bool true)
(define-fun |test_trans_u| ((state |test_trans_s|)) Bool true)
(define-fun |test_trans_i| ((state |test_trans_s|)) Bool true)
(define-fun |test_trans_h| ((state |test_trans_s|)) Bool true)
(define-fun |test_trans_t| ((state |test_trans_s|) (next_state |test_trans_s|)) Bool true) ; end of module test_trans
; yosys-smt2-topmod test_trans
; end of yosys output
```
Note that the type of `|test_trans#1|` and `|test_trans#2|`, which represent `x1` and `x2`, is `(_ BitVec 1)`. From this it follows that the rest of the model that uses `|test_trans#1|` or `|test_trans#2|` expects a value of type `(_ BitVec 1)` and not `Bool`.
If you run the following code, with the above SMT2 model:
```racket
#lang rosette
(require "test_trans_p.rkt")
(let* (
[st (new-zeroed-test_trans_s)]
[st (step (with-input st (input* 'x1 (bv 0 1))))])
(output-p (get-output st)))
```
you get the following error
```
[assert] bvand: expected bitvectors of same length
arguments: ((bv #b0 1) #f)
context...:
/home/zputrle/.local/share/racket/8.7/pkgs/rosette/rosette/base/core/exn.rkt:59:11: raise-exn:fail:svm:assert:core
/home/zputrle/.local/share/racket/8.7/pkgs/rosette/rosette/base/core/bitvector.rkt:174:0: safe-apply-2
/home/zputrle/.local/share/racket/8.7/pkgs/knox/yosys/memoize.rkt:23:2: memoized
/home/zputrle/.local/share/racket/8.7/pkgs/knox/yosys/memoize.rkt:41:30
/home/zputrle/.local/share/racket/8.7/pkgs/knox/yosys/memoize.rkt:23:2: memoized
.../private/map.rkt:40:19: loop
/home/zputrle/.local/share/racket/8.7/pkgs/knox/yosys/memoize.rkt:20:34
/home/zputrle/dev/rosette/SHD-FormalVerificationRec/dev/vrose/src/run_test_trans.rkt:23:0
body of "/home/zputrle/dev/rosette/SHD-FormalVerificationRec/dev/vrose/src/run_test_trans.rkt"
shell returned 1
```
As far as I can see, the reason for the error is that `input*` sets `x2` by default to `#f`. If I also assign a value of type `(_ BitVec 1)` to `x2` when calling `input*`, the code execute without an error.
I'm using the latest version of Knox (4dd42b5).
Note that Yosys has peculiar behavior for when it assigns `Bool` or `(_ BitVec 1)` type to a variable in the state structure when converting Verilog design to SMT2 model. If you use the same Verilog program but just replace the name of the variable `p` with `z`, it will assign the type `Bool` instead of `(_ BitVec 1)`. As far as I can see, the Yosys's `write_smt2` command [1], does not guarantee that single value vectors will always have type `Bool` in the state structure; but it does guarantee that this will be the case for all the getters (e.g. `|test_trans_n x2|`). (I'm was using Yosys 0.46+124 (git sha1 d1695ad99, clang++ 14.0.0-1ubuntu1.1 -Og -fPIC) when running the tests.)
[1] https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/write_smt2.html
Guide de contribution
Aucun guide de contribution indexé pour ce dépôt
Évaluation
Cette issue n'a pas encore été évaluée.