Vesmul-parse
A macro to parse a combinational RTL design and create a simulation
test vector
vesmul-parse can take the following arguments:
- :file has to be provided. It should be a string and point to the relative path to the
target Verilog file.
- :topmodule has to be provided. It should be a string and be the name of the top module
of the Verilog file.
- :name is optional. It should be a symbol. It will be the name
of the objects generated for symbolic simulation vectors in ACL2. When not
provided, the program uses the topmodule for name.
- :save-to-file is optional. It should be a string and be used as a prefix for the outputting file name. When provided, it will
save the created simulation vectors to a file in a compact form (svexl) that
can be read later more quickly. When not provided, the simulation vector will
remain in the session (or in certificate files).
- :modified-modules-file is optional. When provided, it should be a string
pointing to a Verilog file containing alternative definitions of adder modules
that may be used to override the modules of the same name in the original
design.
This is useful
for hierarchical reasoning for cases VeSCmul cannot detect certain adder
patterns in some designs. This will create two simulation vectors: one for the
original design and another for the modified version. VeSCmul will be used to verify the modified
version. And vescmul-verify macro will also prove equivalance between the two versions
with a SAT solver (through FGL). In the end, a theorem stating the correctness of the original design
will be saved.
VeSCmul is usually very good at finding adders on its own, and
hopefully, this option will not be necessary. However, should the need rise, we still
keep hierarchical reasoning as an option.
- :stages is optional. Users can opt to define the stages that will
be passed to sv::defsvtv$. It is especially useful for sequential
circuits. Unless specified, the program will assume the given design is
combinational and bind input and output signals automatically to the variables
of the same case-insensitive names.
- :cycle-phases is optional. Will be passed to sv::defsvtv$. It is relevant for sequential circuits only.
Example call 1:
(vesmul-parse :file "demo/DT_SB4_HC_64_64_multgen.sv"
:topmodule "DT_SB4_HC_64_64"
:name my-multiplier-example
:save-to-file "parsed/")
Example call 2:
(vesmul-parse :file "demo/DT_SB4_HC_64_64_multgen.sv"
:topmodule "DT_SB4_HC_64_64"
:name my-multiplier-example)
Example call 3 (providing hints with hierarchical reasoning):
;; Create a Verilog file that has an alternative definition for Han-Carlson
;; vector adder used in the target multiplier. VeSCmul works well with the +
;; operator.
(write-string-to-file-event "demo/modified-HC_128.v"
"module HC_128(input [127:0] IN1, input [127:0] IN2, output [128:0] OUT);
assign OUT = IN1+IN2;
endmodule")
;; Use this alternative definition to help the verification program
(vesmul-parse :file "demo/DT_SB4_HC_64_64_multgen.sv"
:modified-modules-file "demo/modified-HC_128.v"
:topmodule "DT_SB4_HC_64_64"
:name my-multiplier-example)
;; vescmul-verify will later use this alternative definition to get help
;; for multiplier proofs.
You can proceed to vescmul-verify to run the verification
event.
