Example Files

RTL, testbench code, and compiler disassembly used by the project examples.

Formal request / grant flow

File	Contents
request_grant_fsm.sv	Three-state request/grant RTL
request_grant_properties.sv	Combined SVA safety and liveness property
elb_design.txt	Frontend elaborated-design dump
btor2_high_unopt.txt	Unoptimized BTOR2 HIR
btor2_high_opt.txt	Optimized BTOR2 HIR
btor2_low_unopt.txt	Unoptimized low BTOR2
btor2_low_opt.txt	Optimized low BTOR2
passing/report.json	Proved result
failing/report.json	Injected-fault counterexample result
failing/witness.txt	Decoded counterexample witness
failing/counterexample.vcd	Counterexample waveform data

Adder

File	Contents
adder.sv	Adder RTL
adder_tb.sv	Interactive runtime testbench
program.eir	FPGA execution IR
program.vir	Host runtime IR
program.disasm	Bindings, FPGA ISA, and host VIR

Circular buffer UVM

File	Contents
circular_buffer.sv	Circular-buffer RTL
circular_buffer_uvm_pkg.sv	UVM test package
circular_buffer_uvm_tb.sv	UVM top-level testbench
program.eir	FPGA execution IR
program.vir	Host runtime IR
program.disasm	Bindings, FPGA ISA, and host VIR