File: rv_add_decode.unsat.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (26 lines) | stat: -rw-r--r-- 633 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
default Order dec

$include <prelude.sail>

type regbits = bits(5)

enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}

scattered union ast

union clause ast = ITYPE : (bits(12), regbits, regbits, iop)

val decode : bits(32) -> option(ast) effect pure

function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))

function clause decode _ = None()

$property
function prop(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
    Some(ITYPE(_)) => true,
    _ => false
  }
}