Skip to content
This repository has been archived by the owner on Dec 13, 2022. It is now read-only.

Commit

Permalink
Generate HTML for sum8 ILA capture (#785)
Browse files Browse the repository at this point in the history 
* Generate HTML for sum8 ILA capture

* Update demos/tutorial.v

Co-authored-by: jadephilipoom <[email protected]>

* Remove runshaskell lines

* Delete Setup.hs

Co-authored-by: jadephilipoom <[email protected]>
  • Loading branch information
@satnam6502 @jadephilipoom
satnam6502 and jadephilipoom authored May 17, 2021
1 parent 9c485dc commit af3f969
Show file tree
Hide file tree
Showing 5 changed files with 73 additions and 41 deletions.
7 changes: 3 additions & 4 deletions demos/tutorial.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -941,10 +941,9 @@ Definition sum8_tb :=

(*|
The circuit netlist and testbench can be converted in SystemVerilog and
simulated using a SystemVerilog simulator like Verilator:
simulated using a SystemVerilog simulator like Verilator::
clang++ -L/usr/local/opt/sqlite/lib sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a -o Vsum8_tb -lm -lstdc++
obj_dir/Vsum8_tb
clang++ -L/usr/local/opt/sqlite/lib sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a -o Vsum8_tb -lm -lstdc++ obj_dir/Vsum8_tb
10: tick = 0, i = 3, o = 3
20: tick = 1, i = 5, o = 8
30: tick = 2, i = 7, o = 15
Expand All @@ -970,7 +969,7 @@ run and observe this actually running on an FPGA and capture its output:
:width: 70%
:alt: Logic analyzer trace capture for the sum8 circuit.
Reassuring the actual circuit behaves as predicted by the Cava model
Reassuringly, the actual circuit behaves as predicted by the Cava model
in Coq and the SystemVerilog simulation.
|*)

Expand Down
58 changes: 29 additions & 29 deletions docs/demo/alectryon.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ In any case, make an exception for comments:
.alectryon-toggle-label,
.alectryon-extra-goal-label {
display: block;
font-size: 0.8rem;
font-size: 0.8em;
}

.alectryon-io .alectryon-input {
Expand All @@ -122,33 +122,33 @@ In any case, make an exception for comments:
.alectryon-io label.alectryon-input:after,
.alectryon-io .alectryon-extra-goal-label:before {
border: 1px solid #babdb6;
border-radius: 1rem;
border-radius: 1em;
box-sizing: border-box;
content: '';
display: inline-block;
font-weight: bold;
height: 0.25rem;
margin-bottom: 0.15rem;
height: 0.25em;
margin-bottom: 0.15em;
vertical-align: middle;
width: 0.75rem;
width: 0.75em;
}

.alectryon-toggle-label:before,
.alectryon-io .alectryon-extra-goal-label:before {
margin-right: 0.25rem;
margin-right: 0.25em;
}

.alectryon-io .alectryon-extra-goal-label::before {
margin-top: -0.35rem;
margin-top: -0.35em;
}

.alectryon-io label.alectryon-input {
padding-right: 1rem; /* Prevent line wraps before the checkbox bubble */
padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
}

.alectryon-io label.alectryon-input:after {
margin-left: 0.25rem;
margin-right: -1rem; /* Compensate for the anti-wrapping space */
margin-left: 0.25em;
margin-right: -1em; /* Compensate for the anti-wrapping space */
}

.alectryon-failed {
Expand All @@ -158,7 +158,7 @@ In any case, make an exception for comments:
text-decoration: red dotted underline;
text-decoration-skip-ink: none;
/* Chrome prints background images in low resolution, yielding a blurry underline */
/* background: bottom / 0.3rem auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
/* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
}

/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
Expand Down Expand Up @@ -208,7 +208,7 @@ In any case, make an exception for comments:
left: 0;
right: 0;
position: absolute;
padding: 0.25rem 0;
padding: 0.25em 0;
overflow: visible; /* Let box-shadows overflow */
z-index: 1; /* Default to an index lower than that used by :hover */
}
Expand Down Expand Up @@ -256,7 +256,7 @@ In any case, make an exception for comments:
background: #eeeeec;
border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
display: block;
padding: 0.25rem;
padding: 0.25em;
}

.alectryon-message::before {
Expand All @@ -279,7 +279,7 @@ In any case, make an exception for comments:
position: static;
width: unset;
background: unset; /* Override the backgrounds set in floating in windowed mode */
padding: 0.25rem 0; /* Re-assert so that later :hover rules don't override this padding */
padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
}

.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
Expand Down Expand Up @@ -314,12 +314,12 @@ In any case, make an exception for comments:
.alectryon-io .alectryon-goal,
.alectryon-io .goal-hyp,
.alectryon-io .goal-conclusion {
border-radius: 0.15rem;
border-radius: 0.15em;
}

.alectryon-io .alectryon-goal,
.alectryon-io .alectryon-message {
margin: 0.25rem;
margin: 0.25em;
}

.alectryon-io .alectryon-goal,
Expand All @@ -328,7 +328,7 @@ In any case, make an exception for comments:
background: #d3d7cf;
display: block;
flex-direction: column;
padding: 0.5rem;
padding: 0.5em;
position: relative;
}

Expand All @@ -339,21 +339,21 @@ In any case, make an exception for comments:
flex-flow: column nowrap; /* re-stated in windowed mode */
justify-content: space-around;
/* LATER use a ‘gap’ property instead of margins once supported */
margin: -0.15rem -0.25rem; /* -0.15rem to cancel the item spacing */
padding-bottom: 0.5rem;
margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
padding-bottom: 0.5em;
}

.alectryon-io .goal-hyp,
.alectryon-io .goal-conclusion {
background: #eeeeec;
display: inline-block;
padding: 0.15rem 0.35rem;
padding: 0.15em 0.35em;
}

.alectryon-io .goal-hyp {
align-items: baseline;
display: inline-flex;
margin: 0.15rem 0.25rem;
margin: 0.15em 0.25em;
}

.alectryon-io .hyp-names {
Expand All @@ -365,7 +365,7 @@ In any case, make an exception for comments:

.alectryon-io .hyp-punct {
font-weight: 600;
margin: 0 0.5rem;
margin: 0 0.5em;
}

.alectryon-io .hyp-body-block,
Expand All @@ -387,7 +387,7 @@ In any case, make an exception for comments:
display: block;
flex-grow: 1;
height: 0;
margin: 0 0 0.5rem 0;
margin: 0 0 0.5em 0;
}

.alectryon-io .goal-separator .goal-name {
Expand All @@ -403,9 +403,9 @@ In any case, make an exception for comments:
background: #eeeeec;
border: 1px solid #babcbd;
font-size: 0.75em;
padding: 0.25rem;
padding: 0.25em;
text-align: center;
margin: 1rem 0;
margin: 1em 0;
}

.alectryon-banner a {
Expand Down Expand Up @@ -443,7 +443,7 @@ In any case, make an exception for comments:
top: 0;
left: 100%;
right: -100%;
padding: 0 0.5rem;
padding: 0 0.5em;
position: absolute;
}

Expand Down Expand Up @@ -503,7 +503,7 @@ In any case, make an exception for comments:
/* See note about specificity below */
.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-toggle ~ .alectryon-output {
padding: 0.5rem;
padding: 0.5em;
overflow-y: auto; /* Windowed contents may need to scroll */
}

Expand Down Expand Up @@ -562,7 +562,7 @@ In any case, make an exception for comments:
}

.alectryon-coqdoc .doc .paragraph {
height: 0.75rem;
height: 0.75em;
}

/* Centered, Floating */
Expand Down Expand Up @@ -591,7 +591,7 @@ In any case, make an exception for comments:
margin: 0;
overflow-y: auto;
position: absolute;
padding: 0 1rem;
padding: 0 1em;
}

.alectryon-standalone .alectryon-windowed > * {
Expand Down
Binary file added docs/demo/sum8_ila.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added docs/demo/sum8_sim.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit af3f969

Please sign in to comment.