Skip to content

Commit

Permalink
Merge branch 'master' into Zacas_v4
Browse files Browse the repository at this point in the history
Signed-off-by: Ved Shanbhogue <91900059+ved-rivos@users.noreply.github.com>
  • Loading branch information
ved-rivos committed Sep 3, 2023
2 parents d0cc13c + 861bd6f commit 83a0e51
Show file tree
Hide file tree
Showing 4 changed files with 68 additions and 46 deletions.
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>

/* Settings of the platform implementation. */

Expand Down Expand Up @@ -32,5 +33,6 @@ extern uint64_t rv_clint_size;
extern uint64_t rv_htif_tohost;
extern uint64_t rv_insns_per_tick;

extern FILE *trace_log;
extern int term_fd;
void plat_term_write_impl(char c);
9 changes: 5 additions & 4 deletions c_emulator/riscv_prelude.c
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#include "riscv_prelude.h"
#include "riscv_config.h"
#include "riscv_platform_impl.h"

unit print_string(sail_string prefix, sail_string msg)
{
Expand All @@ -10,28 +11,28 @@ unit print_string(sail_string prefix, sail_string msg)
unit print_instr(sail_string s)
{
if (config_print_instr)
printf("%s\n", s);
fprintf(trace_log, "%s\n", s);
return UNIT;
}

unit print_reg(sail_string s)
{
if (config_print_reg)
printf("%s\n", s);
fprintf(trace_log, "%s\n", s);
return UNIT;
}

unit print_mem_access(sail_string s)
{
if (config_print_mem_access)
printf("%s\n", s);
fprintf(trace_log, "%s\n", s);
return UNIT;
}

unit print_platform(sail_string s)
{
if (config_print_platform)
printf("%s\n", s);
fprintf(trace_log, "%s\n", s);
return UNIT;
}

Expand Down
76 changes: 49 additions & 27 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
#include <ctype.h>
#include <getopt.h>
#include <stdio.h>
#include <stdlib.h>
Expand Down Expand Up @@ -48,10 +49,14 @@ const char *RV32ISA = "RV32IMAC";
#define CSR_MTVAL 0x343
#define CSR_MIP 0x344

#define OPT_TRACE_OUTPUT 1000

static bool do_dump_dts = false;
static bool do_show_times = false;
struct tv_spike_t *s = NULL;
char *term_log = NULL;
static const char *trace_log_path = NULL;
FILE *trace_log = NULL;
char *dtb_file = NULL;
unsigned char *dtb = NULL;
size_t dtb_len = 0;
Expand Down Expand Up @@ -111,33 +116,34 @@ char *sailcov_file = NULL;
#endif

static struct option options[] = {
{"enable-dirty-update", no_argument, 0, 'd'},
{"enable-misaligned", no_argument, 0, 'm'},
{"enable-pmp", no_argument, 0, 'P'},
{"enable-next", no_argument, 0, 'N'},
{"ram-size", required_argument, 0, 'z'},
{"disable-compressed", no_argument, 0, 'C'},
{"disable-writable-misa", no_argument, 0, 'I'},
{"disable-fdext", no_argument, 0, 'F'},
{"mtval-has-illegal-inst-bits", no_argument, 0, 'i'},
{"device-tree-blob", required_argument, 0, 'b'},
{"terminal-log", required_argument, 0, 't'},
{"show-times", required_argument, 0, 'p'},
{"report-arch", no_argument, 0, 'a'},
{"test-signature", required_argument, 0, 'T'},
{"signature-granularity", required_argument, 0, 'g'},
{"enable-dirty-update", no_argument, 0, 'd' },
{"enable-misaligned", no_argument, 0, 'm' },
{"enable-pmp", no_argument, 0, 'P' },
{"enable-next", no_argument, 0, 'N' },
{"ram-size", required_argument, 0, 'z' },
{"disable-compressed", no_argument, 0, 'C' },
{"disable-writable-misa", no_argument, 0, 'I' },
{"disable-fdext", no_argument, 0, 'F' },
{"mtval-has-illegal-inst-bits", no_argument, 0, 'i' },
{"device-tree-blob", required_argument, 0, 'b' },
{"terminal-log", required_argument, 0, 't' },
{"show-times", required_argument, 0, 'p' },
{"report-arch", no_argument, 0, 'a' },
{"test-signature", required_argument, 0, 'T' },
{"signature-granularity", required_argument, 0, 'g' },
#ifdef RVFI_DII
{"rvfi-dii", required_argument, 0, 'r'},
{"rvfi-dii", required_argument, 0, 'r' },
#endif
{"help", no_argument, 0, 'h'},
{"trace", optional_argument, 0, 'v'},
{"no-trace", optional_argument, 0, 'V'},
{"inst-limit", required_argument, 0, 'l'},
{"enable-zfinx", no_argument, 0, 'x'},
{"help", no_argument, 0, 'h' },
{"trace", optional_argument, 0, 'v' },
{"no-trace", optional_argument, 0, 'V' },
{"trace-output", required_argument, 0, OPT_TRACE_OUTPUT},
{"inst-limit", required_argument, 0, 'l' },
{"enable-zfinx", no_argument, 0, 'x' },
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c'},
{"sailcov-file", required_argument, 0, 'c' },
#endif
{0, 0, 0, 0 }
{0, 0, 0, 0 }
};

static void print_usage(const char *argv0, int ec)
Expand All @@ -151,7 +157,10 @@ static void print_usage(const char *argv0, int ec)
#endif
struct option *opt = options;
while (opt->name) {
fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name);
if (isprint(opt->val))
fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name);
else
fprintf(stdout, "\t \t --%s\n", opt->name);
opt++;
}
exit(ec);
Expand Down Expand Up @@ -352,6 +361,10 @@ char *process_args(int argc, char **argv)
sailcov_file = strdup(optarg);
break;
#endif
case OPT_TRACE_OUTPUT:
trace_log_path = optarg;
fprintf(stderr, "using %s for trace output.\n", trace_log_path);
break;
case '?':
print_usage(argv[0], 1);
break;
Expand Down Expand Up @@ -626,6 +639,9 @@ void close_logs(void)
exit(EXIT_FAILURE);
}
#endif
if (trace_log != stdout) {
fclose(trace_log);
}
}

void finish(int ec)
Expand Down Expand Up @@ -724,10 +740,8 @@ int compare_states(struct tv_spike_t *s)
void flush_logs(void)
{
if (config_print_instr) {
fprintf(stderr, "\n");
fflush(stderr);
fprintf(stdout, "\n");
fflush(stdout);
fflush(trace_log);
}
}

Expand Down Expand Up @@ -1010,6 +1024,14 @@ void init_logs()
exit(1);
}

if (trace_log_path == NULL) {
trace_log = stdout;
} else if ((trace_log = fopen(trace_log_path, "w+")) < 0) {
fprintf(stderr, "Cannot create trace log '%s': %s\n", trace_log,
strerror(errno));
exit(1);
}

#ifdef SAILCOV
if (sailcov_file != NULL) {
sail_set_coverage_file(sailcov_file);
Expand Down
27 changes: 12 additions & 15 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -156,22 +156,19 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
unsetting C. If it returns true the write will have no effect. */
val ext_veto_disable_C : unit -> bool effect {rreg}

/* We currently only support dynamic changes for the C extension. */
function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
if sys_enable_writable_misa ()
then { /* Handle modifications to C. */
let v = Mk_Misa(v);
/* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */
let m =
if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | not(sys_enable_rvc())
then m
else update_C(m, v.C());
/* Handle updates for F/D. */
if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
then m
else update_D(update_F(m, v.F()), v.D())
}
else m
let v = Mk_Misa(v);
/* Suppress updates to MISA if MISA is not writable or if by disabling C next PC would become misaligned or an extension vetoes */
if not(sys_enable_writable_misa()) | (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C()))
then m
else {
/* Suppress enabling C if C was disabled at boot (i.e. not supported) */
let m = if not(sys_enable_rvc()) then m else update_C(m, v.C());
/* Handle updates for F/D. */
if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
then m
else update_D(update_F(m, v.F()), v.D())
}
}

/* helpers to check support for various extensions. */
Expand Down

0 comments on commit 83a0e51

Please sign in to comment.