Feature/odc analysis by nblei · Pull Request #8 · CrucibleComputingGroup/PdatScorr

nblei · 2025-11-03T16:51:41Z

No description provided.

Implements observability don't care (ODC) analysis to find hardware optimization opportunities by testing which signal bits can be forced to constants without affecting circuit correctness. Features: - Parse DSL constraints to identify candidate ODC bits - Inject errors by forcing bits to constants in RTL - Synthesize error-injected circuits to AIGER - Run bounded SEC using ABC &cec command - Generate JSON and Markdown reports Components: - odc/ module: constraint analyzer, error injector, SEC checker, synthesis integration, and report generator - scripts/odc_analysis.py: Standalone ODC analysis tool - Workflow integration: --odc-analysis flag in synth_ibex_with_constraints.sh - Config: Added barrel shifter signals to configs/ibex.yaml Testing: - 7 new regression tests (all passing) - 2 test fixtures for ODC scenarios - Verified end-to-end: slli2.dsl correctly identifies all 5 shamt bits as ODCs - All 55 regression tests pass Performance: - SEC checks: ~0.05s each using ABC &cec - Per variant: ~3 min synthesis + 0.05s SEC - Future optimization: Yosys-level injection could achieve 4x speedup Fixes: - Updated synthesis script to use basename for AIGER output paths - Fixed Synlig execution to run from output directory (prevents race conditions) - Added .claude/ and CLAUDE.md to gitignore

The merge-base changed after approval.

Allows running ODC analysis on multiple DSL files in parallel. Example: ./batch_synth.sh --odc-analysis -j 8 rules/*.dsl

Implements automatic application of ODC optimizations: - Pass 1: Run ODC analysis to identify don't care bits - Pass 2: Apply constant tie-offs and re-synthesize - Compare baseline vs optimized area New scripts: - scripts/apply_odc_optimizations.py: Generates RTL with ODC tie-offs - scripts/synth_with_odc_optimization.sh: Two-pass workflow automation - batch_synth.sh: Added --odc-analysis support Features: - Selective bit override: ODC bits tied to constants, non-ODC bits use computed values - Renames shift_amt → shift_amt_original to avoid multiple drivers - Full ABC optimization (scorr + constraint removal + rewrite + fraig + balance) Verified results on slli2.dsl (shift_amt always 1): - Baseline: 11285 AND gates - Optimized: 10723 AND gates - Reduction: 562 gates (4.98%) Usage: ./scripts/synth_with_odc_optimization.sh --config configs/ibex.yaml examples/shifts/slli2.dsl ./batch_synth.sh --odc-analysis -j 8 examples/shifts/*.dsl

When --odc-analysis flag is used and ODCs are found: 1. Automatically generates optimized RTL with constant tie-offs 2. Re-synthesizes with optimized RTL 3. Runs full ABC optimization (scorr + rewrite + fraig + balance) 4. Shows baseline vs optimized comparison Fixes: - Added print_stats to ODC ABC optimization for proper logging - Updated batch_synth.sh to prefer ODC-optimized results in comparison table - Fixed apply_odc_optimizations.py to avoid multiple drivers by renaming shift_amt → shift_amt_original Verified results on slli2.dsl: - Baseline: 11360 AND gates - ODC-optimized: 10723 AND gates - Reduction: 5.61% (637 gates) Batch comparison now correctly shows ODC-optimized gate counts.

When --gates and --odc-analysis are used together: - Runs gate-level synthesis on ODC-optimized circuit - Shows chip area comparison (baseline vs optimized) - Batch script correctly extracts ODC-optimized chip area Fixes: - Use correct field extraction for chip area ( instead of ) - Look for 'Chip area for module' pattern in gates.log - Prefer ODC-optimized gates.log over baseline in batch comparison Verified on slli2.dsl with --gates --odc-analysis: - Baseline: 11360 gates, 41242 µm² - Optimized: 10723 gates, 39250 µm² - Reduction: 5.61% gates, 4.83% area

Copilot

Pull Request Overview

This PR implements ODC (Observability Don't Care) analysis functionality to identify optimization opportunities through error injection and bounded sequential equivalence checking. The feature allows the synthesis workflow to automatically detect bits that can be tied to constants without affecting circuit correctness under given constraints.

Key changes:

New odc/ module with constraint analysis, error injection, SEC checking, and report generation
Integration with existing synthesis workflow via --odc-analysis flag
Two-pass optimization workflow script for applying ODC optimizations
Comprehensive test coverage for ODC analysis components

Reviewed Changes

Copilot reviewed 25 out of 26 changed files in this pull request and generated 29 comments.

Show a summary per file

File	Description
`odc/constraint_analyzer.py`	Analyzes DSL constraints to identify constant bit candidates
`odc/error_injector.py`	Generates RTL with forced constant values for testing
`odc/sec_checker.py`	Performs bounded SEC using ABC to verify equivalence
`odc/report_generator.py`	Creates JSON and markdown reports of ODC analysis results
`odc/synthesis.py`	Synthesizes error-injected circuits to AIGER format
`scripts/odc_analysis.py`	Main ODC analysis workflow orchestrator
`scripts/synth_with_odc_optimization.sh`	Two-pass synthesis with ODC optimization
`scripts/apply_odc_optimizations.py`	Applies ODC tie-offs to RTL based on analysis
`synth_core.sh`	Added `--odc-analysis` flag support
`tests/regression/test_odc_analysis.py`	Comprehensive regression tests for ODC functionality
`configs/ibex.yaml`	Added ODC error injection configuration
`tests/regression/fixtures/odc_*.dsl`	Test fixtures for ODC analysis
`.gitignore`	Added `.claude/` and `CLAUDE.md` to gitignore
`CLAUDE.md`	Deleted file
`.claude/*.md`	Deleted Claude-specific documentation files

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-11-05T03:14:26Z

+
+# Pass 1: Baseline synthesis + ODC analysis
+echo "[Pass 1/2] Baseline synthesis + ODC analysis..."
+./synth_ibex_with_constraints.sh --odc-analysis "$@"


Passing all arguments with \"$@\" will include the DSL file multiple times (once from $last at line 24, and again in $@). This will cause the script to receive duplicate DSL arguments. Use array slicing to exclude the last argument: ./synth_ibex_with_constraints.sh --odc-analysis \"${@:1:$#-1}\" \"$DSL_FILE\"

Suggested change

./synth_ibex_with_constraints.sh --odc-analysis "$@"

./synth_ibex_with_constraints.sh --odc-analysis "${@:1:$#-1}" "$DSL_FILE"

Copilot · 2025-11-05T03:14:27Z

+    for i in range(injection_line - 1, max(0, injection_line - 20), -1):
+        if lines[i].strip() == 'end':
+            for j in range(i - 1, max(0, i - 15), -1):


The hardcoded search range of 20 lines backwards is fragile and may fail if the always_comb block is further away. Consider using a more robust search that continues until finding the block or reaching the beginning of the file, or document the assumption about code structure.

Suggested change

for i in range(injection_line - 1, max(0, injection_line - 20), -1):

if lines[i].strip() == 'end':

for j in range(i - 1, max(0, i - 15), -1):

for i in range(injection_line - 1, -1, -1):

if lines[i].strip() == 'end':

for j in range(i - 1, -1, -1):

Copilot · 2025-11-05T03:14:27Z

+        ["synlig", "-s", synth_script.name],
+        capture_output=True,
+        text=True,
+        timeout=600,


[nitpick] The hardcoded 600-second timeout should match the timeout_sec parameter default from SecChecker (line 53 in sec_checker.py). Consider extracting this as a constant or configuration parameter to avoid inconsistencies.

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Implements mux-level ODC detection that proves entire functional units are unreachable when all instructions using them are forbidden by DSL constraints. Key improvements: - BMC with k-induction proves operator_i values unreachable from all reachable states - Removes unreachable mux cases from ALU result multiplexer - Achieved 5.1% gate reduction and 4.3% area reduction on baseline.dsl Technical approach: - Inject monitor output that fires when operator_i matches forbidden operations - Use ABC bmc3 with fold to check if monitor is reachable - UNSAT result proves mux case is unreachable, enabling RTL removal Results for baseline.dsl (no shifts): - Verified 5 unreachable functional units (shifter, minmax, bitcnt, shuffle, xperm) - Removed 17 ALU operations from result mux - Logic: 582 gate reduction (5.12%) - Physical: 1,755 µm² area reduction (4.25%) Files added: - odc/alu_mapping.py: Instruction → ALU op → result signal mappings - odc/mux_reachability_analyzer.py: BMC-based reachability proof engine - scripts/apply_mux_optimizations.py: RTL mux case removal tool Files modified: - odc/sec_checker.py: Changed from &cec to dsec (then to BMC approach) - scripts/odc_analysis.py: Added --analysis-level flag for bit/mux/both - synth_core.sh: Integrated mux optimization workflow - configs/ibex.yaml: Added result_muxes configuration

…oup/PdatScorr into feature/odc-analysis

Synthesize baseline to gates before ODC analysis when both --odc-analysis and --gates flags are used. This ensures the baseline chip area is available for comparison when displaying ODC optimization results. Also improved Step 6 check to look for the actual gate synthesis log file that gets created (ibex_alu_optimized_gates.log) instead of non-existent synthesis.log. Now the chip area comparison is displayed correctly: - Baseline: 41,313 µm² - Optimized: 39,553 µm² - Reduction: 1,760 µm² (4.26%)

@wrapper

…s utilities The register file was not being synthesized because ibex_core doesn't instantiate it - the register file lives in ibex_top. Created a minimal wrapper module (ibex_core_with_rf) that properly connects the core with the register file, avoiding the PRIM infrastructure complexity. Changes: - Add ibex_core_with_rf.sv wrapper connecting core and register file - Refactor @wrapper@ path resolution into shared synthesis_utils.py module - Update configs/ibex.yaml to use wrapper as top module with updated hierarchy paths - Make --core ibex the default (auto-loads configs/ibex.yaml) - Fix batch_synth.sh to prefer newer results over stale ODC optimizations - Add Result_Type column to comparison CSV for clarity - Fix synth_core.sh to exit with error when ODC optimization fails - Support --output as alias for --output-dir in batch synthesis Verified working: 04regs baseline (1,611 latches) → ODC-optimized (1,036 latches), achieving 896 flop reduction (28 registers × 32 bits).

Make the ODC analysis system core-agnostic by removing hardcoded Ibex-specific paths and signal names. Add support for the RiscvSingleCycle core. Changes: - Update ErrorInjector to use config injection points instead of hardcoded ibex_id_stage.sv - Pass --config to pdat-dsl codegen for signal name mappings - Read ABC depth from config (default_depth: 1 for single-cycle vs 2 for pipelined) - Fix SEC checker to handle constraint outputs properly (constr -r before dsec) - Fix mux analyzer to skip RegisterRangeExpression (register constraints, not instructions) - Add riscvsinglecycle.yaml config for synthesis orchestration - Add experiment DSL files for register count analysis (04/08/16/32 regs) Verified: Single-cycle baseline synthesis works (511 latches with config mode). Note: SEC log capture needs debugging - manual SEC verification shows equivalence checks work.

Fixed critical bug where ABC output was truncated when using multi-line scripts with comments. This caused all SEC checks to report "error" even though they were actually passing. Root cause: ABC's -c flag with multi-line scripts truncates output after the command echo. Solution: Use single-line command string without embedded comments. Additional fixes: - Use absolute paths in SEC scripts to avoid cwd issues - Merge stderr into stdout (stderr=STDOUT) to ensure all output captured - Pass DSL config from PdatRiscvDsl/configs/ for signal name mappings - Read ABC default_depth from config (k=1 for single-cycle, k=2 for pipelined) - Fix RegisterRangeExpression handling in mux analyzer (skip register constraints) - Use config source_files to find register file (supports target/ and rtl/ layouts) Verified: Single-cycle ODC analysis now correctly detects all 9 register field ODCs. Next: Adapt register file transformation for Veryl-generated array style.

The register file optimization now works for single-cycle core, achieving 384 latch reduction (12 registers × 32 bits) when reducing from 16 to 4 registers. Changes: - Update regfile search to check odc_optimized_rtl directory - Add glob pattern for *regfile*_optimized.sv (in addition to *register_file*) - Add register_file_opt injection point to riscvsinglecycle.yaml config - Created manual regfile_optimized.sv for 04regs configuration Verified results for single-cycle 04regs: Baseline: 513 latches (16 regs × 32 bits + 1 PC) Optimized: 129 latches (4 regs × 32 bits + 1 PC) Reduction: 384 latches (74.9%) Both Ibex and RiscvSingleCycle cores now support automatic register file optimization based on DSL register constraints.

Enable automatic register file optimization for Veryl-generated and educational cores that use simple array declarations instead of generate blocks. The transformation now handles two register file styles: 1. Generate-block style (Ibex): for (genvar i...) begin : g_rf_flops 2. Simple array style (Veryl): logic [31:0] regs [0:N-1]; Simple array transformations: - Reduce array size: regs [0:16-1] → regs [0:4-1] - Update for loop bounds: i < 16 → i < 4 - Add bounds checks to read logic: rs1_addr < 4 ? regs[rs1_addr] : 0 - Add bounds checks to write logic: we && rd_addr != 0 && rd_addr < 4 Verified results for RiscvSingleCycle 04regs: Baseline: 513 latches, 10,175 AND gates Optimized: 129 latches, 5,551 AND gates Reduction: 384 latches (74.9%), 4,624 AND gates (45.4%) Both Ibex and RiscvSingleCycle now support fully automatic register file optimization from DSL register constraints!

This commit adds comprehensive static timing analysis using OpenSTA and fixes the dfflibmap issue preventing proper flip-flop mapping to Skywater cells. Key Changes: - Fix dfflibmap by adding -clk_name to read_aiger for proper FF conversion - Add configurable clock and module name parameters from config files - Integrate OpenSTA timing analysis (optional, runs if installed) - Add timing comparison between baseline and ODC-optimized circuits - Update requirements.txt with aigverse and pyyaml dependencies Timing Analysis Features: - Automatic STA after gate synthesis (when OpenSTA available) - Reports WNS, TNS, and maximum achievable frequency - Generates JSON metrics for automated comparison - Module name auto-detection with config override support The integration is optional - synthesis works without OpenSTA installed.

nblei requested a review from Allenjin123 November 3, 2025 16:51

Allenjin123 previously approved these changes Nov 3, 2025

View reviewed changes

Increased regression test timeout

a7917e6

Allenjin123 previously approved these changes Nov 3, 2025

View reviewed changes

nblei added 6 commits November 4, 2025 05:28

Add --odc-analysis support to batch_synth.sh

592502a

Allows running ODC analysis on multiple DSL files in parallel. Example: ./batch_synth.sh --odc-analysis -j 8 rules/*.dsl

Removed claude stuff

0d95b14

merged with main

c237286

Allenjin123 requested a review from Copilot November 5, 2025 03:09

Copilot AI reviewed Nov 5, 2025

View reviewed changes

Allenjin123 and others added 9 commits November 4, 2025 22:27

Update odc/constraint_analyzer.py

e1de1d0

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update odc/constraint_analyzer.py

cd784b5

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update odc/synthesis.py

231a89a

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update odc/sec_checker.py

165d5a1

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update odc/sec_checker.py

f7a3e1f

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Update odc/error_injector.py

2896594

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

added batch_odc_optimization

9cf3980

Merge branch 'feature/odc-analysis' of github.com:CrucibleComputingGr…

a12f6a5

…oup/PdatScorr into feature/odc-analysis

Allenjin123 previously approved these changes Nov 5, 2025

View reviewed changes

nblei dismissed Allenjin123’s stale review via 2d35064 November 5, 2025 22:14

nblei added 5 commits November 8, 2025 11:55

Synthesizing to flops

318b38d

Allenjin123 previously approved these changes Nov 8, 2025

View reviewed changes

Updated requirements for CI pipeline

a185771

nblei dismissed Allenjin123’s stale review via a185771 November 8, 2025 22:41

nblei added 3 commits November 8, 2025 19:17

fixed failing tests (false positives)

a70f37e

Lengthened timeout and increased job size

f793a53

Allenjin123 approved these changes Nov 9, 2025

View reviewed changes

Allenjin123 merged commit d06f9f0 into main Nov 9, 2025
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feature/odc analysis#8

Feature/odc analysis#8
Allenjin123 merged 28 commits into
mainfrom
feature/odc-analysis

nblei commented Nov 3, 2025

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI Nov 5, 2025

Uh oh!

Copilot AI Nov 5, 2025

Uh oh!

Copilot AI Nov 5, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	./synth_ibex_with_constraints.sh --odc-analysis "$@"
	./synth_ibex_with_constraints.sh --odc-analysis "${@:1:$#-1}" "$DSL_FILE"

Conversation

nblei commented Nov 3, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Uh oh!

Copilot AI Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants