diff --git a/src/riscv/Utility/InstructionCoercions.v b/src/riscv/Utility/InstructionCoercions.v index 3a867f4..c10acae 100644 --- a/src/riscv/Utility/InstructionCoercions.v +++ b/src/riscv/Utility/InstructionCoercions.v @@ -1,10 +1,14 @@ Require Import riscv.Spec.Decode. -Coercion IInstruction: InstructionI >-> Instruction. -Coercion MInstruction: InstructionM >-> Instruction. -Coercion I64Instruction: InstructionI64 >-> Instruction. -Coercion M64Instruction: InstructionM64 >-> Instruction. -Coercion CSRInstruction: InstructionCSR >-> Instruction. +Coercion IInstruction : InstructionI >-> Instruction. +Coercion MInstruction : InstructionM >-> Instruction. +Coercion AInstruction : InstructionA >-> Instruction. +Coercion FInstruction : InstructionF >-> Instruction. +Coercion I64Instruction : InstructionI64 >-> Instruction. +Coercion M64Instruction : InstructionM64 >-> Instruction. +Coercion A64Instruction : InstructionA64 >-> Instruction. +Coercion F64Instruction : InstructionF64 >-> Instruction. +Coercion CSRInstruction : InstructionCSR >-> Instruction. (* separate notation to make sure coercions kick in *) Declare Scope ilist_scope. diff --git a/src/riscv/Utility/InstructionNotations.v b/src/riscv/Utility/InstructionNotations.v index d8c0217..6d6c3b8 100644 --- a/src/riscv/Utility/InstructionNotations.v +++ b/src/riscv/Utility/InstructionNotations.v @@ -1,104 +1,382 @@ -(* File generated by ./make_InstructionNotations.sh, do not edit *) +(* File generated by ./src/riscv/Utility/make_InstructionNotations.py, do not edit *) Require Export riscv.Spec.Decode. Require Export riscv.Utility.InstructionCoercions. -Notation "'RISCV:' x y .. z" := (@cons Instruction x (@cons Instruction y .. (@cons Instruction z nil) ..)) (at level 10). +Require Export riscv.Utility.RegisterNameNotations. -Notation "'mulw' 'x' r1 , 'x' r2 , 'x' r3" := (Mulw r1 r2 r3) (at level 10, format "'//' 'mulw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'divw' 'x' r1 , 'x' r2 , 'x' r3" := (Divw r1 r2 r3) (at level 10, format "'//' 'divw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'divuw' 'x' r1 , 'x' r2 , 'x' r3" := (Divuw r1 r2 r3) (at level 10, format "'//' 'divuw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'remw' 'x' r1 , 'x' r2 , 'x' r3" := (Remw r1 r2 r3) (at level 10, format "'//' 'remw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'remuw' 'x' r1 , 'x' r2 , 'x' r3" := (Remuw r1 r2 r3) (at level 10, format "'//' 'remuw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'mul' 'x' r1 , 'x' r2 , 'x' r3" := (Mul r1 r2 r3) (at level 10, format "'//' 'mul' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'mulh' 'x' r1 , 'x' r2 , 'x' r3" := (Mulh r1 r2 r3) (at level 10, format "'//' 'mulh' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'mulhsu' 'x' r1 , 'x' r2 , 'x' r3" := (Mulhsu r1 r2 r3) (at level 10, format "'//' 'mulhsu' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'mulhu' 'x' r1 , 'x' r2 , 'x' r3" := (Mulhu r1 r2 r3) (at level 10, format "'//' 'mulhu' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'div' 'x' r1 , 'x' r2 , 'x' r3" := (Div r1 r2 r3) (at level 10, format "'//' 'div' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'divu' 'x' r1 , 'x' r2 , 'x' r3" := (Divu r1 r2 r3) (at level 10, format "'//' 'divu' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'rem' 'x' r1 , 'x' r2 , 'x' r3" := (Rem r1 r2 r3) (at level 10, format "'//' 'rem' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'remu' 'x' r1 , 'x' r2 , 'x' r3" := (Remu r1 r2 r3) (at level 10, format "'//' 'remu' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'ld' 'x' r1 , 'x' r2 , i" := (Ld r1 r2 i) (at level 10, i at level 200, format "'//' 'ld' 'x' r1 , 'x' r2 , i"). -Notation "'lwu' 'x' r1 , 'x' r2 , i" := (Lwu r1 r2 i) (at level 10, i at level 200, format "'//' 'lwu' 'x' r1 , 'x' r2 , i"). -Notation "'addiw' 'x' r1 , 'x' r2 , i" := (Addiw r1 r2 i) (at level 10, i at level 200, format "'//' 'addiw' 'x' r1 , 'x' r2 , i"). -Notation "'slliw' 'x' r1 , 'x' r2 , i" := (Slliw r1 r2 i) (at level 10, i at level 200, format "'//' 'slliw' 'x' r1 , 'x' r2 , i"). -Notation "'srliw' 'x' r1 , 'x' r2 , i" := (Srliw r1 r2 i) (at level 10, i at level 200, format "'//' 'srliw' 'x' r1 , 'x' r2 , i"). -Notation "'sraiw' 'x' r1 , 'x' r2 , i" := (Sraiw r1 r2 i) (at level 10, i at level 200, format "'//' 'sraiw' 'x' r1 , 'x' r2 , i"). -Notation "'sd' 'x' r1 , 'x' r2 , i" := (Sd r1 r2 i) (at level 10, i at level 200, format "'//' 'sd' 'x' r1 , 'x' r2 , i"). -Notation "'addw' 'x' r1 , 'x' r2 , 'x' r3" := (Addw r1 r2 r3) (at level 10, format "'//' 'addw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'subw' 'x' r1 , 'x' r2 , 'x' r3" := (Subw r1 r2 r3) (at level 10, format "'//' 'subw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sllw' 'x' r1 , 'x' r2 , 'x' r3" := (Sllw r1 r2 r3) (at level 10, format "'//' 'sllw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'srlw' 'x' r1 , 'x' r2 , 'x' r3" := (Srlw r1 r2 r3) (at level 10, format "'//' 'srlw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sraw' 'x' r1 , 'x' r2 , 'x' r3" := (Sraw r1 r2 r3) (at level 10, format "'//' 'sraw' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'lb' 'x' r1 , 'x' r2 , i" := (Lb r1 r2 i) (at level 10, i at level 200, format "'//' 'lb' 'x' r1 , 'x' r2 , i"). -Notation "'lh' 'x' r1 , 'x' r2 , i" := (Lh r1 r2 i) (at level 10, i at level 200, format "'//' 'lh' 'x' r1 , 'x' r2 , i"). -Notation "'lw' 'x' r1 , 'x' r2 , i" := (Lw r1 r2 i) (at level 10, i at level 200, format "'//' 'lw' 'x' r1 , 'x' r2 , i"). -Notation "'lbu' 'x' r1 , 'x' r2 , i" := (Lbu r1 r2 i) (at level 10, i at level 200, format "'//' 'lbu' 'x' r1 , 'x' r2 , i"). -Notation "'lhu' 'x' r1 , 'x' r2 , i" := (Lhu r1 r2 i) (at level 10, i at level 200, format "'//' 'lhu' 'x' r1 , 'x' r2 , i"). -Notation "'fence' i , j" := (Fence i j) (at level 10, i at level 200, j at level 200, format "'//' 'fence' i , j"). -Notation "'fence_i'" := (Fence_i) (at level 10, format "'//' 'fence_i'"). -Notation "'addi' 'x' r1 , 'x' r2 , i" := (Addi r1 r2 i) (at level 10, i at level 200, format "'//' 'addi' 'x' r1 , 'x' r2 , i"). -Notation "'slli' 'x' r1 , 'x' r2 , i" := (Slli r1 r2 i) (at level 10, i at level 200, format "'//' 'slli' 'x' r1 , 'x' r2 , i"). -Notation "'slti' 'x' r1 , 'x' r2 , i" := (Slti r1 r2 i) (at level 10, i at level 200, format "'//' 'slti' 'x' r1 , 'x' r2 , i"). -Notation "'sltiu' 'x' r1 , 'x' r2 , i" := (Sltiu r1 r2 i) (at level 10, i at level 200, format "'//' 'sltiu' 'x' r1 , 'x' r2 , i"). -Notation "'xori' 'x' r1 , 'x' r2 , i" := (Xori r1 r2 i) (at level 10, i at level 200, format "'//' 'xori' 'x' r1 , 'x' r2 , i"). -Notation "'ori' 'x' r1 , 'x' r2 , i" := (Ori r1 r2 i) (at level 10, i at level 200, format "'//' 'ori' 'x' r1 , 'x' r2 , i"). -Notation "'andi' 'x' r1 , 'x' r2 , i" := (Andi r1 r2 i) (at level 10, i at level 200, format "'//' 'andi' 'x' r1 , 'x' r2 , i"). -Notation "'srli' 'x' r1 , 'x' r2 , i" := (Srli r1 r2 i) (at level 10, i at level 200, format "'//' 'srli' 'x' r1 , 'x' r2 , i"). -Notation "'srai' 'x' r1 , 'x' r2 , i" := (Srai r1 r2 i) (at level 10, i at level 200, format "'//' 'srai' 'x' r1 , 'x' r2 , i"). -Notation "'auipc' 'x' r1 , i" := (Auipc r1 i) (at level 10, i at level 200, format "'//' 'auipc' 'x' r1 , i"). -Notation "'sb' 'x' r1 , 'x' r2 , i" := (Sb r1 r2 i) (at level 10, i at level 200, format "'//' 'sb' 'x' r1 , 'x' r2 , i"). -Notation "'sh' 'x' r1 , 'x' r2 , i" := (Sh r1 r2 i) (at level 10, i at level 200, format "'//' 'sh' 'x' r1 , 'x' r2 , i"). -Notation "'sw' 'x' r1 , 'x' r2 , i" := (Sw r1 r2 i) (at level 10, i at level 200, format "'//' 'sw' 'x' r1 , 'x' r2 , i"). -Notation "'add' 'x' r1 , 'x' r2 , 'x' r3" := (Add r1 r2 r3) (at level 10, format "'//' 'add' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sub' 'x' r1 , 'x' r2 , 'x' r3" := (Sub r1 r2 r3) (at level 10, format "'//' 'sub' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sll' 'x' r1 , 'x' r2 , 'x' r3" := (Sll r1 r2 r3) (at level 10, format "'//' 'sll' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'slt' 'x' r1 , 'x' r2 , 'x' r3" := (Slt r1 r2 r3) (at level 10, format "'//' 'slt' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sltu' 'x' r1 , 'x' r2 , 'x' r3" := (Sltu r1 r2 r3) (at level 10, format "'//' 'sltu' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'xor' 'x' r1 , 'x' r2 , 'x' r3" := (Xor r1 r2 r3) (at level 10, format "'//' 'xor' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'srl' 'x' r1 , 'x' r2 , 'x' r3" := (Srl r1 r2 r3) (at level 10, format "'//' 'srl' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'sra' 'x' r1 , 'x' r2 , 'x' r3" := (Sra r1 r2 r3) (at level 10, format "'//' 'sra' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'or' 'x' r1 , 'x' r2 , 'x' r3" := (Or r1 r2 r3) (at level 10, format "'//' 'or' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'and' 'x' r1 , 'x' r2 , 'x' r3" := (And r1 r2 r3) (at level 10, format "'//' 'and' 'x' r1 , 'x' r2 , 'x' r3"). -Notation "'lui' 'x' r1 , i" := (Lui r1 i) (at level 10, i at level 200, format "'//' 'lui' 'x' r1 , i"). -Notation "'beq' 'x' r1 , 'x' r2 , i" := (Beq r1 r2 i) (at level 10, i at level 200, format "'//' 'beq' 'x' r1 , 'x' r2 , i"). -Notation "'bne' 'x' r1 , 'x' r2 , i" := (Bne r1 r2 i) (at level 10, i at level 200, format "'//' 'bne' 'x' r1 , 'x' r2 , i"). -Notation "'blt' 'x' r1 , 'x' r2 , i" := (Blt r1 r2 i) (at level 10, i at level 200, format "'//' 'blt' 'x' r1 , 'x' r2 , i"). -Notation "'bge' 'x' r1 , 'x' r2 , i" := (Bge r1 r2 i) (at level 10, i at level 200, format "'//' 'bge' 'x' r1 , 'x' r2 , i"). -Notation "'bltu' 'x' r1 , 'x' r2 , i" := (Bltu r1 r2 i) (at level 10, i at level 200, format "'//' 'bltu' 'x' r1 , 'x' r2 , i"). -Notation "'bgeu' 'x' r1 , 'x' r2 , i" := (Bgeu r1 r2 i) (at level 10, i at level 200, format "'//' 'bgeu' 'x' r1 , 'x' r2 , i"). -Notation "'jalr' 'x' r1 , 'x' r2 , i" := (Jalr r1 r2 i) (at level 10, i at level 200, format "'//' 'jalr' 'x' r1 , 'x' r2 , i"). -Notation "'jal' 'x' r1 , i" := (Jal r1 i) (at level 10, i at level 200, format "'//' 'jal' 'x' r1 , i"). -Notation "'ecall'" := (Ecall) (at level 10, format "'//' 'ecall'"). -Notation "'ebreak'" := (Ebreak) (at level 10, format "'//' 'ebreak'"). -Notation "'uret'" := (Uret) (at level 10, format "'//' 'uret'"). -Notation "'sret'" := (Sret) (at level 10, format "'//' 'sret'"). -Notation "'mret'" := (Mret) (at level 10, format "'//' 'mret'"). -Notation "'wfi'" := (Wfi) (at level 10, format "'//' 'wfi'"). -Notation "'sfence_vma' 'x' r1 , 'x' r2" := (Sfence_vma r1 r2) (at level 10, format "'//' 'sfence_vma' 'x' r1 , 'x' r2"). -Notation "'csrrw' 'x' r1 , 'x' r2 , i" := (Csrrw r1 r2 i) (at level 10, i at level 200, format "'//' 'csrrw' 'x' r1 , 'x' r2 , i"). -Notation "'csrrs' 'x' r1 , 'x' r2 , i" := (Csrrs r1 r2 i) (at level 10, i at level 200, format "'//' 'csrrs' 'x' r1 , 'x' r2 , i"). -Notation "'csrrc' 'x' r1 , 'x' r2 , i" := (Csrrc r1 r2 i) (at level 10, i at level 200, format "'//' 'csrrc' 'x' r1 , 'x' r2 , i"). -Notation "'csrrwi' 'x' r1 , i , j" := (Csrrwi r1 i j) (at level 10, i at level 200, j at level 200, format "'//' 'csrrwi' 'x' r1 , i , j"). -Notation "'csrrsi' 'x' r1 , i , j" := (Csrrsi r1 i j) (at level 10, i at level 200, j at level 200, format "'//' 'csrrsi' 'x' r1 , i , j"). -Notation "'csrrci' 'x' r1 , i , j" := (Csrrci r1 i j) (at level 10, i at level 200, j at level 200, format "'//' 'csrrci' 'x' r1 , i , j"). -Notation "'lr_d' 'x' r1 , 'x' r2 , i" := (Lr_d r1 r2 i) (at level 10, i at level 200, format "'//' 'lr_d' 'x' r1 , 'x' r2 , i"). -Notation "'sc_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Sc_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'sc_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoswap_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoswap_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoswap_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoadd_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoadd_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoadd_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoand_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoand_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoand_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoor_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoor_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoor_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoxor_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoxor_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoxor_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomax_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomax_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomax_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomaxu_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomaxu_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomaxu_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomin_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomin_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomin_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amominu_d' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amominu_d r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amominu_d' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'lr_w' 'x' r1 , 'x' r2 , i" := (Lr_w r1 r2 i) (at level 10, i at level 200, format "'//' 'lr_w' 'x' r1 , 'x' r2 , i"). -Notation "'sc_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Sc_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'sc_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoswap_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoswap_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoswap_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoadd_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoadd_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoadd_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoand_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoand_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoand_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoor_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoor_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoor_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amoxor_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amoxor_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amoxor_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomax_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomax_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomax_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomaxu_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomaxu_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomaxu_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amomin_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amomin_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amomin_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). -Notation "'amominu_w' 'x' r1 , 'x' r2 , 'x' r3 , i" := (Amominu_w r1 r2 r3 i) (at level 10, i at level 200, format "'//' 'amominu_w' 'x' r1 , 'x' r2 , 'x' r3 , i"). +Notation "'RISCV:' x y .. z" := + (@cons Instruction x (@cons Instruction y .. (@cons Instruction z nil) ..)) + (at level 10, format "'RISCV:' x y .. z '//'"). + +Notation "'mulw' rd , rs1 , rs2" := (Mulw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'mulw' rd , rs1 , rs2"). +Notation "'divw' rd , rs1 , rs2" := (Divw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'divw' rd , rs1 , rs2"). +Notation "'divuw' rd , rs1 , rs2" := (Divuw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'divuw' rd , rs1 , rs2"). +Notation "'remw' rd , rs1 , rs2" := (Remw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'remw' rd , rs1 , rs2"). +Notation "'remuw' rd , rs1 , rs2" := (Remuw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'remuw' rd , rs1 , rs2"). +Notation "'mul' rd , rs1 , rs2" := (Mul rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'mul' rd , rs1 , rs2"). +Notation "'mulh' rd , rs1 , rs2" := (Mulh rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'mulh' rd , rs1 , rs2"). +Notation "'mulhsu' rd , rs1 , rs2" := (Mulhsu rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'mulhsu' rd , rs1 , rs2"). +Notation "'mulhu' rd , rs1 , rs2" := (Mulhu rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'mulhu' rd , rs1 , rs2"). +Notation "'div' rd , rs1 , rs2" := (Div rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'div' rd , rs1 , rs2"). +Notation "'divu' rd , rs1 , rs2" := (Divu rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'divu' rd , rs1 , rs2"). +Notation "'rem' rd , rs1 , rs2" := (Rem rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'rem' rd , rs1 , rs2"). +Notation "'remu' rd , rs1 , rs2" := (Remu rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'remu' rd , rs1 , rs2"). +Notation "'ld' rd , rs1 , oimm12" := (Ld rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'ld' rd , rs1 , oimm12"). +Notation "'lwu' rd , rs1 , oimm12" := (Lwu rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lwu' rd , rs1 , oimm12"). +Notation "'addiw' rd , rs1 , imm12" := (Addiw rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'addiw' rd , rs1 , imm12"). +Notation "'slliw' rd , rs1 , shamt5" := (Slliw rd rs1 shamt5) + (at level 10, rd custom register_name, rs1 custom register_name, shamt5 constr at level 35, + format "'//' 'slliw' rd , rs1 , shamt5"). +Notation "'srliw' rd , rs1 , shamt5" := (Srliw rd rs1 shamt5) + (at level 10, rd custom register_name, rs1 custom register_name, shamt5 constr at level 35, + format "'//' 'srliw' rd , rs1 , shamt5"). +Notation "'sraiw' rd , rs1 , shamt5" := (Sraiw rd rs1 shamt5) + (at level 10, rd custom register_name, rs1 custom register_name, shamt5 constr at level 35, + format "'//' 'sraiw' rd , rs1 , shamt5"). +Notation "'sd' rs1 , rs2 , simm12" := (Sd rs1 rs2 simm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, simm12 constr at level 35, + format "'//' 'sd' rs1 , rs2 , simm12"). +Notation "'addw' rd , rs1 , rs2" := (Addw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'addw' rd , rs1 , rs2"). +Notation "'subw' rd , rs1 , rs2" := (Subw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'subw' rd , rs1 , rs2"). +Notation "'sllw' rd , rs1 , rs2" := (Sllw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sllw' rd , rs1 , rs2"). +Notation "'srlw' rd , rs1 , rs2" := (Srlw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'srlw' rd , rs1 , rs2"). +Notation "'sraw' rd , rs1 , rs2" := (Sraw rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sraw' rd , rs1 , rs2"). +Notation "'lb' rd , rs1 , oimm12" := (Lb rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lb' rd , rs1 , oimm12"). +Notation "'lh' rd , rs1 , oimm12" := (Lh rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lh' rd , rs1 , oimm12"). +Notation "'lw' rd , rs1 , oimm12" := (Lw rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lw' rd , rs1 , oimm12"). +Notation "'lbu' rd , rs1 , oimm12" := (Lbu rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lbu' rd , rs1 , oimm12"). +Notation "'lhu' rd , rs1 , oimm12" := (Lhu rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'lhu' rd , rs1 , oimm12"). +Notation "'fence' pred , succ" := (Fence pred succ) + (at level 10, pred constr at level 35, succ constr at level 35, + format "'//' 'fence' pred , succ"). +Notation "'fence_i'" := Fence_i (at level 10, format "'//' 'fence_i'"). +Notation "'addi' rd , rs1 , imm12" := (Addi rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'addi' rd , rs1 , imm12"). +Notation "'slli' rd , rs1 , shamt6" := (Slli rd rs1 shamt6) + (at level 10, rd custom register_name, rs1 custom register_name, shamt6 constr at level 35, + format "'//' 'slli' rd , rs1 , shamt6"). +Notation "'slti' rd , rs1 , imm12" := (Slti rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'slti' rd , rs1 , imm12"). +Notation "'sltiu' rd , rs1 , imm12" := (Sltiu rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'sltiu' rd , rs1 , imm12"). +Notation "'xori' rd , rs1 , imm12" := (Xori rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'xori' rd , rs1 , imm12"). +Notation "'ori' rd , rs1 , imm12" := (Ori rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'ori' rd , rs1 , imm12"). +Notation "'andi' rd , rs1 , imm12" := (Andi rd rs1 imm12) + (at level 10, rd custom register_name, rs1 custom register_name, imm12 constr at level 35, + format "'//' 'andi' rd , rs1 , imm12"). +Notation "'srli' rd , rs1 , shamt6" := (Srli rd rs1 shamt6) + (at level 10, rd custom register_name, rs1 custom register_name, shamt6 constr at level 35, + format "'//' 'srli' rd , rs1 , shamt6"). +Notation "'srai' rd , rs1 , shamt6" := (Srai rd rs1 shamt6) + (at level 10, rd custom register_name, rs1 custom register_name, shamt6 constr at level 35, + format "'//' 'srai' rd , rs1 , shamt6"). +Notation "'auipc' rd , oimm20" := (Auipc rd oimm20) + (at level 10, rd custom register_name, oimm20 constr at level 35, + format "'//' 'auipc' rd , oimm20"). +Notation "'sb' rs1 , rs2 , simm12" := (Sb rs1 rs2 simm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, simm12 constr at level 35, + format "'//' 'sb' rs1 , rs2 , simm12"). +Notation "'sh' rs1 , rs2 , simm12" := (Sh rs1 rs2 simm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, simm12 constr at level 35, + format "'//' 'sh' rs1 , rs2 , simm12"). +Notation "'sw' rs1 , rs2 , simm12" := (Sw rs1 rs2 simm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, simm12 constr at level 35, + format "'//' 'sw' rs1 , rs2 , simm12"). +Notation "'add' rd , rs1 , rs2" := (Add rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'add' rd , rs1 , rs2"). +Notation "'sub' rd , rs1 , rs2" := (Sub rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sub' rd , rs1 , rs2"). +Notation "'sll' rd , rs1 , rs2" := (Sll rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sll' rd , rs1 , rs2"). +Notation "'slt' rd , rs1 , rs2" := (Slt rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'slt' rd , rs1 , rs2"). +Notation "'sltu' rd , rs1 , rs2" := (Sltu rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sltu' rd , rs1 , rs2"). +Notation "'xor' rd , rs1 , rs2" := (Xor rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'xor' rd , rs1 , rs2"). +Notation "'srl' rd , rs1 , rs2" := (Srl rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'srl' rd , rs1 , rs2"). +Notation "'sra' rd , rs1 , rs2" := (Sra rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sra' rd , rs1 , rs2"). +Notation "'or' rd , rs1 , rs2" := (Or rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'or' rd , rs1 , rs2"). +Notation "'and' rd , rs1 , rs2" := (And rd rs1 rs2) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, + format "'//' 'and' rd , rs1 , rs2"). +Notation "'lui' rd , imm20" := (Lui rd imm20) + (at level 10, rd custom register_name, imm20 constr at level 35, + format "'//' 'lui' rd , imm20"). +Notation "'beq' rs1 , rs2 , sbimm12" := (Beq rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'beq' rs1 , rs2 , sbimm12"). +Notation "'bne' rs1 , rs2 , sbimm12" := (Bne rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'bne' rs1 , rs2 , sbimm12"). +Notation "'blt' rs1 , rs2 , sbimm12" := (Blt rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'blt' rs1 , rs2 , sbimm12"). +Notation "'bge' rs1 , rs2 , sbimm12" := (Bge rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'bge' rs1 , rs2 , sbimm12"). +Notation "'bltu' rs1 , rs2 , sbimm12" := (Bltu rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'bltu' rs1 , rs2 , sbimm12"). +Notation "'bgeu' rs1 , rs2 , sbimm12" := (Bgeu rs1 rs2 sbimm12) + (at level 10, rs1 custom register_name, rs2 custom register_name, sbimm12 constr at level 35, + format "'//' 'bgeu' rs1 , rs2 , sbimm12"). +Notation "'jalr' rd , rs1 , oimm12" := (Jalr rd rs1 oimm12) + (at level 10, rd custom register_name, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'jalr' rd , rs1 , oimm12"). +Notation "'jal' rd , jimm20" := (Jal rd jimm20) + (at level 10, rd custom register_name, jimm20 constr at level 35, + format "'//' 'jal' rd , jimm20"). +Notation "'fcvt_l_s' rd , rs1 , rm" := (Fcvt_l_s rd rs1 rm) + (at level 10, rd custom register_name, rs1 constr at level 35, rm constr at level 35, + format "'//' 'fcvt_l_s' rd , rs1 , rm"). +Notation "'fcvt_lu_s' rd , rs1 , rm" := (Fcvt_lu_s rd rs1 rm) + (at level 10, rd custom register_name, rs1 constr at level 35, rm constr at level 35, + format "'//' 'fcvt_lu_s' rd , rs1 , rm"). +Notation "'fcvt_s_l' rd , rs1 , rm" := (Fcvt_s_l rd rs1 rm) + (at level 10, rd constr at level 35, rs1 custom register_name, rm constr at level 35, + format "'//' 'fcvt_s_l' rd , rs1 , rm"). +Notation "'fcvt_s_lu' rd , rs1 , rm" := (Fcvt_s_lu rd rs1 rm) + (at level 10, rd constr at level 35, rs1 custom register_name, rm constr at level 35, + format "'//' 'fcvt_s_lu' rd , rs1 , rm"). +Notation "'flw' rd , rs1 , oimm12" := (Flw rd rs1 oimm12) + (at level 10, rd constr at level 35, rs1 custom register_name, oimm12 constr at level 35, + format "'//' 'flw' rd , rs1 , oimm12"). +Notation "'fsw' rs1 , rs2 , simm12" := (Fsw rs1 rs2 simm12) + (at level 10, rs1 custom register_name, rs2 constr at level 35, simm12 constr at level 35, + format "'//' 'fsw' rs1 , rs2 , simm12"). +Notation "'fmadd_s' rd , rs1 , rs2 , rs3 , rm" := (Fmadd_s rd rs1 rs2 rs3 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rs3 constr at level 35, rm constr at level 35, + format "'//' 'fmadd_s' rd , rs1 , rs2 , rs3 , rm"). +Notation "'fmsub_s' rd , rs1 , rs2 , rs3 , rm" := (Fmsub_s rd rs1 rs2 rs3 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rs3 constr at level 35, rm constr at level 35, + format "'//' 'fmsub_s' rd , rs1 , rs2 , rs3 , rm"). +Notation "'fnmsub_s' rd , rs1 , rs2 , rs3 , rm" := (Fnmsub_s rd rs1 rs2 rs3 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rs3 constr at level 35, rm constr at level 35, + format "'//' 'fnmsub_s' rd , rs1 , rs2 , rs3 , rm"). +Notation "'fnmadd_s' rd , rs1 , rs2 , rs3 , rm" := (Fnmadd_s rd rs1 rs2 rs3 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rs3 constr at level 35, rm constr at level 35, + format "'//' 'fnmadd_s' rd , rs1 , rs2 , rs3 , rm"). +Notation "'fadd_s' rd , rs1 , rs2 , rm" := (Fadd_s rd rs1 rs2 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rm constr at level 35, + format "'//' 'fadd_s' rd , rs1 , rs2 , rm"). +Notation "'fsub_s' rd , rs1 , rs2 , rm" := (Fsub_s rd rs1 rs2 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rm constr at level 35, + format "'//' 'fsub_s' rd , rs1 , rs2 , rm"). +Notation "'fmul_s' rd , rs1 , rs2 , rm" := (Fmul_s rd rs1 rs2 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rm constr at level 35, + format "'//' 'fmul_s' rd , rs1 , rs2 , rm"). +Notation "'fdiv_s' rd , rs1 , rs2 , rm" := (Fdiv_s rd rs1 rs2 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, rm constr at level 35, + format "'//' 'fdiv_s' rd , rs1 , rs2 , rm"). +Notation "'fsqrt_s' rd , rs1 , rm" := (Fsqrt_s rd rs1 rm) + (at level 10, rd constr at level 35, rs1 constr at level 35, rm constr at level 35, + format "'//' 'fsqrt_s' rd , rs1 , rm"). +Notation "'fsgnj_s' rd , rs1 , rs2" := (Fsgnj_s rd rs1 rs2) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fsgnj_s' rd , rs1 , rs2"). +Notation "'fsgnjn_s' rd , rs1 , rs2" := (Fsgnjn_s rd rs1 rs2) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fsgnjn_s' rd , rs1 , rs2"). +Notation "'fsgnjx_s' rd , rs1 , rs2" := (Fsgnjx_s rd rs1 rs2) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fsgnjx_s' rd , rs1 , rs2"). +Notation "'fmin_s' rd , rs1 , rs2" := (Fmin_s rd rs1 rs2) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fmin_s' rd , rs1 , rs2"). +Notation "'fmax_s' rd , rs1 , rs2" := (Fmax_s rd rs1 rs2) + (at level 10, rd constr at level 35, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fmax_s' rd , rs1 , rs2"). +Notation "'fcvt_w_s' rd , rs1 , rm" := (Fcvt_w_s rd rs1 rm) + (at level 10, rd custom register_name, rs1 constr at level 35, rm constr at level 35, + format "'//' 'fcvt_w_s' rd , rs1 , rm"). +Notation "'fcvt_wu_s' rd , rs1 , rm" := (Fcvt_wu_s rd rs1 rm) + (at level 10, rd custom register_name, rs1 constr at level 35, rm constr at level 35, + format "'//' 'fcvt_wu_s' rd , rs1 , rm"). +Notation "'fmv_x_w' rd , rs1" := (Fmv_x_w rd rs1) + (at level 10, rd custom register_name, rs1 constr at level 35, + format "'//' 'fmv_x_w' rd , rs1"). +Notation "'feq_s' rd , rs1 , rs2" := (Feq_s rd rs1 rs2) + (at level 10, rd custom register_name, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'feq_s' rd , rs1 , rs2"). +Notation "'flt_s' rd , rs1 , rs2" := (Flt_s rd rs1 rs2) + (at level 10, rd custom register_name, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'flt_s' rd , rs1 , rs2"). +Notation "'fle_s' rd , rs1 , rs2" := (Fle_s rd rs1 rs2) + (at level 10, rd custom register_name, rs1 constr at level 35, rs2 constr at level 35, + format "'//' 'fle_s' rd , rs1 , rs2"). +Notation "'fclass_s' rd , rs1" := (Fclass_s rd rs1) + (at level 10, rd custom register_name, rs1 constr at level 35, + format "'//' 'fclass_s' rd , rs1"). +Notation "'fcvt_s_w' rd , rs1 , rm" := (Fcvt_s_w rd rs1 rm) + (at level 10, rd constr at level 35, rs1 custom register_name, rm constr at level 35, + format "'//' 'fcvt_s_w' rd , rs1 , rm"). +Notation "'fcvt_s_wu' rd , rs1 , rm" := (Fcvt_s_wu rd rs1 rm) + (at level 10, rd constr at level 35, rs1 custom register_name, rm constr at level 35, + format "'//' 'fcvt_s_wu' rd , rs1 , rm"). +Notation "'fmv_w_x' rd , rs1" := (Fmv_w_x rd rs1) + (at level 10, rd constr at level 35, rs1 custom register_name, + format "'//' 'fmv_w_x' rd , rs1"). +Notation "'ecall'" := Ecall (at level 10, format "'//' 'ecall'"). +Notation "'ebreak'" := Ebreak (at level 10, format "'//' 'ebreak'"). +Notation "'uret'" := Uret (at level 10, format "'//' 'uret'"). +Notation "'sret'" := Sret (at level 10, format "'//' 'sret'"). +Notation "'mret'" := Mret (at level 10, format "'//' 'mret'"). +Notation "'wfi'" := Wfi (at level 10, format "'//' 'wfi'"). +Notation "'sfence_vma' rs1 , rs2" := (Sfence_vma rs1 rs2) + (at level 10, rs1 custom register_name, rs2 custom register_name, + format "'//' 'sfence_vma' rs1 , rs2"). +Notation "'csrrw' rd , rs1 , csr12" := (Csrrw rd rs1 csr12) + (at level 10, rd custom register_name, rs1 custom register_name, csr12 constr at level 35, + format "'//' 'csrrw' rd , rs1 , csr12"). +Notation "'csrrs' rd , rs1 , csr12" := (Csrrs rd rs1 csr12) + (at level 10, rd custom register_name, rs1 custom register_name, csr12 constr at level 35, + format "'//' 'csrrs' rd , rs1 , csr12"). +Notation "'csrrc' rd , rs1 , csr12" := (Csrrc rd rs1 csr12) + (at level 10, rd custom register_name, rs1 custom register_name, csr12 constr at level 35, + format "'//' 'csrrc' rd , rs1 , csr12"). +Notation "'csrrwi' rd , zimm , csr12" := (Csrrwi rd zimm csr12) + (at level 10, rd custom register_name, zimm constr at level 35, csr12 constr at level 35, + format "'//' 'csrrwi' rd , zimm , csr12"). +Notation "'csrrsi' rd , zimm , csr12" := (Csrrsi rd zimm csr12) + (at level 10, rd custom register_name, zimm constr at level 35, csr12 constr at level 35, + format "'//' 'csrrsi' rd , zimm , csr12"). +Notation "'csrrci' rd , zimm , csr12" := (Csrrci rd zimm csr12) + (at level 10, rd custom register_name, zimm constr at level 35, csr12 constr at level 35, + format "'//' 'csrrci' rd , zimm , csr12"). +Notation "'lr_d' rd , rs1 , aqrl" := (Lr_d rd rs1 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, aqrl constr at level 35, + format "'//' 'lr_d' rd , rs1 , aqrl"). +Notation "'sc_d' rd , rs1 , rs2 , aqrl" := (Sc_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'sc_d' rd , rs1 , rs2 , aqrl"). +Notation "'amoswap_d' rd , rs1 , rs2 , aqrl" := (Amoswap_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoswap_d' rd , rs1 , rs2 , aqrl"). +Notation "'amoadd_d' rd , rs1 , rs2 , aqrl" := (Amoadd_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoadd_d' rd , rs1 , rs2 , aqrl"). +Notation "'amoand_d' rd , rs1 , rs2 , aqrl" := (Amoand_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoand_d' rd , rs1 , rs2 , aqrl"). +Notation "'amoor_d' rd , rs1 , rs2 , aqrl" := (Amoor_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoor_d' rd , rs1 , rs2 , aqrl"). +Notation "'amoxor_d' rd , rs1 , rs2 , aqrl" := (Amoxor_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoxor_d' rd , rs1 , rs2 , aqrl"). +Notation "'amomax_d' rd , rs1 , rs2 , aqrl" := (Amomax_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomax_d' rd , rs1 , rs2 , aqrl"). +Notation "'amomaxu_d' rd , rs1 , rs2 , aqrl" := (Amomaxu_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomaxu_d' rd , rs1 , rs2 , aqrl"). +Notation "'amomin_d' rd , rs1 , rs2 , aqrl" := (Amomin_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomin_d' rd , rs1 , rs2 , aqrl"). +Notation "'amominu_d' rd , rs1 , rs2 , aqrl" := (Amominu_d rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amominu_d' rd , rs1 , rs2 , aqrl"). +Notation "'lr_w' rd , rs1 , aqrl" := (Lr_w rd rs1 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, aqrl constr at level 35, + format "'//' 'lr_w' rd , rs1 , aqrl"). +Notation "'sc_w' rd , rs1 , rs2 , aqrl" := (Sc_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'sc_w' rd , rs1 , rs2 , aqrl"). +Notation "'amoswap_w' rd , rs1 , rs2 , aqrl" := (Amoswap_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoswap_w' rd , rs1 , rs2 , aqrl"). +Notation "'amoadd_w' rd , rs1 , rs2 , aqrl" := (Amoadd_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoadd_w' rd , rs1 , rs2 , aqrl"). +Notation "'amoand_w' rd , rs1 , rs2 , aqrl" := (Amoand_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoand_w' rd , rs1 , rs2 , aqrl"). +Notation "'amoor_w' rd , rs1 , rs2 , aqrl" := (Amoor_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoor_w' rd , rs1 , rs2 , aqrl"). +Notation "'amoxor_w' rd , rs1 , rs2 , aqrl" := (Amoxor_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amoxor_w' rd , rs1 , rs2 , aqrl"). +Notation "'amomax_w' rd , rs1 , rs2 , aqrl" := (Amomax_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomax_w' rd , rs1 , rs2 , aqrl"). +Notation "'amomaxu_w' rd , rs1 , rs2 , aqrl" := (Amomaxu_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomaxu_w' rd , rs1 , rs2 , aqrl"). +Notation "'amomin_w' rd , rs1 , rs2 , aqrl" := (Amomin_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amomin_w' rd , rs1 , rs2 , aqrl"). +Notation "'amominu_w' rd , rs1 , rs2 , aqrl" := (Amominu_w rd rs1 rs2 aqrl) + (at level 10, rd custom register_name, rs1 custom register_name, rs2 custom register_name, aqrl constr at level 35, + format "'//' 'amominu_w' rd , rs1 , rs2 , aqrl"). diff --git a/src/riscv/Utility/RegisterNameNotations.v b/src/riscv/Utility/RegisterNameNotations.v new file mode 100644 index 0000000..0514d2d --- /dev/null +++ b/src/riscv/Utility/RegisterNameNotations.v @@ -0,0 +1,35 @@ +Require Import Coq.ZArith.BinInt. +Declare Custom Entry register_name. + +Notation "'zero'" := 0%Z (in custom register_name). +Notation "'ra'" := 1%Z (in custom register_name). +Notation "'sp'" := 2%Z (in custom register_name). +Notation "'gp'" := 3%Z (in custom register_name). +Notation "'tp'" := 4%Z (in custom register_name). +Notation "'t0'" := 5%Z (in custom register_name). +Notation "'t1'" := 6%Z (in custom register_name). +Notation "'t2'" := 7%Z (in custom register_name). +Notation "'s0'" := 8%Z (in custom register_name). +Notation "'s1'" := 9%Z (in custom register_name). +Notation "'a0'" := 10%Z (in custom register_name). +Notation "'a1'" := 11%Z (in custom register_name). +Notation "'a2'" := 12%Z (in custom register_name). +Notation "'a3'" := 13%Z (in custom register_name). +Notation "'a4'" := 14%Z (in custom register_name). +Notation "'a5'" := 15%Z (in custom register_name). +Notation "'a6'" := 16%Z (in custom register_name). +Notation "'a7'" := 17%Z (in custom register_name). +Notation "'s2'" := 18%Z (in custom register_name). +Notation "'s3'" := 19%Z (in custom register_name). +Notation "'s4'" := 20%Z (in custom register_name). +Notation "'s5'" := 21%Z (in custom register_name). +Notation "'s6'" := 22%Z (in custom register_name). +Notation "'s7'" := 23%Z (in custom register_name). +Notation "'s8'" := 24%Z (in custom register_name). +Notation "'s9'" := 25%Z (in custom register_name). +Notation "'s10'" := 26%Z (in custom register_name). +Notation "'s11'" := 27%Z (in custom register_name). +Notation "'t3'" := 28%Z (in custom register_name). +Notation "'t4'" := 29%Z (in custom register_name). +Notation "'t5'" := 30%Z (in custom register_name). +Notation "'t6'" := 31%Z (in custom register_name). diff --git a/src/riscv/Utility/make_InstructionNotations.py b/src/riscv/Utility/make_InstructionNotations.py new file mode 100755 index 0000000..55222dc --- /dev/null +++ b/src/riscv/Utility/make_InstructionNotations.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python3 + +import re +import sys + +types = [ + "InstructionM64", + "InstructionM", + "InstructionI64", + "InstructionI", + "InstructionCSR", + "InstructionA64", + "InstructionA", + "InstructionF64", + "InstructionF", +] + +def ends_with_colon_instruction(s): + for tp in types: + if s.endswith(":" + tp): + return True + return False + +print(f"""(* File generated by {sys.argv[0]}, do not edit *) +Require Export riscv.Spec.Decode. +Require Export riscv.Utility.InstructionCoercions. +Require Export riscv.Utility.RegisterNameNotations. + +Notation "'RISCV:' x y .. z" := + (@cons Instruction x (@cons Instruction y .. (@cons Instruction z nil) ..)) + (at level 10, format "'RISCV:' x y .. z '//'"). +""") + +with open('./src/riscv/Spec/Decode.v', 'r') as file: + chunks = file.read().replace('\n', '').replace(' ', '').split('|') + ctors = filter(ends_with_colon_instruction, chunks) + for s in ctors: + s = re.sub(":Instruction[^:]+$", "", s) + parts = s.replace(')', '').split('(') + iname = parts[0] + argtuples = [part.split(':') for part in parts[1:]] + if len(argtuples) == 0: + print(f"""Notation "'{iname.lower()}'" := {iname} (at level 10, format "'//' '{iname.lower()}'").""") + else: + argnames = [argname for [argname, argtype] in argtuples] + print(f"""Notation "'{iname.lower()}' {' , '.join(argnames)}" := ({iname} {' '.join(argnames)}) + (at level 10, {', '.join([argname + (' custom register_name' if argtype == 'Register' else ' constr at level 35') for [argname, argtype] in argtuples])}, + format "'//' '{iname.lower()}'{' ' * (7 - len(iname))} {' , '.join(argnames)}").""") diff --git a/src/riscv/Utility/make_InstructionNotations.sh b/src/riscv/Utility/make_InstructionNotations.sh deleted file mode 100755 index 6fc1428..0000000 --- a/src/riscv/Utility/make_InstructionNotations.sh +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/sh - -F="./src/riscv/Utility/InstructionNotations.v" - -echo "(* File generated by ./make_InstructionNotations.sh, do not edit *)" > "$F" -echo "Require Export riscv.Spec.Decode." >> "$F" -echo "Require Export riscv.Utility.InstructionCoercions." >> "$F" -echo 'Notation "!RISCV:! x y .. z" := (@cons Instruction x (@cons Instruction y .. (@cons Instruction z nil) ..)) (at level 10).' | tr '!' "'" >> "$F" - -echo "" >> "$F" - -cat ./src/riscv/Utility/PrintInstructions.v.redirect \ - | coqtop -Q ../coqutil/src/coqutil coqutil -R ./src/riscv riscv \ - | grep -E -e '^ . .*Instruction(M64|M|I64|I|CSR|A64|A)$' \ - | grep -v 'Invalid' \ - | sed -E \ - -e 's/MachineInt/Z/g' \ - -e 's/^ / | /g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Register -> Register -> Z -> Instruction.*/Notation "!\L\1\2! !x! r1 , !x! r2 , !x! r3 , i" := (\U\1\L\2 r1 r2 r3 i) (at level 10, i at level 200, format "!\/\/! !\L\1\2!%fill%!x! r1 , !x! r2 , !x! r3 , i")./g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Register -> Register -> Instruction.*/Notation "!\L\1\2! !x! r1 , !x! r2 , !x! r3" := (\U\1\L\2 r1 r2 r3) (at level 10, format "!\/\/! !\L\1\2!%fill%!x! r1 , !x! r2 , !x! r3")./g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Register -> Z -> Instruction.*/Notation "!\L\1\2! !x! r1 , !x! r2 , i" := (\U\1\L\2 r1 r2 i) (at level 10, i at level 200, format "!\/\/! !\L\1\2!%fill%!x! r1 , !x! r2 , i")./g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Z -> Z -> Instruction.*/Notation "!\L\1\2! !x! r1 , i , j" := (\U\1\L\2 r1 i j) (at level 10, i at level 200, j at level 200, format "!\/\/! !\L\1\2!%fill%!x! r1 , i , j")./g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Register -> Instruction.*/Notation "!\L\1\2! !x! r1 , !x! r2" := (\U\1\L\2 r1 r2) (at level 10, format "!\/\/! !\L\1\2!%fill%!x! r1 , !x! r2")./g' \ - -e 's/ *\| *(.)([^ ]+) : Register -> Z -> Instruction.*/Notation "!\L\1\2! !x! r1 , i" := (\U\1\L\2 r1 i) (at level 10, i at level 200, format "!\/\/! !\L\1\2!%fill%!x! r1 , i")./g' \ - -e 's/ *\| *(.)([^ ]+) : Z -> Z -> Instruction.*/Notation "!\L\1\2! i , j" := (\U\1\L\2 i j) (at level 10, i at level 200, j at level 200, format "!\/\/! !\L\1\2!%fill%i , j")./g' \ - -e 's/ *\| *(.)([^ ]+) : Instruction.*/Notation "!\L\1\2!" := (\U\1\L\2) (at level 10, format "!\/\/! !\L\1\2!")./g' \ - -e 's/(remove this text to debug) *\| *(.*)/(*\0*)/g' \ - -e 's/\!(.)\!%fill%/!\1! /g' \ - -e 's/\!(..)\!%fill%/!\1! /g' \ - -e 's/\!(...)\!%fill%/!\1! /g' \ - -e 's/\!(....)\!%fill%/!\1! /g' \ - -e 's/\!(.....)\!%fill%/!\1! /g' \ - -e 's/\!(......)\!%fill%/!\1! /g' \ - -e 's/\!(.+)\!%fill%/!\1! /g' \ - | tr '!' "'" >> "$F"