Tsukasa OI a4lg

a4lg / .gdbinit

Last active June 3, 2021 03:20

GDB initialization file I am using for JTAG-based debugging

	set arch riscv:rv64
	define hook-quit
	set confirm off
	end
	target extended-remote localhost:3333

a4lg / invariant_macro.rs

Created March 9, 2023 05:30

`invariant!` macro to declare an invariant

	// If `unsafe` and `nightly` are enabled, enable unstable `core_intrinsics` feature
	// with #![feature(core_intrinsics)] (Nightly only).

	macro_rules! invariant {
	($expr: expr) => {
	cfg_if::cfg_if! {
	if #[cfg(all(feature = "unsafe", feature = "nightly"))] {
	core::intrinsics::assume($expr);
	}
	else if #[cfg(feature = "unsafe")] {

a4lg / riscv-sim.exp

Created September 3, 2023 13:34

DejaGnu: RISC-V Simulator with QEMU sample

	# Copyright (C) 1997-2019, 2020 Free Software Foundation, Inc.
	#
	# This file is part of DejaGnu. For RISC-V target simulation.
	#
	# DejaGnu is free software; you can redistribute it and/or modify it
	# under the terms of the GNU General Public License as published by
	# the Free Software Foundation; either version 2 of the License, or
	# (at your option) any later version.
	#
	# DejaGnu is distributed in the hope that it will be useful, but

a4lg / riscv-imply-convergence-prover.py

Created April 11, 2025 07:27

Prover: ensure that specific times of loops on certain groups will be sufficient to prove convergence

	#! /bin/env python3
	# SPDX-License-Identifier: MIT
	# SPDX-FileCopyrightText: Copyright (C) 2025 Tsukasa OI <[email protected]>.

	import sys
	import z3

	VARS: dict[str, list[list[any]]] = {}
	N_ITERS = 1

a4lg / riscv-c-implications.py

Last active August 25, 2025 00:49

prover: RISC-V: implication rules around the "C" extension