3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-21 06:35:49 +00:00

Merge from upstream

This commit is contained in:
Akash Levy 2025-08-21 17:56:55 -07:00
commit e54fa487b8
29 changed files with 1314 additions and 793 deletions

View file

@ -0,0 +1,30 @@
read_verilog <<EOT
module half_clock (CLK, Q, magic);
input CLK;
output reg Q = 0;
input magic;
always @(posedge CLK)
Q <= ~Q;
endmodule
EOT
proc
design -save half_clock
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
abstract -state -initstates 1 */Q
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
design -load half_clock
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 2 Q 0 -set-at 3 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 3 Q 0 -set-at 4 Q 0
abstract -state -initstates 2 */Q
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0
sat -set-init-undef -enable_undef -verify -seq 5 -set-at 1 Q 0 -set-at 2 Q 0 -set-at 3 Q 0
sat -set-init-undef -enable_undef -falsify -seq 5 -set-at 3 Q 0 -set-at 4 Q 0

View file

@ -39,3 +39,18 @@ select -assert-count 1 w:d__1
select -assert-count 1 w:_e
select -assert-count 1 w:wire_
select -assert-count 1 w:$add$<<EOF:*$1_Y
# Ports are updated during rename
design -reset
read_verilog << EOT
module top(output \$e );
submod \a$ (\$e );
endmodule
module submod(output \a[0] );
assign \a[0] = 0;
endmodule
EOT
rename -unescape
check