Two major commits for two topics:

1)  Initial checkin of cookbook with numerous code examples.
2)  Integration of libfyaml and a regex library for use in
    reading RISCV-Config YAML configuration files (for
    configuration of the Golden Model).

Makefile

@@ -119,8 +119,8 @@ export LEM_DIR
 
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h)
-C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c)
+C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h rv_cfg_func.h)
+C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c rv_cfg_func.c)
 
 SOFTFLOAT_DIR    = c_emulator/SoftFloat-3e
 SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include
@@ -134,9 +134,13 @@ GMP_FLAGS = $(shell pkg-config --cflags gmp)
 GMP_LIBS = $(shell pkg-config --libs gmp || echo -lgmp)
 ZLIB_FLAGS = $(shell pkg-config --cflags zlib)
 ZLIB_LIBS = $(shell pkg-config --libs zlib)
+FYAML_FLAGS = $(shell pkg-config --cflags libfyaml)
+FYAML_LIBS = $(shell pkg-config --libs libfyaml)
+PCRE2_FLAGS = $(shell pkg-config --cflags)
+PCRE2_LIBS = $(shell pkg-config --libs libpcre2-8)
 
-C_FLAGS = -I $(SAIL_LIB_DIR) -I c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS) -fcommon
-C_LIBS  = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS)
+C_FLAGS = -I $(SAIL_LIB_DIR) -I c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS) $(FYAML_FLAGS) $(PCRE2_FLAGS)-fcommon
+C_LIBS  = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS) $(FYAML_LIBS) $(PCRE2_LIBS)
 
 # The C simulator can be built to be linked against Spike for tandem-verification.
 # This needs the C bindings to Spike from https://github.com/SRI-CSL/l3riscv
@@ -237,7 +241,7 @@ ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
 
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c
-	$(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
+	$(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_include rv_cfg_func.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
 
 generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c2
@@ -275,7 +279,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
 
 generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c
-	$(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
+	$(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_include rv_cfg_func.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
 	sed -i -e '/^[[:space:]]*$$/d' $@
 
 c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
@@ -365,7 +369,7 @@ ifndef EXPLICIT_COQ_SAIL
   EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
 endif
 
-COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R generated_definitions/coq '' -R handwritten_support ''
+COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common
 ifeq ($(EXPLICIT_COQ_BBV),yes)
   COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
 endif

README.md

@@ -270,6 +270,9 @@ sail-riscv
 - test                    // test files
   - riscv-tests           // snapshot of tests from the riscv/riscv-tests github repo
 - os-boot                 // information and sample files for booting OS images
+- cookbook                // RISC-V cookbook examples and documentation
+  - doc                   // the asciidoc documentation
+  - functional_code_examples // code examples 
 ```
 
 Getting started
@@ -345,9 +348,33 @@ Some useful options are: configuring whether misaligned accesses trap
 whether page-table walks update PTE bits (`--enable-dirty-update` for C
 and `-enable-dirty-update` for OCaml).
 
-### Experimental integration with riscv-config
+### Integration with RISCV-Config
+
+RISCV-Config ( https://github.com/riscv-software-src/riscv-config ) is the
+configuration standard used by the RISC-V Architectural Compatability Tests
+to specify how a RISC-V core is configured.  The RISC-V architecture allows
+for many implementation specific configurations such as:
+
+- Supported (implemented) ISA extensions
+- Misaligned address support (ie - HW support or trap)
+- Configuration of WARL fields in CSRs
+- Memory map
+
+RISCV-Config utilizes YAML and YAML schemas to describe the configuration.
+There are two YAML files that get examined:  1) an ISA YAML file that 
+describes the configuration of a RISC-V core (ie - supported ISA extensions,
+CSR configurations, etc), and 2) a platform YAML file that describes
+the platform configurations (ie - reset address, CLIC support, etc).
+
+Configuration is done at run-time not at compile time.  (Note:  there
+was an earlier PR (PR #43) that integrated RISCV-Config as a compile-time 
+capability. See: [integration with riscv-config](https://github.com/rems-project/sail-riscv/pull/43)
+It was determined that a run-time solution was needed rather than a compile-time solution.)
+Command line switches specify the YAML files that are to be used.
+
+When adding new extensions to the model,  corresponding configuration parameters
+need to be added to RISCV-Config.
 
-There is also (as yet unmerged) support for [integration with riscv-config](https://github.com/rems-project/sail-riscv/pull/43) to allow configuring the compiled model according to a riscv-config yaml specification.
 
 ### Booting OS images
 
@@ -383,6 +410,7 @@ Authors
  Nathaniel Wesley Filardo, Microsoft;
  Peter Rugg, University of Cambridge;
  Scott Johnson, Aril Computer Corp.
+ William C. McSpadden, RISC-V, International;
 
 Funding
 -------

c_emulator/riscv_platform_impl.c

@@ -3,6 +3,10 @@
 #include <stdio.h>
 
 /* Settings of the platform implementation, with common defaults. */
+char     *RV64ISA                   = "";
+char     *RV32ISA                   = "";
+char     *RV128ISA                  = "";
+
 bool rv_enable_pmp                  = false;
 bool rv_enable_zfinx                = false;
 bool rv_enable_rvc                  = true;
@@ -14,6 +18,8 @@ bool rv_enable_dirty_update         = false;
 bool rv_enable_misaligned           = false;
 bool rv_mtval_has_illegal_inst_bits = false;
 
+uint64_t rv_reset_address = UINT64_C(0x0);
+
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);
 

c_emulator/riscv_platform_impl.h

@@ -5,7 +5,12 @@
 
 /* Settings of the platform implementation. */
 
-#define DEFAULT_RSTVEC     0x00001000
+// #define DEFAULT_RSTVEC     0x00001000
+#define DEFAULT_RSTVEC     rv_cfg_c_int("/reset/address")
+
+extern char     *RV64ISA;
+extern char     *RV32ISA;
+extern char     *RV128ISA;
 
 extern bool rv_enable_pmp;
 extern bool rv_enable_zfinx;
@@ -17,6 +22,8 @@ extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 extern bool rv_mtval_has_illegal_inst_bits;
 
+extern uint64_t rv_reset_address;
+
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;