Repository navigation
Add 'simbench' to run against Verilator - #8
Merged
Merged
Conversation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…I clock) One bench per compile: bench.sv defines class sb_bench_impl extends simbench_pkg::sb_bench. run() reads +sb_n/+sb_warmup/+sb_seed/+sb_dump/ +sb_timeout_ns and prints a SIMBENCH_RESULT json line. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…_burst Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ESULT parser Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
runner.py builds per (tool, bench) with a session cache and runs with the config's solver env and sampler plusargs. Harness: seed via a process variable (Verilator 5.040 rejects process::self().srandom()). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…erf/schema.py Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…, vlt-dvs-default / vlt540-z3 (secondary) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e 5.053 devel; record simulator_path Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
probe_sampler() runs the image once (+sb_n=1) with +verilator+solver+file+ and reads the '; sampler: <name>' line the dev runtime writes there. test_bench fails if it differs from cfg.sampler; records carry tools.sampler_active. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ion through dv-solve without Verilator Config field 'replay' names bench_vlt_replay; the Verilator run captures the session via +verilator+solver+file+, and the api-cache pass gives us/check-sat and the new-context (first call) time. Known: bench_vlt_replay segfaults in pass_text on sessions using (push) (dist.weighted); the test fails with the replay error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…call by check-sats per call api-cache (reused compiled context) is 12x slower than api on construct.range (1012 vs 84 us/check-sat), so time both and report the fastest. dist.weighted makes 2 check-sats per call (push); per-call time is now us/check-sat x (n_check-1)/(n+warmup). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ruct/logic/parity/unique) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
unsigned_ops uses 16'(a ^ b): Verilator mis-solves c == a[15:0] ^ b[15:0] on int unsigned (seen with z3 solver). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
implication, if/else, soft, solve-before, constraint_mode, rand_mode, inline with, inheritance. 12/12 pass on vlt-z3-default. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
foreach, sum/sum-with, ordering, unique (fixed/dyn), dynamic/queue/assoc, index, 2-D, reductions, object-handle arrays. 16/16 pass on vlt-z3-default. cls_arr_member repeats the member bound in the parent: Verilator ignores the member object's own constraint block here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
6 ported from dv-solve zuspec models (soc_mem_map, soc_addr_map_32/40, addr_map_64, memmap_tight_32, mem_partition_knapsack) plus nonoverlap_regions_8 and page_table_entry (Sv39 PTE). Knapsack offsets are named off<i>: Verilator's solver assumption literals a<N> clash with user variables named a<N>. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…are_3, graph_color_8, knapsack_small, unique_64, global_nested) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Default mode's auto engine bitblasts distinct-over-array-selects, making B ~3x slower than A on unique-heavy benches; verilator mode is the documented VERILATOR_SOLVER mode (B 0.1-0.4x of A on hard.unique_64, array.unique_32, memmap.nonoverlap_regions_8 in hand runs). Smoke: 30 passed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
B matrix N=200 (100 benches): geomean vs old B 0.92x, vs A 0.13x. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…hi2 vs reference config, opt. first-value diversity) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Replay the captured session text (B's, dv-solve sampler) through one solver process (z3 -smt2 / dv-solve-smt2); best wall time over replay_reps / calls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
+verilator+solver+file+ wraps long commands; continuation lines were dropped, so z3 -smt2 replay hit parse errors on 12 benches. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
build_cmds/image_path/run_cmd per simulator; sb_time.c compiled by each tool. Solver/sampler/replay are rejected for non-Verilator configs; version flag per tool; build_args field. Example configs vcs/xcelium/questa are skipped unless the tool is found. Verilator commands and cache keys unchanged. Commercial command lines are checked by unit tests only (no tools here). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…table Records gain simbench.bench_sha (sha1 of bench.sv), run.dirty, and an optional machine.label from SIMBENCH_HOST. New dv_solve_simbench.report merges JSONL from several machines into a markdown table of benches x config@host, us/call with ratio vs a reference config, and a geomean row. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… sharing, report) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.