libre-chip/cpu
3
0
Fork 2
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

tests/units_formal: test more instructions
All checks were successful
/ test (pull_request) Successful in 56m57s
Details

Browse source
This commit is contained in:
Jacob Lifshay 2026-06-17 20:00:20 -07:00
parent d38bc786a7
commit ad9ec46aca
Signed by: programmerjake
SSH key fingerprint: SHA256:HnFTLGpSm4Q4Fj502oCFisjZSoakwEuTsJJMSke63RQ
4 changed files with 551326 additions and 119 deletions
Download patch file Download diff file Expand all files Collapse all files

500
crates/cpu/tests/expected/units_formal_power_isa_add_sim.vcd generated
View file

@ -9,6 +9,7 @@ $var wire 64 @$@j=$ any_const_4 $end
$var wire 64 @$@j=% any_const_5 $end
$var wire 64 @$@j=& any_const_6 $end
$var wire 64 @$@j=' any_const_7 $end
$var wire 1 @$@j=( any_const_8 $end
$var wire 1 n$)=T ran $end
$scope struct cd $end
$var wire 1 mAPf1 clk $end
@ -1363,6 +1364,13 @@ $var wire 5 '=~,@ MLS_D_RT_5 $end
$scope struct power_isa_gpr_or_zero_reg_2 $end
$var wire 8 ?rD:V" value $end
$upscope $end
$scope struct power_isa_gpr_or_zero_reg_3 $end
$var wire 8 ?rD:V# value $end
$upscope $end
$var wire 1 {!]++ DX_d2_1 $end
$var wire 10 bj=V` DX_d0_10 $end
$var wire 5 ^98rl DX_d1_5 $end
$var wire 5 dmHRS DX_RT_5 $end
$var wire 5 VT+LS XO_RB_5 $end
$var wire 5 n'8X< XO_RA_5 $end
$var wire 5 /')9{ XO_RT_5 $end
@ -1406,28 +1414,18 @@ $var string 1 k^+pu$ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_5 $end
$var string 1 #a]5!% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_5 $end
$var string 1 k^+pu% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_6 $end
$var string 1 #a]5!& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_6 $end
$var string 1 k^+pu& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_7 $end
$var string 1 #a]5!' \$tag $end
$scope struct flag_reg_0_5 $end
$var string 1 #a]5!% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
@ -1436,8 +1434,8 @@ $var string 1 k^+pu' \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_8 $end
$var string 1 #a]5!( \$tag $end
$scope struct flag_reg_0_6 $end
$var string 1 #a]5!& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
@ -1446,6 +1444,191 @@ $var string 1 k^+pu( \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_7 $end
$var string 1 #a]5!' \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_9 $end
$var string 1 k^+pu) \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_8 $end
$var string 1 #a]5!( \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_10 $end
$var string 1 k^+pu* \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_11 $end
$var string 1 k^+pu+ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_9 $end
$var string 1 #a]5!) \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_12 $end
$var string 1 k^+pu, \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_10 $end
$var string 1 #a]5!* \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_13 $end
$var string 1 k^+pu- \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_11 $end
$var string 1 #a]5!+ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_14 $end
$var string 1 k^+pu. \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_12 $end
$var string 1 #a]5!, \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_15 $end
$var string 1 k^+pu/ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_13 $end
$var string 1 #a]5!- \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_16 $end
$var string 1 k^+pu0 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_14 $end
$var string 1 #a]5!. \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_17 $end
$var string 1 k^+pu1 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_15 $end
$var string 1 #a]5!/ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_18 $end
$var string 1 k^+pu2 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_16 $end
$var string 1 #a]5!0 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_19 $end
$var string 1 k^+pu3 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_17 $end
$var string 1 #a]5!1 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_20 $end
$var string 1 k^+pu4 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_18 $end
$var string 1 #a]5!2 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_21 $end
$var string 1 k^+pu5 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_19 $end
$var string 1 #a]5!3 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_22 $end
$var string 1 k^+pu6 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_20 $end
$var string 1 #a]5!4 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_23 $end
$var string 1 k^+pu7 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_21 $end
$var string 1 #a]5!5 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_24 $end
$var string 1 k^+pu8 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_22 $end
$var string 1 #a]5!6 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_25 $end
$var string 1 k^+pu9 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_23 $end
$var string 1 #a]5!7 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_26 $end
$var string 1 k^+pu: \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_24 $end
$var string 1 #a]5!8 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_27 $end
$var string 1 k^+pu; \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$upscope $end
$scope struct decoder_input $end
$var wire 32 x,~Jt \0 $end
@ -15214,6 +15397,8 @@ $var wire 1 O9nl\ matched_any_case $end
$var wire 1 2J><` matched_case_addi $end
$var wire 1 F[XQ_ matched_case_paddi $end
$var wire 1 F[XQ_" matched_case_paddi_2 $end
$var wire 1 zYEiT matched_case_addis $end
$var wire 1 -="Wg matched_case_addpcis $end
$var wire 1 f](?M matched_case_add $end
$var wire 1 6@6XS \matched_case_add. $end
$var wire 1 KbSE, matched_case_addo $end
@ -15222,8 +15407,28 @@ $var wire 1 >{-\6 matched_case_addc $end
$var wire 1 dL::r \matched_case_addc. $end
$var wire 1 [Cj%o matched_case_addco $end
$var wire 1 Bo#P' \matched_case_addco. $end
$var wire 1 %B}aF matched_case_adde $end
$var wire 1 Wq?29 \matched_case_adde. $end
$var wire 1 n!{wU matched_case_addeo $end
$var wire 1 Vx+<b \matched_case_addeo. $end
$var wire 1 c*1&z matched_case_subf $end
$var wire 1 ,MvJK \matched_case_subf. $end
$var wire 1 |hLD> matched_case_subfo $end
$var wire 1 4{K<B \matched_case_subfo. $end
$var wire 1 lhv\- matched_case_subfc $end
$var wire 1 ~o?\W \matched_case_subfc. $end
$var wire 1 U+v"6 matched_case_subfco $end
$var wire 1 \%hAd \matched_case_subfco. $end
$var wire 1 zNlG} matched_case_subfe $end
$var wire 1 Y^=~a \matched_case_subfe. $end
$var wire 1 ^$mZ< matched_case_subfeo $end
$var wire 1 K+"Lg \matched_case_subfeo. $end
$var wire 1 ;UoIk matched_case_addic $end
$var wire 1 g:;Z_ \matched_case_addic. $end
$var wire 1 pAfEx matched_case_subfic $end
$var wire 64 <$d:7 input_r3 $end
$var wire 64 h<mmR input_r4 $end
$var wire 1 %^<Il input_ca $end
$scope struct output_reg $end
$scope struct regs $end
$scope struct regs $end
@ -15536,14 +15741,92 @@ $upscope $end
$var wire 16 Hd*94 addi_imm $end
$var wire 34 5bo?w paddi_imm $end
$var wire 34 5bo?w" paddi_imm_2 $end
$var string 1 <gfVf add_expected_out $end
$var string 1 <gfVf" add_expected_out_2 $end
$var string 1 <gfVf# add_expected_out_3 $end
$var string 1 <gfVf$ add_expected_out_4 $end
$var string 1 <gfVf% add_expected_out_5 $end
$var string 1 <gfVf& add_expected_out_6 $end
$var string 1 <gfVf' add_expected_out_7 $end
$var string 1 <gfVf( add_expected_out_8 $end
$var wire 16 ~W%v& addis_imm $end
$var wire 10 ei=V2 addpcis_d0 $end
$var wire 5 09o]U addpcis_d1 $end
$var wire 1 3E]&t addpcis_d2 $end
$var wire 16 N<`^[ addpcis_d $end
$var wire 64 .PpG. add_sub_add_in0 $end
$var wire 1 !>=Fa add_sub_ca_in $end
$var string 1 ;Mki5 add_sub_expected_out $end
$var wire 64 .PpG." add_sub_add_in0_2 $end
$var wire 1 !>=Fa" add_sub_ca_in_2 $end
$var string 1 ;Mki5" add_sub_expected_out_2 $end
$var wire 64 .PpG.# add_sub_add_in0_3 $end
$var wire 1 !>=Fa# add_sub_ca_in_3 $end
$var string 1 ;Mki5# add_sub_expected_out_3 $end
$var wire 64 .PpG.$ add_sub_add_in0_4 $end
$var wire 1 !>=Fa$ add_sub_ca_in_4 $end
$var string 1 ;Mki5$ add_sub_expected_out_4 $end
$var wire 64 .PpG.% add_sub_add_in0_5 $end
$var wire 1 !>=Fa% add_sub_ca_in_5 $end
$var string 1 ;Mki5% add_sub_expected_out_5 $end
$var wire 64 .PpG.& add_sub_add_in0_6 $end
$var wire 1 !>=Fa& add_sub_ca_in_6 $end
$var string 1 ;Mki5& add_sub_expected_out_6 $end
$var wire 64 .PpG.' add_sub_add_in0_7 $end
$var wire 1 !>=Fa' add_sub_ca_in_7 $end
$var string 1 ;Mki5' add_sub_expected_out_7 $end
$var wire 64 .PpG.( add_sub_add_in0_8 $end
$var wire 1 !>=Fa( add_sub_ca_in_8 $end
$var string 1 ;Mki5( add_sub_expected_out_8 $end
$var wire 64 .PpG.) add_sub_add_in0_9 $end
$var wire 1 !>=Fa) add_sub_ca_in_9 $end
$var string 1 ;Mki5) add_sub_expected_out_9 $end
$var wire 64 .PpG.* add_sub_add_in0_10 $end
$var wire 1 !>=Fa* add_sub_ca_in_10 $end
$var string 1 ;Mki5* add_sub_expected_out_10 $end
$var wire 64 .PpG.+ add_sub_add_in0_11 $end
$var wire 1 !>=Fa+ add_sub_ca_in_11 $end
$var string 1 ;Mki5+ add_sub_expected_out_11 $end
$var wire 64 .PpG., add_sub_add_in0_12 $end
$var wire 1 !>=Fa, add_sub_ca_in_12 $end
$var string 1 ;Mki5, add_sub_expected_out_12 $end
$var wire 64 .PpG.- add_sub_add_in0_13 $end
$var wire 1 !>=Fa- add_sub_ca_in_13 $end
$var string 1 ;Mki5- add_sub_expected_out_13 $end
$var wire 64 .PpG.. add_sub_add_in0_14 $end
$var wire 1 !>=Fa. add_sub_ca_in_14 $end
$var string 1 ;Mki5. add_sub_expected_out_14 $end
$var wire 64 .PpG./ add_sub_add_in0_15 $end
$var wire 1 !>=Fa/ add_sub_ca_in_15 $end
$var string 1 ;Mki5/ add_sub_expected_out_15 $end
$var wire 64 .PpG.0 add_sub_add_in0_16 $end
$var wire 1 !>=Fa0 add_sub_ca_in_16 $end
$var string 1 ;Mki50 add_sub_expected_out_16 $end
$var wire 64 .PpG.1 add_sub_add_in0_17 $end
$var wire 1 !>=Fa1 add_sub_ca_in_17 $end
$var string 1 ;Mki51 add_sub_expected_out_17 $end
$var wire 64 .PpG.2 add_sub_add_in0_18 $end
$var wire 1 !>=Fa2 add_sub_ca_in_18 $end
$var string 1 ;Mki52 add_sub_expected_out_18 $end
$var wire 64 .PpG.3 add_sub_add_in0_19 $end
$var wire 1 !>=Fa3 add_sub_ca_in_19 $end
$var string 1 ;Mki53 add_sub_expected_out_19 $end
$var wire 64 .PpG.4 add_sub_add_in0_20 $end
$var wire 1 !>=Fa4 add_sub_ca_in_20 $end
$var string 1 ;Mki54 add_sub_expected_out_20 $end
$var wire 64 .PpG.5 add_sub_add_in0_21 $end
$var wire 1 !>=Fa5 add_sub_ca_in_21 $end
$var string 1 ;Mki55 add_sub_expected_out_21 $end
$var wire 64 .PpG.6 add_sub_add_in0_22 $end
$var wire 1 !>=Fa6 add_sub_ca_in_22 $end
$var string 1 ;Mki56 add_sub_expected_out_22 $end
$var wire 64 .PpG.7 add_sub_add_in0_23 $end
$var wire 1 !>=Fa7 add_sub_ca_in_23 $end
$var string 1 ;Mki57 add_sub_expected_out_23 $end
$var wire 64 .PpG.8 add_sub_add_in0_24 $end
$var wire 1 !>=Fa8 add_sub_ca_in_24 $end
$var string 1 ;Mki58 add_sub_expected_out_24 $end
$var wire 16 .-Zk( addic_subfic_imm $end
$var wire 64 $a0'K addic_subfic_in $end
$var string 1 4CV)U addic_subfic_expected_out $end
$var wire 16 .-Zk(" addic_subfic_imm_2 $end
$var wire 64 $a0'K" addic_subfic_in_2 $end
$var string 1 4CV)U" addic_subfic_expected_out_2 $end
$var wire 16 .-Zk(# addic_subfic_imm_3 $end
$var wire 64 $a0'K# addic_subfic_in_3 $end
$var string 1 4CV)U# addic_subfic_expected_out_3 $end
$upscope $end
$enddefinitions $end
$dumpvars
@ -16720,6 +17003,11 @@ b0 5]QZg
b0 pQ'}$
b0 '=~,@
b0 ?rD:V"
b0 ?rD:V#
0{!]++
b0 bj=V`
b0 ^98rl
b0 dmHRS
b0 VT+LS
b0 n'8X<
b0 /')9{
@ -16731,14 +17019,49 @@ sHdlSome\x20(1) #a]5!#
sHdlNone\x20(0) k^+pu#
sHdlSome\x20(1) #a]5!$
sHdlSome\x20(1) k^+pu$
sHdlNone\x20(0) #a]5!%
sHdlNone\x20(0) k^+pu%
sHdlNone\x20(0) #a]5!&
sHdlSome\x20(1) k^+pu&
sHdlSome\x20(1) #a]5!'
sHdlNone\x20(0) #a]5!%
sHdlNone\x20(0) k^+pu'
sHdlSome\x20(1) #a]5!(
sHdlNone\x20(0) #a]5!&
sHdlSome\x20(1) k^+pu(
sHdlSome\x20(1) #a]5!'
sHdlNone\x20(0) k^+pu)
sHdlSome\x20(1) #a]5!(
sHdlSome\x20(1) k^+pu*
sHdlNone\x20(0) k^+pu+
sHdlNone\x20(0) #a]5!)
sHdlNone\x20(0) k^+pu,
sHdlNone\x20(0) #a]5!*
sHdlSome\x20(1) k^+pu-
sHdlSome\x20(1) #a]5!+
sHdlNone\x20(0) k^+pu.
sHdlSome\x20(1) #a]5!,
sHdlSome\x20(1) k^+pu/
sHdlNone\x20(0) #a]5!-
sHdlNone\x20(0) k^+pu0
sHdlNone\x20(0) #a]5!.
sHdlSome\x20(1) k^+pu1
sHdlSome\x20(1) #a]5!/
sHdlNone\x20(0) k^+pu2
sHdlSome\x20(1) #a]5!0
sHdlSome\x20(1) k^+pu3
sHdlNone\x20(0) #a]5!1
sHdlNone\x20(0) k^+pu4
sHdlNone\x20(0) #a]5!2
sHdlSome\x20(1) k^+pu5
sHdlSome\x20(1) #a]5!3
sHdlNone\x20(0) k^+pu6
sHdlSome\x20(1) #a]5!4
sHdlSome\x20(1) k^+pu7
sHdlNone\x20(0) #a]5!5
sHdlNone\x20(0) k^+pu8
sHdlNone\x20(0) #a]5!6
sHdlSome\x20(1) k^+pu9
sHdlSome\x20(1) #a]5!7
sHdlNone\x20(0) k^+pu:
sHdlSome\x20(1) #a]5!8
sHdlSome\x20(1) k^+pu;
b0 x,~Jt
sHdlNone\x20(0) \L:8?
b0 sD<$[
@ -23137,6 +23460,8 @@ b1000000000100 @$@j=%
02J><`
0F[XQ_
0F[XQ_"
0zYEiT
0-="Wg
1f](?M
06@6XS
0KbSE,
@ -23145,10 +23470,31 @@ b1000000000100 @$@j=%
0dL::r
0[Cj%o
0Bo#P'
0%B}aF
0Wq?29
0n!{wU
0Vx+<b
0c*1&z
0,MvJK
0|hLD>
04{K<B
0lhv\-
0~o?\W
0U+v"6
0\%hAd
0zNlG}
0Y^=~a
0^$mZ<
0K+"Lg
0;UoIk
0g:;Z_
0pAfEx
b1001000110100 <$d:7
b1001000110100 @$@j=&
b1001000110100 h<mmR
b1001000110100 @$@j='
0%^<Il
0@$@j=(
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} qfRqB
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} 1O=Dy
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} Mhd"F
@ -23429,14 +23775,92 @@ sPhantomConst({\"units\":[{\"kind\":\"AluBranch\",\"max_in_flight\":null}],\"out
b10001000010100 Hd*94
b1100100010000101000000000000000000 5bo?w
b1100100010000101000000000000000000 5bo?w"
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf"
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf#
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf$
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf%
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf&
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf'
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} <gfVf(
b10001000010100 ~W%v&
b10001000 ei=V2
b11 09o]U
03E]&t
b10001000000110 N<`^[
b1001000110100 .PpG.
0!>=Fa
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5
b1001000110100 .PpG."
0!>=Fa"
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5"
b1001000110100 .PpG.#
0!>=Fa#
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5#
b1001000110100 .PpG.$
0!>=Fa$
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5$
b1001000110100 .PpG.%
0!>=Fa%
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5%
b1001000110100 .PpG.&
0!>=Fa&
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5&
b1001000110100 .PpG.'
0!>=Fa'
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5'
b1001000110100 .PpG.(
0!>=Fa(
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5(
b1001000110100 .PpG.)
0!>=Fa)
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5)
b1001000110100 .PpG.*
0!>=Fa*
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5*
b1001000110100 .PpG.+
0!>=Fa+
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5+
b1001000110100 .PpG.,
0!>=Fa,
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5,
b1001000110100 .PpG.-
0!>=Fa-
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5-
b1001000110100 .PpG..
0!>=Fa.
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5.
b1001000110100 .PpG./
0!>=Fa/
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki5/
b1001000110100 .PpG.0
0!>=Fa0
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki50
b1001000110100 .PpG.1
0!>=Fa1
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki51
b1001000110100 .PpG.2
0!>=Fa2
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki52
b1001000110100 .PpG.3
0!>=Fa3
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki53
b1001000110100 .PpG.4
0!>=Fa4
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki54
b1001000110100 .PpG.5
0!>=Fa5
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki55
b1001000110100 .PpG.6
0!>=Fa6
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki56
b1001000110100 .PpG.7
0!>=Fa7
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki57
b1001000110100 .PpG.8
0!>=Fa8
sPRegValue\x20{\x20int_fp:\x200x2468_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} ;Mki58
b10001000010100 .-Zk(
b1001000110100 $a0'K
sPRegValue\x20{\x20int_fp:\x200x3448_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} 4CV)U
b10001000010100 .-Zk("
b1001000110100 $a0'K"
sPRegValue\x20{\x20int_fp:\x200x3448_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} 4CV)U"
b10001000010100 .-Zk(#
b1001000110100 $a0'K#
sPRegValue\x20{\x20int_fp:\x200x3448_u64,\x20flags:\x20Pwr\x20{\x20cr_gt:\x20true,\x20..\x20}\x20} 4CV)U#
$end
#500000
1mAPf1
@ -23458,6 +23882,10 @@ b11 p'{1C
b11 XQ7U4
b100011 ?rD:V
b110010001000010100 lX!]F
b100011 ?rD:V#
b10001000 bj=V`
b11 ^98rl
b11 dmHRS
b100 VT+LS
b11 n'8X<
b11 /')9{
@ -23789,6 +24217,10 @@ b0 p'{1C
b0 XQ7U4
b0 ?rD:V
b0 lX!]F
b0 ?rD:V#
b0 bj=V`
b0 ^98rl
b0 dmHRS
b0 VT+LS
b0 n'8X<
b0 /')9{

549977
crates/cpu/tests/expected/units_formal_power_isa_add_sub_sim.vcd generated Normal file
View file

File diff suppressed because it is too large Load diff

494
crates/cpu/tests/expected/units_formal_power_isa_paddi_sim.vcd generated
View file

@ -9,6 +9,7 @@ $var wire 64 @$@j=$ any_const_4 $end
$var wire 64 @$@j=% any_const_5 $end
$var wire 64 @$@j=& any_const_6 $end
$var wire 64 @$@j=' any_const_7 $end
$var wire 1 @$@j=( any_const_8 $end
$var wire 1 n$)=T ran $end
$scope struct cd $end
$var wire 1 mAPf1 clk $end
@ -1363,6 +1364,13 @@ $var wire 5 '=~,@ MLS_D_RT_5 $end
$scope struct power_isa_gpr_or_zero_reg_2 $end
$var wire 8 ?rD:V" value $end
$upscope $end
$scope struct power_isa_gpr_or_zero_reg_3 $end
$var wire 8 ?rD:V# value $end
$upscope $end
$var wire 1 {!]++ DX_d2_1 $end
$var wire 10 bj=V` DX_d0_10 $end
$var wire 5 ^98rl DX_d1_5 $end
$var wire 5 dmHRS DX_RT_5 $end
$var wire 5 VT+LS XO_RB_5 $end
$var wire 5 n'8X< XO_RA_5 $end
$var wire 5 /')9{ XO_RT_5 $end
@ -1406,28 +1414,18 @@ $var string 1 k^+pu$ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_5 $end
$var string 1 #a]5!% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_5 $end
$var string 1 k^+pu% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_6 $end
$var string 1 #a]5!& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_6 $end
$var string 1 k^+pu& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_7 $end
$var string 1 #a]5!' \$tag $end
$scope struct flag_reg_0_5 $end
$var string 1 #a]5!% \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
@ -1436,8 +1434,8 @@ $var string 1 k^+pu' \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_8 $end
$var string 1 #a]5!( \$tag $end
$scope struct flag_reg_0_6 $end
$var string 1 #a]5!& \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
@ -1446,6 +1444,191 @@ $var string 1 k^+pu( \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_7 $end
$var string 1 #a]5!' \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_9 $end
$var string 1 k^+pu) \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_8 $end
$var string 1 #a]5!( \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_10 $end
$var string 1 k^+pu* \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_11 $end
$var string 1 k^+pu+ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_9 $end
$var string 1 #a]5!) \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_12 $end
$var string 1 k^+pu, \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_10 $end
$var string 1 #a]5!* \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_13 $end
$var string 1 k^+pu- \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_11 $end
$var string 1 #a]5!+ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_14 $end
$var string 1 k^+pu. \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_12 $end
$var string 1 #a]5!, \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_15 $end
$var string 1 k^+pu/ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_13 $end
$var string 1 #a]5!- \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_16 $end
$var string 1 k^+pu0 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_14 $end
$var string 1 #a]5!. \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_17 $end
$var string 1 k^+pu1 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_15 $end
$var string 1 #a]5!/ \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_18 $end
$var string 1 k^+pu2 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_16 $end
$var string 1 #a]5!0 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_19 $end
$var string 1 k^+pu3 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_17 $end
$var string 1 #a]5!1 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_20 $end
$var string 1 k^+pu4 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_18 $end
$var string 1 #a]5!2 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_21 $end
$var string 1 k^+pu5 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_19 $end
$var string 1 #a]5!3 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_22 $end
$var string 1 k^+pu6 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_20 $end
$var string 1 #a]5!4 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_23 $end
$var string 1 k^+pu7 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_21 $end
$var string 1 #a]5!5 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_24 $end
$var string 1 k^+pu8 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_22 $end
$var string 1 #a]5!6 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_25 $end
$var string 1 k^+pu9 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_23 $end
$var string 1 #a]5!7 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_26 $end
$var string 1 k^+pu: \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_0_24 $end
$var string 1 #a]5!8 \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$scope struct flag_reg_1_27 $end
$var string 1 k^+pu; \$tag $end
$scope struct HdlSome $end
$upscope $end
$upscope $end
$upscope $end
$scope struct decoder_input $end
$var wire 32 x,~Jt \0 $end
@ -15214,6 +15397,8 @@ $var wire 1 O9nl\ matched_any_case $end
$var wire 1 2J><` matched_case_addi $end
$var wire 1 F[XQ_ matched_case_paddi $end
$var wire 1 F[XQ_" matched_case_paddi_2 $end
$var wire 1 zYEiT matched_case_addis $end
$var wire 1 -="Wg matched_case_addpcis $end
$var wire 1 f](?M matched_case_add $end
$var wire 1 6@6XS \matched_case_add. $end
$var wire 1 KbSE, matched_case_addo $end
@ -15222,8 +15407,28 @@ $var wire 1 >{-\6 matched_case_addc $end
$var wire 1 dL::r \matched_case_addc. $end
$var wire 1 [Cj%o matched_case_addco $end
$var wire 1 Bo#P' \matched_case_addco. $end
$var wire 1 %B}aF matched_case_adde $end
$var wire 1 Wq?29 \matched_case_adde. $end
$var wire 1 n!{wU matched_case_addeo $end
$var wire 1 Vx+<b \matched_case_addeo. $end
$var wire 1 c*1&z matched_case_subf $end
$var wire 1 ,MvJK \matched_case_subf. $end
$var wire 1 |hLD> matched_case_subfo $end
$var wire 1 4{K<B \matched_case_subfo. $end
$var wire 1 lhv\- matched_case_subfc $end
$var wire 1 ~o?\W \matched_case_subfc. $end
$var wire 1 U+v"6 matched_case_subfco $end
$var wire 1 \%hAd \matched_case_subfco. $end
$var wire 1 zNlG} matched_case_subfe $end
$var wire 1 Y^=~a \matched_case_subfe. $end
$var wire 1 ^$mZ< matched_case_subfeo $end
$var wire 1 K+"Lg \matched_case_subfeo. $end
$var wire 1 ;UoIk matched_case_addic $end
$var wire 1 g:;Z_ \matched_case_addic. $end
$var wire 1 pAfEx matched_case_subfic $end
$var wire 64 <$d:7 input_r3 $end
$var wire 64 h<mmR input_r4 $end
$var wire 1 %^<Il input_ca $end
$scope struct output_reg $end
$scope struct regs $end
$scope struct regs $end
@ -15536,14 +15741,92 @@ $upscope $end
$var wire 16 Hd*94 addi_imm $end
$var wire 34 5bo?w paddi_imm $end
$var wire 34 5bo?w" paddi_imm_2 $end
$var string 1 <gfVf add_expected_out $end
$var string 1 <gfVf" add_expected_out_2 $end
$var string 1 <gfVf# add_expected_out_3 $end
$var string 1 <gfVf$ add_expected_out_4 $end
$var string 1 <gfVf% add_expected_out_5 $end
$var string 1 <gfVf& add_expected_out_6 $end
$var string 1 <gfVf' add_expected_out_7 $end
$var string 1 <gfVf( add_expected_out_8 $end
$var wire 16 ~W%v& addis_imm $end
$var wire 10 ei=V2 addpcis_d0 $end
$var wire 5 09o]U addpcis_d1 $end
$var wire 1 3E]&t addpcis_d2 $end
$var wire 16 N<`^[ addpcis_d $end
$var wire 64 .PpG. add_sub_add_in0 $end
$var wire 1 !>=Fa add_sub_ca_in $end
$var string 1 ;Mki5 add_sub_expected_out $end
$var wire 64 .PpG." add_sub_add_in0_2 $end
$var wire 1 !>=Fa" add_sub_ca_in_2 $end
$var string 1 ;Mki5" add_sub_expected_out_2 $end
$var wire 64 .PpG.# add_sub_add_in0_3 $end
$var wire 1 !>=Fa# add_sub_ca_in_3 $end
$var string 1 ;Mki5# add_sub_expected_out_3 $end
$var wire 64 .PpG.$ add_sub_add_in0_4 $end
$var wire 1 !>=Fa$ add_sub_ca_in_4 $end
$var string 1 ;Mki5$ add_sub_expected_out_4 $end
$var wire 64 .PpG.% add_sub_add_in0_5 $end
$var wire 1 !>=Fa% add_sub_ca_in_5 $end
$var string 1 ;Mki5% add_sub_expected_out_5 $end
$var wire 64 .PpG.& add_sub_add_in0_6 $end
$var wire 1 !>=Fa& add_sub_ca_in_6 $end
$var string 1 ;Mki5& add_sub_expected_out_6 $end
$var wire 64 .PpG.' add_sub_add_in0_7 $end
$var wire 1 !>=Fa' add_sub_ca_in_7 $end
$var string 1 ;Mki5' add_sub_expected_out_7 $end
$var wire 64 .PpG.( add_sub_add_in0_8 $end
$var wire 1 !>=Fa( add_sub_ca_in_8 $end
$var string 1 ;Mki5( add_sub_expected_out_8 $end
$var wire 64 .PpG.) add_sub_add_in0_9 $end
$var wire 1 !>=Fa) add_sub_ca_in_9 $end
$var string 1 ;Mki5) add_sub_expected_out_9 $end
$var wire 64 .PpG.* add_sub_add_in0_10 $end
$var wire 1 !>=Fa* add_sub_ca_in_10 $end
$var string 1 ;Mki5* add_sub_expected_out_10 $end
$var wire 64 .PpG.+ add_sub_add_in0_11 $end
$var wire 1 !>=Fa+ add_sub_ca_in_11 $end
$var string 1 ;Mki5+ add_sub_expected_out_11 $end
$var wire 64 .PpG., add_sub_add_in0_12 $end
$var wire 1 !>=Fa, add_sub_ca_in_12 $end
$var string 1 ;Mki5, add_sub_expected_out_12 $end
$var wire 64 .PpG.- add_sub_add_in0_13 $end
$var wire 1 !>=Fa- add_sub_ca_in_13 $end
$var string 1 ;Mki5- add_sub_expected_out_13 $end
$var wire 64 .PpG.. add_sub_add_in0_14 $end
$var wire 1 !>=Fa. add_sub_ca_in_14 $end
$var string 1 ;Mki5. add_sub_expected_out_14 $end
$var wire 64 .PpG./ add_sub_add_in0_15 $end
$var wire 1 !>=Fa/ add_sub_ca_in_15 $end
$var string 1 ;Mki5/ add_sub_expected_out_15 $end
$var wire 64 .PpG.0 add_sub_add_in0_16 $end
$var wire 1 !>=Fa0 add_sub_ca_in_16 $end
$var string 1 ;Mki50 add_sub_expected_out_16 $end
$var wire 64 .PpG.1 add_sub_add_in0_17 $end
$var wire 1 !>=Fa1 add_sub_ca_in_17 $end
$var string 1 ;Mki51 add_sub_expected_out_17 $end
$var wire 64 .PpG.2 add_sub_add_in0_18 $end
$var wire 1 !>=Fa2 add_sub_ca_in_18 $end
$var string 1 ;Mki52 add_sub_expected_out_18 $end
$var wire 64 .PpG.3 add_sub_add_in0_19 $end
$var wire 1 !>=Fa3 add_sub_ca_in_19 $end
$var string 1 ;Mki53 add_sub_expected_out_19 $end
$var wire 64 .PpG.4 add_sub_add_in0_20 $end
$var wire 1 !>=Fa4 add_sub_ca_in_20 $end
$var string 1 ;Mki54 add_sub_expected_out_20 $end
$var wire 64 .PpG.5 add_sub_add_in0_21 $end
$var wire 1 !>=Fa5 add_sub_ca_in_21 $end
$var string 1 ;Mki55 add_sub_expected_out_21 $end
$var wire 64 .PpG.6 add_sub_add_in0_22 $end
$var wire 1 !>=Fa6 add_sub_ca_in_22 $end
$var string 1 ;Mki56 add_sub_expected_out_22 $end
$var wire 64 .PpG.7 add_sub_add_in0_23 $end
$var wire 1 !>=Fa7 add_sub_ca_in_23 $end
$var string 1 ;Mki57 add_sub_expected_out_23 $end
$var wire 64 .PpG.8 add_sub_add_in0_24 $end
$var wire 1 !>=Fa8 add_sub_ca_in_24 $end
$var string 1 ;Mki58 add_sub_expected_out_24 $end
$var wire 16 .-Zk( addic_subfic_imm $end
$var wire 64 $a0'K addic_subfic_in $end
$var string 1 4CV)U addic_subfic_expected_out $end
$var wire 16 .-Zk(" addic_subfic_imm_2 $end
$var wire 64 $a0'K" addic_subfic_in_2 $end
$var string 1 4CV)U" addic_subfic_expected_out_2 $end
$var wire 16 .-Zk(# addic_subfic_imm_3 $end
$var wire 64 $a0'K# addic_subfic_in_3 $end
$var string 1 4CV)U# addic_subfic_expected_out_3 $end
$upscope $end
$enddefinitions $end
$dumpvars
@ -16720,6 +17003,11 @@ b0 5]QZg
b0 pQ'}$
b0 '=~,@
b0 ?rD:V"
b0 ?rD:V#
0{!]++
b0 bj=V`
b0 ^98rl
b0 dmHRS
b0 VT+LS
b0 n'8X<
b0 /')9{
@ -16731,14 +17019,49 @@ sHdlSome\x20(1) #a]5!#
sHdlNone\x20(0) k^+pu#
sHdlSome\x20(1) #a]5!$
sHdlSome\x20(1) k^+pu$
sHdlNone\x20(0) #a]5!%
sHdlNone\x20(0) k^+pu%
sHdlNone\x20(0) #a]5!&
sHdlSome\x20(1) k^+pu&
sHdlSome\x20(1) #a]5!'
sHdlNone\x20(0) #a]5!%
sHdlNone\x20(0) k^+pu'
sHdlSome\x20(1) #a]5!(
sHdlNone\x20(0) #a]5!&
sHdlSome\x20(1) k^+pu(
sHdlSome\x20(1) #a]5!'
sHdlNone\x20(0) k^+pu)
sHdlSome\x20(1) #a]5!(
sHdlSome\x20(1) k^+pu*
sHdlNone\x20(0) k^+pu+
sHdlNone\x20(0) #a]5!)
sHdlNone\x20(0) k^+pu,
sHdlNone\x20(0) #a]5!*
sHdlSome\x20(1) k^+pu-
sHdlSome\x20(1) #a]5!+
sHdlNone\x20(0) k^+pu.
sHdlSome\x20(1) #a]5!,
sHdlSome\x20(1) k^+pu/
sHdlNone\x20(0) #a]5!-
sHdlNone\x20(0) k^+pu0
sHdlNone\x20(0) #a]5!.
sHdlSome\x20(1) k^+pu1
sHdlSome\x20(1) #a]5!/
sHdlNone\x20(0) k^+pu2
sHdlSome\x20(1) #a]5!0
sHdlSome\x20(1) k^+pu3
sHdlNone\x20(0) #a]5!1
sHdlNone\x20(0) k^+pu4
sHdlNone\x20(0) #a]5!2
sHdlSome\x20(1) k^+pu5
sHdlSome\x20(1) #a]5!3
sHdlNone\x20(0) k^+pu6
sHdlSome\x20(1) #a]5!4
sHdlSome\x20(1) k^+pu7
sHdlNone\x20(0) #a]5!5
sHdlNone\x20(0) k^+pu8
sHdlNone\x20(0) #a]5!6
sHdlSome\x20(1) k^+pu9
sHdlSome\x20(1) #a]5!7
sHdlNone\x20(0) k^+pu:
sHdlSome\x20(1) #a]5!8
sHdlSome\x20(1) k^+pu;
b0 x,~Jt
sHdlNone\x20(0) \L:8?
b0 sD<$[
@ -23137,6 +23460,8 @@ b1000000001000 @$@j=%
02J><`
1F[XQ_
0F[XQ_"
0zYEiT
0-="Wg
0f](?M
06@6XS
0KbSE,
@ -23145,10 +23470,31 @@ b1000000001000 @$@j=%
0dL::r
0[Cj%o
0Bo#P'
0%B}aF
0Wq?29
0n!{wU
0Vx+<b
0c*1&z
0,MvJK
0|hLD>
04{K<B
0lhv\-
0~o?\W
0U+v"6
0\%hAd
0zNlG}
0Y^=~a
0^$mZ<
0K+"Lg
0;UoIk
0g:;Z_
0pAfEx
b1001100100000111010011110010011000000000000000000000000000000010 <$d:7
b1001100100000111010011110010011000000000000000000000000000000010 @$@j=&
b110000000000000000001000010010000010111110111111111111011111101 h<mmR
b110000000000000000001000010010000010111110111111111111011111101 @$@j='
0%^<Il
0@$@j=(
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} qfRqB
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} 1O=Dy
sPRegValue\x20{\x20int_fp:\x200x0_u64,\x20flags:\x20Pwr\x20{\x20..\x20}\x20} Mhd"F
@ -23429,14 +23775,92 @@ sPhantomConst({\"units\":[{\"kind\":\"AluBranch\",\"max_in_flight\":null}],\"out
b0 Hd*94
b1000000000000 5bo?w
b1000000000000 5bo?w"
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf"
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf#
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf$
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf%
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf&
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf'
sPRegValue\x20{\x20int_fp:\x200xF907534A17DFFEFF_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} <gfVf(
b0 ~W%v&
b0 ei=V2
b0 09o]U
03E]&t
b0 N<`^[
b110011011111000101100001101100111111111111111111111111111111101 .PpG.
1!>=Fa
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5
b110011011111000101100001101100111111111111111111111111111111101 .PpG."
1!>=Fa"
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5"
b110011011111000101100001101100111111111111111111111111111111101 .PpG.#
1!>=Fa#
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5#
b110011011111000101100001101100111111111111111111111111111111101 .PpG.$
1!>=Fa$
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5$
b110011011111000101100001101100111111111111111111111111111111101 .PpG.%
1!>=Fa%
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5%
b110011011111000101100001101100111111111111111111111111111111101 .PpG.&
1!>=Fa&
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5&
b110011011111000101100001101100111111111111111111111111111111101 .PpG.'
1!>=Fa'
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5'
b110011011111000101100001101100111111111111111111111111111111101 .PpG.(
1!>=Fa(
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5(
b110011011111000101100001101100111111111111111111111111111111101 .PpG.)
1!>=Fa)
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5)
b110011011111000101100001101100111111111111111111111111111111101 .PpG.*
1!>=Fa*
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5*
b110011011111000101100001101100111111111111111111111111111111101 .PpG.+
1!>=Fa+
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5+
b110011011111000101100001101100111111111111111111111111111111101 .PpG.,
1!>=Fa,
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5,
b110011011111000101100001101100111111111111111111111111111111101 .PpG.-
1!>=Fa-
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5-
b110011011111000101100001101100111111111111111111111111111111101 .PpG..
1!>=Fa.
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5.
b110011011111000101100001101100111111111111111111111111111111101 .PpG./
1!>=Fa/
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki5/
b110011011111000101100001101100111111111111111111111111111111101 .PpG.0
1!>=Fa0
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki50
b110011011111000101100001101100111111111111111111111111111111101 .PpG.1
1!>=Fa1
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki51
b110011011111000101100001101100111111111111111111111111111111101 .PpG.2
1!>=Fa2
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki52
b110011011111000101100001101100111111111111111111111111111111101 .PpG.3
1!>=Fa3
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki53
b110011011111000101100001101100111111111111111111111111111111101 .PpG.4
1!>=Fa4
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki54
b110011011111000101100001101100111111111111111111111111111111101 .PpG.5
1!>=Fa5
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki55
b110011011111000101100001101100111111111111111111111111111111101 .PpG.6
1!>=Fa6
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki56
b110011011111000101100001101100111111111111111111111111111111101 .PpG.7
1!>=Fa7
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki57
b110011011111000101100001101100111111111111111111111111111111101 .PpG.8
1!>=Fa8
sPRegValue\x20{\x20int_fp:\x200xC6F8B4FE17DFFEFB_u64,\x20flags:\x20Pwr\x20{\x20xer_ca32:\x20true,\x20xer_ov:\x20true,\x20cr_lt:\x20true,\x20so:\x20true,\x20..\x20}\x20} ;Mki58
b0 .-Zk(
b1001111111111111111110111101101111101000001000000000000100000010 $a0'K
sPRegValue\x20{\x20int_fp:\x200x9FFFFBDBE8200103_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} 4CV)U
b0 .-Zk("
b1001111111111111111110111101101111101000001000000000000100000010 $a0'K"
sPRegValue\x20{\x20int_fp:\x200x9FFFFBDBE8200103_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} 4CV)U"
b0 .-Zk(#
b1001111111111111111110111101101111101000001000000000000100000010 $a0'K#
sPRegValue\x20{\x20int_fp:\x200x9FFFFBDBE8200103_u64,\x20flags:\x20Pwr\x20{\x20cr_lt:\x20true,\x20..\x20}\x20} 4CV)U#
$end
#500000
1mAPf1
@ -23465,6 +23889,7 @@ b1000000000000 5]QZg
b100 pQ'}$
b11 '=~,@
b100100 ?rD:V"
b10000 dmHRS
b10000 /')9{
b110000000000000000000000000 x,~Jt
sHdlSome\x20(1) \L:8?
@ -23738,6 +24163,7 @@ b0 5]QZg
b0 pQ'}$
b0 '=~,@
b0 ?rD:V"
b0 dmHRS
b0 /')9{
b0 x,~Jt
sHdlNone\x20(0) \L:8?

474
crates/cpu/tests/units_formal.rs
View file

@ -133,6 +133,7 @@ enum Case {
asm: &'static str,
encoded: u32,
imm_mask: u32,
inputs: Vec<u32>,
check: UnprefixedCheckFn,
source_location: SourceLocation,
},
@ -140,6 +141,7 @@ enum Case {
asm: &'static str,
encoded: (u32, u32),
imm_mask: (u32, u32),
inputs: Vec<u32>,
check: PrefixedCheckFn,
source_location: SourceLocation,
},
@ -158,6 +160,11 @@ impl Case {
.next()
.expect("asm should have mnemonic")
}
fn inputs(&self) -> &[u32] {
match self {
Self::Unprefixed { inputs, .. } | Self::Prefixed { inputs, .. } => inputs,
}
}
fn source_location(&self) -> SourceLocation {
match *self {
Self::Unprefixed {
@ -182,6 +189,7 @@ impl Case {
asm: _,
encoded,
imm_mask,
inputs: _,
check: _,
source_location: _,
} => {
@ -194,6 +202,7 @@ impl Case {
asm: _,
encoded: (encoded_prefix, encoded_suffix),
imm_mask: (imm_mask_prefix, imm_mask_suffix),
inputs: _,
check: _,
source_location: _,
} => {
@ -331,11 +340,19 @@ impl Cases {
self.cases.push(case);
}
#[track_caller]
fn add(&mut self, asm: &'static str, encoded: u32, imm_mask: u32, check: UnprefixedCheckFn) {
fn add(
&mut self,
asm: &'static str,
encoded: u32,
imm_mask: u32,
inputs: impl AsRef<[u32]>,
check: UnprefixedCheckFn,
) {
self.add_maybe_prefixed(Case::Unprefixed {
asm,
encoded,
imm_mask,
inputs: inputs.as_ref().to_vec(),
check,
source_location: SourceLocation::caller(),
});
@ -346,12 +363,14 @@ impl Cases {
asm: &'static str,
encoded: (u32, u32),
imm_mask: (u32, u32),
inputs: impl AsRef<[u32]>,
check: PrefixedCheckFn,
) {
self.add_maybe_prefixed(Case::Prefixed {
asm,
encoded,
imm_mask,
inputs: inputs.as_ref().to_vec(),
check,
source_location: SourceLocation::caller(),
});
@ -360,7 +379,8 @@ impl Cases {
#[hdl]
fn case_check_addi(cases: &mut Cases) {
cases.add("addi 3, 4, imm", 0x3864_0000, 0xFFFF, check_addi);
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
cases.add("addi 3, 4, imm", 0x3864_0000, 0xFFFF, [r4], check_addi);
#[hdl]
fn check_addi(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
#[hdl]
@ -380,16 +400,19 @@ fn case_check_addi(cases: &mut Cases) {
#[hdl]
fn case_check_paddi(cases: &mut Cases) {
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
cases.add_prefixed(
"paddi 3, 4, imm, 0",
(0x0600_0000, 0x3864_0000),
(0x0003_FFFF, 0x0000_FFFF),
[r4],
check_paddi::<false>,
);
cases.add_prefixed(
"paddi 3, 4, imm, 1",
(0x0610_0000, 0x3864_0000),
(0x0003_FFFF, 0x0000_FFFF),
[r4],
check_paddi::<true>,
);
#[hdl]
@ -414,19 +437,104 @@ fn case_check_paddi(cases: &mut Cases) {
}
#[hdl]
fn case_check_add_addc(cases: &mut Cases) {
cases.add("add 3, 3, 4", 0x7C63_2214, 0, check_add);
cases.add("add. 3, 3, 4", 0x7C63_2215, 0, check_add);
cases.add("addo 3, 3, 4", 0x7C63_2614, 0, check_add);
cases.add("addo. 3, 3, 4", 0x7C63_2615, 0, check_add);
cases.add("addc 3, 3, 4", 0x7C63_2014, 0, check_add);
cases.add("addc. 3, 3, 4", 0x7C63_2015, 0, check_add);
cases.add("addco 3, 3, 4", 0x7C63_2414, 0, check_add);
cases.add("addco. 3, 3, 4", 0x7C63_2415, 0, check_add);
fn case_check_addis(cases: &mut Cases) {
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
cases.add("addis 3, 4, imm", 0x3C64_0000, 0xFFFF, [r4], check_addis);
#[hdl]
fn check_add(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
let is_addc = (input.decoder_input.0 & 0x200u32).cmp_eq(0u32);
fn check_addis(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
#[hdl]
let addis_imm = wire();
connect(
addis_imm,
input.decoder_input.0.cast_to_static::<SInt<16>>(),
);
let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
hdl_assert(
clk,
(r4_in + (addis_imm << 16).cast_to_static::<UInt<64>>())
.cast_to_static::<UInt<64>>()
.cmp_eq(r3_out),
"",
);
}
}
#[hdl]
fn case_check_addpcis(cases: &mut Cases) {
cases.add("addpcis 3, imm", 0x4C60_0004, 0x1F_FFC1, [], check_addpcis);
#[hdl]
fn check_addpcis(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
#[hdl]
let addpcis_d0 = wire();
connect(
addpcis_d0,
input.decoder_input.0[6..].cast_to_static::<UInt<10>>(),
);
#[hdl]
let addpcis_d1 = wire();
connect(
addpcis_d1,
input.decoder_input.0[16..].cast_to_static::<UInt<5>>(),
);
#[hdl]
let addpcis_d2 = wire();
connect(
addpcis_d2,
input.decoder_input.0.cast_to_static::<UInt<1>>(),
);
#[hdl]
let addpcis_d = wire();
connect(
addpcis_d,
(addpcis_d2 + (addpcis_d1 << 1) + (addpcis_d0 << 6)).cast_to_static::<SInt<16>>(),
);
let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
hdl_assert(
clk,
(input.pc + 4u64 + (addpcis_d << 16).cast_to_static::<UInt<64>>())
.cast_to_static::<UInt<64>>()
.cmp_eq(r3_out),
"",
);
}
}
#[hdl]
fn case_check_add_addc_adde_subf_subfc_subfe(cases: &mut Cases) {
let r3 = MOpRegNum::power_isa_gpr_reg_num(3);
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
let ca = MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM;
cases.add("add 3, 3, 4", 0x7C63_2214, 0, [r3, r4], check);
cases.add("add. 3, 3, 4", 0x7C63_2215, 0, [r3, r4], check);
cases.add("addo 3, 3, 4", 0x7C63_2614, 0, [r3, r4], check);
cases.add("addo. 3, 3, 4", 0x7C63_2615, 0, [r3, r4], check);
cases.add("addc 3, 3, 4", 0x7C63_2014, 0, [r3, r4], check);
cases.add("addc. 3, 3, 4", 0x7C63_2015, 0, [r3, r4], check);
cases.add("addco 3, 3, 4", 0x7C63_2414, 0, [r3, r4], check);
cases.add("addco. 3, 3, 4", 0x7C63_2415, 0, [r3, r4], check);
cases.add("adde 3, 3, 4", 0x7C63_2114, 0, [r3, r4, ca], check);
cases.add("adde. 3, 3, 4", 0x7C63_2115, 0, [r3, r4, ca], check);
cases.add("addeo 3, 3, 4", 0x7C63_2514, 0, [r3, r4, ca], check);
cases.add("addeo. 3, 3, 4", 0x7C63_2515, 0, [r3, r4, ca], check);
cases.add("subf 3, 3, 4", 0x7C63_2050, 0, [r3, r4], check);
cases.add("subf. 3, 3, 4", 0x7C63_2051, 0, [r3, r4], check);
cases.add("subfo 3, 3, 4", 0x7C63_2450, 0, [r3, r4], check);
cases.add("subfo. 3, 3, 4", 0x7C63_2451, 0, [r3, r4], check);
cases.add("subfc 3, 3, 4", 0x7C63_2010, 0, [r3, r4], check);
cases.add("subfc. 3, 3, 4", 0x7C63_2011, 0, [r3, r4], check);
cases.add("subfco 3, 3, 4", 0x7C63_2410, 0, [r3, r4], check);
cases.add("subfco. 3, 3, 4", 0x7C63_2411, 0, [r3, r4], check);
cases.add("subfe 3, 3, 4", 0x7C63_2110, 0, [r3, r4, ca], check);
cases.add("subfe. 3, 3, 4", 0x7C63_2111, 0, [r3, r4, ca], check);
cases.add("subfeo 3, 3, 4", 0x7C63_2510, 0, [r3, r4, ca], check);
cases.add("subfeo. 3, 3, 4", 0x7C63_2511, 0, [r3, r4, ca], check);
#[hdl]
fn check(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
let has_ca_out = (input.decoder_input.0 & 0x240u32).cmp_eq(0u32);
let oe = (input.decoder_input.0 & 0x400u32).cmp_ne(0u32);
let use_ca_in = (input.decoder_input.0 & 0x100u32).cmp_ne(0u32);
let is_sub = (input.decoder_input.0 & 0x4u32).cmp_eq(0u32);
let rc = (input.decoder_input.0 & 1u32).cmp_ne(0u32);
let r3_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp;
let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
@ -438,8 +546,26 @@ fn case_check_add_addc(cases: &mut Cases) {
let ov_out = output.reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
let cr0_out = output.reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
#[hdl]
let add_expected_out = wire(r3_out.ty());
connect_any(add_expected_out.int_fp, r3_in + r4_in);
let add_sub_add_in0 = wire();
connect(add_sub_add_in0, r3_in);
#[hdl]
let add_sub_ca_in = wire();
connect(add_sub_ca_in, is_sub.cast_to_static::<UInt<1>>());
#[hdl]
if is_sub {
connect(add_sub_add_in0, !r3_in);
}
#[hdl]
if use_ca_in {
connect(
add_sub_ca_in,
PRegFlags::view::<PRegFlagsPowerISA>(ca_in.flags)
.xer_ca
.cast_to_static::<UInt<1>>(),
);
}
#[hdl]
let add_sub_expected_out = wire(r3_out.ty());
let PRegFlagsPowerISAView {
unused: _,
xer_ca,
@ -451,14 +577,20 @@ fn case_check_add_addc(cases: &mut Cases) {
cr_eq,
so,
..
} = PRegFlags::view::<PRegFlagsPowerISA>(add_expected_out.flags);
let r3_s = r3_in.cast_to_static::<SInt<64>>();
} = PRegFlags::view::<PRegFlagsPowerISA>(add_sub_expected_out.flags);
let add_sub_add_in0_s = add_sub_add_in0.cast_to_static::<SInt<64>>();
let r4_s = r4_in.cast_to_static::<SInt<64>>();
let u64_sum = r3_in + r4_in;
let s64_sum = r3_s + r4_s;
let u32_sum = r3_in.cast_to(UInt[32]) + r4_in.cast_to(UInt[32]);
let s32_sum = r3_in.cast_to(SInt[32]) + r4_in.cast_to(SInt[32]);
let u64_sum = add_sub_add_in0 + r4_in + add_sub_ca_in;
let s64_sum = add_sub_add_in0_s + r4_s + add_sub_ca_in.cast_to(SInt[2]);
let u32_sum = add_sub_add_in0.cast_to(UInt[32]) + r4_in.cast_to(UInt[32]) + add_sub_ca_in;
let s32_sum = add_sub_add_in0.cast_to(SInt[32])
+ r4_in.cast_to(SInt[32])
+ add_sub_ca_in.cast_to(SInt[2]);
let sum_as_s64 = u64_sum.cast_to(SInt[64]);
connect(
add_sub_expected_out.int_fp,
u64_sum.cast_to_static::<UInt<64>>(),
);
connect(xer_ca, u64_sum[64]);
connect(xer_ca32, u32_sum[32]);
connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
@ -472,22 +604,103 @@ fn case_check_add_addc(cases: &mut Cases) {
connect(so, xer_ov); // TODO: also propagate from input SO
#[hdl]
if is_addc {
hdl_assert(clk, add_expected_out.cmp_eq(ca_out), "");
if has_ca_out {
hdl_assert(clk, add_sub_expected_out.cmp_eq(ca_out), "");
} else {
hdl_assert(clk, ca_in.cmp_eq(ca_out), "");
}
#[hdl]
if oe {
hdl_assert(clk, add_expected_out.cmp_eq(ov_out), "");
hdl_assert(clk, add_sub_expected_out.cmp_eq(ov_out), "");
} else {
hdl_assert(clk, ov_in.cmp_eq(ov_out), "");
}
#[hdl]
if rc {
hdl_assert(clk, add_expected_out.cmp_eq(cr0_out), "");
hdl_assert(clk, add_sub_expected_out.cmp_eq(cr0_out), "");
} else {
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
}
}
}
#[hdl]
fn case_check_addic_subfic(cases: &mut Cases) {
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
cases.add("addic 3, 4, imm", 0x3064_0000, 0xFFFF, [r4], check);
cases.add("addic. 3, 4, imm", 0x3464_0000, 0xFFFF, [r4], check);
cases.add("subfic 3, 4, imm", 0x2064_0000, 0xFFFF, [r4], check);
#[hdl]
fn check(clk: Expr<Clock>, input: Expr<CheckInput>, output: &mut CaseOutput) {
let rc = (input.decoder_input.0 & 0x400_0000u32).cmp_ne(0u32);
let is_sub = (input.decoder_input.0 & 0x1000_0000u32).cmp_eq(0u32);
let r4_in = input.regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp;
let cr0_in = input.regs.regs[MOpRegNum::power_isa_cr_0_reg().value];
let r3_out = output.reg(MOpRegNum::power_isa_gpr_reg_num(3));
let ca_out = output.reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
let cr0_out = output.reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
#[hdl]
let addic_subfic_imm = wire();
connect(
addic_subfic_imm,
input.decoder_input.0.cast_to_static::<SInt<16>>(),
);
#[hdl]
let addic_subfic_in = wire();
connect(addic_subfic_in, r4_in);
#[hdl]
if is_sub {
connect(addic_subfic_in, !r4_in);
}
#[hdl]
let addic_subfic_expected_out = wire(r3_out.ty());
connect_any(
addic_subfic_expected_out.int_fp,
addic_subfic_in + addic_subfic_imm.cast_to(UInt[64]) + is_sub.cast_to(UInt[1]),
);
let PRegFlagsPowerISAView {
unused: _,
xer_ca,
xer_ca32,
xer_ov,
xer_ov32,
cr_lt,
cr_gt,
cr_eq,
so,
..
} = PRegFlags::view::<PRegFlagsPowerISA>(addic_subfic_expected_out.flags);
let addic_subfic_in_s = addic_subfic_in.cast_to_static::<SInt<64>>();
let u64_sum =
addic_subfic_in + addic_subfic_imm.cast_to(UInt[64]) + is_sub.cast_to(UInt[1]);
let s64_sum =
addic_subfic_in_s + addic_subfic_imm + is_sub.cast_to(UInt[1]).cast_to(SInt[64]);
let u32_sum = addic_subfic_in.cast_to(UInt[32])
+ addic_subfic_imm.cast_to(UInt[32])
+ is_sub.cast_to(UInt[1]);
let s32_sum = addic_subfic_in.cast_to(SInt[32])
+ addic_subfic_imm.cast_to(SInt[32])
+ is_sub.cast_to(UInt[1]).cast_to(SInt[32]);
let sum_as_s64 = u64_sum.cast_to(SInt[64]);
connect(xer_ca, u64_sum[64]);
connect(xer_ca32, u32_sum[32]);
connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
connect(
xer_ov32,
s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
);
connect(cr_gt, sum_as_s64.cmp_gt(0i64));
connect(cr_lt, sum_as_s64.cmp_lt(0i64));
connect(cr_eq, sum_as_s64.cmp_eq(0i64));
connect(so, xer_ov); // TODO: also propagate from input SO
hdl_assert(clk, addic_subfic_expected_out.cmp_eq(ca_out), "");
#[hdl]
if rc {
hdl_assert(clk, addic_subfic_expected_out.cmp_eq(cr0_out), "");
} else {
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
}
@ -498,28 +711,10 @@ fn cases_add_sub() -> Cases {
let mut cases = Cases::default();
case_check_addi(&mut cases);
case_check_paddi(&mut cases);
// TODO: "addis"
// TODO: "addpcis"
case_check_add_addc(&mut cases);
// TODO: "addic"
// TODO: "addic."
// TODO: "subf"
// TODO: "subf."
// TODO: "subfo"
// TODO: "subfo."
// TODO: "subfic"
// TODO: "subfc"
// TODO: "subfc."
// TODO: "subfco"
// TODO: "subfco."
// TODO: "adde"
// TODO: "adde."
// TODO: "addeo"
// TODO: "addeo."
// TODO: "subfe"
// TODO: "subfe."
// TODO: "subfeo"
// TODO: "subfeo."
case_check_addis(&mut cases);
case_check_addpcis(&mut cases);
case_check_add_addc_adde_subf_subfc_subfe(&mut cases);
case_check_addic_subfic(&mut cases);
// TODO: "addme"
// TODO: "addme."
// TODO: "addmeo"
@ -551,6 +746,7 @@ struct AnyConsts {
decoder_second_word_any_const: Expr<UInt<32>>,
r3_any_const: Expr<UInt<64>>,
r4_any_const: Expr<UInt<64>>,
ca_any_const: Expr<Bool>,
pc_any_const: Expr<UInt<64>>,
predicted_next_pc_any_const: Expr<UInt<64>>,
}
@ -564,6 +760,7 @@ impl AnyConsts {
decoder_second_word_any_const: any_const(StaticType::TYPE),
r3_any_const: any_const(StaticType::TYPE),
r4_any_const: any_const(StaticType::TYPE),
ca_any_const: any_const(StaticType::TYPE),
pc_any_const: any_const(StaticType::TYPE),
predicted_next_pc_any_const: any_const(StaticType::TYPE),
}
@ -573,7 +770,7 @@ impl AnyConsts {
#[hdl_module]
fn check_power_isa_alu_formal(
config: PhantomConst<CpuConfig>,
cases: Cases,
cases: &Cases,
any_consts: Option<AnyConsts>,
) {
#[hdl]
@ -613,6 +810,7 @@ fn check_power_isa_alu_formal(
decoder_second_word_any_const,
r3_any_const,
r4_any_const,
ca_any_const,
pc_any_const,
predicted_next_pc_any_const,
} = any_consts.unwrap_or_else(|| AnyConsts::new());
@ -654,6 +852,7 @@ fn check_power_isa_alu_formal(
encoded,
imm_mask,
check: _,
inputs: _,
source_location: _,
} => {
#[hdl]
@ -669,6 +868,7 @@ fn check_power_isa_alu_formal(
asm: _,
encoded: (encoded_prefix, encoded_suffix),
imm_mask: (imm_mask_prefix, imm_mask_suffix),
inputs: _,
check: _,
source_location: _,
} => {
@ -699,6 +899,9 @@ fn check_power_isa_alu_formal(
#[hdl]
let input_r4 = wire();
connect(input_r4, r4_any_const);
#[hdl]
let input_ca = wire();
connect(input_ca, ca_any_const);
connect(
input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp,
input_r3,
@ -707,6 +910,13 @@ fn check_power_isa_alu_formal(
input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp,
input_r4,
);
connect(
PRegFlags::view::<PRegFlagsPowerISA>(
input_regs.regs[MOpRegNum::power_isa_xer_ca_ca32_reg().value].flags,
)
.xer_ca,
input_ca,
);
// a copy of the output so you can see the signal values in formal proof error traces
#[hdl]
let output_reg = reg_builder()
@ -745,6 +955,7 @@ fn check_power_isa_alu_formal(
asm: _,
encoded: _,
imm_mask: _,
inputs: _,
check,
source_location: _,
} => check(cd.clk, harness.input, &mut case_output),
@ -752,6 +963,7 @@ fn check_power_isa_alu_formal(
asm: _,
encoded: _,
imm_mask: _,
inputs: _,
check,
source_location: _,
} => check(
@ -779,7 +991,7 @@ fn test_power_isa_add_sub_formal() {
vec![UnitConfig::new(UnitKind::AluBranch)],
NonZero::new(20).unwrap(),
));
let m = check_power_isa_alu_formal(config, cases_add_sub(), None);
let m = check_power_isa_alu_formal(config, &cases_add_sub(), None);
assert_formal(
"test_power_isa_add_sub_formal",
m,
@ -793,6 +1005,162 @@ fn test_power_isa_add_sub_formal() {
);
}
#[hdl]
fn test_power_isa_alu_sim(
cases: Cases,
checked_vcd_output: impl FnOnce(
&mut Simulation<check_power_isa_alu_formal>,
) -> fayalite::testing::CheckedVcdOutput,
) {
let config = PhantomConst::new_sized(CpuConfig::new(
vec![UnitConfig::new(UnitKind::AluBranch)],
NonZero::new(20).unwrap(),
));
let any_consts = AnyConsts::new();
let m = check_power_isa_alu_formal(config, &cases, Some(any_consts));
let mut sim = Simulation::new(m);
let _checked_vcd_output = checked_vcd_output(&mut sim);
let AnyConsts {
decoder_first_word_any_const,
decoder_has_second_word_any_const,
decoder_second_word_any_const,
r3_any_const,
r4_any_const,
ca_any_const,
pc_any_const,
predicted_next_pc_any_const,
} = any_consts;
const REG_VALUES: &[u64] = &[0x0, 0xAAAA_AAAA_AAAA_AAAA, 0xFFFF_FFFF_FFFF_FFFF];
const IMM_S16_VALUES: &[i16] = &[0, 1, -1, i16::MAX, i16::MIN, 0x100];
const S34_MAX: i64 = (1 << 33) - 1;
const S34_MIN: i64 = -1 << 33;
const IMM_S34_VALUES: &[i64] = &[0, 1, -1, S34_MAX, S34_MIN];
const PC: u64 = 0x1000;
for case in &cases.cases {
let r3_values = if case.inputs().contains(&MOpRegNum::power_isa_gpr_reg_num(3)) {
REG_VALUES
} else {
&[0]
};
let r4_values = if case.inputs().contains(&MOpRegNum::power_isa_gpr_reg_num(4)) {
REG_VALUES
} else {
&[0]
};
let ca_values: &[bool] = if case
.inputs()
.contains(&MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM)
{
&[false, true]
} else {
&[false]
};
for &r3 in r3_values {
for &r4 in r4_values {
for &ca in ca_values {
let mut imm_index = 0;
loop {
let asm = case.asm();
let source_location = case.source_location();
println!(
"\ncase: {asm}\n\
r3={r3:#x} r4={r4:#x} ca={ca}\n\
at: {source_location}"
);
sim.write(r3_any_const, r3);
sim.write(r4_any_const, r4);
sim.write(ca_any_const, ca);
sim.write(pc_any_const, PC);
let imm_count;
match *case {
Case::Unprefixed {
asm: _,
encoded,
imm_mask,
inputs: _,
check: _,
source_location: _,
} => {
sim.write(predicted_next_pc_any_const, PC + 4);
let imm = IMM_S16_VALUES[imm_index] as i64;
if imm_mask == 0 {
imm_count = 1;
} else {
imm_count = IMM_S16_VALUES.len();
println!("imm = {imm:#x}");
}
let mut imm = imm as u32;
if case.mnemonic() == "addpcis" {
let d2 = imm & 1;
let d1 = (imm >> 1) & 0x1F;
let d0 = (imm >> 6) & 0x3FF;
imm = d2 | (d1 << 16) | (d0 << 6);
}
sim.write(decoder_first_word_any_const, encoded | (imm_mask & imm));
sim.write(decoder_has_second_word_any_const, false);
sim.write(decoder_second_word_any_const, 0u32);
}
Case::Prefixed {
asm: _,
encoded: (encoded_prefix, encoded_suffix),
imm_mask: (imm_mask_prefix, imm_mask_suffix),
inputs: _,
check: _,
source_location: _,
} => {
sim.write(predicted_next_pc_any_const, PC + 8);
let imm = IMM_S34_VALUES[imm_index];
if imm_mask_prefix == 0 && imm_mask_suffix == 0 {
imm_count = 1;
} else {
imm_count = IMM_S34_VALUES.len();
println!("imm = {imm:#x}");
}
sim.write(
decoder_first_word_any_const,
encoded_prefix | (imm_mask_prefix & (imm >> 16) as u32),
);
sim.write(decoder_has_second_word_any_const, true);
sim.write(
decoder_second_word_any_const,
encoded_suffix | (imm_mask_suffix & (imm & 0xFFFF) as u32),
);
}
}
let clk = formal_global_clock();
let rst = formal_reset();
sim.write_clock(clk, false);
sim.write_reset(rst, true);
for cycle in 0..10 {
sim.advance_time(SimDuration::from_nanos(500));
println!("clock tick: {cycle}");
sim.write_clock(clk, true);
sim.advance_time(SimDuration::from_nanos(500));
sim.write_clock(clk, false);
sim.write_reset(rst, false);
if sim.read_bool(sim.io().ran) {
break;
}
}
assert!(sim.read_bool(sim.io().ran));
imm_index += 1;
if imm_index >= imm_count {
break;
}
}
}
}
}
}
}
#[test]
fn test_power_isa_add_sub_sim() {
test_power_isa_alu_sim(cases_add_sub(), |sim| {
checked_vcd_output!(sim, "tests/expected/units_formal_power_isa_add_sub_sim.vcd")
});
}
#[hdl]
#[test]
fn test_power_isa_add_sim() {
@ -801,7 +1169,7 @@ fn test_power_isa_add_sim() {
NonZero::new(20).unwrap(),
));
let any_consts = AnyConsts::new();
let m = check_power_isa_alu_formal(config, cases_add_sub(), Some(any_consts));
let m = check_power_isa_alu_formal(config, &cases_add_sub(), Some(any_consts));
let mut sim = Simulation::new(m);
let _checked_vcd_output = checked_vcd_output!(
&mut sim,
@ -813,6 +1181,7 @@ fn test_power_isa_add_sim() {
decoder_second_word_any_const,
r3_any_const,
r4_any_const,
ca_any_const,
pc_any_const,
predicted_next_pc_any_const,
} = any_consts;
@ -821,6 +1190,7 @@ fn test_power_isa_add_sim() {
sim.write(decoder_second_word_any_const, 0u32);
sim.write(r3_any_const, 0x1234u64);
sim.write(r4_any_const, 0x1234u64);
sim.write(ca_any_const, false);
sim.write(pc_any_const, 0x1000u64);
sim.write(predicted_next_pc_any_const, 0x1004u64);
let clk = formal_global_clock();
@ -846,7 +1216,7 @@ fn test_power_isa_paddi_sim() {
NonZero::new(20).unwrap(),
));
let any_consts = AnyConsts::new();
let m = check_power_isa_alu_formal(config, cases_add_sub(), Some(any_consts));
let m = check_power_isa_alu_formal(config, &cases_add_sub(), Some(any_consts));
let mut sim = Simulation::new(m);
let _checked_vcd_output = checked_vcd_output!(
&mut sim,
@ -858,6 +1228,7 @@ fn test_power_isa_paddi_sim() {
decoder_second_word_any_const,
r3_any_const,
r4_any_const,
ca_any_const,
pc_any_const,
predicted_next_pc_any_const,
} = any_consts;
@ -866,6 +1237,7 @@ fn test_power_isa_paddi_sim() {
sim.write(decoder_second_word_any_const, 0x3864_1000u32); // paddi 3, 4, 0x1000, 0
sim.write(r3_any_const, 0x9907_4F26_0000_0002u64);
sim.write(r4_any_const, 0x6000_0424_17DF_FEFDu64);
sim.write(ca_any_const, false);
sim.write(pc_any_const, 0x1000u64);
sim.write(predicted_next_pc_any_const, 0x1008u64);
let clk = formal_global_clock();