Skip to content

Commit

Permalink
support 64bit instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
PhilippvK committed May 30, 2024
1 parent 69e981d commit 04133a7
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 2 deletions.
1 change: 1 addition & 0 deletions examples/cfg/filter.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ filter:
- RVSMode
- RVDebug
- RV32I
- RV64I
- RVNMod
instructions:
# drop: [CV_CLIPU, CV_CLIPR, CV_CLIPUR, CV_SLET, CV_SLETU, SEAL5_CV_SHUFFLE2_B, SEAL5_CV_SHUFFLE2_H, ".*_(SC|SCI)_.*"]
Expand Down
3 changes: 3 additions & 0 deletions seal5/backends/patterngen/writer.py
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ def main():
parser.add_argument("--index", default=None, help="Output index to file")
parser.add_argument("--ext", type=str, default="td", help="Default file extension (if using --splitted)")
parser.add_argument("--parallel", type=int, default=1, help="How many instructions should be processed in parallel")
# parser.add_argument("--xlen", type=int, default=32, help="RISC-V XLEN")
args = parser.parse_args()

# initialize logging
Expand Down Expand Up @@ -109,6 +110,7 @@ def main():

assert out_path.is_dir(), "Expecting output directory when using --splitted"
for set_name, set_def in model["sets"].items():
xlen = set_def.xlen
artifacts[set_name] = []
metrics["n_sets"] += 1
ext_settings = set_def.settings
Expand Down Expand Up @@ -161,6 +163,7 @@ def process_instrunction(instr_def):
skip_formats=not args.formats,
ext=predicate,
mattr=mattr,
xlen=xlen,
)
if output_file.is_file():
metrics["n_success"] += 1
Expand Down
3 changes: 2 additions & 1 deletion seal5/backends/riscv_instr_info/writer.py
Original file line number Diff line number Diff line change
Expand Up @@ -345,6 +345,7 @@ def main():
for set_name, set_def in model["sets"].items():
set_name_lower = set_name.lower()
artifacts[set_name] = []
xlen = set_def.xlen
includes = []
set_dir = out_path / set_name
set_dir.mkdir(exist_ok=True)
Expand All @@ -360,7 +361,7 @@ def main():
content = gen_riscv_instr_info_str(instr_def)
if len(content) > 0:
assert pred is not None
predicate_str = f"Predicates = [{pred}, IsRV32]"
predicate_str = f"Predicates = [{pred}, IsRV{xlen}]"
content = f"let {predicate_str} in {{\n{content}\n}}"
with open(output_file, "w") as f:
f.write(content)
Expand Down
12 changes: 12 additions & 0 deletions seal5/model.py
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
Function,
BaseNode,
InstrAttribute,
MemoryAttribute,
BitField,
BitVal,
DataType,
Expand Down Expand Up @@ -53,6 +54,17 @@ def __init__(
self.registers = registers
self.register_groups = register_groups
self.settings: ExtensionsSettings = None
self._xlen = None

@property
def xlen(self):
if self._xlen is None:
for mem_name, mem_def in self.memories.items():
if mem_name == "X" or MemoryAttribute.IS_MAIN_REG in mem_def.attributes:
self._xlen = mem_def.size
break
assert self._xlen is not None, "Could not determine XLEN"
return self._xlen


class Seal5RegisterClass(IntEnum):
Expand Down
9 changes: 8 additions & 1 deletion seal5/tools/cdsl2llvm.py
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,7 @@ def run_pattern_gen(
verbose: bool = False,
ext=None,
mattr=None,
xlen=None,
skip_formats=False,
skip_patterns=False,
skip_verify=True,
Expand All @@ -139,7 +140,9 @@ def run_pattern_gen(

if ext:
# pattern_gen_args.extend(["--ext", ext])
pattern_gen_args.extend(["-p", f"Has{ext}"])
preds = [f"Has{ext}", f"IsRV{xlen}"]
preds_str = ", ".join(preds)
pattern_gen_args.extend(["-p", preds_str])

if mattr is None:
attrs = ["+m", "+fast-unaligned-access"]
Expand All @@ -152,6 +155,10 @@ def run_pattern_gen(
if mattr:
pattern_gen_args.extend(["--mattr2", mattr])

if xlen:
assert xlen in [32, 64]
pattern_gen_args.extend(["--riscv-xlen", str(xlen)])

if skip_patterns:
pattern_gen_args.append("--skip-patterns")

Expand Down

0 comments on commit 04133a7

Please sign in to comment.