{"id":"11b533c2-3b08-48a4-a423-3a05a3940b0d","arxiv_id":"1908.01324","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"CREST translates full ANSI-C reference models into Verilog, enabling RTL equivalence checking against high-level C specifications.","lead":"This paper describes CREST, a tool that converts arbitrary ANSI-C specifications into Verilog for use in hardware formal verification. It works by adapting the CBMC model checker to generate low-level Verilog that can be compared against RTL designs with commercial equivalence checking tools.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 'arbitrary ANSI-C' claim is unsupported: CREST inherits CBMC's bounded unwinding, recursive code in Section III-C had to be hand-unrolled, and no loop-handling protocol is given.","rationale":"The paper has genuine strengths: it is a focused tool paper reporting five case studies, including timing data for SoftFloat/VGM equivalence and a sequential adder, and it builds on CBMC, a mature and widely used C model checker. These case studies provide some evidence that for straight-line or fully unrolled reference models, the SSA-to-Verilog translation can work end to end. The reader's weakest-assumption analysis correctly identifies that the translation from CBMC's SSA representation to Verilog is not formally verified. I agree that this is a real risk. However, the most load-bearing point for the paper's headline claim is broader: the claim to support 'arbitrary ANSI-C' is not supported even before the translation step, because CBMC's symbolic execution is bounded and the only recursive example in the paper required manual hand-unrolling. That is an explicit, in-scope limitation stated in Section III-C. The absence of any loop-unwinding protocol or artifact means the strongest claim is unverified. Since the case studies do show practical usage and the tool is described as a prototype, the appropriate verdict remains CONDITIONAL rather than ACCEPT; nothing in this stress test requires changing the reader's verdict.","tokens_in":6272,"tokens_out":6851,"duration_ms":70348,"concrete_test":"Run CREST directly on the original recursive Intel RECIP14 C code from Section III-C, without the hand unrolling. If the tool rejects it, emits only a fixed recursion-depth unrolling, or generates a Verilog module that is not equivalent to the C function on every input, the 'full ANSI-C / no synthesizable-subset restriction' claim is falsified for recursion. As a complementary check for loops, build a deterministic C reference function whose loop trip count depends on input data (for example a Euclidean GCD loop), run CREST on it, and exhaustively compare the generated Verilog against the C function for small word sizes. If CREST emits an unwinding assertion or any mismatch appears, the paper must be revised to claim only 'C programs whose loops and recursion can be automatically fully unwound.'","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that CREST accepts arbitrary ANSI-C and generates Verilog capturing its bit-level semantics. Section II says CREST taps CBMC 'just after symbolic execution' and translates the SSA assignments into Verilog. But CBMC's symbolic execution is bounded: loops are unwound to a finite depth and recursion is not handled automatically. The paper gives no unwinding bound, no completeness criterion, and no mechanism for proving that the unwound prefix covers all possible behaviors of the C reference model. This is not a hypothetical edge case: Section III-C states that the Intel approximate-reciprocal model 'was written recursively' and that 'We chose to unroll the recursion by hand.' That is a manual, specification-dependent transformation, so the tool did not process that ANSI-C specification as written. For any C model with a loop whose trip count depends on input values, the generated combinational Verilog can represent only a finite prefix of symbolic execution unless the unwinding is proved sufficient. The paper provides no such proof and no artifact, so the strongest claim of full ANSI-C coverage is not established. The reader's concern about the unverified SSA-to-Verilog translator is legitimate, but it is secondary: even a bug-free translator would still face the up-front loss of generality from bounded symbolic execution.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents CREST, a prototype front-end that translates ANSI-C reference specifications into Verilog for use as reference models in RTL formal verification. The translation taps into the CBMC bounded model checker after symbolic execution, converting the resulting SSA form into combinational Verilog. The authors claim that CREST handles arbitrary ANSI-C without restricting to a synthesizable subset, and they report five case studies: SoftFloat versus VGM floating-point addition (with concrete runtimes), floating-point multiplication with manual proof decomposition, an Intel approximate-reciprocal model, WebM VP9 matrix transforms with dynamic function pointers, and a sequential floating-point adder. The paper positions CREST as a generic front-end for commercial EDA verification flows and describes possible future extensions.","tokens_in":6528,"tokens_out":2989,"duration_ms":33193,"significance":"If the central claim holds, CREST would offer a general path from natural, unconstrained C models to RTL formal verification, leveraging CBMC's mature bit-level semantics of C. The paper's strength is that the evaluation is anchored to external benchmarks and references: SoftFloat is checked against the VGM library, the reciprocal model against a proprietary reference and a shipping RTL design, and the VP9 assertions against a commercial tool. The concrete runtimes for floating-point addition and the explicit case split for multiplication are informative. However, the paper does not provide an artifact or a formal correctness argument for the SSA-to-Verilog translation, and the case studies contain manual interventions that substantially weaken the claim of handling arbitrary ANSI-C as written. The significance of the work is therefore conditional on a more carefully scoped statement of what CREST actually accepts and a clear account of its soundness.","major_comments":[{"comment":"The central claim that CREST processes 'arbitrary ANSI-C' is not supported by the described architecture. CBMC's symbolic execution is bounded: loops are unwound to a finite depth, and the paper gives no unwinding bound, no completeness criterion, and no protocol for loops with input-dependent trip counts. The generated combinational Verilog therefore represents only a finite prefix of the C program's symbolic execution, unless additional proof is supplied. The paper should either qualify the 'arbitrary ANSI-C' claim to 'ANSI-C for which a sufficient loop unwinding can be established' or describe a mechanism for discharging the completeness obligation.","section":"Section II (Architecture and Implementation)"},{"comment":"This case study directly contradicts the unrestricted-language claim. The Intel reciprocal model was written recursively, and the authors state, 'We chose to unroll the recursion by hand, and used CBMC as a model checker to prove the assertions that justify the correctness of the unrolling transformation.' This is a manual, specification-dependent transformation performed before CREST processes the code; CREST did not translate the original ANSI-C as written. The paper must either present an automated handling of such recursion or explicitly exclude recursive code from the supported subset.","section":"Section III-C (Approximate Reciprocal)"},{"comment":"The correctness of the SSA-to-Verilog translation is assumed rather than established. The paper states that CREST 'translates each variable in this representation to a Verilog bitvector and each C expression on the right-hand side of the assignments to a corresponding Verilog expression,' but it gives no formal semantics preservation argument and no differential validation of the translation against CBMC's own bit-level semantics. Because CREST-generated Verilog is used as the reference model in equivalence proofs, a translation bug would invalidate all downstream verification results. The paper should at least report the results of running generated Verilog and C on the same test vectors, ideally with randomized or exhaustive bit-pattern tests for each supported construct.","section":"Section II (Translation to Verilog)"}],"minor_comments":[{"comment":"There are numerous typographical errors and spacing artifacts, such as 'verifcat ion', 'V erification', and 'specifica tions', which should be corrected with careful proofreading.","section":"Throughout"},{"comment":"The bit-vector correspondence equations contain 'quotesingle' artifacts in the PDF text (e.g., 'SoftFloat.mul_in_1[63:31] = 33/quotesingle.Varb0'), which makes them unreadable. These should be typeset as proper Verilog or mathematical notation.","section":"Section III-B"},{"comment":"The runtimes for floating-point addition are presented as an inline table without a caption or formatting. A proper numbered table with units and a column for precision width would improve clarity.","section":"Section III-A"},{"comment":"The sentence 'The code also contains several user-written assertions, which are are translated into SV A assertions by our tool' contains a duplicated 'are' and should read 'which are translated into SVA assertions'.","section":"Section III-D"}],"recommendation":"major_revision","confidential_remarks":"The paper reads as a preliminary tool report with an overbroad central claim. The reviewer's main concern is not the idea but the mismatch between the stated 'arbitrary ANSI-C' coverage and the actual manual steps and bounded-execution limitations revealed in the case studies. A careful revision that scopes the claim, documents the unwinding and unrolling obligations, and reports validation of the translator would substantially strengthen the paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague, here's my read.\n\nThe genuinely new thing here is CREST's pipeline: tap CBMC after symbolic execution, turn its SSA assignments into Verilog bitvectors, and feed that to an RTL equivalence checker. That is a sensible engineering move, and it lets hardware teams keep natural C reference models--including type punning and function pointers--without rewriting them in a synthesizable subset. The five case studies are the right kind of evidence: SoftFloat against VGM, Intel's RECIP14 model against a shipping design, VP9 asserts, a sequential FP adder. They use external benchmarks, report runtimes, and the multiplication study is honest about needing manual decomposition. That is real credit.\n\nThe soft spot is the abstract's 'arbitrary ANSI-C.' CREST inherits CBMC's bounds: loops are unwound to a finite depth, and recursion is not automatic. Section III-C admits the RECIP14 model was hand-unrolled. So the tool does not process arbitrary ANSI-C as written; it processes the finite unwinding of a given program. The paper never states the unwinding bound or a completeness argument. For datapath specs with compile-time-bounded loops that may be fine, but the claim as printed is stronger than the demonstration.\n\nSecondary, but real: the SSA-to-Verilog translator itself is hand-coded and not verified. A bug there would break every downstream equivalence claim. The paper does not release an artifact, so I can't check it. That limits confidence, but this is a tool paper; I would not demand a proof of the translator, just a clear statement of its tested coverage.\n\nThe stress-test note is right that the bounded-execution issue is primary; the translator concern is secondary but still fair.\n\nWho gets value: anyone working on C-based hardware reference models or high-level synthesis validation. It deserves peer review, not desk reject. A good referee should ask for a clear statement of the actual subset handled and, ideally, an artifact or more case studies.\n\nRecommendation: send to review, but expect a revision that calibrates the 'arbitrary ANSI-C' claim and documents the loop-unwinding protocol.","headline":"A genuinely useful C-to-Verilog pipeline with an overstated 'arbitrary ANSI-C' claim; worth reviewing with a request to document CBMC's unwinding bounds.","tokens_in":7030,"tokens_out":2370,"would_cite":true,"duration_ms":24847,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"CREST establishes a general path from full ANSI-C reference specifications to bit-level Verilog for RTL formal verification.","keywords":["formal hardware verification","C-to-Verilog translation","ANSI-C reference specifications","equivalence checking","bounded model checking","symbolic execution","floating-point verification","RTL verification"],"falsifier":"Compile the generated Verilog and the original C function to two oracles and run them on the same exhaustive input set for a small datapath, such as all 16-bit floating-point operand pairs including subnormals, NaNs, and infinities, plus targeted programs using pointer casts, unions, and function pointers; any discrepancy between the Verilog simulation and the C execution would refute the claim that the translation captures ANSI-C semantics.","tokens_in":6106,"feed_emoji":"⚙️","tokens_out":6873,"duration_ms":69496,"temperature":0.7,"pith_summary":"This paper tries to establish that high-level ANSI-C datapath models, written in unrestricted, natural C with pointers, casts, unions, recursion, and function pointers, can serve as reference specifications for formal RTL verification. To do this, CREST takes the symbolic-execution output of a mature bounded model checker for C and lowers each assignment to a Verilog bitvector expression, producing simple Verilog that a commercial equivalence-checking tool can read. The point is to make \"verify this RTL against my C model\" practical without forcing the C into a synthesizable subset or a hardware-oriented dialect. The paper demonstrates the claim on floating-point addition and multiplication, an approximate-reciprocal instruction model, a video-codec transform, and a sequential floating-point adder.","feed_headline":"Full ANSI-C specs become Verilog for RTL verification","feed_subtitle":"No synthesizable subset: natural datapath C models can serve as formal reference specs in EDA tools.","key_machinery":"The load-bearing mechanism is the single-static-assignment (SSA) assignment stream produced after symbolic execution: after loop unwinding and interpretation of pointers, casts, and conversions, the C program is reduced to a flat set of assignments over bitvector variables, with every expression still annotated back to its source line. CREST translates that stream directly: each SSA variable becomes a Verilog bitvector, each C operator becomes the equivalent Verilog operator, and unsupported expression forms, such as bit-range extraction from an arbitrary expression, are lowered through auxiliary variables. This is what lets the tool inherit full ANSI-C coverage without building a new C front end.","core_discovery":"The central claim is that the bit-level semantics of full ANSI-C can be captured in a low-level Verilog model by tapping into a bounded model checker after symbolic execution, when all high-level C constructs have already been interpreted away and the program is a set of single-static-assignment assignments over bitvectors. CREST maps each such variable to a Verilog bitvector and each right-hand-side expression to the corresponding Verilog expression, adding auxiliary signals where Verilog forbids operations such as extracting a bit range from an expression. The resulting Verilog is not a synthesized circuit but a proof-oriented representation that reproduces the exact bit-level behavior of the C code, including arithmetic conversions, pointer dereferencing, and type punning. The paper further claims that the generated model can be used by off-the-shelf RTL formal-verification tools to prove equivalence against other reference models or implementations.","pith_inferences":["Inference: If the translator is trusted, the same C-to-Verilog path could also turn arbitrary C testbenches or reference models into simulation oracles for coverage-driven and dynamic validation flows, not just formal equivalence checks.","Inference: The architecture suggests a general recipe: reuse a mature software model checker's middle end as a C-to-logic front end, so improvements in software verification automatically strengthen hardware verification coverage.","Inference: A testable extension is differential testing of the generated Verilog against the original C compiled with a reference compiler across a corpus of tricky ANSI-C constructs, which would empirically certify the hand-written translation mapping."],"forward_implications":["Equivalence checking against a C reference model can be run inside commercial EDA tools for floating-point operations, with 16-, 32-, and 64-bit addition passing automatically.","For designs where two models compute in structurally different ways, the C-to-Verilog spec does not remove the need for case splits and intermediate invariants; multiplication required a three-case decomposition.","User-written assertions in C are translated to SVA assertions, so the same properties can be checked both in the C model and in the generated Verilog.","Sequential RTL can be verified against a combinational C specification: the clocked floating-point adder was shown to be standard compliant exactly when the CREST spec is standard compliant.","The generated Verilog can serve as an independent reference for checking circuits produced by high-level synthesis from the same C source."],"supporting_citations":[{"why":"Supplies the bit-level ANSI-C semantics and symbolic-execution engine that CREST adapts.","marker":"[3]"},{"why":"Defines the target scenario of equivalence checking a floating-point unit against a high-level C model.","marker":"[2]"},{"why":"Provides the ANSI-C reference implementation used for the addition and multiplication case studies.","marker":"[5]"},{"why":"Supplies a natural C model that uses pointer arguments and type punning, showing coverage beyond synthesizable subsets.","marker":"[8]"},{"why":"Provides a C implementation whose function pointers and user-written assertions exercise translation features.","marker":"[9]"},{"why":"Supplies the sequential RTL design verified against the combinational C specification.","marker":"[10]"}],"fun_headline_variants":["Full C semantics as Verilog for RTL formal checks","ANSI-C to Verilog: no subset, full proof power","Verified RTL from arbitrary ANSI-C reference specs","C models become Verilog for exhaustive RTL verification","Bounded model checking turns C into formal Verilog specs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The hand-written mapping from the intermediate assignment representation to Verilog is assumed to preserve the meaning of every ANSI-C construct, and this mapping is not itself verified by an independent checker.","fun_headline_variants_meta":{"raw":{"variants":["Full C semantics as Verilog for RTL formal checks","ANSI-C to Verilog: no subset, full proof power","Verified RTL from arbitrary ANSI-C reference specs","C models become Verilog for exhaustive RTL verification","Bounded model checking turns C into formal Verilog specs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000127,"raw_usage":{"total_tokens":1040,"prompt_tokens":795,"completion_tokens":245,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":411,"completion_tokens_details":{"reasoning_tokens":164}},"tokens_in":411,"tokens_out":245,"duration_ms":3409,"temperature":1.0,"reasoning_tokens":164,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T15:15:42.836926+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile the generated Verilog and the original C function to two oracles and run them on the same exhaustive input set for a small datapath, such as all 16-bit floating-point operand pairs including subnormals, NaNs, and infinities, plus targeted programs using pointer casts, unions, and function pointers; any discrepancy between the Verilog simulation and the C execution would refute the claim that the translation captures ANSI-C semantics.","supporting_citations":[{"cited_title":"Mukherjee, S","cited_arxiv_id":null,"evidence_quote":"Supplies the bit-level ANSI-C semantics and symbolic-execution engine that CREST adapts."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the target scenario of equivalence checking a floating-point unit against a high-level C model."},{"cited_title":"O'Leary, R","cited_arxiv_id":null,"evidence_quote":"Supplies a natural C model that uses pointer arguments and type punning, showing coverage beyond synthesizable subsets."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides a C implementation whose function pointers and user-written assertions exercise translation features."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the sequential RTL design verified against the combinational C specification."}],"review_version":1}