3 trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR
5 cat > chparam1.sv
<< "EOT"
16 parameter
[31:0] X
= 0
20 always @
* assert
(dout
!= X
);
23 bind top top_props
#(.X(123456789)) props (.*);
26 cat > chparam2.sv
<< "EOT"
28 parameter
[31:0] X
= 0
34 always @
* assert
(dout
!= 123456789);
38 if ..
/..
/yosys
-q -p 'verific -sv chparam1.sv'; then
39 ..
/..
/yosys
-q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
40 -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
41 -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
43 ..
/..
/yosys
-q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
44 -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
45 -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
47 ..
/..
/yosys
-q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
48 -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
49 -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'